3.0.0.13293
macs:Mac OS X10.5.8
FchP
newFormat
=openproof.zen.Openproof{p=openproof.fitch.FitchProofDriver{p=openproof.proofdriver.DRProof{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r&1;})r=openproof.proofdriver.DRProofRule{u=uProof;s=proof;}o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()f(openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="@x (@y (y < x $ Q(y)) $ Q(x))";}})r=openproof.stepdriver.SRPremiseRule{u=uPremise;s=step;}o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="@y ((y = c0 | y < c0) $ Q(y))";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="@x @y (x < y % /z x+s(z) = y) ; definition of < ";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="@x @y (s(x) = s(y) $ x = y) ; Peano axiom 2";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="@x x + 0 = x ; Peano axiom 3";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="@x @y x + s(y) = s(x+y) ; Peano axiom 4";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRProof=openproof.proofdriver.DRProof{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r&1;})r&5;o&6;u=openproof.proofdriver.DRSupport{t()}b()f(openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="a = s(c0) | a < s(c0)";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b(s=a;)},openproof.proofdriver.DRProof=openproof.proofdriver.DRProof{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r&1;})r&5;o&6;u=openproof.proofdriver.DRSupport{t()}b()f(openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="a = s(c0)";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="@y (y < s(c0) $ Q(y)) $ Q(s(c0))     ; :x>s(c0)";}})r=openproof.fold.OPUniversalElimRule{u="u\u2200 Elim";s=fol;}o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRProof=openproof.proofdriver.DRProof{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r&1;})r&5;o&6;u=openproof.proofdriver.DRSupport{t()}b()f(openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="b < s(c0)";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b(s=b;)},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="; Lemma";}})r=openproof.stepdriver.SDUnknownRule{u="uRule?";s=step;}o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&30;ss=2;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&38;ss=3;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&46;ss=4;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&54;ss=5;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="";}})r&94;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&116;ss=6.1.2.1;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="b = c0 | b < c0";}})r=openproof.fold.OPImplicationElimRule{u="u\u2192 Elim";s=fol;}o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="(b = c0 | b < c0) $ Q(b)";}})r&118;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&22;ss=1;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="Q(b)";}})r&140;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&147;ss=6.1.2.4;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&138;ss=6.1.2.3;sb=false;})}b()})},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="";}})r=openproof.fold.OPUniversalIntroRule{u="u\u2200 Intro";s=fol;}o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="Q(s(c0))";}})r&140;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&92;ss=6.1.1;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="Q(a)";}})r&118;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&84;ss=6.1.0;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&175;ss=6.1.4;sb=false;})}b()})},openproof.proofdriver.DRProof=openproof.proofdriver.DRProof{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r&1;})r&5;o&6;u=openproof.proofdriver.DRSupport{t()}b()f(openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="a < s(c0)";}})r&15;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="; Lemma";}})r&118;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&30;ss=2;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&38;ss=3;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&46;ss=4;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&54;ss=5;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="";}})r&94;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&209;ss=6.2.1;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="a = c0 | a < c0";}})r&118;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&201;ss=6.2.0;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&221;ss=6.2.2;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="(a = c0 | a < c0) $ Q(a)";}})r&118;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&22;ss=1;sb=false;})}b()},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="";}})r&118;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&230;ss=6.2.3;sb=false;},openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&240;ss=6.2.4;sb=false;})}b()})},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="Q(a)";}})r=openproof.fold.OPDisjunctionElimRule{u="u\u2228 Elim";s=fol;}o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t()}b()})},openproof.proofdriver.DRSimpleStep=openproof.proofdriver.DRSimpleStep{s(openproof.proofdriver.DRStepInfo=openproof.proofdriver.DRStepInfo{r=openproof.foldriver.FOLDriver{t="";}})r&168;o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}u=openproof.proofdriver.DRSupport{t(openproof.proofdriver.DRSupportPack=openproof.proofdriver.DRSupportPack{si&62;ss=6.;sb=false;})}b()})}g=openproof.proofdriver.DRGoalList{g(openproof.proofdriver.DRGoal=openproof.proofdriver.DRGoal{g=openproof.proofdriver.DRGoalInfo{r=openproof.foldriver.FOLDriver{t="@y ((y = s(c0) | y < s(c0)) $ Q(y))";r&277;}}r=openproof.fold.OPFOLGoalRule{u=uFOLGoalRule;s=fol;}s()o=openproof.zen.proofdriver.OPDStatusObject{c=0;s="";l="";d@k="";t=false;}c(openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n="t/f Connectives";a=true;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=Identity;a=true;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=Quantifiers;a=true;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=ExMidd;a=false;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=TwoTaut;a=false;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=TautCon;a=false;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n="FO Con";a=false;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=BabyAna;a=false;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=TwoMore;a=false;},openproof.fold.FOLGoalConstraint=openproof.fold.FOLGoalConstraint{n=AnaCon;a=false;})})}a=true;}}c=1240026;
s=1761345;