zf2.nql

/*

# Premise

This is a specification of a Turing machine which searches for
contradictions in ZF set theory and halts iff one exists.

# Underlying logic

Our starting point is Tarski's system S2 [Tar65], the axioms and inference
rules (detachment and generalization) of which are reproduced below.  ph, ps,
and ch range over formulae; x, y, and z range over set variables; v_0, v_1,
v_2, and v_3 are specific set variables; -> -. A. = e. E. /\ <-> represent
respectively implication, negation, universal quantification, equality, set
membership (here an opaque predicate of rank 2), existential quantification,
biconditional, and conjunction respectively.

This is similar to a subset of the logic used by the metamath.org computer
proof system; the notation for formulas and most of the ZF axioms are taken
from there.

Tar65: Tarski, Alfred, "A Simplified Formalization of Predicate Logic with
Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79
(1965)

    DET ph
            where ( ph -> ps ) and ps are previously proved
    GEN A. x ph
            where ph is previously proved

    B1  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
    B2  ( ( -. ph -> ph ) -> ph )
    B3  ( ph -> ( -. ph -> ps ) )
    B4  ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
    B5  ( A. x ph -> ph )
    B6  ( ph -> A. x ph )
            where x does not appear syntactically in ph
    B7  E. x x = y
            where x and y are different variables
    B8  ( x = y -> ( ph -> ps ) )
            where ph and ps are atomic formulas and ps is obtained from ph
            by replacing a single instance of x with y

State count is affected strongly by logic but much less so by the lengths of
axioms, so we want to move as much complexity as possible into axioms and out
of side conditions.  S2 is already much better for us than most systems, as it
avoids the notions of free variable and proper substitution (or more precisely
these notions are implicit and emergent: suitable universal closures of ph ->
A. x ph fill the role of "x is not free in ph", and suitable closures of ( x =
y -> ( ph <-> ps ) ) fill the role of "substituting x for y in ph produces
ps"); we can do do better for axioms B5, B6, B7, and B8 however.

Axiom B5 is simply unneeded; it was proven redundant by KM65.

KM65: Kalish, D. and R. Montague, "On Tarski's formalization of predicate logic
with identity," Archiv für Mathematische Logik und Grundlagenforschung,
7:81-101 (1965)

B6 requires a recursive decomposition of the formula ph.  We can simplify this
by providing axioms to cover the cases and requiring the recursion to be done
in the proof; there are five cases that need to be covered:

    B6 I    ( x = y -> A. z x = y )
            where z != x, z != y
    B6 II   ( x e. y -> A. z x e. y )
            where z != x, z != y
    B6 III  ( A. z ( ph -> A. z ph ) -> ( A. z ( ps -> A. z ps ) ->
                ( ( ph -> ps ) -> A. z ( ph -> ps ) ) ) )
    B6 IV   ( A. z ( ph -> A. z ph ) -> ( -. ph -> A. z -. ph ) )
    B6 V    ( A. x ( ph -> A. z ph ) -> ( A. x ph -> A. z A. x ph ) )

This recursive scheme is used in the Metamath system to handle cases where x is
free in ph but not syntactically absent.  Here we use it merely to avoid the
complexity of syntactic absence.  We do not need an axiom for B6(III) as it can
be proven from B6(IV), B4, and propositional logic; likewise shorter axioms can
be found which prove IV and V over the remainder of the system.  I and II are
combined to share their conditional clause.  Thus we replace B6 with:

    B6a ( x = y -> A. z x = y /\ x e. y -> A. z x e. y )
            where x != z, y != z
    B6b ( A. x A. y ph -> A. y A. x ph )
    B6c ( E. x A. x ph -> A. x ph )

The constraint on B7 reduces the number of axioms generated by the scheme, but
it is not necessary for soundness so we omit it.  Our B7 becomes:

    B7  E. x x = y

B8 as written has four cases, since we have two primitive relations (equality
and membership) and each relation can be substituted on either side.  It is not
necessary to provide substitutions for both sides of the equality predicate
since equality is commutative.  Some care is needed because B8 is used to prove
commutativatity of equality, and the form that is provided must suffice for
that proof; B8a below suffices for Lemma 3 of KM65.  B8 becomes:

    B8a ( x = y -> ( x = z -> y = z ) )
    B8b ( x = y -> ( x e. z -> y e. z ) )
    B8c ( x = y -> ( z e. x -> z e. y ) )

# Set theory

The axiom system we use is significantly different from other formulations
of set theory, since minimizing the length of the axioms reduces the number of
states.

We omit Regularity, Choice, and Extensionality, since they do not affect the
consistency strength of the system.

Unlike the predicate calculus axioms, we use fixed variables for the axioms of
set theory, since instances with other variables are derivable.

Alongside the schemes of predicate calculus and the axioms of Powerset and
Union, we include only one additional scheme, which implies the traditional
schemes of Separation and Collection (which, unlike Replacement, is usable
even without Extensionality), as well as the Axiom of Infinity.

This new scheme, after a few simplifications, renaming some instances of v_0
to v_3 to avoid shadowing, and assuming that P does not use v_1, is:

E. v_1 (
    A. v_2 e. v_3 ( E. v_0 P -> v_2 e. v_1 ) 
    /\ A. v_2 e. v_1 E. v_0 P
    /\ A. v_0 e. v_1 A. v_2 ( P -> E. v_2 e. v_1 P ) )

P is intended to express a relation from v_0 to v_2. The second conjunct
asserts that every element of v_1 is in the image of P. The first conjunct
asserts that every element of v_3 which is in the image of P is also in v_1.
Separation can be derived using P = (Q /\ v_0 e. v_3), where Q is a predicate
on v_0.

The third conjunct asserts something similar to the conclusion of Collection,
but with the source and target sets being identical. Instantiating P with
((v_0 = v_4 /\ v_2 e. v_3) \/ (v_0 e. v_3 /\ Q)), where v_0 is the source set
of an instance of Collection and Q is the relation to collect, and setting v_4
to a set not in v_3, v_3 is a subset of any value for v_1 satisfying the above
scheme by the first disjunct of P, and thus by the second disjunct v_1 is a
witness to that instance of Collection.

Since the third conjunct of the above scheme uses the output set as an input to
collection, simple recursive definitions that would normally be produced using
Infinity and Replacement can instead be constructed more directly. For example,
the set of iterated unions of a set X can be constructed by setting P to
((v_0 = v_4 /\ v_2 = X) \/ (v_0 e. v_3 /\ v_2 = U. v_0)), where v_4 is as in
the previous paragraph and U. denotes the union of elements of a set. Infinity
itself can be proved similarly.

The constructible universe satisfies Foundation, Choice, and Extensionality
regardless of whether or not the full universe does (for the latter, only if
the ambient equality is omitted from the language used to generate definable
powersets). The construction of the constructible universe can be carried out
normally (for the most part), since most of the structures involved have
bounded depth, so they can be compared using sufficiently hereditarily
extensional replacements for equality, to avoid issues with non-extensional
differences between sets permitted by the lack of Extensionality. The two
exceptions are the levels of the constructible hierarchy themselves, which are
extensional enough that they can be compared with ordinary extensional equality
(that is, (A. v_0 e. X v_0 e. Y /\ A. v_0 e. Y v_0 e. X)), and von Neumann
ordinals, which can instead be compared with order-equivalence.

The above constructions shows that the theory used by this machine interprets
ZFC. Thus, since it can easily be interpreted into ZFC, it is equiconsistent
with ZFC, and so this machine halts if and only if ZFC is inconsistent.

Our final axiom set is:

    DET | MAJOR ( ph -> ps )
        | MINOR ph
        | ps

    GEN | FROM ph
        | A. x ph

    B1  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
    B2  ( ( -. ph -> ph ) -> ph )
    B3  ( ph -> ( -. ph -> ps ) )
    B4  ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
    B6a ( x = y -> A. z x = y /\ x e. y -> A. z x e. y )
            where x != z, y != z
    B6b ( A. x A. y ph -> A. y A. x ph )
    B6c ( E. x A. x ph -> A. x ph )
    B7  E. x x = y
    B8a ( x = y -> ( x = z -> y = z ) )
    B8b ( x = y -> ( x e. z -> y e. z ) )
    B8c ( x = y -> ( z e. x -> z e. y ) )

    POW E. v_1 A. v_2 ( A. v_1 ( v_1 e. v_2 -> v_1 e. v_0 ) -> v_2 e. v_1 )
    UNI E. v_1 A. v_2 ( E. v_1 ( v_2 e. v_1 /\ v_1 e. v_0 ) -> v_2 e. v_1 )
    ICS E. v_1 ( A. v_2 ( ( v_2 e. v_0 -> ( E. v_0 A. v_1 P -> v_2 e. v_1 ) )
        /\ ( v_2 e. v_1 -> E. v_0 P ) ) /\ A. v_0 ( v_0 e. v_1 -> A. v_2
        ( A. v_1 P -> E. v_2 ( v_2 e. v_1 /\ P ) ) ) )
                                                                               |
# Encoding wffs and proofs as integers

Define (X . Y) as X + (X + Y) * (X + Y + 1) / 2.  This is the Cantor pairing
function; it takes nonnegative integer values and is bijective, in particular
(X . Y) = 0 iff X = Y = 0, and Y < (X . Y) if (X . Y) != 0.  Extend the
notation as follows:

    (X Y Z) = (X . (Y Z))
    (Z)     = (Z . 0)
    (X; Y)  = (X . (; Y)) = (X . 1 + (Y . 0))

There are a countable infinity of set variables, numbered in the most direct
way.

Wffs are numbered recursively using the pairing function:

    | v_i = v_j  |      ( ( i . j ) . 0 )
    | v_i e. v_j |      ( ( i . j ) . 1 )
    | ph -> ps   |      ( ( |ph| . |ps| ) . 2 )
    | -. ph      |      ( |ph| . 3 )
    | A. v_i ph  |      ( ( i . |ph| ) . 4 )

No checking is done to verify that a wff has one of these forms before creating
a substitution instance of an axiom, so other forms will exist during
execution.  They may consistently be treated as vacuous or unsatisfiable.

The wff with numeric value 0 is |v_0 = v_0|.  This is a theorem of ZF, and may
be substituted anywhere a theorem is required.  The wff with numeric value 1 is
|v_0 e. v_0|; this is not a theorem, as its universal closure states that all
sets contain themselves.  It serves as the canonical contradiction; the search
stops when a proof of 1 is found.

A proof is a list of integers taken in repeating groups of 4, each an axiom
code followed by three parameters, such as (ACa P1a P2A P3a; ACb P1b P2b P3b;
...).  A proof manipulates a stack of proved theorems.  A step in the proof
corresponding to an inference rule pops one or two theorems from the stack;
every step pushes a new theorem.  Invalid steps push the moot theorem |v_0 =
v_0|.  Execution halts if at any point |v_0 e. v_0| is pushed.  The stack is
not cleared between "proofs" and it is possible for one proof to see theorems
left on the stack by previous proofs; however the stack contains only theorems,
so a false halt cannot occur by this reason.  Stack underflow returns proofs
of |v_0 = v_0| because 0 = (0 . 0).

Axiom codes are assigned as follows.  -- means ignored.

    AC  P1  P2  P3  WHAT
    1   ps  --  --  Detachment rule.  Pops a minor premise (proof of ph), then
                    pops a major premise which is expected to match
                    ( ph -> P1 ).  If the major premise matches, pushes ps,
                    else pushes moot.
    2   x   --  --  Generalization rule.  Pops a theorem of statement ph;
                    proves A. x ph.
    3   ph  ps  ch  Push B1
    4   ph  --  --  Push B2
    5   ph  ps  --  Push B3
    6   x   ph  ps  Push B4
    7   x   y   z   Push B6a if distinctness conds met, else moot
    8   x   y   ph  Push B6b
    9   x   ph  --  Push B6c
    10  x   y   --  Push B7
    11  x   y   z   Push B8a
    12  x   y   z   Push B8b
    13  x   y   z   Push B8c
    14  --  --  --  Push EXT
    15  ph  --  --  Push REP
    16  --  --  --  Push POW
    17  --  --  --  Push UNI
    >17 --  --  --  Push INF

# Use of variables

The main loop runs over all sequences of proof steps, encoded by nextproof.
Each sequence is temporarily in prooflist; the next outermost loop breaks down
prooflist one step at a time, with the parts of the step in axiomcode, param1,
param2, and param3.  prooflist is reset when it reaches zero, which happens
infinitely often because prooflist is reduced by at least 1 in every iteration
where it is not reset.

(topwff . wffstack) represents a single list, the wff-stack.  Between
iterations of the step loop, the wff stack corresponds to the stack of
previously proved statements described above.  Within the step loop, there may
be unproved statements on the wff-stack.

The bulk of the step loop consists of a sequence of clauses, each of which ends
with a call to select().  A clause is _active_ if axiomcode == 1; axiomcode is
decremented after each clause, so the initial value of axiomcode selects which
clause is active.  An inactive clause must not remove proofs from the proof
section of the wffstack or modify the params variables.

Wffs are constructed using a sequence of calls to functions that manipulate the
wff stack, effectively using a reverse-Polish notation.

    v_0()       ( -- v_0 ) Pushes variable 0, or the moot theorem
    v_1()       ( -- v_1 )
    v_2()       ( -- v_2 )
    v_3()       ( -- v_3 )
    par1()      ( -- P1 ) Pushes a scheme parameter
    par2()      ( -- P2 )
    par3()      ( -- P3 )
    wim()       ( ph ps -- ( ph -> ps ) )
    wn()        ( ph -- -. ph )
    wal()       ( x ph -- A. x ph )
    wex()       ( x ph -- E. x ph )
    wa()        ( ph ps -- ( ph /\ ps ) )
    wel()       ( x y -- x e. y )
    weq()       ( x y -- x = y )

No operator is provided for \/ or <->; they must be expanded.

*/

