Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

PRENEX_CONV : conv

SYNOPSIS

Puts a term already in NNF into prenex form.

DESCRIPTION

When applied to a term already in negation normal form (see NNF_CONV, for example), the conversion PRENEX_CONV proves it equal to an equivalent in prenex form, with all quantifiers at the top level and a propositional body.

FAILURE CONDITIONS

Never fails; even on non-Boolean terms it will just produce a reflexive theorem.

EXAMPLE

  # PRENEX_CONV `(!x. ?y. P x y) \/ (?u. !v. ?w. Q u v w)`;;
  Warning: inventing type variables
  val it : thm =
    |- (!x. ?y. P x y) \/ (?u. !v. ?w. Q u v w) <=>
       (!x. ?y u. !v. ?w. P x y \/ Q u v w)