(* Here are some example files.  To run them step by step (in demo mode)
run the commands

startdemo();
use "stewartexamples.txt";

(* after hitting return a lot of times *)

stopdemo();

under the prover.  You will need to hit return after each command or 
sequent display. *)

Start "P1->P2->P3 == P1&P2->P3";

r(); (* presents us with forward conditional *)

r();l(); gl 3; l(); (* this causes branching *)

Done();  (* end of first branch *)

l();  (* branches again *)
Triv 2 1; (* first subbranch done *)
Done();  (* second subbranch and second branch done *)

(* now we are presented with the conditional in the other direction *)

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

Prove 1 "PROPEXAMPLE";

(* quantifier example *)

(* the example is all about how it is *almost* true that a symmetric,
transitive relation must be reflexive *)

Start "(Ax1.(Ex2.x1R1x2)) & (Ax1.(Ax2.x1R1x2->x2R1x1)) & (Ax1.(Ax2.(Ax3.x1R1x2&x2R1x3 -> x1 R1 x3))) -> (Ax1.x1R1x1)";

r();l();Gl 2;  (* premises and conclusion sorted out now *)

bookmark "Quant_Example";

r(); (* we introduce an arbitrary object, aiming to show that it is
related to itself by R1 *)

Gl 3; su 2 "a1"; l();

Gl 3; l();  su 3 "a1";  su 4 "a2"; l();  Triv 4 1;

Gl 4; l();l();  su 4 "a1"; su 5 "a2"; su 6 "a1";

l();r();  Triv 4 1;  Triv 6 1; Done();

ProveMarked "Quant_Example" "Quant_Example";

(* I'm planning to reprove the previous example in a style that does
not use the su command, and then give some algebra examples with perhaps
examples of definitions, using theorems, and so forth *)

(* observe how in this second proof of the same theorem just proved 
all assignments of values to
Un's are made implicitly *)

Start "(Ax1.(Ex2.x1R1x2)) & (Ax1.(Ax2.x1R1x2->x2R1x1)) & (Ax1.(Ax2.(Ax3.x1R1x2&x2R1x3 -> x1 R1 x3))) -> (Ax1.x1R1x1)";

r();r();

l();Gl 2;

Gl 3;l();

Gl 3; l();l(); Triv 4 1;

Gl 4;l();l();

l();r(); Triv 4 1; Triv 6 1; Done();

(* now for an algebraic example *)
(* this uses implicit evaluation of unknown variables quite
aggressively *)

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

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

setprecrightabove "*" "+";

Axiom "ADDCOMM" nil ["a1+a2=a2+a1"];

Axiom "ADDASSOC" nil ["[a1+a2]+a3=a1+[a2+a3]"];

Start "a1+a2+a3=a3+a2+a1";

ThmCut "ADDCOMM";

rwr [1];  (* notice that the unknown variables 
are automatically assigned values *)

ThmCut "ADDCOMM";

rwr [2];  (* the argument tells the prover where to rewrite *)

ThmCut "ADDASSOC";

rwr [1];

r();