global prooflist;
global nextproof;

global topwff;
global wffstack;

global axiomcode;
global param1;
global param2;
global param3;

global t2;

/* Cantor pair manipulation proctions */
/* zeros in1, in2 */
proc pair(out, in1, in2) {
    builtin_pair(out, in1, in2);
}

/* zeros in */
proc unpair(out1, out2, in) {
    builtin_unpair(out1, out2, in);
}

proc pushwff() { pair(wffstack, topwff, wffstack); }
proc v_0_() { pushwff(); topwff = topwff + 0; }
proc v_1_() { pushwff(); topwff = topwff + 1; }
proc v_2_() { pushwff(); topwff = topwff + 2; }
proc v_3_() { pushwff(); topwff = topwff + 3; }
proc v_4_() { pushwff(); topwff = topwff + 4; }

/* from the bb(745) paper */
proc cons() { unpair(t2, wffstack, wffstack); pair(topwff, topwff, t2); }

proc weq() { cons(); v_0_(); cons(); }
proc wel() { cons(); v_1_(); cons(); }
proc wim() { cons(); v_2_(); cons(); }
proc wn()  { v_3_(); cons(); }
proc wal() { cons(); v_4_(); cons(); }

/*
proc weq() { cons(); t2 = t2 + 0; pair(topwff, t2, topwff); }
proc wel() { cons(); t2 = t2 + 1; pair(topwff, t2, topwff); }
proc wim() { cons(); t2 = t2 + 2; pair(topwff, t2, topwff); }
proc wn()  { t2 = 3; pair(topwff, t2, topwff); }
proc wal() { cons(); t2 = t2 + 4; pair(topwff, t2, topwff); }
*/


