CS's system S

15 files changed, 562 insertions, 0 deletions

diff --git a/examples/systemS/Formula.gf b/examples/systemS/Formula.gf
new file mode 100644
index 000000000..62bc67eb7
--- /dev/null
+++ b/examples/systemS/Formula.gf
@@ -0,0 +1,20 @@
+-- 20 Dec 2005, 9.45
+
+abstract Formula = {
+
+  cat 
+    Formula ;
+    Term ;
+
+  fun
+    And, Or, If : (_,_ : Formula) -> Formula ;
+    Not : Formula -> Formula ;
+    Abs : Formula ;
+
+----    All, Exist : (Term -> Formula) -> Formula ;
+
+  -- to test
+
+    A, B, C : Formula ;
+
+}
\ No newline at end of file
diff --git a/examples/systemS/FormulaSymb.gf b/examples/systemS/FormulaSymb.gf
new file mode 100644
index 000000000..5c2360673
--- /dev/null
+++ b/examples/systemS/FormulaSymb.gf
@@ -0,0 +1,22 @@
+--# -path=.:prelude
+
+concrete FormulaSymb of Formula = open Precedence in {
+
+  lincat
+    Formula, Term = PrecExp ;
+
+  lin
+    And = infixL 3 "&" ;
+    Or  = infixL 2 "v" ;
+    If  = infixR 1 "->" ;
+    Not = prefixR 4 "~" ;
+    Abs = constant "_|_" ;
+
+----    All P = mkPrec 4 PR (paren ("All" ++ P.$0) ++ usePrec P 4) ;
+----    Exist P = mkPrec 4 PR (paren ("Ex" ++ P.$0) ++ usePrec P 4) ;
+
+    A = constant "A" ;
+    B = constant "B" ;
+    C = constant "C" ;
+
+}
\ No newline at end of file
diff --git a/examples/systemS/Precedence.gf b/examples/systemS/Precedence.gf
new file mode 100644
index 000000000..7defd19aa
--- /dev/null
+++ b/examples/systemS/Precedence.gf
@@ -0,0 +1,42 @@
+resource Precedence = open (Predef = Predef) in {
+
+  param 
+    PAssoc = PN | PL | PR ;
+
+  oper 
+    Prec    : PType = Predef.Ints 4 ;
+    PrecExp : Type = {s : Str ; p : Prec ; a : PAssoc} ;
+
+    mkPrec : Prec -> PAssoc -> Str -> PrecExp = \p,a,f -> 
+      {s = f ; p = p ; a = a} ;
+
+    usePrec : PrecExp -> Prec -> Str = \x,p ->
+      case <<x.p,p> : Prec * Prec> of {
+        <3,4> | <2,3> | <2,4> => paren x.s ;
+        <1,1> | <1,0> | <0,0> => x.s ;
+        <1,_> | <0,_>         => paren x.s ;
+        _ => x.s
+        } ;
+
+    useTop : PrecExp -> Str = \e -> usePrec e 0 ;
+
+    constant : Str -> PrecExp = mkPrec 4 PN ;
+
+    infixN : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y ->
+      mkPrec p PN (usePrec x (nextPrec p) ++ f ++ usePrec y (nextPrec p)) ;
+    infixL : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y ->
+      mkPrec p PL (usePrec x p ++ f ++ usePrec y (nextPrec p)) ;
+    infixR : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y ->
+      mkPrec p PR (usePrec x (nextPrec p) ++ f ++ usePrec y p) ;
+
+    prefixR : Prec -> Str -> PrecExp -> PrecExp = \p,f,x ->
+      mkPrec p PR (f ++ usePrec x p) ;
+
+    nextPrec : Prec -> Prec = \p -> case <p : Prec> of {
+      4 => 4 ; 
+      n => Predef.plus n 1
+      } ;
+
+    paren : Str -> Str = \s -> "(" ++ s ++ ")" ;
+
+}
diff --git a/examples/systemS/Proof.gf b/examples/systemS/Proof.gf
new file mode 100644
index 000000000..06a6f1c68
--- /dev/null
+++ b/examples/systemS/Proof.gf
@@ -0,0 +1,23 @@
+abstract Proof = Formula ** {
+
+  cat
+    Text ;
+    Proof ;
+    [Formula] ;
+
+  fun
+    Start : [Formula] -> Formula -> Proof -> Text ;
+
+    Hypo : Proof ;
+    Implic : [Formula] -> Formula -> Proof -> Proof ;
+    RedAbs : Formula -> Proof -> Proof ;
+    ExFalso : Formula -> Proof ;
+    ConjSplit : Formula -> Formula -> Formula -> Proof -> Proof ;
+    ModPon : [Formula] -> Formula -> Proof -> Proof ;
+    Forget : [Formula] -> Formula -> Proof -> Proof ;
+
+    DeMorgan1, DeMorgan2 : Formula -> Formula -> Proof -> Proof ;
+    ImplicNeg : [Formula] -> Formula -> Proof -> Proof ;
+    NegRewrite : Formula -> [Formula] -> Proof -> Proof ;
+
+}
diff --git a/examples/systemS/ProofEng.gf b/examples/systemS/ProofEng.gf
new file mode 100644
index 000000000..612e228c8
--- /dev/null
+++ b/examples/systemS/ProofEng.gf
@@ -0,0 +1,133 @@
+--# -path=.:prelude
+
+concrete ProofEng of Proof = FormulaSymb ** open Prelude, Precedence in {
+
+  flags startcat=Text ; unlexer=text ; lexer = text ;
+
+  lincat
+    Text, Proof = {s : Str} ; 
+    [Formula] = {s : Str ; isnil : Bool} ;
+
+  lin
+    Start prems concl proof = {
+      s = ifNotNil (\p -> "Suppose" ++ p ++ ".") prems ++
+          ["We will show that"] ++ useTop concl ++ "." ++
+          proof.s
+      } ; 
+
+    Hypo = {
+      s = new ++ ["But this holds trivially ."]
+      } ;
+
+    Implic prems concl proof = {
+      s = new ++ ["It is enough to"] ++
+          ifNotNil (\p -> "assume" ++ p ++ "and") prems ++
+          "show" ++ concl.s ++ 
+          "." ++
+          proof.s ;
+      } ;
+
+    RedAbs form proof = 
+      let neg = useTop (prefixR 4 "~" form) in {
+      s = new ++ ["To that end , we will assume"] ++ 
+          neg ++
+          ["and show"] ++ "_|_" ++ 
+          "." ++
+          new ++ ["So let us assume that"] ++
+          neg ++ 
+          "." ++
+          proof.s
+      } ;
+
+    ExFalso form = {
+      s = new ++ ["Hence we get"] ++ 
+          useTop form ++ ["as desired"] ++ 
+          "." 
+      } ;
+
+    ConjSplit a b c proof = {
+      s = new ++ ["So by splitting we get"] ++ 
+          useTop a ++ "," ++ useTop b ++
+          toProve c ++
+          "." ++ 
+          proof.s
+      } ;
+
+    ModPon prems concl proof = {
+      s = new ++ ["Then , by Modus ponens , we get"] ++ prems.s ++
+          toProve concl ++
+          "." ++ 
+          proof.s
+      } ;
+
+    Forget prems concl proof = {
+      s = new ++ ["In particular we get"] ++ prems.s ++
+          toProve concl ++
+          "." ++ 
+          proof.s
+      } ;
+
+--
+
+    DeMorgan1 = \form, concl, proof -> {
+      s = new ++ ["Then , by the first de Morgan's law , we get"] ++ useTop form ++
+          toProve concl ++
+          "." ++ 
+          proof.s
+      } ;
+
+    DeMorgan2 = \form, concl, proof -> {
+      s = new ++ ["Then , by the second de Morgan's law , we get"] ++ useTop form ++
+          toProve concl ++
+          "." ++ 
+          proof.s
+      } ;
+
+    ImplicNeg forms concl proof = {
+      s = new ++ ["By implication negation , we get"] ++ forms.s ++
+          toProve concl ++
+          "." ++ 
+          proof.s
+      } ;
+
+    NegRewrite form forms proof = 
+      let 
+        neg  = useTop (prefixR 4 "~" form) ;
+        impl = useTop (infixR 1 "->" form (constant "_|_")) ;
+      in {
+      s = new ++ ["Thus , by rewriting"] ++ 
+          neg ++
+          ifNotNil (\p -> ["we may assume"] ++ p ++ "and") forms ++ 
+          "show" ++ impl ++ 
+          "." ++
+          proof.s
+      } ;
+
+--
+
+    BaseFormula = {
+      s = [] ; 
+      isnil = True
+      } ;
+
+    ConsFormula f fs = {
+      s = useTop f ++ ifNotNil (\p -> "," ++ p) fs ; 
+      isnil = False
+      } ;
+    
+  oper
+    ifNotNil : (Str -> Str) -> {s : Str ; isnil : Bool} -> Str = \cons,prems ->
+      case prems.isnil of {
+         True  => prems.s ;
+         False => cons prems.s
+         } ;
+
+    new = variants {"&-" ; []} ; -- unlexing and parsing, respectively
+
+    toProve : PrecExp -> Str = \c -> 
+      variants {
+        [] ;                      -- for generation
+        ["to prove"] ++ useTop c  -- for parsing
+        } ;
+
+}
diff --git a/examples/systemS/ProofSymb.gf b/examples/systemS/ProofSymb.gf
new file mode 100644
index 000000000..4ff18ca14
--- /dev/null
+++ b/examples/systemS/ProofSymb.gf
@@ -0,0 +1,84 @@
+--# -path=.:prelude
+
+concrete ProofSymb of Proof = FormulaSymb ** open Prelude, Precedence in {
+
+  flags startcat=Text ; unlexer=text ; lexer = text ;
+
+  lincat
+    Text, Proof = {s : Str} ; 
+    [Formula] = {s : Str ; isnil : Bool} ;
+
+  lin
+    Start prems concl = continue [] (task prems.s concl.s) ;
+
+    Hypo = finish "Hypothesis" "Ø" ;
+
+    Implic prems concl = continue ["Implication strategy"] (task prems.s concl.s) ;
+
+    RedAbs form = continue ["Reductio ad absurdum"] (task neg abs)
+      where { neg = useTop (prefixR 4 "~" form) } ;
+
+    ExFalso form = finish (["Ex falso quodlibet"] ++ form.s) "Ø" ; --- form
+
+    ConjSplit a b c = 
+      continue ["Conjunction split"] 
+        (task (useTop a ++ "," ++ useTop b) (useTop c)) ;
+
+    ModPon prems concl = continue ["Modus ponens"] (task prems.s concl.s) ;
+
+    Forget prems concl = continue "Forgetting" (task prems.s concl.s) ;
+
+--
+
+    DeMorgan1 = \form, concl ->
+      continue ["de Morgan 1"] (task form.s concl.s) ;
+    DeMorgan2 = \form, concl ->
+      continue ["de Morgan 2"] (task form.s concl.s) ;
+
+    ImplicNeg forms concl = 
+      continue ["Implication negation"] (task forms.s concl.s) ;
+
+    NegRewrite form forms = 
+      let 
+        neg  = useTop (prefixR 4 "~" form) ;
+        impl = useTop (infixR 1 "->" form (constant "_|_")) ;
+      in 
+      continue ["Negation rewrite"] (task forms.s impl) ;
+
+--
+
+    BaseFormula = {
+      s = [] ; 
+      isnil = True
+      } ;
+
+    ConsFormula f fs = {
+      s = useTop f ++ ifNotNil (\p -> "," ++ p) fs ; 
+      isnil = False
+      } ;
+    
+  oper
+    ifNotNil : (Str -> Str) -> {s : Str ; isnil : Bool} -> Str = \cons,prems ->
+      case prems.isnil of {
+         True  => prems.s ;
+         False => cons prems.s
+         } ;
+
+    continue : Str -> Str -> {s : Str} -> {s : Str} = \label,task,proof -> {
+      s = label ++ new ++ task ++ new ++ line ++ proof.s
+      } ;
+
+    finish : Str -> Str -> {s : Str} = \label,task -> {
+      s = label ++ new ++ task 
+      } ;
+
+    task : Str -> Str -> Str = \prems,concl ->
+      "[" ++ prems ++ "|-" ++ concl ++ "]" ;
+
+    new = variants {"&-" ; []} ; -- unlexing and parsing, respectively
+
+    line = "------------------------------" ;
+
+    abs = "_|_" ;
+ 
+}
\ No newline at end of file
diff --git a/examples/systemS/README b/examples/systemS/README
new file mode 100644
index 000000000..ebbd92ce6
--- /dev/null
+++ b/examples/systemS/README
@@ -0,0 +1,65 @@
+AR 20/12/2005
+
+This is a translator of a part of the proof system
+by Claes Strannegård, as defined in the manuscript
+"Translating Formal Proofs into English".
+
+The functionality is to translate between a formal
+and an informal notation for proofs.
+
+As examples, we provide 3 of the 4 examples in
+Strannegård's paper. His example 3 is left as exercise.
+
+A good way to start is
+
+  % gf <test.gfs
+
+which will translate the proofs back and forth.
+
+If you modify the grammars and want to compile from source, you also need
+
+  % export GF_LIB_PATH=/home/aarne/GF/lib -- set to the path in your system
+
+Files:
+
+  ex1eng.txt      -- the 3 tests
+  ex1.txt    
+  ex2eng.txt
+  ex2.txt
+  ex4eng.txt
+  ex4.txt
+
+  Formula.gf      -- abstract syntax of formulas
+  FormulaSymb.gf  -- concrete syntax of formulas
+  Precedence.gf   -- precedence package
+  ProofEng.gf     -- top concrete syntax, English
+  Proof.gf        -- top abstract syntax
+  ProofSymb.gf    -- top concrete syntax, symboli
+
+  proof.gfcm      -- precompiled translator
+
+  README          -- this file
+  test.gfs        -- the test script
+
+
+Notes:
+
+1. The abstract syntax does not do proof checking.
+
+2. de Morgan labels have been disambiguated with "1" and "2".
+
+3. The symbolic Ex falso quodlibet rule needs to show the
+   conclusion formula in the label to make linearization 
+   possible (in the absence of smart proof checking).
+
+4. The English concrete syntax needs some extra formula
+   arguments for the same reason. These arguments can be
+   omitted, but the resulting parser returns some 
+   metavariables.
+
+An interesting further task would be to implement the
+proof checker and a proof search procedure, in Haskell or,
+even better, in the GF Transfer Language.
+
+Another nice thing would be to linearize the formulas
+into real English.
diff --git a/examples/systemS/ex1.txt b/examples/systemS/ex1.txt
new file mode 100644
index 000000000..d62b5882b
--- /dev/null
+++ b/examples/systemS/ex1.txt
@@ -0,0 +1,8 @@
+[ |- A -> B -> A ] 
+------------------------------ Implication strategy 
+[ A |- B -> A ] 
+------------------------------ Implication strategy 
+[ A , B |- A ] 
+------------------------------ Hypothesis 
+Ø
+
diff --git a/examples/systemS/ex1eng.txt b/examples/systemS/ex1eng.txt
new file mode 100644
index 000000000..255440486
--- /dev/null
+++ b/examples/systemS/ex1eng.txt
@@ -0,0 +1,4 @@
+We will show that A -> B -> A.
+It is enough to assume A and show B -> A.
+It is enough to assume A, B and show A.
+But this holds trivially.
diff --git a/examples/systemS/ex2.txt b/examples/systemS/ex2.txt
new file mode 100644
index 000000000..1dffb6bf9
--- /dev/null
+++ b/examples/systemS/ex2.txt
@@ -0,0 +1,13 @@
+[ A -> B |- ~ B -> ~ A ]
+------------------------------ Implication strategy
+[ A -> B , ~ B |- ~ A ]
+------------------------------ Negation rewrite
+[ A -> B , ~ B |- A -> _|_ ]
+------------------------------ Implication strategy
+[ A , A -> B , ~ B |- _|_ ]
+------------------------------ Modus ponens
+[ A , A -> B , B , ~ B |- _|_ ]
+------------------------------ Forgetting
+[ B , ~ B |- _|_ ]
+------------------------------ Ex falso quodlibet _|_
+Ø
diff --git a/examples/systemS/ex2eng.txt b/examples/systemS/ex2eng.txt
new file mode 100644
index 000000000..f1ef836ae
--- /dev/null
+++ b/examples/systemS/ex2eng.txt
@@ -0,0 +1,7 @@
+Suppose A -> B. We will show that ~ B -> ~ A.
+It is enough to assume A -> B, ~ B and show ~ A.
+Thus, by rewriting ~ A we may assume A -> B, ~ B and show A -> _|_.
+It is enough to assume A, A -> B, ~ B and show _|_.
+Then, by Modus ponens, we get A, A -> B, B, ~ B to prove _|_.
+In particular we get B, ~ B to prove _|_.
+Hence we get _|_ as desired.
diff --git a/examples/systemS/ex4.txt b/examples/systemS/ex4.txt
new file mode 100644
index 000000000..7a91011da
--- /dev/null
+++ b/examples/systemS/ex4.txt
@@ -0,0 +1,13 @@
+[ |- (A -> B) v (B -> A) ]
+------------------------------ Reductio ad absurdum
+[ ~ ((A -> B) v (B -> A)) |- _|_ ]
+------------------------------ de Morgan 1
+[ ~ (A -> B) & ~ (B -> A) |- _|_ ]
+------------------------------ Conjunction split
+[ ~ (A -> B), ~ (B -> A) |- _|_ ]
+------------------------------ Implication negation
+[ A, ~ (B -> A) |- _|_ ]
+------------------------------ Implication negation
+[ A, ~ A |- _|_ ]
+------------------------------ Ex falso quodlibet _|_
+Ø
diff --git a/examples/systemS/ex4eng.txt b/examples/systemS/ex4eng.txt
new file mode 100644
index 000000000..3ad4f3549
--- /dev/null
+++ b/examples/systemS/ex4eng.txt
@@ -0,0 +1,8 @@
+We will show that (A -> B) v (B -> A).
+To that end, we will assume ~ ((A -> B) v (B -> A)) and show _|_.
+So let us assume that ~ ((A -> B) v (B -> A)).
+Then, by the first de Morgan's law, we get ~ (A -> B) & ~ (B -> A) to prove _|_.
+So by splitting we get ~ (A -> B), ~ (B -> A) to prove _|_.
+By implication negation, we get A, ~ (B -> A) to prove _|_.
+By implication negation, we get A, ~ A to prove _|_.
+Hence we get _|_ as desired.
diff --git a/examples/systemS/proof.gfcm b/examples/systemS/proof.gfcm
new file mode 100644
index 000000000..6e9692769
--- /dev/null
+++ b/examples/systemS/proof.gfcm
@@ -0,0 +1,113 @@
+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;
+}
diff --git a/examples/systemS/test.gfs b/examples/systemS/test.gfs
new file mode 100644
index 000000000..db5e64cbf
--- /dev/null
+++ b/examples/systemS/test.gfs
@@ -0,0 +1,7 @@
+i proof.gfcm
+rf ex1.txt | p -tr -lang=ProofSymb | l -lang=ProofEng
+rf ex2.txt | p -tr -lang=ProofSymb | l -lang=ProofEng
+rf ex4.txt | p -tr -lang=ProofSymb | l -lang=ProofEng
+rf ex1eng.txt | p -tr -lang=ProofEng | l -lang=ProofSymb
+rf ex2eng.txt | p -tr -lang=ProofEng | l -lang=ProofSymb
+rf ex4eng.txt | p -tr -lang=ProofEng | l -lang=ProofSymb