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

15 files changed, 0 insertions, 568 deletions

diff --git a/examples/systemS/Formula.gf b/examples/systemS/Formula.gf
deleted file mode 100644
index 62bc67eb7..000000000
--- a/examples/systemS/Formula.gf
+++ /dev/null
@@ -1,20 +0,0 @@
--- 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
deleted file mode 100644
index 5c2360673..000000000
--- a/examples/systemS/FormulaSymb.gf
+++ /dev/null
@@ -1,22 +0,0 @@
---# -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
deleted file mode 100644
index 7defd19aa..000000000
--- a/examples/systemS/Precedence.gf
+++ /dev/null
@@ -1,42 +0,0 @@
-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
deleted file mode 100644
index 06a6f1c68..000000000
--- a/examples/systemS/Proof.gf
+++ /dev/null
@@ -1,23 +0,0 @@
-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
deleted file mode 100644
index 612e228c8..000000000
--- a/examples/systemS/ProofEng.gf
+++ /dev/null
@@ -1,133 +0,0 @@
---# -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
deleted file mode 100644
index 3de1b91b7..000000000
--- a/examples/systemS/ProofSymb.gf
+++ /dev/null
@@ -1,90 +0,0 @@
---# -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"] ++ toProve form) "Ø" ; --- 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 = "_|_" ;
- 
-    toProve : PrecExp -> Str = \c -> 
-      variants {
-        [] ;      -- for generation
-        useTop c  -- for parsing
-        } ;
-
-}
\ No newline at end of file
diff --git a/examples/systemS/README b/examples/systemS/README
deleted file mode 100644
index ebbd92ce6..000000000
--- a/examples/systemS/README
+++ /dev/null
@@ -1,65 +0,0 @@
-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
deleted file mode 100644
index d62b5882b..000000000
--- a/examples/systemS/ex1.txt
+++ /dev/null
@@ -1,8 +0,0 @@
-[ |- 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
deleted file mode 100644
index 255440486..000000000
--- a/examples/systemS/ex1eng.txt
+++ /dev/null
@@ -1,4 +0,0 @@
-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
deleted file mode 100644
index 1dffb6bf9..000000000
--- a/examples/systemS/ex2.txt
+++ /dev/null
@@ -1,13 +0,0 @@
-[ 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
deleted file mode 100644
index f1ef836ae..000000000
--- a/examples/systemS/ex2eng.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-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
deleted file mode 100644
index 7a91011da..000000000
--- a/examples/systemS/ex4.txt
+++ /dev/null
@@ -1,13 +0,0 @@
-[ |- (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
deleted file mode 100644
index 3ad4f3549..000000000
--- a/examples/systemS/ex4eng.txt
+++ /dev/null
@@ -1,8 +0,0 @@
-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
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;
-}
diff --git a/examples/systemS/test.gfs b/examples/systemS/test.gfs
deleted file mode 100644
index db5e64cbf..000000000
--- a/examples/systemS/test.gfs
+++ /dev/null
@@ -1,7 +0,0 @@
-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