proc wex() { wn(); cons(); v_4_(); cons(); wn(); }
proc wa()  { wn(); cons(); v_2_(); cons(); wn(); }

/*
proc wex() { wn(); cons(); t2 = t2 + 4; pair(topwff, t2, topwff); wn(); }
proc wa()  { wn(); cons(); t2 = t2 + 2; pair(topwff, t2, topwff); wn(); }
*/
/*
proc wex() { wn(); wal(); wn(); }
proc wa()  { wn(); wim(); wn(); }
*/

proc v_0() { v_0_(); align_7(); }
proc v_1() { v_1_(); align_7(); }
proc v_2() { v_2_(); align_7(); }
proc v_3() { v_3_(); align_7(); }

proc par1() { pushwff(); topwff = param1; align_7(); }
proc par2() { pushwff(); topwff = param2; align_7(); }
proc par3() { pushwff(); topwff = param3; align_7(); }

/* pop element under top earlier, pop top later */
proc select() {
    unpair(t2, wffstack, wffstack);
    if (decz axiomcode) {
        builtin_move(topwff, t2);
    }
    /* align_7(); */
}

proc param(p) {
    unpair(t2, wffstack, wffstack);
    builtin_move(p, t2);
}

proc cparam(p) {
    if (axiomcode == 1) {
        unpair(t2, wffstack, wffstack);
        builtin_move(p, t2);
    }
}

