changed names of resource-1.3; added a note on homepage on release

1 files changed, 0 insertions, 113 deletions

diff --git a/examples/systemS/proof.gfcm b/examples/systemS/proof.gfcm
deleted file mode 100644
index 6e9692769..000000000
--- a/examples/systemS/proof.gfcm
+++ /dev/null
@@ -1,113 +0,0 @@
-concrete ProofSymb of Proof=FormulaSymb**open Prelude,Precedence in{flags modulesize=n27;flags startcat=Text;flags unlexer=text;flags lexer=text;A in FormulaSymb;
-Abs in FormulaSymb;
-And in FormulaSymb;
-B in FormulaSymb;
-lin BaseFormula:Proof.ListFormula=\->{s=[];isnil=<Prelude.True>};"[]";
-C in FormulaSymb;
-lin ConjSplit:Proof.Proof=\Formula@0,Formula@1,Formula@2,Proof@3->{s="Conjunction"++"split"++(variants{"&-"[]}++("["++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(","++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})++("|-"++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@2.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@2.s++")")}!{p1=Formula@2.p;p2=0}++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@3.s))))};"(Conjunction split)&- ([ (Formula_0 , Formula_1)|- Formula_2 ])&- ------------------------------ Proof_3";
-lin ConsFormula:Proof.ListFormula=\Formula@0,ListFormula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++table Prelude.Bool{(Prelude.True)=>ListFormula@1.s;(Prelude.False)=>","++ListFormula@1.s}!(ListFormula@1.isnil);isnil=<Prelude.False>};"Formula_0 ListFormula_1";
-lin DeMorgan1:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s="de"++("Morgan"++"1")++(variants{"&-"[]}++("["++(Formula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(de Morgan 1)&- ([ Formula_0 |- Formula_1 ])&- ------------------------------ Proof_2";
-lin DeMorgan2:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s="de"++("Morgan"++"2")++(variants{"&-"[]}++("["++(Formula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(de Morgan 2)&- ([ Formula_0 |- Formula_1 ])&- ------------------------------ Proof_2";
-lin ExFalso:Proof.Proof=\Formula@0->{s="Ex"++("falso"++"quodlibet")++Formula@0.s++(variants{"&-"[]}++"Ø")};"((Ex falso quodlibet)Formula_0)&- Ø";
-lin Forget:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Forgetting"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"Forgetting &- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2";
-Formula in FormulaSymb;
-lin Hypo:Proof.Proof=\->{s="Hypothesis"++(variants{"&-"[]}++"Ø")};"Hypothesis &- Ø";
-If in FormulaSymb;
-lin Implic:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Implication"++"strategy"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Implication strategy)&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2";
-lin ImplicNeg:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Implication"++"negation"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Implication negation)&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2";
-lincat ListFormula={s:Str;isnil:Prelude.Bool}={s=str@0;isnil=<Prelude.True>};"ListFormula";
-lin ModPon:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Modus"++"ponens"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Modus ponens)&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2";
-lin NegRewrite:Proof.Proof=\Formula@0,ListFormula@1,Proof@2->{s="Negation"++"rewrite"++(variants{"&-"[]}++("["++(ListFormula@1.s++("|-"++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("->"++"_|_")++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Negation rewrite)&- ([ ListFormula_1 |- (Formula_0 -> _|_)])&- ------------------------------ Proof_2";
-Not in FormulaSymb;
-Or in FormulaSymb;
-lincat Proof={s:Str}={s=str@0};"Proof";
-lin RedAbs:Proof.Proof=\Formula@0,Proof@1->{s="Reductio"++("ad"++"absurdum")++(variants{"&-"[]}++("["++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++("|-"++("_|_"++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@1.s))))};"(Reductio ad absurdum)&- ([ (~ Formula_0)|- _|_ ])&- ------------------------------ Proof_1";
-lin Start:Proof.Text=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s)))};"&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2";
-Term in FormulaSymb;
-lincat Text={s:Str}={s=str@0};"Text";
-}
-concrete ProofEng of Proof=FormulaSymb**open Prelude,Precedence in{flags modulesize=n27;flags startcat=Text;flags unlexer=text;flags lexer=text;A in FormulaSymb;
-Abs in FormulaSymb;
-And in FormulaSymb;
-B in FormulaSymb;
-lin BaseFormula:Proof.ListFormula=\->{s=[];isnil=<Prelude.True>};"[]";
-C in FormulaSymb;
-lin ConjSplit:Proof.Proof=\Formula@0,Formula@1,Formula@2,Proof@3->{s=variants{"&-"[]}++("So"++("by"++("splitting"++("we"++"get")))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(","++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0}++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@2.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@2.s++")")}!{p1=Formula@2.p;p2=0})}++("."++Proof@3.s))))))};"&- (So by splitting we get)Formula_0 , Formula_1 [] . Proof_3";
-lin ConsFormula:Proof.ListFormula=\Formula@0,ListFormula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++table Prelude.Bool{(Prelude.True)=>ListFormula@1.s;(Prelude.False)=>","++ListFormula@1.s}!(ListFormula@1.isnil);isnil=<Prelude.False>};"Formula_0 ListFormula_1";
-lin DeMorgan1:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("Then"++(","++("by"++("the"++("first"++("de"++("Morgan's"++("law"++(","++("we"++"get")))))))))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (Then , by the first de Morgan's law , we get)Formula_0 [] . Proof_2";
-lin DeMorgan2:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("Then"++(","++("by"++("the"++("second"++("de"++("Morgan's"++("law"++(","++("we"++"get")))))))))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (Then , by the second de Morgan's law , we get)Formula_0 [] . Proof_2";
-lin ExFalso:Proof.Proof=\Formula@0->{s=variants{"&-"[]}++("Hence"++("we"++"get")++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++("as"++"desired"++".")))};"&- (Hence we get)Formula_0 (as desired).";
-lin Forget:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("In"++("particular"++("we"++"get"))++(ListFormula@0.s++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (In particular we get)ListFormula_0 [] . Proof_2";
-Formula in FormulaSymb;
-lin Hypo:Proof.Proof=\->{s=variants{"&-"[]}++("But"++("this"++("holds"++("trivially"++"."))))};"&- But this holds trivially .";
-If in FormulaSymb;
-lin Implic:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("It"++("is"++("enough"++"to"))++(table Prelude.Bool{(Prelude.True)=>ListFormula@0.s;(Prelude.False)=>"assume"++(ListFormula@0.s++"and")}!(ListFormula@0.isnil)++("show"++(Formula@1.s++("."++Proof@2.s)))))};"&- (It is enough to)ListFormula_0 show Formula_1 . Proof_2";
-lin ImplicNeg:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("By"++("implication"++("negation"++(","++("we"++"get"))))++(ListFormula@0.s++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (By implication negation , we get)ListFormula_0 [] . Proof_2";
-lincat ListFormula={s:Str;isnil:Prelude.Bool}={s=str@0;isnil=<Prelude.True>};"ListFormula";
-lin ModPon:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("Then"++(","++("by"++("Modus"++("ponens"++(","++("we"++"get"))))))++(ListFormula@0.s++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (Then , by Modus ponens , we get)ListFormula_0 [] . Proof_2";
-lin NegRewrite:Proof.Proof=\Formula@0,ListFormula@1,Proof@2->{s=variants{"&-"[]}++("Thus"++(","++("by"++"rewriting"))++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++(table Prelude.Bool{(Prelude.True)=>ListFormula@1.s;(Prelude.False)=>"we"++("may"++"assume")++(ListFormula@1.s++"and")}!(ListFormula@1.isnil)++("show"++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("->"++"_|_")++("."++Proof@2.s))))))};"&- (Thus , by rewriting)(~ Formula_0)ListFormula_1 show (Formula_0 -> _|_). Proof_2";
-Not in FormulaSymb;
-Or in FormulaSymb;
-lincat Proof={s:Str}={s=str@0};"Proof";
-lin RedAbs:Proof.Proof=\Formula@0,Proof@1->{s=variants{"&-"[]}++("To"++("that"++("end"++(","++("we"++("will"++"assume")))))++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++("and"++"show"++("_|_"++("."++(variants{"&-"[]}++("So"++("let"++("us"++("assume"++"that")))++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++("."++Proof@1.s)))))))))};"&- (To that end , we will assume)(~ Formula_0)(and show)_|_ . &- (So let us assume that)(~ Formula_0). Proof_1";
-lin Start:Proof.Text=\ListFormula@0,Formula@1,Proof@2->{s=table Prelude.Bool{(Prelude.True)=>ListFormula@0.s;(Prelude.False)=>"Suppose"++(ListFormula@0.s++".")}!(ListFormula@0.isnil)++("We"++("will"++("show"++"that"))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0}++("."++Proof@2.s)))};"ListFormula_0 (We will show that)Formula_1 . Proof_2";
-Term in FormulaSymb;
-lincat Text={s:Str}={s=str@0};"Text";
-}
-abstract Proof=Formula**{flags modulesize=n27;A in Formula;
-Abs in Formula;
-And in Formula;
-B in Formula;
-fun BaseFormula:Proof.ListFormula=data;
-C in Formula;
-fun ConjSplit:(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-fun ConsFormula:(h_:Formula.Formula)->(h_:Proof.ListFormula)->Proof.ListFormula=data;
-fun DeMorgan1:(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-fun DeMorgan2:(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-fun ExFalso:(h_:Formula.Formula)->Proof.Proof={};
-fun Forget:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-Formula in Formula;
-fun Hypo:Proof.Proof={};
-If in Formula;
-fun Implic:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-fun ImplicNeg:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-cat ListFormula[]=;
-fun ModPon:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-fun NegRewrite:(h_:Formula.Formula)->(h_:Proof.ListFormula)->(h_:Proof.Proof)->Proof.Proof={};
-Not in Formula;
-Or in Formula;
-cat Proof[]=;
-fun RedAbs:(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={};
-fun Start:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Text={};
-Term in Formula;
-cat Text[]=;
-}
-concrete FormulaSymb of Formula=open Precedence in{flags modulesize=n10;lin A:Formula.Formula=\->{s="A";p=4;a=<Precedence.PN>};"A";
-lin Abs:Formula.Formula=\->{s="_|_";p=4;a=<Precedence.PN>};"_|_";
-lin And:Formula.Formula=\Formula@0,Formula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=3}++("&"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=4});p=3;a=<Precedence.PL>};"Formula_0 & Formula_1";
-lin B:Formula.Formula=\->{s="B";p=4;a=<Precedence.PN>};"B";
-lin C:Formula.Formula=\->{s="C";p=4;a=<Precedence.PN>};"C";
-lincat Formula={s:Str;p:Ints 4;a:Precedence.PAssoc}={s=str@0;p=0;a=<Precedence.PN>};"Formula";
-lin If:Formula.Formula=\Formula@0,Formula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("->"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=1});p=1;a=<Precedence.PR>};"Formula_0 -> Formula_1";
-lin Not:Formula.Formula=\Formula@0->{s="~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4};p=4;a=<Precedence.PR>};"~ Formula_0";
-lin Or:Formula.Formula=\Formula@0,Formula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("v"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=3});p=2;a=<Precedence.PL>};"Formula_0 v Formula_1";
-lincat Term={s:Str;p:Ints 4;a:Precedence.PAssoc}={s=str@0;p=0;a=<Precedence.PN>};"Term";
-}
-abstract Formula={flags modulesize=n10;fun A:Formula.Formula={};
-fun Abs:Formula.Formula={};
-fun And:(h_:Formula.Formula)->(h_:Formula.Formula)->Formula.Formula={};
-fun B:Formula.Formula={};
-fun C:Formula.Formula={};
-cat Formula[]=;
-fun If:(h_:Formula.Formula)->(h_:Formula.Formula)->Formula.Formula={};
-fun Not:(h_:Formula.Formula)->Formula.Formula={};
-fun Or:(h_:Formula.Formula)->(h_:Formula.Formula)->Formula.Formula={};
-cat Term[]=;
-}
-resource Precedence=open Predef in{flags modulesize=n1;param PAssoc=PN|PL|PR;
-}
-resource Prelude=open Predef in{flags modulesize=n2;param Bool=True|False;
-param ENumber=E0|E1|E2|Emore;
-}
-resource Predef={flags modulesize=n1;param PBool=PTrue|PFalse;
-}