(* In this file we once again develop Landau's analysis book,
using the latest version of the prover, and using an axiomatic approach
(we do not prove the axioms from set theory; we may come back and
do that again later *)

(* from August 10 on I'm maintaining dated version notes here *)

(* August 13:

Almost to the end of chapter I!  Theorems after Satz32 up to the end of 
the chapter are stated but not yet proved.

*)

(* August 11:

I must fix the back function so that it works correctly with
usubs.  It is useless for backing through algebraic calculations as
it is.

How about a version of rewrites which uses a matching term as an argument?

*)

(* August 10, posted again:

Completed proof of Satz 29, commutativity of multiplication.  Note
the blowup of type checking obligations in the proof of the lemma
LeftTimesSucc.  I think that automatic recognition of Triv's would
help, combined with automatic theorem matching and a list of theorems
to be automatically applied (in type checking, perhaps automatic
theorem cuts as well?)

*)

(* August 10:  just finished Satz 27, the well-ordering principle, and am
about to start proving theorems about multiplication.

The proof of Satz 27 is in some sense a direct induction proof
 *)

(* comments calling for some action later:

it would be useful to get the prover to say something like
<hit enter> when it is pausing.

It might be possible to automate proofs that objects are of
appropriate types?

It is clear that it would be useful to automate proof of anything
immediately trivial after a certain level; this would eliminate
a lot of explicit type proofs, for example.  The more complicated
type proofs are also automatable though.  If we see a conclusion
of the form X+Y E Nat we could look for hypotheses X E Nat
and Y E Nat and auto-prove if they are found.

Automatic search for appropriate hyps and conclusions for UseThm
is eventually a must.

A formal implementation of "exactly one of the following n
statements is true" and of "respectively" would be useful.  It
might be manageable with some set theory?

If the bookmark command actually copied the current sequent
one level higher in proof tree and moved to it, then automatic
reordering and elimination of redundant hypotheses would not
generate surprises in the forms of theorems.  Just a thought.

*)

(* Theory of the natural numbers *)

(* For Landau version we want to start with 1, not 0 *)

(* we use more standard axioms for addition and multiplication,
rather than Landau's second-order definition of + and *;
we also use x+1 instead of x'.  This does not seem to
affect the Landau development beyond a certain point, but
we will see. *)

(* definite description operator *)

(* this enables us to introduce operations which pick out any
uniquely definable object *)

DeclareFunction "The" [0,1];

(* if the object to be described is a set, this is definable *)

(* Theset(a1) is the unique element of a1 if this is a set, otherwise
it is the empty set *)

DefineFunction 1 "Theset" 
"Theset(x1)" "{x2|(Ax3.(Ax4.x3Ex1&x4Ex1->x3=x4))&(Ex3.x3Ex1&x2Ex3)}";

Axiom "THE" [] ["The({x2|x2=a1})=a1"];

(* the basic property of The *)

Start "(Ax1.(Ax2.x1Ea1&x2Ea1->x1=x2))&a2Ea1->a2=The(a1)";
r();l();  bookmark "THE2";

Cut "a1 = {x1|x1=a2}";

r(); Triv 2 1;
r(); r(); r();
Gl 2; l();
l(); r(); Triv 4 1; Triv 3 1; Done();
l(); rwr nil; Triv 3 1;
rwr nil;
ThmCut "THE";
rwr nil; r();

ProveMarked "THE2" "THE2";

(* Theset has a similar basic theorem *)

(* declarations *)

DeclareFunction "Nat" [0];

DeclareFunction "+" [0,0,0];

DeclareFunction "*" [0,0,0];

(* order of operations *)

Spra "*" "+";

(* axioms *)

Axiom "OneNat" nil ["1ENat"];

(* the next axiom looks different because I write successor
as x+1 (not as a separate operation) so closure under successor is
a special case of closure under addition  *)

Axiom "SumNat" ["a1ENat","a2ENat"] ["a1+a2ENat"];

(* I prove the expected axiom as a theorem *)

Start "a1ENat -> a1+1ENat";
r(); ThmCut "SumNat";
Done(); UseThm "OneNat" nil [1];
Done();

Prove 2 "SuccNat";

Axiom "OneNotSucc" ["a1ENat","a1+1=1"] nil;

Axiom "SameSucc" ["a1ENat","a2ENat","a1+1=a2+1"] ["a1=a2"];

(* notice use of a restricted quantifier *)

Axiom "Induction" ["1Ea1","(Ax1:Nat.x1Ea1->x1+1Ea1)","a2ENat"] ["a2Ea1"];

(* additional axioms to handle recursive definition of addition
and multiplication *)

Axiom "PlusSucc" ["a1ENat","a2ENat"] ["a1+[a2+1]=[a1+a2]+1"];

Axiom "TimesOne" ["a1ENat"] ["a1*1=a1"];

Axiom "TimesSucc" ["a1ENat","a2ENat"] ["a1*[a2+1]=a1*a2+a1"];

(* a very easy theorem *)

(* an odd feature of this theorem is that the ind hyp
is never used *)

Start "a1ENat -> a1=1 v (Ex1:Nat.x1+1=a1)";
ThmCut "Induction";
su 2 "{x1:Nat|x1=1v(Ex2:Nat.x2+1=x1)}";
r();(* r(); *) UseThm "OneNat" nil [1];
r();r();

(* proof of induction step starts *)

r();r();r();(* r(); *)
ThmCut "OneNat"; UseThm "SumNat" [3,1] [1];
r(); gr 2; r(); Triv 2 1; r();

(* from here on seems to be tidying up ThmCut *)

su 3 "a1"; Gr 2; Triv 1 2;

l(); (* rf(); *) r(); Triv 3 1;

Prove 1 "OneOrSucc";

(* here starts the proposition by proposition implementation of Landau *)

DefinePredicate 2 "neq" "x1 neq x2" "~x1=x2";

Start "a1ENat & a2ENat & a1 neq a2 -> a1+1 neq a2+1";
r();l();Gl 2;

Gl 2; l(); Gr 2; r();

UseThm "SameSucc" [2,3,1] [1];

NameSequent 4 "Satz1";

Start "a1ENat -> a1 neq a1+1";
r();r();r();
ThmCut "Induction";
su 2 "{x1:Nat|x1 neq x1+1}";
r(); UseThm "OneNat" nil [1];
r();r();  ThmCut "OneNotSucc";
UseThm "OneNat" nil [1];
crwr nil; r();
r();r();l();r(); UseThm "SuccNat" [1] [1];
ThmCut "Satz1"; Triv 2 1; Done();UseThm "SuccNat" [1] [1]; Done();
Triv 2 1; l(); Gl 2; l(); Done();

Prove 2 "Satz2";

Start "a1ENat & a1 neq 1 -> (Ex1:Nat.x1+1=a1)";
r(); l(); bookmark "Satz3";
ThmCut "Induction";
su 2 "{x1:Nat|x1=1v(Ex2:Nat.x2+1=x1)}";
r(); UseThm "OneNat" nil [1];
r();r();
r();r();r(); UseThm "SuccNat" [2] [1];
r(); Gr 2; 
Triv 2 1;

r(); Done();
l(); Gl 2; Gl 3; l(); Triv 2 1; Done();

ProveMarked "Satz3" "Satz3";

(* Satz4 is an axiom in our scheme *)
(* though it might be interesting to try to prove it *)

Start "a1ENat&a2ENat&a3ENat->[a1+a2]+a3=a1+a2+a3";
r(); l(); Gl 2; gl 3;  bookmark "Satz5";
ThmCut "Induction";
su 4 "{x1:Nat|[a1+a2]+x1=a1+a2+x1}";
r(); UseThm "OneNat" nil [1];
ThmCut "PlusSucc"; sg(); sg();
crwr [1]; r(); Done(); Triv 2 1;

r();r();l();r(); UseThm "SuccNat" [1][1];
ThmCut "PlusSucc"; sg(); sg();
rwr [1];
ThmCut "PlusSucc"; sg(); sg();
rwr [1];
ThmCut "PlusSucc"; sg(); sg();
rwr [1];
gl 5; rwr [1];r();
Triv 6 1; UseThm "SumNat" [7,5] [1]; Triv 6 1; Triv 4 1;

UseThm "SumNat" [4,5] [1]; Done(); Triv 3 1; l(); Triv 2 1;

ProveMarked "Satz5" "Satz5";

Start "a1ENat->1+a1=a1+1";
r(); bookmark "OneComm";
ThmCut "Induction";
su 2 "{x1:Nat|1+x1=x1+1}";
r(); UseThm "OneNat" nil [1]; r();

r();r();l();r(); UseThm "SuccNat" [1] [1];
gl 2; crwr [2];
ThmCut2 "Satz5";
crwr [1]; r();
UseThm "OneNat" nil [1]; Triv 2 1;UseThm "OneNat" nil [1];

Done(); l(); Triv 2 1;

(* two lemmas needed for Satz 6 *)

ProveMarked "OneComm" "OneComm";

Start "a1ENat&a2ENat->[a1+1]+a2=[a1+a2]+1";
r();l(); bookmark "LeftPlusSucc";
ThmCut "Induction";
su 3 "{x1:Nat|[a1+1]+x1=[a1+x1]+1}";
r(); UseThm "OneNat" nil [1]; r();

r();r();l();r(); UseThm "SuccNat" [1][1];
ThmCut2 "PlusSucc"; rwr [1];
gl 3; rwr [1];
ThmCut2 "PlusSucc"; rwr [1]; r();
Triv 3 1; Triv 6 1; UseThm "SuccNat" [4] [1]; Triv 3 1;
sg();l(); Triv 2 1; Triv 2 1;

ProveMarked "LeftPlusSucc" "LeftPlusSucc";

Start "a1ENat & a2ENat -> a1+a2=a2+a1";
r();l(); bookmark "Satz6";
ThmCut "Induction";
su 3 "{x1:Nat|a1+x1=x1+a1}";
r(); UseThm "OneNat" nil [1];
ThmCut2 "OneComm";
rwr [1]; r(); Done();

r();r();l();r(); UseThm "SuccNat" [1][1];
gl 2;
ThmCut2 "LeftPlusSucc"; rwr [1];
ThmCut2 "PlusSucc"; rwr [1];
gl 3; rwr [1]; r();
Triv 4 1; Triv 3 1; Triv 5 1; Triv 3 1;

sg();l(); Triv 2 1; Triv 2 1;

ProveMarked "Satz6" "Satz6";

Start "a1ENat&a2ENat->a2 neq a1 + a2";

r();l(); bookmark "Satz7";

ThmCut "Induction";

su 3 "{x1:Nat|x1 neq a1+x1}";

r(); UseThm "OneNat" nil [1];

r(); r();  ThmCut "OneNotSucc";

Triv 2 1; crwr [1]; r();

r();r();l();r(); UseThm "SuccNat" [1][1];

Gl 2;l();Gr 2;r();

ThmCut2 "PlusSucc"; rwl [1];

ThmCut2 "SameSucc";

Triv 1 2; Triv 6 1; UseThm "SumNat" [4,3] [1]; Triv 2 1; Triv 3 1;
   Triv 2 1;

sg();l(); Triv 2 1; Triv 2 1;

ProveMarked "Satz7" "Satz7";

(* a technical variation of Satz7 *)

Start "a1ENat&a2ENat->a1 neq a1+a2";
r();l(); bookmark "Satz7b";
ThmCut2 "Satz6"; rwr nil;
UseThm "Satz7" [3,2] [1];
Done(); Triv 2 1;

ProveMarked "Satz7b" "Satz7b";

(* start proof of Satz 8 *)

Start "a1ENat&a2ENat&a3ENat->a2neq a3 ->a1+a2 neq a1+a3";

r();l();Gl 2;gl 3;

r(); bookmark "Satz8";

ThmCut2 "Induction";  (* using ThmCut2 seems to be an improvement *)

su 5 "a1"; su 4 "{x1:Nat|x1+a2 neq x1+a3}";

l(); Triv 2 1;

r(); UseThm "OneNat" nil [1];

l();l(); Gr 2; r();

ThmCut "OneComm"; sg(); rwl nil;
ThmCut "OneComm"; sg(); gl2 3; rwl nil;

UseThm "SameSucc" [4,5,2] [2];

Triv 5 1; Triv 3 1;

r();r();l();r(); UseThm "SuccNat" [1][1];

Gl 2;l();Gr 2;r();

ThmCut2 "LeftPlusSucc"; rwl nil; pl 1;
ThmCut2 "LeftPlusSucc"; rwl nil; pl 1;

ThmCut2 "SameSucc"; Triv 1 2;
UseThm "SumNat" [7,5] [1];
UseThm "SumNat" [7,6] [1];
Done(); Triv 7 1; Triv 6 1; Triv 7 1; Triv 5 1; Triv 2 1;

ProveMarked "Satz8" "Satz8";

(* start proof of Satz 9 *)

(* it is divided into two parts, one asserting the disjunction
of the three alternatives and one excluding the possibility that
the second and third alternatives both hold *)

(* the first alternative is shown to be incompatible
with the other two by an earlier theorem (Satz 7) *)

(* this should be called Satz9B *)

Start "a1ENat&a2ENat->a1=a2v(Ex1:Nat.a1=a2+x1)v(Ex1:Nat.a2=a1+x1)";
r();l();

bookmark "Satz9B";

ThmCut2 "Induction";

su 4 "a2";
su 3 "{x1:Nat|a1=x1v(Ex2:Nat.a1=x1+x2)v(Ex2:Nat.x1=a1+x2)}";

l(); Triv 2 1;

r(); UseThm "OneNat" nil [1];

r(); Gr 2;

ThmCut "Satz3"; su 3 "a1"; Done();  (* Satz3 needed to be reproved! *)

r();r(); Triv 1 4;

(* this should be called Satz9A *)

Start "a1ENat&a2ENat&a3ENat&a4ENat->a1=a2+a3->a2 neq a1+a4";

r(); l(); Gl 2; Gl 2; gl 3; r(); bookmark "Satz9A";
rwr nil;
ThmCut2 "Satz5"; rwr nil;
ThmCut2 "Satz7b"; Done();
Triv 4 1; UseThm "SumNat" [5,6] [1];  Triv 3 1; Triv 4 1; Triv 5 1;

ProveMarked "Satz9A" "Satz9A";

(* Satz9b *)

Start "a1ENat&a2ENat->a1=a2v(Ex1:Nat.a1=a2+x1)v(Ex1:Nat.a2=a1+x1)";
r();l();r();Gr 2; bookmark "Satz9b";
ThmCut2 "Induction";
su 4 "a2";
su 3 "{x1:Nat | a1=x1 v (Ex2:Nat.a1=x1+x2)v(Ex2:Nat.x1=a1+x2)}";

l(); Gl 2; Triv 1 3;
l(); Done(); Triv 1 2;

r(); UseThm "OneNat" nil [1];
ThmCut2 "Satz3"; l();
su 3 "a1";

r(); Gr 2; r(); sg(); gl 2; crwr [1];
ThmCut2 "Satz6"; Done(); Triv 4 1; UseThm "OneNat" nil [1]; Done();
Done(); r(); r(); r(); Done();

(* survived basis step! *)

r();r();r(); UseThm "SuccNat" [2] [1];

l();r(); Gl 2;

Gr 2; Gr 2; sg(); rwr [1]; r();

UseThm "OneNat" nil [1];

l(); l(); ThmCut "OneOrSucc";

l(); Done();

l(); gl2 3; rwl nil; Triv 2 1;

l(); gl 2; gl2 3; crwl nil;

Gr 2; ThmCut2 "PlusSucc";

gl2 3; rwl nil; ThmCut2 "LeftPlusSucc";

gl2 3; crwl nil; crwl nil;

r(); sg(); Triv 2 1;

Triv 7 1; Triv 3 1; Triv 7 1; Triv 3 1; Triv 7 1;

l(); Gr 2; Gr 2; sg();

su 9 "a8+1"; gl 2; rwr nil;

ThmCut2 "PlusSucc"; rwr [1]; r();

Triv 3 1; Triv 6 1; UseThm "SuccNat" [1] [1];

Triv 2 1;

ProveMarked "Satz9b" "Satz9B";

DefinePredicate 2 ">" "x1>x2" "(Ex3:Nat.x1=x2+x3)";

DefinePredicate 2 "<" "x1<x2" "(Ex3:Nat.x2=x1+x3)";

DefinePredicate 2 ">=" "x1>=x2" "x1>x2vx1=x2";

DefinePredicate 2 "<=" "x1<=x2" "x1<x2vx1=x2"; 

(* that annoying "exactly one" problem again... *)

Start "a1ENat->~a1<a1";
r();r();bookmark "Satz10A";l();l(); gl 2;

ThmCut2 "Satz7";
l();l();  ThmCut2 "Satz6"; rwl nil; Triv 2 1;

Triv 2 1; Triv 3 1; Triv 3 1; Triv 2 1;

ProveMarked "Satz10A" "Satz10A";

Start "a1ENat->~a1>a1";
r();r(); bookmark "Satz10B";
l();l();  ThmCut2 "Satz7";
l();l();  ThmCut2 "Satz6"; gl2 3; rwl nil; Triv 2 1;

Triv 3 1; Done(); Done(); Triv 3 1;

ProveMarked "Satz10B" "Satz10B";

Start "a1ENat&a2ENat->~(a1<a2&a2<a1)";
r();l();r();l(); bookmark "Satz10C";
l();Gl 2;l();Gl 5;

ThmCut2 "Satz9A";

l();l(); Triv 2 1; Triv 4 1;

Triv 6 1; Triv 3 1; Done();

ProveMarked "Satz10C" "Satz10C";

(* there is a bug here one of the hypotheses is missing -- NO it is
fine -- the missing hyp is redundant and was removed by autoprune *)

Start "a1ENat&a2ENat->~(a1<a2&a1>a2)";
r();r();l();Gl 3;
bookmark "Satz10D";
Cut "a2<a1";r();Gl 4;Done();

UseThm "Satz10C" [4,1,3] nil;

ProveMarked "Satz10D" "Satz10D";

Start "a1ENat&a2ENat->a1=a2va1>a2va1<a2";
r();l();r();Gr 2;
bookmark "Satz10E";
r();Gr 2;

UseThm "Satz9B" [1,2] [3,1,2];

ProveMarked "Satz10E" "Satz10E";

Start "a1<a2->a2>a1";
r(); bookmark "Satz12";
l();r();Done();

ProveMarked "Satz12" "Satz12";

Start "a1>a2->a2<a1";
r(); bookmark "Satz11";
l();r();Done();

ProveMarked "Satz11" "Satz11";

Start "a1>a2==a2<a1";
r(); UseThm "Satz11" [1] [1];
UseThm "Satz12" [1] [1];

Prove 1 "OrderRewrite";

Start "a1>=a2->a2<=a1";
r(); bookmark "Satz13";
l();r();r();
l(); UseThm "Satz11" [1] [1];

gr 2; rwr nil; r();

ProveMarked "Satz13" "Satz13";

Start "a1<=a2->a2>=a1";
r(); bookmark "Satz14";
l();r();r();
l(); UseThm "Satz12" [1] [1];

gr 2; rwr nil; r();

ProveMarked "Satz14" "Satz14";

Start "a1>=a2==a2<=a1";
r(); UseThm "Satz13" [1][1];
UseThm "Satz14" [1][1];

Prove 1 "OrderRewrite2";

Start "a1ENat&a2ENat&a3ENat->a1<a2&a2<a3->a1<a3";
r();l();Gl 2;gl 3;
r();l(); bookmark "Satz15";

l();l();Gl 3;l();

r();r();sg();su 6 "a4+a5";

ThmCut2 "Satz5";
crwr nil;
gl 8; crwr nil;Triv 4 1;

Triv 3 1;Triv 6 1;Done();
UseThm "SumNat" [6,1][1];

ProveMarked "Satz15" "Satz15";

(* notice that hypotheses are automatically reduced here;
only a1 actually needs to be assumed natural *)

Start "a3ENat->a1>a2&a2>a3->a1>a3";
r();r();l(); bookmark "Satz15B";
ThmCut "OrderRewrite"; rwl nil; pl 1;
gl 2;ThmCut "OrderRewrite"; rwl nil; pl 1;
ThmCut "OrderRewrite"; rwr nil; pl 1;

UseThm "Satz15" [1,3,2] [1];

ProveMarked "Satz15B" "Satz15B";

(* notice use of biconditionals to rewrite in previous proof! *)

(* notice also that Landau's remarks on _not_ proving
something like Satz15B bring up exactly the issue of rewriting
inequalities which we here implement formally *)

(* Satz16A *)

Start "a1ENat->a1<=a2&a2<a3->a1<a3";
r();r();l(); bookmark "Satz16A";

l();l(); UseThm "Satz15" [1,2,3][1];

rwr nil; Triv 2 1;

ProveMarked "Satz16A" "Satz16A";

(* Satz16B *)

Start "a1ENat->a1<a2&a2<=a3->a1<a3";
r();r();l(); bookmark "Satz16B";

Gl 2;l(); UseThm "Satz15" [3,1,2] [1];

crwr nil; Triv 3 1;

ProveMarked "Satz16B" "Satz16B";

Start "a1ENat->a1<=a2&a2<=a3->a1<=a3";
r();r();l(); bookmark "Satz17";

(* define predecessor *)

DefineFunction 1 "Pred" "Pred(x1)" "The({x2 : Nat|(x1=1->x2=1)&(x1 neq 1 ->x2+1=x1)})";

(* prove basic properties of Pred *)

Start "a1 E Nat & a1 neq 1 -> Pred(a1)+1 = a1";

r(); l(); bookmark "PREDTHM";
ThmCut "Satz3"; Done(); Triv 2 1;
l();

Cut "a2=Pred(a1)";r();(* pr 1;pr 1; *)

ThmCut "THE2";

su 3 "{x3:Nat|(a1=1->x3=1)&(a1 neq 1 -> x3+1=a1)}";

r();r();r();l();l();Gl 2;Gl 3;Gl 2;

Gl 2;Triv 4 1;Gl 8;Triv 7 1;
gl 4;gl2 8;crwl nil;  UseThm "SameSucc" [9,3,2] [1];

r();Done();
r();r();gl 5;l();l();Done();
r();Triv 3 1;Done(); gl2 3; rwl nil; Triv 2 1;

ProveMarked "PREDTHM" "PREDTHM";

(* another theorem about The *)

Start "(Ax1.x1Ea1 == x1=a2) -> a2=The(a1)";
r(); bookmark "THE3";

Cut "a1={x2|x2=a2}";
r(); Gr 2; r();
r();l(); su 5 "a4";
r();r();Gl 2;l();Triv 3 1;Done();
l();Gl 2;Gl 2;Triv 2 1;Done();
rwr nil; ThmCut "THE"; rwr nil; r();

ProveMarked "THE3" "THE3";

(* back to the main line of Landau development *)

Start "a1ENat&a1<=a2&a2<=a3->a1<=a3";
r();l();Gl 2; bookmark "Satz17";
l();l();r();r();UseThm "Satz16B" [2,3,1] [1];
rwr nil;Triv 2 1; 

ProveMarked "Satz17" "Satz17";

Start "a1ENat&a2ENat->a1+a2>a1";
r();l(); bookmark "Satz18";
r();r();sg();r();Triv 2 1;

ProveMarked "Satz18" "Satz18";

(* note just above that hypotheses about a1 being in Nat
turn out not to be needed *)

Start "a1ENat&a2ENat&a3ENat&a1>a2->a1+a3>a2+a3";
r();l();Gl 2;Gl 2;  bookmark "Satz19A";
Gl 2;l();

r();r();sg(); su 5 "a4";
gl 2; rwr nil;

ThmCut2 "Satz6";
rwr [2];
ThmCut2 "Satz6";
rwr [3];
ThmCut2 "Satz5";
rwr nil; r();

Triv 7 1;Triv 5 1;Triv 6 1;
UseThm "SumNat" [4,5] [1];
Triv 6 1;Triv 3 1;Triv 5 1;Done();

ProveMarked "Satz19A" "Satz19A";

Start "a1ENat&a2ENat&a3ENat&a1<a2->a1+a3<a2+a3";
r();l();Gl 2;Gl 2; bookmark "Satz19B";
ThmCut "Satz12"; Triv 2 1;
ThmCut "Satz19A";
Done();Triv 4 1;
sg(); UseThm "Satz11" [1][1];
Triv 2 1;

ProveMarked "Satz19B" "Satz19B";

Start "a1ENat&a2ENat&a3ENat&a1+a3>a2+a3->a1>a2";
r();l();Gl 2;Gl 2;  bookmark "Satz20A";
ThmCut "Satz10E"; sg(); sg(); Done();
Cut "a1+a3<a2+a3"; UseThm "Satz19B" [2,1,4][1];

ThmCut2 "Satz10C";
Done(); UseThm "Satz11" [4][1];
UseThm "SumNat" [6,3][1];
gl2 3; rwl nil;

ThmCut2 "Satz10B"; Triv 2 1;
UseThm "SumNat" [4,5][1];

Triv 3 1; Triv 4 1;

ProveMarked "Satz20A" "Satz20A";

Start "a1ENat&a2ENat&a3ENat&a1+a3=a2+a3->a1=a2";
r();l();Gl 2;Gl 2;  bookmark "Satz20B";
ThmCut "Satz10E"; sg();sg();sg();sg();Done();
Triv 3 1;Triv 4 1;

ThmCut2 "Satz19A"; su 4 "a1"; su 5 "a2"; su 6 "a3";
gl 4; gl2 4; rwl nil; ThmCut "Satz10B"; Triv 2 1;
UseThm "SumNat" [6,4][1];Done();Triv 5 1;Triv 2 1;

ThmCut2 "Satz19B"; su 7 "a1"; su 8 "a2"; su 6 "a3";
gl 4; gl2 4; rwl nil; ThmCut "Satz10A"; Triv 2 1;
UseThm "SumNat" [6,4] [1];Triv 2 1;Done();Triv 4 1;

ProveMarked "Satz20B" "Satz20B";

Start "a1ENat&a2ENat&a3ENat&a1+a3<a2+a3->a1<a2";
r();l();Gl 2;Gl 2;  bookmark "Satz20C";

ThmCut "Satz12"; Triv 2 1;

ThmCut "Satz20A"; sg(); Done(); Triv 5 1; Triv 4 1;
UseThm "Satz11" [1] [1]; Triv 2 1;

ProveMarked "Satz20C" "Satz20C";

Start "a1ENat&a2ENat&a3ENat&a4ENat&a1>a2&a3>a4->a1+a3>a2+a4";
r();l();Gl 2;Gl 2;Gl 2; Gl 2; bookmark "Satz21";
ThmCut "Satz19A"; Done(); Triv 4 1; sg(); su 7 "a3";
ThmCut "Satz19A"; Triv 3 1; Triv 7 1; sg(); su 9 "a2";
ThmCut2 "Satz6"; rwl nil; pl 1;
ThmCut2 "Satz6"; rwl [2];
ThmCut2 "Satz15B"; Done(); Triv 3 1; Triv 2 1;
UseThm "SumNat" [7,9][1]; 
Triv 8 1; Triv 6 1; Triv 7 1; Triv 6 1;
Triv 5 1;Triv 5 1;

ProveMarked "Satz21" "Satz21";

(* Satz22A *)

Start "a1ENat&a2ENat&a3ENat&a4ENat&a1>=a2&a3>a4->a1+a3>a2+a4";

r();l();Gl 2;Gl 2;Gl 2;Gl 2;  bookmark "Satz22A";

l();l();ThmCut "Satz21";Done();Triv 2 1;
Triv 4 1;Triv 5 1;Triv 6 1;Done();

rwr nil; ThmCut "Satz19A";
Triv 2 1; Triv 6 1;
sg(); ThmCut2 "Satz6"; rwr [1];
ThmCut2 "Satz6"; rwr [2]; Triv 3 1;
Triv 6 1; Triv 8 1; Triv 5 1; Triv 6 1; Triv 4 1;

ProveMarked "Satz22A" "Satz22A";

(* Satz22B *)

Start "a1ENat&a2ENat&a3ENat&a4ENat&a1>a2&a3>=a4->a1+a3>a2+a4";
r();l();Gl 2;Gl 2;Gl 2;Gl 2;  bookmark "Satz22B";
ThmCut2 "Satz6"; rwr [1];
ThmCut2 "Satz6"; rwr [2];
ThmCut "Satz22A"; Triv 4 1; Triv 3 1;
Triv 8 1;Triv 5 1;Triv 6 1;Done();
Triv 5 1;Triv 7 1;Triv 3 1;Triv 5 1;

ProveMarked "Satz22B" "Satz22B";

(* Satz23 *)

Start "a1ENat&a2ENat&a3ENat&a4ENat&a1>=a2&a3>=a4->a1+a3>=a2+a4";
r();l();Gl 2;Gl 2;Gl 2;Gl 2;  bookmark "Satz23";
l();l();r();r();
UseThm "Satz22B" [1,2,3,4,5,6] [1];

rwr nil;r();r();Gl 2;l();
ThmCut2 "Satz6"; rwr [1];
ThmCut2 "Satz6"; rwr [2];

UseThm "Satz19A" [3,7,5] [1];

Triv 4 1;Triv 6 1;Triv 3 1;Triv 4 1;

gr 2; rwr nil; r();

ProveMarked "Satz23" "Satz23";

(* notice in the last couple of theorems contrast between
a style using ThmCut and a style using UseThm *)

(* Satz24 *) (* Aug. 9, number 1 *)

Start "a1ENat->a1>=1";
r(); bookmark "Satz24";

r();r();r();ThmCut "OneOrSucc";

l();Done();l();Triv 1 2;
l();r();Done();gl 2; crwr nil; ThmCut2 "Satz6"; 
Done(); Triv 3 1; UseThm "OneNat" nil [1];

ProveMarked "Satz24" "Satz24";

(* Satz24B *)

Start "~(a1ENat&a1<1)";
r();l(); bookmark "Satz24B";
ThmCut "Satz24"; Done();
l();l(); ThmCut "Satz10C";  Triv 3 1; UseThm "Satz11" [1][1];
UseThm "OneNat" nil [1];
gl2 3; rwl nil; ThmCut "Satz10A"; Triv 2 1;UseThm "OneNat" nil [1];

ProveMarked "Satz24B" "Satz24B";

(* Satz25 *)  (* Aug. 9, number 2 *)

Start "a1ENat&a2ENat&a1>a2->a1>=a2+1";
r();l();Gl 2;
l(); bookmark "Satz25";

Gl 2;l();gl 2; rwr nil;

ThmCut2 "Satz23"; Done();
r();r();Gr 2;

ThmCut2 "Satz24"; Done(); Triv 4 1; Triv 3 1; Triv 3 1; Triv 4 1;

UseThm "OneNat" nil [1];

ProveMarked "Satz25" "Satz25";

(* Satz26 *) (* Aug. 9, number 3 *)

Start "a1ENat&a2ENat&a2<a1+1->a2<=a1";
r();l();Gl 2; bookmark "Satz26";

Gl 2;l(); Cut "a2<=a1va2>a1";
r();r();r();Gr 4; r();

ThmCut2 "Satz10E"; Triv 1 5; Done(); Triv 1 2; Triv 4 1; Triv 3 1;

l(); Done();

Cut "a2+a3>a1+1";

ThmCut2 "Satz22B"; Done(); Done(); UseThm "Satz24" [2][1];

Triv 5 1; Triv 4 1; Triv 2 1; UseThm "OneNat" nil [1];

gl 4; gl2 4; rwl nil; ThmCut "Satz10B"; Triv 2 1;

UseThm "SumNat" [6,4] [1];

ProveMarked "Satz26" "Satz26";

(* Satz27 *) (* the well-ordering principle... *)

Start "a1ENat&a1Ea2->(Ex1:Nat.x1Ea2&(Ax2:Nat.x2Ea2->x2>=x1))";
r();l(); bookmark "Satz27";

ThmCut "Induction";

su 3 "{x1:Nat|(Ax2:Nat.x2<=x1->~x2Ea2)v(Ex2:Nat.x2<=x1&x2Ea2&(Ax3:Nat.x3Ea2->x3>=x2))}";

r(); UseThm "OneNat" nil [1];

r(); r(); r(); r(); Gl 2; l(); UseThm "Satz24B" [2,1] nil;
gl2 5; rwl nil;

Gr 2; UseThm "OneNat" nil [1];

r(); Triv 2 1; r(); r(); UseThm "Satz24" [2] [1];

r();r();l();

r(); UseThm "SuccNat" [1][1];

r(); r(); r(); r();  Gl 5;

Gl 6; l(); ThmCut "Satz26"; Done(); Triv 5 1; Triv 2 1;

Gl 5; Triv 8 1; l(); Triv 6 1; l(); Triv 5 1;

Gr 2; Triv 2 1; r(); Triv 8 1; r(); r();

Gl 6; Triv 7 1; l();

gl 8; gr 2; rwr nil; ThmCut2 "Satz10E"; su 10 "a9"; su 11 "a7";

ThmCut2 "Satz25"; Done(); Done(); Triv 6 1;

Gr 4; r(); Done(); Gr 4; r(); Triv 1 2;

Triv 10 1; Triv 3 1; l(); Triv 6 1; (* Done(); *)

l(); r(); Done();

r(); Gl 2;

Cut "a7 <= a7+1"; r();r();r();r();sg();r();UseThm "OneNat" nil [1];

ThmCut2 "Satz17"; Done();

Triv 2 1; Done();

Triv 11 1;

Gl 2; Triv 2 1;

Done(); l(); Gl 2; l(); sg(); l(); r(); r(); Gr 2; l(); Triv 3 1;

Triv 4 1; (* Done(); *)

l(); r(); sg(); r();

Gl 2; Gl 2; Done();

Gl 2; Gl 2; Triv 2 1; Done();

ProveMarked "Satz27" "Satz27";

(* the axioms for multiplication appear above *)
(* two lemmas implicit in Landau's Satz 28 are needed *)

(* lemma on left multiplication by one *)

Start "a1ENat->1*a1=a1";
r(); bookmark "OneTimesComm";

ThmCut "Induction";

su 2 "{x1:Nat|1*x1=x1}";

r(); UseThm "OneNat" nil [1];

ThmCut2 "TimesOne"; Done();
UseThm "OneNat" nil [1];

r(); r(); l(); r(); UseThm "SuccNat" [1][1];

ThmCut2 "TimesSucc"; rwr nil;

gl 3; rwr nil; r(); UseThm "OneNat" nil [1];
Done();Done();l();Triv 2 1;

ProveMarked "OneTimesComm" "OneTimesComm";

(* closure property of multiplication, not given as an axiom
but is provable *)

Start "a1ENat&a2ENat->a1*a2ENat";
r();l(); bookmark "TimesNat";

ThmCut "Induction";

su 3 "{x1:Nat|a1*x1ENat}";

r(); UseThm "OneNat" nil [1];

ThmCut2 "TimesOne"; rwr nil; Triv 2 1; Done();

r(); r(); l(); r(); UseThm "SuccNat" [1][1];

ThmCut2 "TimesSucc"; rwr nil;

ThmCut2 "SumNat"; Done(); Triv 3 1;Triv 5 1;Triv 4 1;Done();

Triv 2 1;l();Triv 2 1;

ProveMarked "TimesNat" "TimesNat";



(* lemma on left multiplication by a successor *)

Start "a1ENat&a2ENat->[a1+1]*a2=a1*a2+a2";
r();l(); bookmark "LeftTimesSucc";



ThmCut "Induction";

su 3 "{x1:Nat|[a1+1]*x1=a1*x1+x1}";

r(); UseThm "OneNat" nil [1];
ThmCut2 "TimesOne"; rwr nil;
ThmCut2 "TimesOne"; rwr nil;
r();
Triv 2 1;UseThm "SuccNat" [1][1];

r();r();l();r();UseThm "SuccNat" [1][1];

ThmCut2 "TimesSucc"; rwr nil;
ThmCut2 "TimesSucc"; rwr nil;

gl 4; rwr nil;

ThmCut2 "Satz5"; rwr nil;

ThmCut2 "Satz5"; crwr [2];

ThmCut2 "Satz6"; rwr [3];

ThmCut2 "Satz5"; rwr nil;ThmCut2 "Satz5"; rwr nil;r();

ThmCut2 "TimesNat"; Done(); Triv 7 1; Triv 11 1; Triv 7 1;

UseThm "SuccNat" [11][1]; Triv 6 1; Triv 10 1; UseThm "OneNat" nil [1];
Triv 9 1;Triv 5 1;Triv 8 1;Triv 4 1;UseThm "OneNat" nil [1];

ThmCut2 "TimesNat"; Done();Triv 3 1;Triv 7 1;Triv 7 1;
UseThm "SuccNat" [3] [1];Triv 5 1;Triv 4 1;UseThm "SuccNat" [4] [1];
Done(); Triv 2 1; l(); Triv 2 1;Done();

ProveMarked "LeftTimesSucc" "LeftTimesSucc";


(* Satz 29 *)

Start "a1ENat&a2ENat->a1*a2=a2*a1";
r();l(); bookmark "Satz29";

ThmCut "Induction";

su 3 "{x1:Nat|x1*a2=a2*x1}";

r(); UseThm "OneNat" nil [1];

ThmCut2 "TimesOne"; rwr nil;

ThmCut2 "OneTimesComm"; rwr nil; r();

Triv 3 1; Triv 2 1;

r();r();r(); UseThm "SuccNat" [2][1];

l(); ThmCut2 "TimesSucc"; rwr nil;

ThmCut2 "LeftTimesSucc"; rwr nil;

gl 4; rwr nil; r();

Triv 4 1;Triv 6 1;Triv 5 1;Done();Done();l();Triv 2 1;

ProveMarked "Satz29" "Satz29";

(* Satz 30 *)

s "a1ENat&a2ENat&a3ENat->a1*[a2+a3]=a1*a2+a1*a3";
r();l();Gl 2; bookmark "Satz30";

ThmCut "Induction";

su 4 "{x1:Nat|x1*[a2+a3]=x1*a2+x1*a3}";

r(); UseThm "OneNat" nil [1];

ThmCut2 "OneTimesComm"; rwr nil;
ThmCut2 "OneTimesComm"; rwr nil;
ThmCut2 "OneTimesComm"; rwr nil; r();

Triv 4 1;Triv 2 1;
UseThm "SumNat" [1,2] [1];

r();r();l();r(); UseThm "SuccNat" [1] [1];

ThmCut2 "LeftTimesSucc"; rwr nil;
ThmCut2 "LeftTimesSucc"; rwr nil;
ThmCut2 "LeftTimesSucc"; rwr nil;

gl 5; rwr nil;  (* from this point it is algebraic calculation,
                which is irritating *)

ThmCut2 "Satz5"; rwr nil;
ThmCut2 "Satz5"; crwr [2];
ThmCut2 "Satz6"; rwr [3];
ThmCut2 "Satz5"; rwr nil;
ThmCut2 "Satz5"; rwr nil;r();

(* now comes a block of type checking -- this needs to be automated *)

UseThm "TimesNat" [13,7] [1]; Triv 7 1;
ThmCut2 "SumNat"; Done();
UseThm "TimesNat" [13,8] [1]; Triv 8 1; Triv 6 1;
UseThm "TimesNat" [12,7] [1]; Triv 7 1;
UseThm "TimesNat" [11,6] [1]; Triv 5 1;
UseThm "TimesNat" [10,5] [1]; Triv 4 1; Triv 5 1;
UseThm "TimesNat" [9,3] [1];
UseThm "TimesNat" [9,4] [1];
UseThm "SumNat" [3,4] [1]; Triv 5 1; Triv 7 1; Triv 4 1;
Triv 5 1; Done();
UseThm "SumNat" [4,5] [1];

Triv 3 1;l();Triv 2 1;

ProveMarked "Satz30" "Satz30";

(* Satz30B -- left distributivity *)

s "a1ENat&a2ENat&a3ENat->[a1+a2]*a3=a1*a3+a2*a3";

r();l();Gl 2; bookmark "Satz30B";

ThmCut2 "Satz29";rwr nil;
ThmCut2 "Satz30";rwr nil;
ThmCut2 "Satz29";rwr nil;
ThmCut2 "Satz29";rwr [2];r();

Triv 5 1;Triv 4 1;Triv 4 1;Triv 5 1;Triv 4 1;Triv 2 1;Triv 3 1;
UseThm "SumNat" [3,1] [1];Triv 2 1;

ProveMarked "Satz30B" "Satz30B";

(* Satz31:  associativity of multiplication *)

s "a1ENat&a2ENat&a3ENat->[a1*a2]*a3=a1*a2*a3";

r();l();Gl 2;  bookmark "Satz31";

ThmCut "Induction"; 
su 4 "{x1:Nat|[a1*a2]*x1=a1*a2*x1}";

r(); UseThm "OneNat" nil [1];
ThmCut2 "TimesOne"; rwr nil;
ThmCut2 "TimesOne"; rwr nil;r();

Triv 2 1; UseThm "TimesNat" [3,1] [1];
r();r();r();l(); UseThm "SuccNat" [1] [1];
l(); ThmCut2 "TimesSucc"; rwr nil;
ThmCut2 "TimesSucc"; rwr nil;

gl 4; rwr nil; ThmCut2 "Satz30"; rwr nil;r();
UseThm "TimesNat" [3,8] [1];
Triv 3 1;Triv 5 1;Triv 5 1;Triv 4 1;
UseThm "TimesNat" [6,4] [1];
Triv 3 1;

Triv 2 1;l();Triv 2 1;

ProveMarked "Satz31" "Satz31";

(* Satz32 -- three versions *)

s "a1ENat&a2ENat&a3ENat->a1>a2->a1*a3>a2*a3";

r();l();Gl 2;r(); bookmark "Satz32A";

l();l();gl 2;rwr nil;

ThmCut2 "Satz30B"; rwr nil;

r();r();sg();r();

UseThm "TimesNat" [6,4] [1]; Triv 5 1;Triv 3 1;Triv 2 1;

ProveMarked "Satz32A" "Satz32A";

s "a1ENat&a2ENat&a3ENat->a1=a2->a1*a3=a2*a3";

r();l();Gl 2;r(); bookmark "Satz32B";

rwr nil; r();

ProveMarked "Satz32B" "Satz32B";  (* this is trivial of course *)

s "a1ENat&a2ENat&a3ENat->a1<a2->a1*a3<a2*a3";

r();l();Gl 2;r(); bookmark "Satz32C";

l();l();gl 2;rwr nil;

ThmCut2 "Satz30B"; rwr nil;

r();r();sg();r();

UseThm "TimesNat" [6,4] [1]; Triv 5 1;Triv 3 1;Triv 4 1;

ProveMarked "Satz32C" "Satz32C";

(* Satz33 -- three variants *)

s "a1ENat&a2ENat&a3ENat->a1*a3>a2*a3->a1>a2";

r();l();Gl 2;r(); bookmark "Satz33A";

s "a1ENat&a2ENat&a3ENat->a1*a3=a2*a3->a1=a2";

r();l();Gl 2;r(); bookmark "Satz33B";

s "a1ENat&a2ENat&a3ENat->a1*a3<a2*a3->a1<a2";

r();l();Gl 2;r(); bookmark "Satz33C";

(* Satz 34 *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1>a2&a3>a4->a1*a3>a2*a4";

(* Satz 34B *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1<a2&a3<a4->a1*a3<a2*a4";

(* Satz35A *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1>=a2&a3>a4->a1*a3>a2*a4";

(* Satz35B *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1>a2&a3>=a4->a1*a3>a2*a4";

(* Satz35C *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1<=a2&a3<a4->a1*a3<a2*a4";

(* Satz35D *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1<a2&a3<=a4->a1*a3<a2*a4";

(* Satz 36 *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1>=a2&a3>=a4->a1*a3>=a2*a4";

(* Satz 36B *)

s "a1ENat&a2ENat&a3ENat&a4ENat->a1<=a2&a3<=a4->a1*a3<=a2*a4";

(* this completes Landau Chapter I *)