proc safety(p1, p2){
    if (p1 == p2) {
        p1 = p1 + 1;
    }
}

proc main() {
    if (decz prooflist) {
        prooflist = nextproof;
        nextproof = nextproof + 1;
    }

    unpair(t2, prooflist, prooflist); builtin_move(axiomcode, t2);
    unpair(t2, prooflist, prooflist); builtin_move(param1, t2);
    unpair(t2, prooflist, prooflist); builtin_move(param2, t2);
    unpair(t2, prooflist, prooflist); builtin_move(param3, t2);

    /* B1 */
    /* no select since if axiomcode=0 all selects reject the new entry */
    par1(); par2(); wim(); par2(); par3(); wim(); par1(); par3(); wim(); wim(); wim();

    /* B3 */
    par1(); par1(); wn(); par2(); wim(); wim(); select();

    /* B2 */
    par1(); wn(); par1(); wim(); par1(); wim(); select();

    /* B4 */
    par1(); par2(); par3(); wim(); wal(); par1(); par2(); wal(); par1(); par3(); wal(); wim(); wim(); select();

    /* B6b */
    par1(); par2(); par3(); wal(); wal();  par2(); par1(); par3(); wal(); wal();  wim();  select();
    

    /* B8b */
    par1(); par2(); weq();  par1(); par3(); wel();  par2(); par3(); wel(); wim(); wim();  select();

    /* B6c */
    par1(); par1(); par2(); wal(); wex();  par1(); par2(); wal();  wim();  select();

    /* B8a */
    /* ( P = Q -> ( P = R -> Q = R ) ) */
    /* derivable using EXT */
    par1(); par2(); weq();  par1(); par3(); weq();  par2(); par3(); weq(); wim(); wim();  select();

    /* B8c */
    par1(); par2(); weq();  par3(); par1(); wel();  par3(); par2(); wel(); wim(); wim();  select();

    /* B7 */
    par1(); par1(); par2(); weq(); wex(); select();

    /* EXT */
    /* requires B8a */
    /*
    v_2();
    v_2(); v_0(); wel();  v_2(); v_1(); wel(); wim();
    v_2(); v_1(); wel();  v_2(); v_0(); wel(); wim(); wa();
    wal();  v_0(); v_1(); weq(); wim();  select();
    */
    /* doesn't require B8a */
    /*
    par2();
    par2(); par3(); wel();  par2(); par1(); wel(); wim();
    par2(); par1(); wel();  par2(); par3(); wel(); wim(); wa();
    par3(); par1(); weq(); wim();  wex();  select();
    */

    /*
    Below are descriptions in this machine's language of various axioms and
    schemes which were not used in the final system, but which may be useful
    for further research. The uncommented ones are POW, UNI, and INF+COL+SEP.
    */

    /* SEP */
    /* E. y A. z ( ( z e. y -> ( z e. x /\ P ) ) /\ ( z e. x -> ( A. y P -> z e. y ) ) ) */
    /*
    v_1(); v_2();
    v_2(); v_1(); wel(); v_2(); v_0(); wel(); par1(); wa(); wim();
    v_2(); v_0(); wel(); v_1(); par1(); wal(); v_2(); v_1(); wel(); wim(); wim(); wa();
    wal(); wex(); select();
    */

    /* REP+SEP */
    /* ( A. w E. y A. z ( A. y P -> z = y ) -> E. y A. z ( ( z e. y -> E. w ( w e. x /\ A. y P ) ) /\ ( E. w ( w e. x /\ A. y P ) -> z e. y ) ) ) */
    /*
    v_3(); v_1(); v_2();  v_1(); par1(); wal(); v_2(); v_1(); weq(); wim();  wal(); wex(); wal();
    v_1(); v_2();
    v_2(); v_1(); wel();  v_3(); v_3(); v_0(); wel(); v_1(); par1(); wal(); wa(); wex();  wim();
    v_3(); v_3(); v_0(); wel(); v_1(); par1(); wal(); wa(); wex();  v_2(); v_1(); wel();  wim(); wa();
    wal(); wex();
    wim(); select();
    */

    /* COL+SEP */
    /* E. y ( A. z ( z e. x -> A. w ( A. y P -> E. w ( w e. y /\ P ) ) ) /\ A. w ( w e. y -> E. z P ) ) */
    /*
    v_1(); v_2(); v_2(); v_0(); wel(); v_3(); v_1(); par1(); wal(); v_3(); v_3(); v_1(); wel(); par1(); wa(); wex(); wim(); wal(); wim(); wal();
    v_3(); v_3(); v_1(); wel(); v_2(); par1(); wex(); wim(); wal(); wa(); wex();  select();
    */

    /* WCOL+SEP+UNI */
    /* E. y ( A. z ( z e. x -> ( E. w A. x ( P -> x e. w ) -> A. x ( A. y A. w P -> x e. y ) ) ) /\ A. x ( x e. y -> E. z P ) ) */
    /*
    v_1(); v_2(); v_2(); v_0(); wel(); v_3(); v_0(); par1(); v_0(); v_3(); wel(); wim(); wal(); wex(); v_0(); v_1();
    v_3(); par1(); wal(); wal(); v_0(); v_1(); wel(); wim(); wal(); wim(); wim(); wal(); v_0(); v_0(); v_1(); wel(); v_2(); par1(); wex(); wim();
    wal(); wa(); wex();  select();
    */
    /* E. y ( A. z ( z e. x -> A. w ( A. x ( P -> x e. w ) -> A. x ( A. y A. w P -> x e. y ) ) ) /\ A. x ( x e. y -> E. z P ) ) */
    /*
    v_1(); v_2(); v_2(); v_0(); wel(); v_3(); v_0(); par1(); v_0(); v_3(); wel(); wim(); wal(); v_0(); v_1();
    v_3(); par1(); wal(); wal(); v_0(); v_1(); wel(); wim(); wal(); wim(); wal(); wim(); wal(); v_0(); v_0(); v_1(); wel(); v_2(); par1(); wex(); wim();
    wal(); wa(); wex();  select();
    */
    /* E. y ( A. z ( z e. x -> ( E. y A. x ( P -> x e. y ) -> A. x ( A. y P -> x e. y ) ) ) /\ A. x ( x e. y -> E. z P ) ) */
    /*
    v_1(); v_2(); v_2(); v_0(); wel(); v_1(); v_0(); par1(); v_0(); v_1(); wel(); wim(); wal(); wex(); v_0(); v_1();
    par1(); wal(); v_0(); v_1(); wel(); wim(); wal(); wim(); wim(); wal(); v_0(); v_0(); v_1(); wel(); v_2(); par1(); wex(); wim();
    wal(); wa(); wex();  select();
    */

    /* POW */
    /* E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) */
    /*
    v_1(); v_2();  v_3(); v_3(); v_2(); wel(); v_3(); v_0(); wel(); wim(); wal();  v_2(); v_1(); wel(); wim();  wal(); wex();  select();
    */
    /* E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) */
    
    v_1(); v_2();  v_1(); v_1(); v_2(); wel(); v_1(); v_0(); wel(); wim(); wal();  v_2(); v_1(); wel(); wim();  wal(); wex();  select();
    

    /* UNI */
    /* E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) */
    /*
    v_1(); v_2();  v_3(); v_2(); v_3(); wel(); v_3(); v_0(); wel(); wa(); wex();  v_2(); v_1(); wel(); wim();  wal(); wex();  select();
    */
    /* E. y A. z ( E. y ( z e. y /\ y e. x ) -> z e. y ) */
    
    v_1(); v_2();  v_1(); v_2(); v_1(); wel(); v_1(); v_0(); wel(); wa(); wex();  v_2(); v_1(); wel(); wim();  wal(); wex();  select();
    

    /* UNI+POW */
    /* E. y A. z ( ( ~ A. w ( w e. z -> w e. x ) -> E. w ( z e. w /\ w e. x ) ) -> z e. y ) */
    /*
    v_1(); v_2();
    v_3(); v_3(); v_2(); wel(); v_3(); v_0(); wel(); wim(); wal(); wn();
    v_3(); v_2(); v_3(); wel(); v_3(); v_0(); wel(); wa(); wex(); wim();
    v_2(); v_1(); wel(); wim();  wal(); wex();  select();
    */
    /* E. y A. z ( ( ~ A. y ( y e. z -> y e. x ) -> E. y ( z e. y /\ y e. x ) ) -> z e. y ) */
    /*
    v_1(); v_2();
    v_1(); v_1(); v_2(); wel(); v_1(); v_0(); wel(); wim(); wal(); wn();
    v_1(); v_2(); v_1(); wel(); v_1(); v_0(); wel(); wa(); wex(); wim();
    v_2(); v_1(); wel(); wim();  wal(); wex();  select();
    */

    /* INF */
    /* E. y ( x e. y /\ A. x ( x e. y -> A. z ( A. y P -> E. z ( z e. y /\ P ) ) ) ) */
    /*
    v_1(); v_0(); v_1(); wel(); v_0(); v_0(); v_1(); wel(); v_2(); v_1(); par1(); wal();
    v_2(); v_2(); v_1(); wel(); par1(); wa(); wex(); wim(); wal(); wim(); wal(); wa(); wex();
    select();
    */

    /* INF+COL */
    /* E. y ( A. z ( z e. x -> z e. y ) /\ A. x ( x e. y -> A. z ( A. y P -> E. z ( z e. y /\ P ) ) ) ) */
    /*
    v_1(); v_2(); v_2(); v_0(); wel(); v_2(); v_1(); wel(); wim(); wal(); v_0(); v_0(); v_1(); wel(); v_2(); v_1(); par1(); wal();
    v_2(); v_2(); v_1(); wel(); par1(); wa(); wex(); wim(); wal(); wim(); wal(); wa(); wex();
    select();
    */

    /* INF+COL+SEP */
    /* E. y ( A. z ( ( z e. x -> ( E. x A. y P -> z e. y ) ) /\ ( z e. y -> E. x P ) ) /\ A. x ( x e. y -> A. z ( A. y P -> E. z ( z e. y /\ P ) ) ) ) */

    v_1(); v_2(); v_2(); v_0(); wel(); v_0(); v_1(); par1(); wal(); wex(); v_2(); v_1(); wel(); wim(); wim();
    v_2(); v_1(); wel(); v_0(); par1(); wex(); wim(); wa();
    wal(); v_0(); v_0(); v_1(); wel(); v_2(); v_1(); par1(); wal();
    v_2(); v_2(); v_1(); wel(); par1(); wa(); wex(); wim(); wal(); wim(); wal(); wa(); wex();
    select();

    /* B6a */
    safety(param1, param3);
    safety(param2, param3);
    par1(); par2(); weq();  par3(); par1(); par2(); weq(); wal();  wim();
    select();
    par1(); par2(); wel();  par3(); par1(); par2(); wel(); wal();  wim();
    select();

    /* GEN */
    /* ph */
    cparam(param2);
    par1(); par2(); wal(); select();

    /* DET */
    /* ph */
    cparam(param2);
    /* ph -> ps */
    cparam(param3);
    /* param1 = ps */
    par2(); par1(); wim();
    if (topwff == param3) {
        topwff = param1;
    } else {
        topwff = 0;
    }
    select();

    if (topwff == 1) {
        /* vacuously false wff (v_0 e. v_0) proved, we're done */
        return;
    }
}