#!/usr/bin/php
<?php 
// Strings can be written on two lines by using a period to concatenate the lines.
// We did this in some places to permit this file to be printed for archival purposes.
error_reporting(E_ALL|E_STRICT); 
ini_set('display_errors', true); 

class Theorem
{	var $name;
	var $PositiveForm;     // If a list, means conjunction of the elements; can involve a Skolem symbol
	var $NegatedForm;      // supposed to be equivalent to the negation of the PositiveForm
	                       //  with Skolem terms replaced by variables. 
	var $Diagram;          // an array of diagram equations
	var $SkolemSymbols = "";  // array of Skolem symbols introduced, in order needed
	var $Cases = "";     //  cases we used to split the problem, if any.
	function Theorem($a,$b,$c,$d="",$e="",$f="")
	   { $this->name = $a;
		 $this->PositiveForm = $b;
		 $this->NegatedForm = $c;
		 $this->Diagram = $d;
		 $this->SkolemSymbols = $e;
		 $this->Cases = $f;
	   }
}

class Axiom
{	var $name;
	var $PositiveForm;
	function Axiom($a,$b )
	   { $this->name = $a;
		 $this->PositiveForm = $b;
	   }
}

class Definition         //  relations are defined.  Functions are introduced as Skolem symbols in axioms or theorems.
{	var $name;
	var $definiens;
	var $LeftToRight;  // a list of clauses
	var $RightToLeft;  // a list of clauses
	function Definition($a,$b,$c,$d)
	   { $this->name = $a;
		 $this->definiens = $b;
		 $this->LeftToRight = $c;
		 $this->RightToLeft = $d;
	   }
}

$TarskiAxioms = array(
	new Axiom ("A1", "E(x,y,y,x)"),
	new Axiom ("A2", "-E(x,y,z,v) | -E(x,y,z2,v2) | E(z,v,z2,v2)"),
	new Axiom ("A3", "-E(x,y,z,z) | x=y"),
	new Axiom ("A4-i",  "T(x,y,ext(x,y,w,v))"),
	new Axiom ("A4-ii", "E(y,ext(x,y,w,v),w,v)"),
	new Axiom ("A5","-E(x,y,x1,y1) | -E(y,z,y1,z1) | -E(x,v,x1,v1) | -E(y,v,y1,v1) | -T(x,y,z) | -T(x1,y1,z1) | x=y | E(z,v,z1,v1)"),
	new Axiom ("A6"," -T(x,y,x) | x=y"),
	new Axiom ("A7-i","-T(xa,xp,xc) | -T(xb,xq,xc) | T(xp,ip(xa,xp,xc,xb,xq),xb)"),
	new Axiom ("A7-ii","-T(xa,xp,xc) | -T(xb,xq,xc) | T(xq,ip(xa,xp,xc,xb,xq),xa)"),
	new Axiom ("A8-i","-T(alpha,beta,gamma)"),
	new Axiom ("A8-ii","-T(beta,gamma,alpha)"),
	new Axiom ("A8-iii","-T(gamma,alpha,beta)"),
	new Axiom ("A9", "xp=xq | -E(xa,xp,xz,xq) | -E(xb,xp,xb,xq) | -E(xc,xp,xc,xq) | T(xa,xb,xc) | T(xb,xc,xa) | T(xc,xa,xb)"),
	new Axiom ("A10-i", "-T(xa,xd,xt) | -T(xb,xd,xc) | xa = xd | T(xa,xb,f10(xa,xb,xc,xd,xt))"),
	new Axiom ("A10-ii", "-T(xa,xd,xt) | -T(xb,xd,xc) | xa = xd | T(xa,xc,g10(xa,xb,xc,xd,xt))"),
	new Axiom ("A10-iii", "-T(xa,xd,xt) | -T(xb,xd,xc) | xa = xd | T(f10(xa,xb,xc,xd,xt),xt,g10(xa,xb,xc,xd,xt))")
);


$TarskiDefinitions = array(
  new Definition("Defn2.10", "AFS",
        array( 
	 	  "-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc)",
          "-AFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc)",
          "-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xb,za,zb)",
          "-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc)",
          "-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd)",
          "-AFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xd,zb,zd)"
         ),
         array(
		 "-T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xb,za,zb) | -E(xb,xc,zb,zc) | -E(xa,xd,za,zd) | -E(xb,xd,zb,zd)| AFS(xa,xb,xc,xd,za,zb,zc,zd)"
		)
	),
	new Definition("Defn4.1", "IFS",
	    array(
		  "-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(xa,xb,xc)",
		  "-IFS(xa,xb,xc,xd,za,zb,zc,zd) | T(za,zb,zc)",
		  "-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xc,za,zc)",
		  "-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xb,xc,zb,zc)",
		  "-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xa,xd,za,zd)",
		  "-IFS(xa,xb,xc,xd,za,zb,zc,zd) | E(xc,xd,zc,zd)"
	    ),
	    array(
		 " -T(xa,xb,xc) | -T(za,zb,zc) | -E(xa,xc,za,zc) | -E(xb,xc,zb,zc) | -E(xa,xd,za,zd) | -E(xc,xd,zc,zd)| IFS(xa,xb,xc,xd,za,zb,zc,zd)"
		)
	),
	new Definition("Defn4.4","E3",  // for n = 3
	    array(
		 "-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa2,xb1,xb2)",
		 "-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa1,xa3,xb1,xb3)",
		 "-E3(xa1,xa2,xa3,xb1,xb2,xb3) | E(xa2,xa3,xb2,xb3)"
		),
		array(
		 "-E(xa1,xa2,xb1,xb2) | -E(xa1,xa3,xb1,xb3) | -E(xa2,xa3,xb2,xb3) | E3(xa1,xa2,xa3,xb1,xb2,xb3)"
		)
	),
	new Definition("Defn4.10","Col",
	    array(
		  "-Col(xa,xb,xc) | T(xa,xb,xc) | T(xb,xc,xa) | T(xc,xa,xb)"
		),
		array( 
		  "Col(xa,xb,xc) | -T(xa,xb,xc)", "Col(xa,xb,xc) | -T(xb,xc,xa)","Col(xa,xb,xc) | -T(xc,xa,xb)"
		)
	),
	new Definition("Defn4.15","FS",
        array(
	        "-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | Col(xa,xb,xc)",
	        "-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E3(xa,xb,xc,xa1,xb1,xc1)",
	        "-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xa,xd,xa1,xd1)",
	        "-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1)"
	    ),
	    array( "-Col(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | -E(xa,xd,xa1,xd1) | -E(xb,xd,xb1,xd1) | FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1)"
	    )
	),
	new Definition("Defn5.4","le",
	      array("-le(xa,xb,xc,xd) | T(xc,insert(xa,xb,xc,xd),xd)",  
		   "-le(xa,xb,xc,xd) | E(xa,xb,xc,insert(xa,xb,xc,xd))"
		  ),
		  array("-T(xc,y,xd) | -E(xa,xb,xc,y) | le(xa,xb,xc,xd)"
		  )
	),
    new Definition("Defn6.1","sameside",
	  //  a and b are on the same side of p
	   array("-sameside(xa,xp,xb) | xa != xp",
	     "-sameside(xa,xp,xb) | xb != xp",
	     "-sameside(xa,xp,xb) | T(xp,xa,xb) | T(xp,xb,xa)"
	    ),
	    array( "-T(xp,xa,xb) | xa=xp |xb=xp | sameside(xa,xp,xb)",
          "-T(xp,xb,xa) | xa=xp | xb=xp | sameside(xa,xp,xb)"  
        )
    ),
	new Definition("Defn7.1", "M",   // m is the midpoint of ab
		array("-M(xa,xm,xb) | T(xa,xm,xb)","-M(xa,xm,xb) | E(xm,xa,xm,xb)"
		),
		array("-T(xa,xm,xb) | -E(xm,xa,xm,xb) | M(xa,xm,xb)"
		)
	),
   new Definition("Defn7.23", "KF",  // Krippenfigur 
        array(
		 "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | T(xa1,xc,xa2)",
		 "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) |  T(xb1,xc,xb2)",
		 "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | E(xc,xa1,xc,xb1)",
		 "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | E(xc,xa2,xc,xb2)",
		 "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | M(xa1,xm1,xb1)",
		 "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) |  M(xa2,xm2,xb2)"
		),
		array(" -T(xa1,xc,xa2) | -T(xb1,xc,xb2) | -E(xc,xa1,xc,xb1) | -E(xc,xa2,xc,xb2) | -M(xa1,xm1,xb1) | -M(xa2,xm2,xb2) | KF(xa1,xm1,xb1,xc,xb2,xm2,xa2)"
		)
	),
	new Definition("Defn8.1", "R",  // Right angle
        array(
	 	  "-R(xa,xb,xc) | E(xa,xc,xa,s(xb,xc))"
	    ),
		array("R(xa,xb,xc) | -E(xa,xc,xa,s(xb,xc))"
		)
	),
	new Definition("Defn8.11a", "perpAt",
       array(
			"-perpAt(y,z,x,y1,z1) | Col(y,z,x)",
	  		"-perpAt(y,z,x,y1,z1) | Col(y1,z1,x)",
	  		"-perpAt(y,z,x,y1,z1) |y != z",
	  		"-perpAt(y,z,x,y1,z1) |y1 != z1",
	  		"-perpAt(y,z,x,y1,z1) | -Col(y,z,u) | -Col(y1,z1,v) | R(u,x,v)"
	   ),
	   array(
			"perpAt(y,z,x,y1,z1) | y = z | y1 = z1 | -Col(y,z,x) | -Col(y1,z1,x) |  Col(y,z,f811(y,z,y1,z1,x))",
	  		"perpAt(y,z,x,y1,z1) | y = z | y1 = z1 | -Col(y,z,x) | -Col(y1,z1,x) |  Col(y1,z1,g811(y,z,y1,z1,x))",
	  		"perpAt(y,z,x,y1,z1) | y = z | y1 = z1 | -Col(y,z,x) | -Col(y1,z1,x) |  -R(f811(y,z,y1,z1,x),x,g811(y,z,y1,z1,x))"
	   )
	),
	new Definition("Defn8.11b","perp",
	   array(
			"-perp(xp,xq,xp1,xq1) | perpAt(xp,xq,il(xp,xq,xp1,xq1),xp1,xq1)"
	   ),
	   array("perp(xp,xq,xp1,xq1) | -perpAt(xp,xq,x,xp1,xq1)"
	   )
	),
	new Definition("Defn9.1", "opposite", // opposite(a,p,q,b) means a and b are on opposite sides of Line(p,q)
	   array(
			"xp = xq | Col(xp,xq,xa) | Col(xp,xq,xb) | -T(xa,xt,xb) | -Col(xp,xq,xt) | opposite(xa,xp,xq,xb)",
			"-opposite(xa,xp,xq,xb) | -Col(xp,xq,xa)",
			"-opposite(xa,xp,xq,xb) | -Col(xp,xq,xb)",
	   		"-opposite(xa,xp,xq,xb) | T(xa,il(xa,xb,xp,xq),xb)"
	   ),
	   array(
			"-opposite(xa,xp,xq,xb) | Col(xp,xq,il(xa,xb,xp,xq))"
	   )
	),
	new Definition("Defn9.7", "samesideline", // samesideline(a,p,q,b) means a and b are on the same side of Line(p,q)
	    array( 
			"-samesideline(xa,xb,xp,xq) | Col(xp,xq,ss1(xa,xb,xp,xq))",
			"-samesideline(xa,xb,xp,xq) | Col(xp,xq,ss2(xa,xb,xp,xq))",
			"-samesideline(xa,xb,xp,xq) | T(xa,ss1(xa,xb,xp,xq),ss3(xa,xb,xp,xq))",
			"-samesideline(xa,xb,xp,xq) | T(xb,ss2(xa,xb,xp,xq),ss3(xa,xb,xp,xq))",
			"-samesideline(xa,xb,xp,xq) | xa != ss1(xa,xb,xp,xq)",
			"-samesideline(xa,xb,xp,xq) | xb != ss2(xa,xb,xp,xq)",
			"-samesideline(xa,xb,xp,xq) | ss3(xa,xb,xp,xq) != ss1(xa,xb,xp,xq)",
			"-samesideline(xa,xb,xp,xq) | ss3(xa,xb,xp,xq) != ss2(xa,xb,xp,xq)", 
			"-samesideline(xa,xb,xp,xq) | xp != xq",
			"-samesideline(xa,xb,xp,xq) | -Col(xp,xq,xa)",
			"-samesideline(xa,xb,xp,xq) | -Col(xp,xq,xb)"
		),
		array(
			"-T(xa,xu,xc) | -T(xb,xv,xc) | -Col(xp,xq,xu) | -Col(xp,xq,xv) |xp=xq | xc = xu ".  
			"| xc = xv | xa = xu | xb = xv | Col(xp,xq,xa) | Col(xp,xq,xb)  | samesideline(xa,xb,xp,xq)",
		)
	),
    new Definition( "Defn11.2", "congruent",// congruent angles, not triangles.  Our definition is different from Szmielew's.
      	array(
				"-congruent(xa,xb,xc,xd,xe,xf) | E(ext(xb,xc,xe,xf),ext(xb,xa,xe,xd),ext(xe,xf,xb,xc),ext(xe,xd,xb,xa))",
				"-congruent(xa,xb,xc,xd,xe,xf) | xa != xb",
				"-congruent(xa,xb,xc,xd,xe,xf) | xc != xb",
				"-congruent(xa,xb,xc,xd,xe,xf) | xd != xe",
				"-congruent(xa,xb,xc,xd,xe,xf) | xf != xe"
		),
		array(
				 "congruent(xa,xb,xc,xd,xe,xf) | -T(xb,xa,xa1) | -E(xa,xa1,xe,xd) | -T(xb,xc,xc1)".
				 "| -E(xc,xc1,xe,xf) | -T(xe,xd,xd1) | -E(xd,xd1,xb,xa) | -T(xe,xf,xf1)".
				 "| -E(xf,xf1,xb,xc) | -E(xa1,xc1,xd1,xf1) | xa=xb | xc=xb | xd=xe | xf=xe"
	  	)
	),
	new Definition("Defn12.7", "parallel",  //  i.e. echt parallel
		array( 	"-parallel(xA,yA,xB,yB) | xA != yA", 
				"-parallel(xA,yA,xB,yB) | xB != yB", 
				"-parallel(xA,yA,xB,yB) |  samesideline(xB,yB,xA,yA)", 
				"-parallel(xA,yA,xB,yB) | -Col(xA,yA,x) | -Col(xB,yB,x)"
		),
		array("xA=yA | xB=yB  | parallel(xA,yA,xB,yB) | Col(xA,yA,e5(xA,yA,xB,yB)) | -samesideline(xB,yB,xA,yA)",    
				"xA=yA | xB=yB  | parallel(xA,yA,xB,yB) | Col(xB,yB,e5(xA,yA,xB,yB)) | -samesideline(xB,yB,xA,yA)"
		)
	)
);

/* These are cases when Skolem functions are definable.  */
$TarskiTermDefinitions = array(
	'insert' => "insert(xa,xb,xa1,xc1) = ext(ext(xc1,xa1,alpha,gamma),xa1,xa,xb)",
	'conga' => "conga(xa,xb,xd,xe) = ext(xb,xa,xe,xd)",
	'congc' => "congc(xb,xc,xe,xf) = ext(xb,xc,xe,xf)",
	'congd' => "congd(xa,xb,xd,xe) = ext(xe,xd,xb,xa)",
	'congf' => "congf(xb,xc,xe,xf) = ext(xe,xf,xb,xc)"
);
 
$TarskiTheorems = array(
	new Theorem( "Satz2.1", 
		array("E(xa,xb,xa,xb)"), 
		array("-E(a,b,a,b)")
	),  
	new Theorem( "Satz2.2", 
		array("-E(xa,xb,xc,xd) | E(xc,xd,xa,xb)"),
		array("E(a,b,c,d)","-E(c,d,a,b)")
	),  
	new Theorem( "Satz2.3", 
		array("-E(xa,xb,xc,xd) | -E(xc,xd,xe,xf) | E(xa,xb,xe,xf)"),
		array("E(a,b,c,d)","E(c,d,e,f)","-E(a,b,e,f)")
	),
	new Theorem( "Satz2.4", 
		array("-E(xa,xb,xc,xd) | E(xb,xa,xc,xd)"),
		array("E(a,b,c,d)","-E(b,a,c,d)")
	),	
	new Theorem( "Satz2.5", 
		array("-E(xa,xb,xc,xd) | E(xa,xb,xd,xc)"),
		array("E(a,b,c,d)","-E(a,b,d,c)")
	),
    new Theorem( "Satz2.8", 
		array("E(xa,xa,xb,xb)"),
		array("-E(a,a,b,b)"),
        array("cx = ext(b,a,b,b)")
	), 
	new Theorem( "Satz2.11", 
		array("-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1)"),
		array("T(a,b,c)","T(a1,b1,c1)","E(a,b,a1,b1)","E(b,c,b1,c1)","-E(a,c,a1,c1)"
		)
	),
	new Theorem( "Satz2.12", 
		array("xq = xa | -T(xq,xa,xd) | -E(xa,xd,xb,xc) | xd = ext(xq,xa,xb,xc)"),
		array("q != a","T(q,a,d)","E(a,d,b,c)","d != ext(q,a,b,c)")
	),
    new Theorem( "Satz2.13", 
		array("-E(xb,xc,xa,xa) | xb=xc"),
		array("E(b,c,a,a)","b!=c")
    ),
    new Theorem( "Satz2.14", 
		array("-E(xa,xb,xc,xd) | E(xb,xa,xd,xc)"),
		array( "E(a,b,c,d)", "-E(b,a,d,c)")
    ),
    new Theorem( "Satz2.15", 
		array("-T(xa,xb,xc) | -T(xA,xB,xC) | -E(xa,xb,xB,xC)| -E(xb,xc,xA,xB) | E(xa,xc,xA,xC)"),
		array( "T(a,b,c)", "T(A,B,C)", "E(a,b,B,C)", "E(b,c,A,B)", "-E(a,c,A,C)"),
                   //  easy to prove using Satz 3.1 but we proved it without Satz 3.1 using this diagram:
		array( "d = ext(a,b,b,b)" ),
		"",  // no Skolem functions
		array( "T(b,c,c) | -T(b,c,c)") // eventually eliminated
    ),	
	new Theorem( "Satz3.1", 
		array("T(xa,xb,xb)"),
		array("-T(a,b,b)"),
		array("c31= ext(a,b,b,b)")
	),
    new Theorem( "Satz3.2", 
		array("-T(xa,xb,xc) | T(xc,xb,xa)"),
		array("T(a,b,c)","-T(c,b,a)")
	),
	new Theorem( "Satz3.3", 
		array("T(xa1,xa1,xb1)"),
		array("-T(a1,a1,b1)")
	),
    new Theorem( "Satz3.4",
 		array("-T(xa,xb,xc) | -T(xb,xa,xc) | xa = xb"),
		array("T(a,b,c)","T(b,a,c)","a != b"),
		array("c34 = ip(a,b,c,b,a)")
	),
    new Theorem( "Satz3.5a", 
		array("-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xb,xc)"), 
		array("T(a,b,d)","T(b,c,d)","-T(a,b,c)"),
		array("p = ip(a,b,d,b,c)")
	),
	new Theorem( "Satz3.6a", 
		array("-T(xa,xb,xc) | -T(xa,xc,xd) | T(xb,xc,xd)"),  
		array("T(a,b,c)","T(a,c,d)","-T(b,c,d)")
	),
	new Theorem( "Satz3.7a", 
		array("-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xc,xd)"),
		array("T(a,b,c)","T(b,c,d)","b != c","-T(a,c,d)"),
		array("cx = ext(a,c,c,d)")
	),
	new Theorem( "Satz3.5b",    
		array("-T(xa,xb,xd) | -T(xb,xc,xd) | T(xa,xc,xd)"),
		array("T(a,b,d)","T(b,c,d)","-T(a,c,d)")
	),
	new Theorem( "Satz3.6b",    
		array("-T(xa,xb,xc) | -T(xa,xc,xd) | T(xa,xb,xd)"),
		array("T(a,b,c)","T(a,c,d)","-T(a,b,d)")
	),
	new Theorem( "Satz3.7b", 
		array("-T(xa,xb,xc) | -T(xb,xc,xd) | xb = xc | T(xa,xb,xd)"),
		array("T(a,b,c)","T(b,c,d)","b != c","-T(a,b,d)"),
		array("cx = ext(a,c,c,d)")
	),
	new Theorem( "Satz3.13a", 
		array("alpha != beta"), 
		array("alpha = beta")
	),
	new Theorem( "Satz3.13b", 
		array("beta != gamma"), 
		array("beta = gamma")
	),
	new Theorem( "Satz3.13c", 
		array("alpha != gamma"),
		array("alpha = gamma")
	),
	new Theorem( "Satz3.14a",
		array("T(xa,xb,ext(xa,xb,alpha,gamma))"),
		array("-T(a,b,ext(a,b,alpha,gamma))")
	),
	new Theorem( "Satz3.14b",
		array("xb != ext(xa,xb,alpha,gamma)"),
		array("b=ext(a,b,alpha,gamma)")
	),
	new Theorem( "Satz3.17",
		array(  "-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1) | T(xp,crossbar(xa,xb,xc,xa1,xb1,xp),xc)",
				"-T(xa,xb,xc) | -T(xa1,xb1,xc) | -T(xa,xp,xa1) | T(xb,crossbar(xa,xb,xc,xa1,xb1,xp),xb1)"
			 ),
		array("T(a,b,c)","T(a1,b1,c)","T(a,p,a1)","-T(p,x,c) | -T(b,x,b1)"),
		array("e = ip(c,b1,a1,a,p)","d = ip(c,b,a,b1,e)"),
		array("crossbar")
	),
	new Theorem( "Satz4.2",
		array("-IFS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | E(xb,xd,xb1,xd1)"),  
		array("IFS(a,b,c,d,a1,b1,c1,d1)","-E(b,d,b1,d1)"),
		array( "e = ext(a,c,a,c)", "e1= ext(a1,c1,a,c)")
	),   
	new Theorem( "Satz4.3",
		array("-T(xa,xb,xc) | -T(xa1,xb1,xc1) | -E(xa,xc,xa1,xc1) | -E(xb,xc,xb1,xc1) | E(xa,xb,xa1,xb1)"),
		array("T(a,b,c)","T(a1,b1,c1)","E(a,c,a1,c1)","E(b,c,b1,c1)","-E(a,b,a1,b1)")
	),
	new Theorem( "Satz4.5",
		array("-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) | T(xa1,insert(xa,xb,xa1,xc1),xc1)",
	 		  "-T(xa,xb,xc) | -E(xa,xc,xa1,xc1) | E3(xa,xb,xc,xa1,insert(xa,xb,xa1,xc1),xc1)"
	    ),
		array(  "T(a,b,c)",
				"E(a,c,a1,c1)",
				"-T(a1,insert(a,b,a1,c1),c1) | -E3(a,b,c,a1,insert(a,b,a1,c1),c1)"
			 ),
		array( "d1 = ext(c1,a1,alpha,gamma)",
				"b1 = ext(d1,a1,a,b)",
				"c2 = ext(d1,b1,b,c)"
		)
	),
	new Theorem( "Satz4.6", 
		array("-T(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | T(xa1,xb1,xc1)"),
		array(  "T(a,b,c)",
				"E3(a,b,c,a1,b1,c1)",
				"-T(a1,b1,c1)",
				" x != y | -T(w,z,x) | T(w,z,y)" // an equality axiom!  Without it, we need hints.
		)
	),
	new Theorem( "Satz4.11a", 
		array("-Col(xa,xb,xc) | Col(xb,xc,xa)"),
		array("Col(a,b,c)","-Col(b,c,a)")
	),
	new Theorem( "Satz4.11b", 
		array( "-Col(xa,xb,xc) | Col(xc,xa,xb)"),
		array("Col(a,b,c)", "-Col(c,a,b)")
	),
	new Theorem( "Satz4.11c", 
		array( "-Col(xa,xb,xc) | Col(xc,xb,xa)"),
		array("Col(a,b,c)",  "-Col(c,b,a)")
	),
	new Theorem( "Satz4.11d", 
		array( "-Col(xa,xb,xc) | Col(xb,xa,xc)"),
		array("Col(a,b,c)","-Col(b,a,c)")
	),
	new Theorem( "Satz4.11e", 
		array( "-Col(xa,xb,xc) | Col(xa,xc,xb)"),
		array("Col(a,b,c)","-Col(a,c,b)")
	),
	new Theorem( "Satz4.12", 
		array("Col(xa,xa,xb)"), 
		array("-Col(a,a,b)")
	),
	new Theorem( "Satz4.12b", 
		array("Col(xa,xb,xa)"), 
		array("-Col(a,b,a)")
	),
    new Theorem( "Satz4.13", 
		array("-Col(xa,xb,xc) | - E3(xa,xb,xc,xa1,xb1,xc1) | Col(xa1,xb1,xc1)"),
		array("Col(a,b,c)","E3(a,b,c,a1,b1,c1)","-Col(a1,b1,c1)")
	),
    new Theorem( "Satz4.14", 
		array("-Col(xa,xb,xc) | -E(xa,xb,xa1,xb1) | E3(xa,xb,xc,xa1,xb1,insert5(xa,xb,xc,xa1,xb1))"),
		array("Col(a,b,c)","E(a,b,a1,b1)","-E3(a,b,c,a1,b1,x)"),
		array("c1 = ext(a1,b1,b,c)","c2 = ext(b1,a1,a,c)","c3 = insert(a,c,a1,b1)"),
		array("insert5")
	),
    new Theorem( "Satz4.16", 
		array("-FS(xa,xb,xc,xd,xa1,xb1,xc1,xd1) | xa = xb | E(xc,xd,xc1,xd1)"),
		array("FS(a,b,c,d,a1,b1,c1,d1)","a != b","-E(c,d,c1,d1)")
	),
	new Theorem( "Satz4.17", 
		array("xa = xb | -Col(xa,xb,xc) | -E(xa,xp,xa,xq) | -E(xb,xp,xb,xq) |E(xc,xp,xc,xq)"),
		array("a != b","Col(a,b,c)","E(a,p,a,q)","E(b,p,b,q)","-E(c,p,c,q)")
	),
	new Theorem( "Satz4.18", 
		array("xa = xb | -Col(xa,xb,xc) | -E(xa,xc,xa,xc1) | -E(xb,xc,xb,xc1) | xc = xc1"),
		array("a != b","Col(a,b,c)","E(a,c,a,c1)","E(b,c,b,c1)","c != c1")
	),
	new Theorem( "Satz4.19", 
		array("-T(xa,xc,xb) | -E(xa,xc,xa,xc1) | -E(xb,xc,xb,xc1) | xc = xc1"),
		array("T(a,c,b)","E(a,c,a,c1)","E(b,c,b,c1)","c != c1")
	),
	new Theorem( "Satz5.1",  
		array("xa = xb | -T(xa,xb,xc) | -T(xa,xb,xd) | T(xa,xc,xd) | T(xa,xd,xc)"),
		array("a != b","T(a,b,c)","T(a,b,d)","-T(a,c,d)","-T(a,d,c)"),
		array(  "c1=ext(a,d,c,d)",      
				"d1=ext(a,c,c,d)",
				"p=ext(c1,c,c,d)",
				"r=ext(d1,c,c,e)",
				"q=ext(p,r,r,p)",
				"b1 = ext(a,c1,c,b)",
				"b2 = ext(a,d1,d,b)",
				"e = ip(c1,d,b,d1,c)"
		),
		"",
		array(  "d1=e | d1!=e",
				"c = c1 | c != c1"
			)
	),   
	new Theorem( "Satz5.2", 
		array("xa = xb | -T(xa,xb,xc) | -T(xa,xb,xd)| T(xb,xc,xd) | T(xb,xd,xc)"),
		array("a != b", "T(a,b,c)","T(a,b,d)", "-T(b,c,d)","-T(b,d,c)")
	),
	new Theorem( "Satz5.3", 
		array("-T(xa,xb,xd) | -T(xa,xc,xd) | T(xa,xb,xc) | T(xa,xc,xb)"),
		array("T(a,b,d)","T(a,c,d)","-T(a,b,c)", "-T(a,c,b)")
	),
    new Theorem( "Satz5.5a",  
		array(  "-le(xa,xb,xc,xd) | T(xa,xb,ins(xc,xd,xa,xb))",
				"-le(xa,xb,xc,xd) | E(xa,ins(xc,xd,xa,xb),xc,xd)",
				"-le(xa,xb,xc,xd) | ins(xc,xd,xa,xb) = ext(xa,xb,insert(xa,xb,xc,xd),xd)"
		),
		array(  "le(a,b,c,d)",
				"-T(a,b,x) | -E(a,x,c,d)| x != ext(a,b,insert(a,b,c,d),d) "
			 ),
		"",
		array("ins")
	),
    new Theorem( "Satz5.5b",  
		array(" le(xa,xb,xc,xd) | -T(xa,xb,xe) | -E(xa,xe,xc,xd)"),
		array(  "-le(a,b,c,d)",
				"T(a,b,e)",
				"E(a,e,c,d)"
			 )
	),
	new Theorem( "Satz5.6",  
		array("-le(xa,xb,xc,xd) | -E(xa,xb,xa1,xb1) | - E(xc,xd,xc1,xd1) |le(xa1,xb1,xc1,xd1)"),
		array("le(a,b,c,d)","E(a,b,a1,b1)","E(c,d,c1,d1)","-le(a1,b1,c1,d1)")
	),
    new Theorem( "Satz5.7",  
		array("le(xa,xb,xa,xb)"),
		array("-le(a,b,a,b)")
	),
 
	new Theorem( "Satz5.8",  
		array("-le(xa,xb,xc,xd) | - le(xc,xd,xe,xf) | le(xa,xb,xe,xf)"),
		array("le(a,b,c,d)","le(c,d,e,f)","-le(a,b,e,f)")
	),
	new Theorem( "Satz5.9",  
		array("-le(xa,xb,xc,xd) | -le(xc,xd,xa,xb) | E(xa,xb,xc,xd)"),
		array("le(a,b,c,d)","le(c,d,a,b)","-E(a,b,c,d)"),
		array(  "p = ins(c,d,a,b)",
				"q = insert(c,d,a,b)"
			 )
	),
	new Theorem( "Satz5.10", 
		array("le(xa,xb,xc,xd) | le(xc,xd,xa,xb)"),
		array("-le(a,b,c,d)","-le(c,d,a,b)")
	),
	new Theorem( "Satz5.11", 
		array("le(xa,xa,xc,xd)"), 
		array("-le(a,a,c,d)")
	),
    new Theorem( "Satz5.12a1",  
		array( "-Col(xa,xb,xc) | -T(xa,xb,xc) | le(xa,xb,xa,xc)"),
		array("Col(a,b,c)","T(a,b,c)","-le(a,b,a,c)")
	),
	new Theorem( "Satz5.12a2",  
		array("-Col(xa,xb,xc) | -T(xa,xb,xc) | le(xb,xc,xa,xc)"),
		array("Col(a,b,c)","T(a,b,c)","-le(b,c,a,c)")
	),
	new Theorem( "NarbouxLemma1",
		array("-T(xa,xb,xc) | -E(xa,xc,xa,xb) | xc = xb"),
		array("T(a,b,c)","E(a,c,a,b)","c != b")
	),
	new Theorem( "Satz5.12b",
	 	array("-Col(xa,xb,xc) | T(xa,xb,xc) | -le(xa,xb,xa,xc) | -le(xb,xc,xa,xc)"),
		array("Col(a,b,c)", "-T(a,b,c)","le(a,b,a,c)","le(b,c,a,c)")
	),
	new Theorem( "Satz6.2a", 
		array("xa = xp | xb = xp | xc = xp | -T(xa,xp,xc) | -T(xb,xp,xc) | sameside(xa,xp,xb)"),
		array("a != p","b != p","c != p","T(a,p,c)","T(b,p,c)","-sameside(a,p,b)")
	),
	new Theorem( "Satz6.2b", 
		array("xa = xp | xb = xp | xc = xp | -T(xa,xp,xc) | T(xb,xp,xc) | -sameside(xa,xp,xb)"),
		array("a != p","b != p","c != p","T(a,p,c)","-T(b,p,c)","sameside(a,p,b)")
	),
    new Theorem( "Satz6.3a",  // left to right of Satz 6.3
		array(  "-sameside(xa,xp,xb) | xa != xp",   
				"-sameside(xa,xp,xb) | xb != xp",
				"-sameside(xa,xp,xb) | c63(xa,xp,xb) != xp",
				"-sameside(xa,xp,xb) | T(xa,xp,c63(xa,xp,xb))",
				"-sameside(xa,xp,xb) | T(xb,xp,c63(xa,xp,xb))"
			 ),
		array("sameside(a,p,b)","a=p | b = p | x = p | -T(a,p,x) | -T(b,p,x)"),
		"",   // no diagram 
		array("c63")
	),
	new Theorem( "Satz6.3b", 
		array("sameside(xa,xp,xb) | xa=xp | xb = xp | xc = xp | -T(xa,xp,xc) | -T(xb,xp,xc)"),
		array("-sameside(a,p,b)","a != p","b != p","c != p","T(a,p,c)","T(b,p,c)")
	),
	new Theorem( "Satz6.4a",  // left to right of Satz 6.4
		array(  "-sameside(xa,xp,xb) | Col(xa,xp,xb)",
				"-sameside(xa,xp,xb) | -T(xa,xp,xb)"
        ),
		array("sameside(a,p,b)","-Col(a,p,b) | T(a,p,b)")
	),
    new Theorem( "Satz6.4b",
 		array(" sameside(xa,xp,xb) | -Col(xa,xp,xb) | T(xa,xp,xb)"),
		array("-sameside(a,p,b)","Col(a,p,b)","-T(a,p,b)"),
		array("q64 = ext(a,p,a,p)")
	),				
	new Theorem( "Satz6.5", 
		array("xa = xp | sameside(xa,xp,xa)"),
		array("a != p","-sameside(a,p,a)")
	),
	new Theorem( "Satz6.6", 
		array("-sameside(xa,xp,xb) | sameside(xb,xp,xa)"),
		array("sameside(a,p,b)","-sameside(b,p,a)")
	),
	new Theorem( "Satz6.7", 
		array("-sameside(xa,xp,xb) | -sameside(xb,xp,xc) | sameside(xa,xp,xc)"),
		array("sameside(a,p,b)","sameside(b,p,c)","-sameside(a,p,c)")
	),
	new Theorem( "Satz6.11a", 
		array(  "xr = xa | xb = xc | sameside(insert(xb,xc,xa,xr),xa,xr)",
				"xr = xa | xb = xc | E(xa,insert(xb,xc,xa,xr),xb,xc)"
		),
		array("r != a","b != c","-sameside(insert(b,c,a,r),a,r) | -E(a,insert(b,c,a,r),b,c)"),
		array("q = ext(r,a,alpha,gamma)","c1 = ext(q,a,b,c)")
		// "insert" is a defined function, not introduced as a Skolem function.
	),
	new Theorem( "Satz6.11b", 
		array("xr = xa | xb = xc | -sameside(xp,xa,xr) | -E(xa,xp,xb,xc) | -sameside(xq,xa,xr) |  -E(xa,xq,xb,xc) | xp=xq"),
		array("r != a","b != c","sameside(p,a,r)","E(a,p,b,c)","sameside(q,a,r)","E(a,q,b,c)","p != q")
	),
	new Theorem( "Satz6.13a",     // left to right of Satz 6.13
		array("-sameside(xa,xp,xb) | -le(xp,xa,xp,xb) | T(xp,xa,xb)"),  
		array("sameside(a,p,b)","le(p,a,p,b)","-T(p,a,b)")
	),  
	new Theorem( "Satz6.13b",   // right to left of Satz 6.13
	 	array("-sameside(xa,xp,xb) | le(xp,xa,xp,xb) | -T(xp,xa,xb)"),
		array("sameside(a,p,b)","-le(p,a,p,b)","T(p,a,b)")
	),
	new Theorem( "Satz6.15a", 
		array( "xp = xq | xp = xr | -T(xq,xp,xr) | -Col(xa,xp,xq) | xa = xp | sameside(xa,xp,xq) | sameside(xa,xp,xr)"),
		array( "p != q","p != r","T(q,p,r)","Col(a,p,q)","a != p","-sameside(a,p,q)","-sameside(a,p,r)")
	),
	new Theorem( "Satz6.15b", 
		array( "xp = xq | xp = xr | -T(xq,xp,xr) | -sameside(xa,xp,xq) | Col(xa,xp,xq)"),
		array( "p != q","p != r","T(q,p,r)","sameside(a,p,q)","-Col(a,p,q)")
	),
	new Theorem( "Satz6.15c", 
		array( "xp = xq | xp = xr | -T(xq,xp,xr) | -sameside(xa,xp,xr) | Col(xa,xp,xq)"),
		array( "p != q","p != r","T(q,p,r)","sameside(a,p,r)","-Col(a,p,q)")
	),   
	new Theorem( "Satz6.15d", 
		array( "xp = xq | xp = xr | -T(xq,xp,xr) | xa != xp | Col(xa,xp,xq)"),
		array( "p != q","p != r","T(q,p,r)","a=p","-Col(a,p,q)")
	),  
	new Theorem( "Satz6.16a",  
		array( "xa=xb | -T(xc,xa,xb) | -T(xd,xa,xb) | T(xd,xc,xb) | T(xc,xd,xb)"), 
		array( "a != b","T(c,a,b)","T(d,a,b)","-T(d,c,b)","-T(c,d,b)")
	),
	new Theorem( "Satz6.16b", 
		array( "xp = xq  | xcs = xp | -Col(xp,xq,xcs) | -Col(xp,xq,xr) | Col(xp,xcs,xr)"),
		array( "p != q","cs != p","Col(p,q,cs)","Col(p,q,r)","-Col(p,cs,r)")
	),
	new Theorem( "Satz6.17a", 
		array( "xp = xq | Col(xp,xq,xp)"),
		array( "p != q","-Col(p,q,p)")
	),  
	new Theorem( "Satz6.17b", 
		array( "xp = xq | -Col(xp,xq,xr) | Col(xq,xp,xr)"),
		array( "p != q","Col(p,q,r)","-Col(q,p,r)")
		),
	new Theorem( "Satz6.18", 
		array( "xa = xb | xp = xq | -Col(xp,xq,xa) | -Col(xp,xq,xb) | -Col(xp,xq,xr) | Col(xa,xb,xr)"),
		array( "a != b","p != q","Col(p,q,a)","Col(p,q,b)","Col(p,q,r)","-Col(a,b,r)")
	), 
	new Theorem( "Satz6.21",
		array( "xa = xb | xp = xq | -Col(xa,xb,xc) | -Col(xp,xq,xc) | -Col(xa,xb,xd) | -Col(xp,xq,xd) | xc=xd | -Col(xa,xb,xe) | Col(xp,xq,xe)"),
		array(  "a!=b", "p!=q", "Col(a,b,c)", "Col(p,q,c)", "Col(a,b,d)","Col(p,q,d)", "c!=d", "Col(a,b,e)", "-Col(p,q,e)")
	),
	new Theorem( "Satz6.25",
		array( "xa = xb | -Col(xa,xb,pointOffLine(xa,xb))"),
		array( "a!=b", "Col(a,b,x)"),
		"",  // no diagram
		array("pointOffLine")
	),
	new Theorem( "Satz6.28",   // used in Satz 11.4,  but not proved in the book, so we state and prove it
		array( "-sameside(xa,xb,xc)| -sameside(xa1,xb1,xc1) | -E(xb,xa,xb1,xa1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1)"),
		array(  "sameside(a,b,c)",
				"sameside(a1,b1,c1)",
				"E(b,a,b1,a1)",
				"E(b,c,b1,c1)",
				"-E(a,c,a1,c1)"
			 )
 	),
	new Theorem( "Satz7.2", 
		array( "-M(xa,xm,xb) | M(xb,xm,xa)"),
		array( "M(a,m,b)","-M(b,m,a)")
	),
	new Theorem( "Satz7.3a", 
		array( "-M(xa,xm,xa) | xm = xa"),
		array( "M(a,m,a)","m != a")
	),
	new Theorem( "Satz7.3b", 
		array( "M(xa,xm,xa) | xm != xa"),   
		array( "-M(a,m,a)","m = a")
	),  
	new Theorem( "Satz7.4a", 
		array( "M(xp,xa,s(xa,xp))"),     // Satz 7.4a,  and definition 7.5
		array( "-M(p,a,x)"),
		"",   // no diagram, but a Skolem function
		array("s")
	),
	new Theorem( "Satz7.4b", 
		array( "-M(xp,xa,xr) | -M(xp,xa,xq) | xr=xq"),  // uniqueness of reflection in a point
		array( "M(p,a,r)","M(p,a,q)","r != q")
	),
	new Theorem( "Satz7.6", 
		array( "-M(xp,xa,xq) | xq = s(xa,xp)"),
		array( "M(p,a,q)","q != s(a,p)")
	), 
	new Theorem( "Satz7.7", 
		array( "s(xa,s(xa,xp)) = xp"), 
		array( "s(a,s(a,p)) != p" )
	),   
	new Theorem( "Satz7.8", 
		array( "s(xa,xp) != xr | s(xa,xq) != xr | xp = xq"),
		array( "s(a,p) = r","s(a,q) = r","p != q")
		),
	new Theorem( "Satz7.9", 
		array( "s(xa,xp) != s(xa,xq) | xp = xq"),
		array( "s(a,p) = s(a,q)","p != q")
	),
	new Theorem( "Satz7.10a", 
		array( "s(xa,xp) != xp | xp = xa"),
		array( "s(a,p) = p", "p != a")
	),   
	new Theorem( "Satz7.10b", 
		array( "s(xa,xp)=xp | xp != xa"),  
		array( "s(a,p) != p","p = a")
	),
	new Theorem( "Satz7.13", 
		array( "E(xp,xq,s(xa,xp),s(xa,xq))"),    
		array( "-E(p,q,s(a,p),s(a,q))"),
		array(  "p1 = s(a,p)",
			    "q1= s(a,q)",
				"cx  = ext(p1,p,q,a)",
				"cy = ext(q1,q,p,a)",
				"cx1= ext(cx,p1,q,a)",
				"cy1 = ext(cy,q1,p,a)"   
			 ),
		"",
		array("p=a | p!=a")
	), 
	new Theorem(  "Satz7.15a", 
		array("-T(xp,xq,xr) | T(s(xa,xp),s(xa,xq),s(xa,xr))"),
		array( "T(p,q,r)","-T(s(a,p),s(a,q),s(a,r))")
	),   
	new Theorem( "Satz7.15b", 
		array( "T(xp,xq,xr) | -T(s(xa,xp),s(xa,xq),s(xa,xr))"),   
		array( "-T(p,q,r)","T(s(a,p),s(a,q),s(a,r))")
	),
	new Theorem( "Satz7.16a", 
		array( "-E(xp,xq,xr,xcs) | E(s(xa,xp),s(xa,xq),s(xa,xr),s(xa,xcs))"),
		array( "E(p,q,r,cs)","-E(s(a,p),s(a,q),s(a,r),s(a,cs))")
	),
	new Theorem( "Satz7.16b", 
		array( "E(xp,xq,xr,xcs) | -E(s(xa,xp),s(xa,xq),s(xa,xr),s(xa,xcs))"),
		array( "-E(p,q,r,cs)","E(s(a,p),s(a,q),s(a,r),s(a,cs))")
	),
	new Theorem( "Satz7.17", 
		array( "-M(xp,xa,xq) | -M(xp,xb,xq) | xa = xb"),
		array( "M(p,a,q)","M(p,b,q)","a != b")
	),
	new Theorem( "Satz7.18", 
		array( "s(xa,xp) != s(xb,xp) | xa = xb"), 
		array( "s(a,p) = s(b,p)","a != b")
	), 
	new Theorem( "Satz7.19", 
		array( "s(xa,s(xb,xp)) != s(xb,s(xa,xp)) | xa = xb"),
		array( "s(a,s(b,p)) = s(b,s(a,p))","a != b"),
		array( "p = s(a,p)")
	),
	new Theorem( "Satz7.20", 
		array( "-Col(xa,xm,xb) | -E(xm,xa,xm,xb) | xa = xb | M(xa,xm,xb)"),
		array( "Col(a,m,b)","E(m,a,m,b)","a != b","-M(a,m,b)")
		),
	//  Satz7.21 is called Lemma7.21 in SST
	new Theorem( "Satz7.21", 
		array( "Col(xa,xb,xc) | xb = xd | -E(xa,xb,xc,xd) | -E(xb,xc,xd,xa) | -Col(xa,xp,xc) | -Col(xb,xp,xd) | M(xa,xp,xc)"),
		array( "-Col(a,b,c)","b != d","E(a,b,c,d)","E(b,c,d,a)","Col(a,p,c)","Col(b,p,d)","-M(a,p,c)"),
		array( "p1 = insert5(b,d,p,d,b)")        // see 4.14 for insert5
	),
	new Theorem( "Satz7.22a",   // case 1 of the Krippenlemma (which is the next Satz)
		array( "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | T(xm1,xc,xm2) | -le(xc,xa1,xc,xa2) "),
		array( "KF(a1,m1,b1,c,b2,m2,a2)","-T(m1,c,m2)", "le(c,a1,c,a2)"),
		array(  "a = s(c,a2)",
				"b  = s(c,b2)",
				"m  = s(c,m2)",
				"q = crossbar(a,a1,c,b,b1,m)"		
			 )
	),
    new Theorem( "Satz7.22b",   // Krippenlemma, stated with abbreviation KF
		array( "-KF(xa1,xm1,xb1,xc,xb2,xm2,xa2) | T(xm1,xc,xm2)"),
		array( "KF(a1,m1,b1,c,b2,m2,a2)","-T(m1,c,m2)"),
		array(  "a = s(c,a2)",
				"b  = s(c,b2)",
				"m  = s(c,m2)",
				"q = crossbar(a,a1,c,b1,b,m)"
			 )
	),
	new Theorem( "Satz7.22",   // Krippenlemma, stated as in book, without KF
		array( "-T(xa1,xc,xa2) | -T(xb1,xc,xb2) | -E(xc,xa1,xc,xb1) | -E(xc,xa2,xc,xb2) | -M(xa1,xm1,xb1) | -M(xa2,xm2,xb2) | T(xm1,xc,xm2)"),
		array(  "T(a1,c,a2)",
		 		"T(b1,c,b2)",
				"E(c,a1,c,b1)",
				"E(c,a2,c,b2)",
				"M(a1,m1,b1)",
				"M(a2,m2,b2)",
				"-T(m1,c,m2)"
			 ),
		array(  "a = s(c,a2)",
				"b  = s(c,b2)",
				"m  = s(c,m2)",
				"q = crossbar(a,a1,c,b1,b,m)"
			 )
	),
	
    new Theorem( "Satz7.25",  // also called a Lemma in SST
		array( "-E(xc,xa,xc,xb) | M(xa,isomidpoint(xa,xb,xc),xb)"),
		array( "E(c,a,c,b)","-M(a,x,b)"),
		array(  "p  = ext(c,a,a,c)",
			 	"q = ext(c,b,a,p)",
				"r  = ip(p,a,c,q,b)",
				"cx = ip(b,r,p,c,a)",
				"r1 = insert(b,r,a,q)"
		 ),
		array( "isomidpoint"),  // midpoint of isosceles triangle
		array("Col(a,b,c) | -Col(a,b,c)")
	),   
	new Theorem( "Satz8.2", 
		array( "-R(xa,xb,xc) | R(xc,xb,xa)"),
		array( "R(a,b,c)","-R(c,b,a)")
	),
	new Theorem( "Satz8.3",
		array( "-R(xa,xb,xc) | xa = xb | -Col(xb,xa,xa1) | R(xa1,xb,xc)"),
		array( "R(a,b,c)","a!=b","Col(b,a,a1)", "-R(a1,b,c)")
	),
	new Theorem( "Satz8.4",
		array( "-R(xa,xb,xc) | R(xa,xb,s(xb,xc))"),
		array( "R(a,b,c)","-R(a,b,s(b,c))")
	),
	new Theorem( "Satz8.5", 
		array( "R(xa,xb,xb)"), 
		array( "-R(a,b,b)")
	),
	new Theorem( "Satz8.6",
		array( "-R(xa,xb,xc) | -R(xa1,xb,xc) | -T(xa,xc,xa1) | xb = xc"),
		array( "R(a,b,c)", "R(a1,b,c)", "T(a,c,a1)", "b != c")
	),   
	new Theorem( "Satz8.7", 
		array( "-R(xa,xb,xc) | -R(xa,xc,xb) | xb = xc"),
		array( "R(a,b,c)","R(a,c,b)","b != c"),
		array( "c1=s(b,c)", "a1=s(c,a)")
	),
	new Theorem( "Satz8.8",
		array( "-R(xa,xb,xa) | xa = xb"),
		array( "R(a,b,a)", "a != b")
	),
	new Theorem( "Satz8.9",
		array( "-R(xa,xb,xc) | -Col(xa,xb,xc) | xa=xb | xc=xb"),
		array( "R(a,b,c)","Col(a,b,c)","a!=b","c!=b")
	),   
	new Theorem( "Satz8.10",
		array( "-R(xa,xb,xc) | -E3(xa,xb,xc,xa1,xb1,xc1) | R(xa1,xb1,xc1)"),
		array( "R(a,b,c)","E3(a,b,c,a1,b1,c1)","-R(a1,b1,c1)"),
		array( "d = s(b,c)","d1 = s(b1,c1)")
	),
	new Theorem( "Satz8.12a",
		array( "-perpAt(xa,xb,xc,xp,xq) | perpAt(xp,xq,xc,xa,xb)"),
		array( "perpAt(a,b,c,p,q)", "-perpAt(p,q,c,a,b)")
	),  
	new Theorem( "Satz8.12b",
		array( "-perp(xa,xb,xp,xq) | perp(xp,xq,xa,xb)"),
		array( "perp(a,b,p,q)","-perp(p,q,a,b)")
	),

	new Theorem( "Satz8.13a",   // left-to-right of 8.13 
		array(  "-perpAt(xa,xb,xc,xp,xq) | xa != xb",
				"-perpAt(xa,xb,xc,xp,xq) | xp != xq",
				"-perpAt(xa,xb,xc,xp,xq) | Col(xp,xq,xc)",
				"-perpAt(xa,xb,xc,xp,xq) | Col(xa,xb,xc)",
				"-perpAt(xa,xb,xc,xp,xq) | Col(xa,xb,f813(xa,xb,xp,xq,xc))",
				"-perpAt(xa,xb,xc,xp,xq) | Col(xp,xq,g813(xa,xb,xp,xq,xc))",
				"-perpAt(xa,xb,xc,xp,xq) | xc != f813(xa,xb,xp,xq,xc)",
				"-perpAt(xa,xb,xc,xp,xq) | xc != g813(xa,xb,xp,xq,xc)",
				"-perpAt(xa,xb,xc,xp,xq) | R(f813(xa,xb,xp,xq,xc),xc,g813(xa,xb,xp,xq,xc))"
			),
 		array(  "perpAt(a,b,c,p,q)",
				"a=b | p=q | -Col(p,q,c) | -Col(a,b,c) | -Col(a,b,x) | -Col(p,q,y) | c = x | c = y | -R(x,c,y)"
			 ),
		"",
		array( "f813", "g813")
	), 
	new Theorem( "Satz8.13b",  // right-to-left of 8.13
		array( 
			 "xa=xb | xp=xq | -Col(xp,xq,xcx) | -Col(xa,xb,xcx) | -Col(xa,xb,u) | -Col(xp,xq,v) | xcx = u | xcx=v | -R(u,xcx,v) | perpAt(xa,xb,xcx,xp,xq)",
			 ),
		array( "a!=b","p!=q","Col(p,q,cx)","Col(a,b,cx)","Col(a,b,cu)","Col(p,q,cv)","cx != cu", "cx != cv", 
		       "R(cu,cx,cv)", "-perpAt(a,b,cx,p,q)"
		 	 ),
		array( "t = f811(a,b,p,q,cx)", "r = g811(a,b,p,q,cx)")
	),  
	new Theorem( "Satz8.14a",  // perpendicular lines are distinct lines 
		array( "-perp(xa,xb,xp,xq) | -Col(xa,xb,xp) | -Col(xa,xb,xq)"),
		array( "perp(a,b,p,q)","Col(a,b,p)", "Col(a,b,q)"),
		array( "c = il(a,b,p,q)")
	),
	// 8.14b says, if ab perp pq and c lies on both lines then ab and pq are perp at c.
	new Theorem( "Satz8.14b",
		array( "-perp(xa,xb,xp,xq) | -Col(xa,xb,xc) | -Col(xp,xq,xc) | perpAt(xa,xb,xc,xp,xq)"),
		array( "perp(a,b,p,q)","Col(a,b,c)", "Col(p,q,c)","-perpAt(a,b,c,p,q)")
	),   
	// 8.14c says that if ab and pq are perp at c, then c is unique, specifically il(a,b,p,q).
    new Theorem( "Satz8.14c",
		array( "-perpAt(xa,xb,xc,xp,xq) | xc = il(xa,xb,xp,xq)"),
		array( "perpAt(a,b,c,p,q)","c != il(a,b,p,q)")
	),  
    new Theorem( "Satz8.15",
		array( "xa=xb | -Col(xa,xb,xd) | -perp(xa,xb,xc,xd) | perpAt(xa,xb,xd,xc,xd)"),
		array( "a != b","Col(a,b,d)","perp(a,b,c,d)","-perpAt(a,b,d,c,d)")
	),
    new Theorem( "Satz8.16a",
		array(  "xa = xb | -Col(xa,xb,xp) | -Col(xa,xb,xq) | xq = xp | -Col(xa,xb,xc) | -perp(xa,xb,xc,xp) ",
 				"xa = xb | -Col(xa,xb,xp) | -Col(xa,xb,xq) | xq = xp |  R(xc,xp,xq) | -perp(xa,xb,xc,xp)"
 			 ),
		array( "a != b","Col(a,b,p)","Col(a,b,q)","q != p","Col(a,b,c) | -R(c,p,q)", "perp(a,b,c,p)")
	),
    new Theorem( "Satz8.16b",
		array( "xa = xb | -Col(xa,xb,xp) | -Col(xa,xb,xq) | xq = xp | perp(xa,xb,xc,xp) | Col(xa,xb,xc) | -R(xc,xp,xq)"),
		array( "a != b","Col(a,b,p)","Col(a,b,q)","q != p","-perp(a,b,c,p)","-Col(a,b,c)","R(c,p,q)")
	), 
    new Theorem( "Satz8.18a",  // uniqueness of dropped perpendicular
		array( "Col(xa,xb,xc) | -Col(xa,xb,xp) | -Col(xa,xb,xq) | -perp(xa,xb,xc,xp) | -perp(xa,xb,xc,xq) | xp = xq"),
		array( "-Col(a,b,c)","Col(a,b,p)","Col(a,b,q)","perp(a,b,c,p)","perp(a,b,c,q)","p != q")
	),   
	new Theorem( "Satz8.18",    // existence of dropped perpendicular (Lotsatz)
		array(  "Col(xa,xb,xc) | Col(xa,xb,foot(xa,xb,xc))",
				"Col(xa,xb,xc) | perp(xa,xb,xc,foot(xa,xb,xc))"
			 ),
		array( "-Col(a,b,c)","-Col(a,b,x) | -perp(a,b,c,x)"),
		array(  "cy = ext(b,a,a,c)",
				"p = isomidpoint(cy,c,a)",
				"cz = ext(a,cy,cy,p)",
				"q = ext(p,cy,cy,a)",
				"q1 = s(cz,q)",
				"c1 = ext(q1,cy,cy,c)",
				"cx = isomidpoint(c,c1,cy)"
			 ),
		array("foot")
	),  
	new Theorem( "Satz8.20a",
		array( "-R(xa,xb,xc) | -M(s(xa,xc),xp,s(xb,xc)) | R(xb,xa,xp)"),
		array( "R(a,b,c)","M(s(a,c),p,s(b,c))","-R(b,a,p)"),
		array( "d = s(b,c)","b1 = s(a,b)","c1 = s(a,c)","d1 = s(a,d)","p1 = s(a,p)")
	),
	new Theorem( "Satz8.20b",
		array( "-R(xa,xb,xc) | -M(s(xa,xc),xp,s(xb,xc)) |   xb = xc | xa!=xp"),
		array( "R(a,b,c)","M(s(a,c),p,s(b,c))","b != c","a=p"),
		array( "d = s(b,c)","b1 = s(a,b)","c1 = s(a,c)","d1 = s(a,d)","p1 = s(a,p)")
	),  
	new Theorem( "perp1",
		array( "-perp(xa,xb,xp,xq) | perp(xb,xa,xp,xq)"),
		array( "perp(a,b,p,q)","-perp(b,a,p,q)"),
		array( "c=il(a,b,p,q)")
	),    
	new Theorem( "ExtCol2",
		array( "xa = xb | xc = xd | -Col(xa,xb,xc) | -Col(xa,xb,xd) | -Col(xc,xd,xp) | Col(xa,xb,xp)"),
		array(  "a != b",
				"c != d",
				"Col(a,b,c)",
				"Col(a,b,d)",
				"Col(c,d,p)",
				"-Col(a,b,p)"
	 		 )
	),
	new Theorem( "Satz8.21a",  // case 1 of Satz 8.21
		array(  "xa = xb |  perp(xa,xb,erect21a(xa,xb,xc),xa) | Col(xa,xb,xc)",
				"xa = xb |  Col(xa,xb,erectAux21a(xa,xb,xc)) | Col(xa,xb,xc)",
				"xa = xb | T(xc,erectAux21a(xa,xb,xc),erect21a(xa,xb,xc)) | Col(xa,xb,xc)"
			 ),
		array(  "a != b",
				"-perp(a,b,x,a) | -Col(a,b,y) | -T(c,y,x)",
				"-Col(a,b,c)"
			 ),
		array(  "cx = foot(a,b,c)",
				"c1 = s(cx,c)",
				"a1 = s(a,c)",
				"p = isomidpoint(c1,a1,a)",
				"t = crossbar(a1,a,c,c1,cx,p)"
			 ),
		array( "erect21a", "erectAux21a")
	),
	new Theorem( "Satz8.21",
		array(  "xa = xb |  perp(xa,xb,erect(xa,xb,xc),xa)",
				"xa = xb |  Col(xa,xb,erectAux(xa,xb,xc))",
				"xa = xb | T(xc,erectAux(xa,xb,xc),erect(xa,xb,xc))"
	   		 ),
		array( "a != b","-perp(a,b,x,a) | -Col(a,b,y) | -T(c,y,x)"),
		array( "c1 = pointOffLine(a,b)","p = erect21a(a,b,c1)"),
		array("erect", "erectAux")
	),  
	new Theorem( "Satz8.22b",  // case 1 of Satz8.22
		array( "-le(xa,xp,xb,xq) | -perp(xa,xb,xa,xp) | -perp(xa,xb,xb,xq) |  -T(xp,xt,xq) | -Col(xa,xb,xt) | M(xa,midpointAux(xa,xb,xp,xq,xt),xb)"),
		array(  "le(a,p,b,q)", 
 				"perp(a,b,a,p)",
				"perp(a,b,b,q)",
				"T(p,t,q)",
				"Col(a,b,t)",
				"-M(a,x,b)"     // The main goal of 8.22
	   ),
		array( "r = insert(a,p,b,q)",
				"cx = ip(p,t,q,b,r)",
				"p1 = s(a,p)",
				"r1 = ext(p1,cx,cx,r)",
				"m = isomidpoint(r,r1,cx)" 
			 ),
		array( "midpointAux")
	), 
	new Theorem( "Satz8.22",  // existence of midpoint
		array( "M(xa,midpoint(xa,xb),xb)"),
		array( "-M(a,x,b)"),
		array(  "p = erect(a,b,b)",
				"P = erect(b,a,a)",
				"Q = erect(a,b,P)",
				"tt = erectAux(a,b,P)",
				"rr = insert(b,P,a,Q)",
				"R2 = insert(a,P,b,Q)",
				"q = erect(b,a,p)",
				"t = erectAux(b,a,p)",
				"r = insert(a,p,b,q)",
				"r2 = insert(b,q,a,p)"
			 ),
		array("midpoint")
	), 
	new Theorem( "Satz8.24a",
		array( "-perp(xp,xa,xa,xb) | -perp(xq,xb,xa,xb) | -Col(xa,xb,xt) | -T(xp,xt,xq)".
		 	   "| -T(xb,xr,xq) | -E(xa,xp,xb,xr) | xcx != ip(xp,xt,xq,xb,xr) | M(xa,xcx,xb)"),
		array(  "perp(p,a,a,b)",
				"perp(q,b,a,b)",
				"Col(a,b,t)",
				"T(p,t,q)",
				"T(b,r,q)",
				"E(a,p,b,r)",		
				"cx = ip(p,t,q,b,r)",
				"-M(a,cx,b)"  // first goal of 8.24b and 8.22
			),
		array(  "p1 = s(a,p)", 
				"m =isomidpoint(r,r1,cx)",
				"r1 = ext(p1,cx,cx,r)"
			 )
	),
	new Theorem( "Satz8.24b",
		array( "-perp(xp,xa,xa,xb) | -perp(xq,xb,xa,xb) | -Col(xa,xb,xt) | -T(xp,xt,xq)".
				"| -T(xb,xr,xq) | -E(xa,xp,xb,xr) | xcx != ip(xp,xt,xq,xb,xr) | M(xp,xcx,xr)"),
		array(  "perp(p,a,a,b)",
				"perp(q,b,a,b)",
				"Col(a,b,t)",
				"T(p,t,q)",
				"T(b,r,q)",
				"E(a,p,b,r)",		
				"cx = ip(p,t,q,b,r)",
				"-M(p,cx,r)"  // second goal of 8.24b
			),
		array(  "p1 = s(a,p)", 
				"m =isomidpoint(r,r1,cx)",
				"r1 = ext(p1,cx,cx,r)"
			 )
	),
	new Theorem( "Satz8.24",
		array( "-perp(xp,xa,xa,xb) | -perp(xq,xb,xa,xb) | -Col(xa,xb,xt) | -T(xp,xt,xq)".
		 		"| -T(xb,xr,xq) | -E(xa,xp,xb,xr) | M(xp,midpoint(xa,xb),xr)"),
		array(  "perp(p,a,a,b)",
				"perp(q,b,a,b)",
				"Col(a,b,t)",
				"T(p,t,q)",
				"T(b,r,q)",
				"E(a,p,b,r)",		
				"-M(p,midpoint(a,b),r)"
			),
		array(  "p1 = s(a,p)", 
				"cx = ip(p,t,q,b,r)",
			 )
	),
	new Theorem( "ext1",
		array( "-Col(xa,xb,xc) | -Col(xa,xb,xd) |  xa =xb | Col(xa,xc,xd)"),
		array( "Col(a,b,c)","Col(a,b,d)","a != b", "-Col(a,c,d)")
	),
    new Theorem( "ExtPerp",    
		array( "-Col(xa,xb,xp) | -Col(xa,xb,xq) | xp=xq | xa = xb | -perpAt(xp,xq,xr,xc,xd) | perpAt(xa,xb,xr,xc,xd)"),
		array( "Col(a,b,p)", "Col(a,b,q)", "p != q", "a != b", "perpAt(p,q,r,c,d)","-perpAt(a,b,r,c,d)")
    ),
	new Theorem( "ExtPerp2",   
		array( "-Col(xa,xb,xp) | -Col(xa,xb,xq) | xp=xq | xa = xb | -perp(xp,xq,xc,xd) | perp(xa,xb,xc,xd)"),
		array( "Col(a,b,p)", "Col(a,b,q)", "p != q", "a != b", "perp(p,q,c,d)","-perp(a,b,c,d)"),
		array( "p = il(a,b,p,q)")
	),
	new Theorem( "ExtPerp3",   
		array( "xa = xb | xa = xc | xb = xc | xd = xc | xa = xd | -perp(xb,xa,xa,xc) | -Col(xa,xc,xd) | perp(xb,xa,xa,xd)"),
		array( "a != b", "a != c", "b != c", "d != c", "a != d", "perp(b,a,a,c)", "Col(a,c,d)","-perp(b,a,a,d)")
	),
    new Theorem( "ExtPerp4",
		array( "-perp(xa,xb,xp,xq) | perp(xa,xb,xq,xp)"),
		array(  "perp(a,b,p,q)",
				"-perp(a,b,q,p)"
			 )
	), 
	new Theorem( "ExtPerp5",
		array( "-Col(xa,xb,xp) | -Col(xa,xb,xq) | xp=xq | xa = xb | perp(xp,xq,xc,xd) | -perp(xa,xb,xc,xd)"
 		     ),
		array(  "Col(a,b,p)",
				"Col(a,b,q)",
				"p != q",
				"a != b",
				"-perp(p,q,c,d)",
				"perp(a,b,c,d)"
			 )
	),
	new Theorem( "ExtPerp6",
		array( "-Col(xa,xb,xp) | -Col(xa,xb,xq) | xp=xq  | xa=xb |  perp(xc,xd,xp,xq) | -perp(xc,xd,xa,xb)"
 		     ),
		array(  "Col(a,b,p)",
				"Col(a,b,q)",
				"p != q",
				"a != b",
				"-perp(c,d,p,q)",
				"perp(c,d,a,b)"
			 )
	),
	new Theorem( "ExtSameSide1",
		array( "-Col(xa,xb,xc) | xa = xb | xa = xc | -samesideline(xp,xq,xa,xb) | samesideline(xp,xq,xa,xc)"),
		array(  "Col(a,b,c)",
				"a != b",
				"a != c",
				"samesideline(p,q,a,b)",
				"-samesideline(p,q,a,c)"
	  		 ),
		array(  "t1 = ss1(p,q,a,b)",
				"t2 = ss2(p,q,a,b)",
				"t3 = ss3(p,q,a,b)"
	   		 )
	),	
	new Theorem( "ExtSameSide2",
		array( "xa = xb  | -samesideline(xp,xq,xa,xb) | samesideline(xp,xq,xb,xa)"),
		array(  "a != b",
				"samesideline(p,q,a,b)",
				"-samesideline(p,q,b,a)"
			 ),
		array(  "t1 = ss1(p,q,a,b)",
				"t2 = ss2(p,q,a,b)",
				"t3 = ss3(p,q,a,b)"
			 )
	),
	new Theorem( "Satz9.2",
		array( "-opposite(xa,xp,xq,xb) | opposite(xb,xp,xq,xa)"),
		array( "opposite(a,p,q,b)","-opposite(b,p,q,a)")
    ),
	new Theorem( "Satz9.3a",  // case 1 of Satz 9.3
		array( "-opposite(xa,xp,xq,xc) | -Col(xp,xq,xm) | -M(xa,xm,xc) | -Col(xp,xq,xr)".
		 		"| -sameside(xa,xr,xb) | opposite(xb,xp,xq,xc) | -T(xr,xb,xa)"),
		array(  "opposite(a,p,q,c)",
				"Col(p,q,m)",
				"M(a,m,c)",
				"Col(p,q,r)",
				"sameside(a,r,b)",
				"-opposite(b,p,q,c)",
				"T(r,b,a)"        //  Case 1
	  		 ),
		array( "t = ip(r,b,a,c,m)")
    ),
	new Theorem( "Satz9.3",  
		array( "-opposite(xa,xp,xq,xc) | -Col(xp,xq,xm) | -M(xa,xm,xc) | -Col(xp,xq,xr)".
		 		"| -sameside(xa,xr,xb) | opposite(xb,xp,xq,xc)"),
		array(  "opposite(a,p,q,c)",
				"Col(p,q,m)",
				"M(a,m,c)",
				"Col(p,q,r)",
				"sameside(a,r,b)",
				"-opposite(b,p,q,c)"
	  		 ),
		array(	"b1 = s(m,b)",
				"r1 = s(m,r)"
			 )
	),
	new Theorem( "SideReflect",
		array( "-sameside(xa,xb,xc) | sameside(s(xm,xa),s(xm,xb),s(xm,xc))"),
		array(  "sameside(a,b,c)", 
				"-sameside(s(m,a),s(m,b),s(m,c))"
			 ),
		array(  "a1 = s(m,a)",
				"b1 = s(m,b)",
				"c1 = s(m,c)"
			 ),
		"",
		array("-T(b,a,c) | T(b,a,c)")
	),
	      // next few theorems are all special cases of Satz 9.4 in SST
	new Theorem( "Satz9.4a",   // line 1 implies left-to-right of line 2 assuming r != s and an inequality
		array( "-opposite(xa,xp,xq,xc) | xp = xq | -Col(xp,xq,xcs) | -Col(xp,xq,xr)".
		 		"| -perp(xp,xq,xa,xr) | -perp(xp,xq,xc,xcs) | -M(xr,xm,xcs) | -sameside(u,xr,xa)".
		 		"| -le(xcs,xc,xr,xa) | xr = xcs | sameside(s(xm,u),xcs,xc)"),
		array(  "opposite(a,p,q,c)",
				"p != q", 
				"Col(p,q,cs)",
				"Col(p,q,r)",
				"perp(p,q,a,r)",
				"perp(p,q,c,cs)",
				"M(r,m,cs)",
				"sameside(cu,r,a)",
				"le(cs,c,r,a)",
				"r != cs",
				"-sameside(s(m,cu),cs,c)"
			 ),
		array( 	"t = il(a,c,p,q)",
				"b = insert(cs,c,r,a)",
				"m = ip(c,t,a,r,b)"
			 )
	),  
	new Theorem( "Satz9.4a2",   // line 1 implies right-to-left of line 2 assuming r != s and an inequality
		array( "-opposite(xa,xp,xq,xc) | xp = xq | -Col(xp,xq,xcs) | -Col(xp,xq,xr)".
		 		"| -perp(xp,xq,xa,xr) | -perp(xp,xq,xc,xcs) | -M(xr,xm,xcs) | sameside(u,xr,xa)".
		 		"| -le(xcs,xc,xr,xa) | xr = xcs | -sameside(s(xm,u),xcs,xc)"),
		array(  "opposite(a,p,q,c)",
				"p != q", 
				"Col(p,q,cs)",
				"Col(p,q,r)",
				"perp(p,q,a,r)",
				"perp(p,q,c,cs)",
				"M(r,m,cs)",
				"-sameside(cu,r,a)",
				"le(cs,c,r,a)",
				"r != cs",
				"sameside(s(m,cu),cs,c)"
			 ),
		array( 	"t = il(a,c,p,q)",
				"b = insert(cs,c,r,a)"
			 )
	),
	new Theorem( "Satz9.4b",  //  line 1 implies left-to-right of line 2 assuming r = s and an inequality.
		array( "-opposite(xa,xp,xq,xc) | xp = xq | -Col(xp,xq,xcs) | -Col(xp,xq,xr) | -perp(xp,xq,xa,xr)".
		 		"| -perp(xp,xq,xc,xcs) | -M(xr,xm,xcs) | -sameside(u,xr,xa) | xr != xcs | sameside(s(xm,u),xcs,xc)"),
		array(  "opposite(a,p,q,c)",
				"p != q", 
				"Col(p,q,cs)",
				"Col(p,q,r)",
				"perp(p,q,a,r)",
				"perp(p,q,c,cs)",
				"M(r,m,cs)",
				"sameside(cu,r,a)",
				"r = cs",
				"-sameside(s(m,cu),cs,c)"
			 ),
		array(  "t = il(a,c,p,q)",
				"b = insert(cs,c,r,a)",
				"cu1 = s(m,cu)"
			 )
	),
	new Theorem( "Satz9.4",  // line 1 implies left-to-right of line 2 
		array(  "-opposite(xa,xp,xq,xc) | xp = xq | -Col(xp,xq,xcs) | -Col(xp,xq,xr) | -perp(xp,xq,xa,xr)".
		 		"| -perp(xp,xq,xc,xcs) | -M(xr,xm,xcs) | -sameside(u,xr,xa) |  sameside(s(xm,u),xcs,xc)"),
		array(  "opposite(a,p,q,c)",
				"p != q", 
				"Col(p,q,cs)",
				"Col(p,q,r)",
				"perp(p,q,a,r)",
				"perp(p,q,c,cs)",
				"M(r,m,cs)",
				"sameside(cu,r,a)",
				"-sameside(s(m,cu),cs,c)"
	  		 ),
		array(  "cu1 = s(m,cu)"),
		"",
		array(  "r = cs | r != cs" )
	),
	new Theorem( "Satz9.4c",  // line 1 implies line 3
		array(  "-opposite(xa,xp,xq,xc) | xp = xq | -Col(xp,xq,xcs) | -Col(xp,xq,xr) | -perp(xp,xq,xa,xr)".
		 		"| -perp(xp,xq,xc,xcs) | -M(xr,xm,xcs) |  -sameside(u,xr,xa) | -sameside(v,xcs,xc) | opposite(u,xp,xq,v)"),
		array(  "opposite(a,p,q,c)",
				"p != q", 
				"Col(p,q,cs)",
				"Col(p,q,r)",
				"perp(p,q,a,r)",
				"perp(p,q,c,cs)",
				"M(r,m,cs)",
				"sameside(cu,r,a)",
				"sameside(cv,cs,c)",
				"-opposite(cu,p,q,cv)"
	  		 ),
		array(  "cu1 = s(m,cu)" )
	),
	new Theorem( "Satz9.5",
		array( "-opposite(xa,xp,xq,xc) | -Col(xp,xq,xr) | -sameside(xa,xr,xb) | opposite(xb,xp,xq,xc)"),
		array(  "opposite(a,p,q,c)",
				"Col(p,q,r)",
				"sameside(a,r,b)",
				"-opposite(b,p,q,c)"
	  		 ),
		array(  "cx = foot(p,q,a)",
				"cy = foot(p,q,b)",
				"cz = foot(p,q,c)",
				"m = midpoint(cx, cz)",
				"d = s(m,a)"
	  		 )
	),
	new Theorem( "Satz9.6",   // outer Pasch
		array(  "-T(xa,xc,xp) | -T(xb,xq,xc) | T(xa,op(xq,xb,xp,xc,xa),xb)",
				"-T(xa,xc,xp) | -T(xb,xq,xc) | T(xp,xq,op(xq,xb,xp,xc,xa))"
			 ),
		array(  "T(a,c,p)",
				"T(b,q,c)",
				"-T(a,x,b) | -T(p,q,x)"
			 ),
		array(	 "d = il(a,b,p,q)",
				"t = ip(p,c,a,b,d)"
			 ),
		array( "op")
	),  
	new Theorem( "Satz9.8", 
		array( "-opposite(xa,xp,xq,xc) | opposite(xb,xp,xq,xc) | -samesideline(xa,xb,xp,xq)"),
		array(  "opposite(a,p,q,c)",
				"-opposite(b,p,q,c)",
				"samesideline(a,b,p,q)"
			 ),
	   // following is the diagram in Fig. 38, p. 72 
		array(  "cx = ss1(a,b,p,q)",
				"cy = ss2(a,b,p,q)",
				"d = ss3(a,b,p,q)",
				"cz = ip(a,cx,d,b,cy)"
 			 )
	),
	new Theorem( "Satz9.9",
		array( "-opposite(xa,xp,xq,xb) | -samesideline(xa,xb,xp,xq)"),
		array( 	"opposite(a,p,q,b)",
				"samesideline(a,b,p,q)"
	  		 )
	),
	new Theorem( "Satz9.13",
		array( "xp=xq | -samesideline(xa,xb,xp,xq) | -samesideline(xb,xc,xp,xq) | samesideline(xa,xc,xp,xq)" ),
		array(  "p != q",
				"samesideline(a,b,p,q)",
				"samesideline(b,c,p,q)",
				"-samesideline(a,c,p,q)"
			 ),
		array(  "t = ss3(a,b,p,q)",
				"r = il(t,c,p,q)",
				"cs = ss1(a,b,p,q)",
				"k = ss2(a,b,p,q)"
 			 )
	),
	new Theorem( "Lemma9.13a",
 		array( "-samesideline(xp,xq,xa,xb) | samesideline(xp,xq,xb,xa)"),
		array(  "samesideline(p,q,a,b)",
				"-samesideline(p,q,b,a)"
			 ),
		array(  "r = ss1(p,q,a,b)",
				"cs = ss2(p,q,a,b)",
				"t = ss3(p,q,a,b)"
			 )
	),
	new Theorem( "Lemma9.13b",
 		array( "xa = xb | -M(u,v,w) | -Col(xa,xb,u) | -Col(xa,xb,w) | Col(xa,xb,v)"
			 ),
		array(  "a != b",
				"M(cu,cv,cw)",
				"Col(a,b,cu)",
				"Col(a,b,cw)",
				"-Col(a,b,cv)"
			 )
	),
	new Theorem( "Lemma9.13c",
		array( "xd = xe | -T(xe,xd,xd1) | -samesideline(xa,xb,xd1,xe) | samesideline(xa,xb,xd,xe)"),
		array(  "d != e",
				"T(e,d,d1)",
				"samesideline(a,b,d1,e)",
				"-samesideline(a,b,d,e)"
			 ),
		array(  "one = ss3(a,b,d1,e)",
				"a1 = ss1(a,b,d1,e)",
				"b1 = ss2(a,b,d1,e)"
			 )
	),
	new Theorem( "Lemma9.13d",
		array( "xa = xb | -samesideline(xp,xq,xa,xb) | samesideline(xq,xp,xa,xb)" ),
		array(  "a != b",   
				"samesideline(p,q,a,b)",
				"-samesideline(q,p,a,b)"
			 )
	),
	new Theorem( "Lemma9.13e",
 		array( "-opposite(xa,xp,xq,xb) | -samesideline(xb,xc,xp,xq) | opposite(xa,xp,xq,xc)"
			 ),
		array(  "opposite(a,p,q,b)",
				"samesideline(b,c,p,q)",
				"-opposite(a,p,q,c)"
 			 )
	),
	new Theorem( "Lemma9.13g",
		array( "xp=xq | -perpAt(xp,xq,xc,xa,xc) | -perpAt(xp,xq,xc,xb,xc) | xa = xc | Col(xc,xa,xb)"
			 ),
		array(  "p != q",
				"perpAt(p,q,c,a,c)",
				"perpAt(p,q,c,b,c)",
				"a != c",
				"-Col(c,a,b)"
	  		 ),
		array(  "r = ext(p,q,p,c)",
				"t = s(c,r)"
			 )
	),
	new Theorem( "Lemma9.13f-case1",
		array( "xp = xq | Col(xp,xq,xr) | Col(xp,xq,xcs) | samesideline(xr,xcs,xp,xq) | opposite(xr,xp,xq,xcs)| xp != foot(xp,xq,xr)" 
			 ),
		array(  "p != q",
				"-Col(p,q,r)",
				"-Col(p,q,cs)",
				"-samesideline(r,cs,p,q)",
				"-opposite(r,p,q,cs)",
				 "p = foot(p,q,r)"
 			 ),
		array(  "e = foot(p,q,r)",
				"r1 = erect(e,q,cs)",
				"f = erectAux(e,q,cs)"
			 )
	),
	new Theorem( "Lemma9.13f-case2",
		array(  "xp = xq | Col(xp,xq,xr) | Col(xp,xq,xcs) | samesideline(xr,xcs,xp,xq) | opposite(xr,xp,xq,xcs)".
		 		"| xp = foot(xp,xq,xr)" 
			 ),
		array(  "p != q",
				"-Col(p,q,r)",
				"-Col(p,q,cs)",
				"-samesideline(r,cs,p,q)",
				"-opposite(r,p,q,cs)",
				"p != foot(p,q,r)"
 			 ),
		array(  "e = foot(p,q,r)",
				"r1 = erect(e,q,cs)",
				"f = erectAux(e,q,cs)",
				"r2 = erect(e,p,cs)",
				"f2 = erectAux(e,p,cs)"
			 )
	),
	new Theorem( "Lemma9.13f",
		array( "xp = xq | Col(xp,xq,xr) | Col(xp,xq,xcs) | samesideline(xr,xcs,xp,xq) | opposite(xr,xp,xq,xcs)" 
			 ),
		array(  "p != q",
				"-Col(p,q,r)",
				"-Col(p,q,cs)",
				"-samesideline(r,cs,p,q)",
				"-opposite(r,p,q,cs)"
 			 ),
		array(  "e = foot(p,q,r)",
				"r1 = erect(e,q,cs)",
				"f = erectAux(e,q,cs)",
				"r2 = erect(e,p,cs)",
				"f2 = erectAux(e,p,cs)"
			 ),
		"",
		array("e=p | e!=p")
	),
	new Theorem( "Satz9.16",  // used in Satz 11.15b 
		array( "-samesideline(xa,xb,xp,xq) | -sameside(xa,xq,xr) | samesideline(xr,xb,xp,xq)" ),
		array(  "samesideline(a,b,p,q)",
				"sameside(a,q,r)",
				"-samesideline(r,b,p,q)"		
			 ),
		array(  "t = ss3(a,b,p,q)",
				"a1 = ss1(a,b,p,q)",
				"b1 = ss2(a,b,p,q)",
				"d1 = ip(q,c,a,t,a1)",
				"d2 = op(a1,t,q,a,c)"
			 )
	),
	new Theorem( "Satz9.19b",  // right to left of 9.19
		array("xc = xd | -Col(xc,xd,xp) | -Col(xa,xb,xp) | -sameside(xa,xp,xb) | Col(xc,xd,xa) |  samesideline(xa,xb,xc,xd)"),
		array(  "c != d",
				"Col(c,d,p)",
				"Col(a,b,p)",
				"sameside(a,p,b)",
				"-Col(c,d,a)",
				"-samesideline(a,b,c,d)"
			)
	),
	new Theorem( "Satz10.2a",
		array(  "xa = xb | Col(xa,xb,midpoint(xp,reflect(xa,xb,xp)))",  
				"xa = xb | xp = reflect(xa,xb,xp) | perp(xa,xb,xp,reflect(xa,xb,xp))"
			 ),
		array(  "a!=b",
				"-Col(a,b,midpoint(p,x)) | -perp(a,b,p,x)",
				"-Col(a,b,midpoint(p,x)) | p != x"
			 ), 
		array( 
				"cx = foot(a,b,p)",
				"p1 = s(cx,p)"   
			 ),
		array( "reflect"),
      // reflect is introduced as a Skolem symbol, not as a 
      //  demodulator reflect(a,b,p) = s(foot(a,b,p),p), since foot is only 
      //  defined when p is not on Line(a,b), but reflect(a,b,p) is always defined when a!= b.
      //  In the book,  reflect(a,b,x) is also defined when a=b, to be s(a,x), but in practice 
      //  it is only used when a != b and a,b determine a line.  In our treatment it's only sensible when a!=b.
		array("b=cx | b!= cx")
    ),
	new Theorem( "Satz10.2b",
		array(  "xa = xb | -Col(xa,xb,midpoint(xp,xp1)) | -perp(xa,xb,xp,xp1) | xp1 = reflect(xa,xb,xp)",
				"xa = xb | -Col(xa,xb,midpoint(xp,xp1)) | xp != xp1  | xp1 = reflect(xa,xb,xp)"
			 ),
 		array(  "a != b", 
				"Col(a,b,midpoint(p,p1))",
				"perp(a,b,p,p1) | p = p1",
				"p1 != reflect(a,b,p)"
	  		 ),
 		array(  "q = reflect(a,b,p)",
				"r = midpoint(p,q)",
				"j = midpoint(p,p1)"
			 ),
		"",   // no Skolem symbols
		array(  "p = p1 | p != p1", 
				"Col(a,b,p) | -Col(a,b,p)"
			 )
	),
	new Theorem( "Satz10.4",
		array( "xa = xb | reflect(xa,xb,xp) != xp1 | reflect(xa,xb,xp1) = xp"),
		array(  "a != b",     
				"reflect(a,b,p) = p1",
				"reflect(a,b,p1) != p"
			 ),   
		array( "m = midpoint(p,p1)")
	),
	new Theorem( "Satz10.5",
		array( "xa = xb | reflect(xa,xb,reflect(xa,xb,xp)) = xp"),
		array(  "a != b",  
				"reflect(a,b,reflect(a,b,p)) != p"
			 )
	),
	new Theorem( "Satz10.6",
		array( "xa = xb | reflect(xa,xb,xp) != xp1  | xp = reflect(xa,xb,xp1)"),
 		array(  "a != b",    
				"reflect(a,b,p) = p1",
				"p != reflect(a,b,p1)"
			 )
	),
	new Theorem( "Satz10.7",
		array( "xa = xb | reflect(xa,xb,xp) != reflect(xa,xb,xq) | xp = xq"),
		array(  "a != b",    
				"reflect(a,b,p) = reflect(a,b,q)",
				"p != q"
			 )
	),
	new Theorem( "Satz10.8a",
		array( "xa = xb | reflect(xa,xb,xp) != xp | Col(xa,xb,xp)"),
		array(  "a != b",     
				"reflect(a,b,p) = p",  
				"-Col(a,b,p)"
			 )
	),
	new Theorem( "Satz10.8b",
		array( "xa = xb | -Col(xa,xb,xp) | reflect(xa,xb,xp) = xp"),
 		array(  "a != b",  
				"Col(a,b,p)", 
				"reflect(a,b,p) != p"
			 )
	),
	new Theorem( "Satz10.10a",  //   case of 10.10 when Col(a,b,p)
 		array( "xa=xb | -Col(xa,xb,xp) | E(xp,xq,reflect(xa,xb,xp),reflect(xa,xb,xq))"),
 		array(  "a != b",
				"Col(a,b,p)" ,
				"-E(p,q,reflect(a,b,p),reflect(a,b,q))" 
 			 ),
		array(  "p1 = reflect(a,b,p)",
				"q1 = reflect(a,b,q)",
				"cx = midpoint(p,p1)",
				"cy = midpoint(q,q1)",
				"cz = midpoint(cx,cy)",
				"r = s(cz,p)",
				"r1 = s(cz,p1)"
			 )
	),  
	new Theorem( "Satz10.10",
		array( "xa=xb | E(xp,xq,reflect(xa,xb,xp),reflect(xa,xb,xq))" ),
 		array(  "a != b",
				"-E(p,q,reflect(a,b,p),reflect(a,b,q))"
			 ),
 		array(  "p1 = reflect(a,b,p)",
				"q1 = reflect(a,b,q)",
				"cx = midpoint(p,p1)",
				"cy = midpoint(q,q1)",
				"cz = midpoint(cx,cy)",
				"r = s(cz,p)",
				"r1 = s(cz,p1)"
			 )
	),
 	new Theorem( "Satz10.12b",
		array( "-R(xa,xb,xc) | -R(xa1,xb,xc) | -E(xa,xb,xa1,xb) | E(xa,xc,xa1,xc)"),
		array(  "R(a,b,c)",
				"R(a1,b,c)",
				"E(a,b,a1,b)",
				"-E(a,c,a1,c)"
			 ),
	      // following is diagram 50, page 91 of SST
 		array(  "cz = midpoint(a,a1)",
				"cstar = s(b,c)", 
				"bstar = midpoint(c,cstar)"
 			 ),
		"",
		array(  "a1 != a | a1 = a",
				"b = cz |  b != cz",
				"cstar = c | cstar != c"
			 )
	),
	new Theorem( "Satz10.12c",  // like 10.12a,  but assumes also b = midpoint(c,c1) and c != c1 
		array( "-R(xa,xb,xc) | -R(xa1,xb,xc1) | -E(xa,xb,xa1,xb) | -E(xb,xc,xb,xc1) | E(xa,xc,xa1,xc1) | xb != midpoint(xc,xc1) | xc = xc1"),
 		array(  "R(a,b,c)",
				"R(a1,b,c1)",
				"E(a,b,a1,b)",
				"E(b,c,b,c1)",
				"-E(a,c,a1,c1)",
				"b = midpoint(c,c1)",
				"c != c1"
			 ),
		array(  "cy = midpoint(c,c1)",
				"a2 = reflect(b,cy,a1)"
			 )
	),
	new Theorem( "Satz10.12a",
		array( "-R(xa,xb,xc) | -R(xa1,xb,xc1) | -E(xa,xb,xa1,xb) | -E(xb,xc,xb,xc1) | E(xa,xc,xa1,xc1)"),
		array(  "R(a,b,c)",
				"R(a1,b,c1)",
				"E(a,b,a1,b)",
				"E(b,c,b,c1)",
				"-E(a,c,a1,c1)"
	  		 ),
		array( "cy = midpoint(c,c1)",
				"a2 = reflect(b,cy,a1)"
			 ),
		"",  // no Skolem symbols
		array(" c = c1 | c != c1")
	),
	new Theorem( "Satz10.12",
		array( "-R(xa,xb,xc) | -R(xa1,xb1,xc1) | -E(xa,xb,xa1,xb1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1)"),
		array(  "R(a,b,c)",
				"R(a1,b1,c1)",
				"E(a,b,a1,b1)",
				"E(b,c,b1,c1)",
				"-E(a,c,a1,c1)"
			 ),
		array(  "cx = midpoint(b,b1)",
				"aone = s(cx,a1)",
				"cone = s(cx,c1)"
			 )
	),
	new Theorem( "Satz10.14",
		array(  "xa = xb | reflect(xa,xb,xp) != xp1 | Col(xa,xb,xp) | opposite(xp,xa,xb,xp1)"),
		array(  "a != b",
				"reflect(a,b,p) = p1",
				"-Col(a,b,p)",
				"-opposite(p,a,b,p1)"
			 ),
		array(  "m = midpoint(p,p1)")
	),
	new Theorem( "Satz10.15",
		array(  "xb = xc | -Col(xb,xc,xa) | Col(xb,xc,xq) | perp(xb,xc, erectsameside(xb,xc,xa,xq),xa)",
				"xb = xc | -Col(xb,xc,xa) | Col(xb,xc,xq)| samesideline(erectsameside(xb,xc,xa,xq),xq,xb,xc)"
			 ),
		array(  "b != c",
				"Col(b,c,a)",
				"-Col(b,c,q)",
				"-perp(b,c,x,a) | -samesideline(x,q,b,c)"
			 ),
		array(  "e = ext(b,c,b,a)",  // so e != a
				"p1 = reflect(e,a,q)",		
		        "p = erect(a,e,p1)" ,
				"t  = erectAux(a,e,p1)",
				"m = midpoint(q,p1)"
		     ),   
		array(  "erectsameside")
	),
	new Theorem( "Satz10.16a",
		array(  "xa=xb | Col(xa,xb,xc) | Col(xa1,xb1,xp) | -E(xa,xb,xa1,xb1) | E3(xa,xb,xc,xa1,xb1,triangle(xa,xb,xc,xa1,xb1,xp))",
				"xa=xb | Col(xa,xb,xc) | Col(xa1,xb1,xp) | -E(xa,xb,xa1,xb1) | samesideline(triangle(xa,xb,xc,xa1,xb1,xp),xp,xa1,xb1)" 
			 ),
		array(  "a!= b",   
				"-Col(a,b,c)",
				"-Col(a1,b1,p)",
				"E(a,b,a1,b1)",
				"-E3(a,b,c,a1,b1,x) | -samesideline(x,p,a1,b1)"
			 ),
 		array(  "cx = foot(a,b,c)",
				"cx1 = insert5(a,b,cx,a1,b1)",    
				"q = erectsameside(a1,b1,cx1,p)",
				"c1 = insert(cx,c,cx1,q)"
			 ),
		array( "triangle")
	),
	new Theorem( "Satz10.16b",
		array( "xa = xb | Col(xa,xb,xc) | Col(xa1,xb1,xp) | -E(xa,xb,xa1,xb1) | -E3(xa,xb,xc,xa1,xb1,xc1)".
		 		"| -samesideline(xc1,xp,xa1,xb1) | -E3(xa,xb,xc,xa1,xb1,xc2) | -samesideline(xc2,xp,xa1,xb1) | xc1=xc2"
	         ),
		array(  "a!= b",   
				"-Col(a,b,c)",
				"-Col(a1,b1,p)",
				"E(a,b,a1,b1)",
				"E3(a,b,c,a1,b1,c1)",
				"samesideline(c1,p,a1,b1)", 
				"E3(a,b,c,a1,b1,c2)",
				"samesideline(c2,p,a1,b1)", 
				"c1 != c2"
			 ),
 		array(  "cstar = reflect(a1,b1,c2)",
				"t = il(c1,cstar,a1,b1)"  
			 ),
		"",
		array("t=a1 | t != a1")
	),
	new Theorem( "Satz11.3a",  // left-to-right of Satz 11.3 
		array(  "-congruent(xa,xb,xc,xd,xe,xf) | sameside(ext(xb,xa,xe,xd),xb,xa)",
				"-congruent(xa,xb,xc,xd,xe,xf) | sameside(ext(xb,xc,xe,xf),xb,xc)",
				"-congruent(xa,xb,xc,xd,xe,xf) | sameside(ext(xe,xd,xb,xa),xe,xd)",
				"-congruent(xa,xb,xc,xd,xe,xf) | sameside(ext(xe,xf,xb,xc),xe,xf)",
				"-congruent(xa,xb,xc,xd,xe,xf) | E3(ext(xb,xa,xe,xd),xb, ext(xb,xc,xe,xf),ext(xe,xd,xb,xa),xe,ext(xe,xf,xb,xc))",
			 ),
 		array(  "congruent(a,b,c,d,e,f)", 
				"-sameside(ext(b,a,e,d),b,a) | -sameside(ext(b,c,e,f),b,c) | -sameside(ext(e,d,b,a),e,d)".
				" | -sameside(ext(e,f,b,c),e,f) | -E3(ext(b,a,e,d),b,ext(b,c,e,f),ext(e,d,b,a),e,ext(e,f,b,c))"
			 ),   
 		array(  "a1 =ext(b,a,e,d)",
				"c1 = ext(b,c,e,f)",
				"d1 = ext(e,d,b,a)",
				"f1 = ext(e,f,b,c)"
			)
	),
	new Theorem( "Satz11.3d",  // right-to-left of Satz 11.3 
		array( "-sameside(xa1,xb,xa) | -sameside(xc1,xb,xc) | -sameside(xd1,xe,xd) | -sameside(xf1,xe,xf)".
		 		"| -E3(xa1,xb,xc1,xd1,xe,xf1) | congruent(xa,xb,xc,xd,xe,xf)"
 			 ),
		array(  "sameside(a1,b,a)",
				"sameside(c1,b,c)",
				"sameside(d1,e,d)",
				"sameside(f1,e,f)",
				"E3(a1,b,c1,d1,e,f1)", 
				"-congruent(a,b,c,d,e,f)"
			 ),
 		array(  "a1 = ext(b,a,e,d)",
				"c1 = ext(b,c,e,f)",
				"d1 = ext(e,d,b,a)",
				"f1 = ext(e,f,b,c)"
			 )
	),
	new Theorem( "Satz11.4b",  // right-to-left of Satz 11.4
		array(  "xa = xb | xc = xb | xd = xe | xf = xe | sameside(f113a(xa,xb,xc,xd,xe,xf),xb,xa) | congruent(xa,xb,xc,xd,xe,xf)",
				"xa = xb | xc = xb | xd = xe | xf = xe | sameside(f113c(xa,xb,xc,xd,xe,xf),xb,xc) | congruent(xa,xb,xc,xd,xe,xf)",
				"xa = xb | xc = xb | xd = xe | xf = xe | sameside(f113d(xa,xb,xc,xd,xe,xf),xe,xd) | congruent(xa,xb,xc,xd,xe,xf)",
				"xa = xb | xc = xb | xd = xe | xf = xe | sameside(f113f(xa,xb,xc,xd,xe,xf),xe,xf) | congruent(xa,xb,xc,xd,xe,xf)",
				"xa = xb | xc = xb | xd = xe | xf = xe | E(xb,f113a(xa,xb,xc,xd,xe,xf),xe,f113d(xa,xb,xc,xd,xe,xf)) | congruent(xa,xb,xc,xd,xe,xf)",
				"xa = xb | xc = xb | xd = xe | xf = xe | E(xb,f113c(xa,xb,xc,xd,xe,xf),xe,f113f(xa,xb,xc,xd,xe,xf)) | congruent(xa,xb,xc,xd,xe,xf)",
				"xa = xb | xc = xb | xd = xe | xf = xe | -E(f113a(xa,xb,xc,xd,xe,xf),f113c(xa,xb,xc,xd,xe,xf),f113d(xa,xb,xc,xd,xe,xf),f113f(xa,xb,xc,xd,xe,xf))".
				"| congruent(xa,xb,xc,xd,xe,xf)"
			 ),
 		array( "a != b",
				"c != b",
				"d != e",
				"f != e",
				"-sameside(xa1,b,a) | -sameside(xc1,b,c) | -sameside(xd1,e,d) | -sameside(xf1,e,f) | -E(b,xa1,e,xd1) | -E(b,xc1,e,xf1) | E(xa1,xc1,xd1,xf1)",
				"-congruent(a,b,c,d,e,f)"
			 ),
 		array(  "a1 =ext(b,a,e,d)",
				"c1 = ext(b,c,e,f)",
				"d1 = ext(e,d,b,a)",
				"f1 = ext(e,f,b,c)"
			 ),
		array("f113a","f113c","f113d","f113f")
	),
	new Theorem( "Satz11.4",   // left-to-rightof Satz 11.4,  
		array(  "-congruent(xa,xb,xc,xd,xe,xf) | -sameside(xa2,xb,xa) | -sameside(xc2,xb,xc) | -sameside(xd2,xe,xd) | -sameside(xf2,xe,xf) | -E(xb,xa2,xe,xd2) | -E(xb,xc2,xe,xf2) | E(xa2,xc2,xd2,xf2)"
			),
		array(  "congruent(a,b,c,d,e,f)",
				"sameside(a2,b,a)",
				"sameside(c2,b,c)",
				"sameside(d2,e,d)",
				"sameside(f2,e,f)",
				"E(b,a2,e,d2)",
				"E(b,c2,e,f2)",
				"-E(a2,c2,d2,f2)"
			 ),
		array(  "a1 = ext(b,a,e,d)",
			 	"c1 = ext(b,c,e,f)",
			 	"d1 = ext(e,d,b,a)",
			 	"f1 = ext(e,f,b,c)"
			 )
	),
	new Theorem( "Satz11.4d", // (3) implies (4) on page 95
		array(  "-sameside(xa1,xb,xa2) | -sameside(xc1,xb,xc2) | -sameside(xd1,xe,xd2) | -sameside(xf1,xe,xf2)".
		 		"| -E3(xa1,xb,xc1,xd1,xe,xf1) | xa=xb | xc=xb | xd=xe | xf=xe | -sameside(xa2,xb,xa)".
		 		"| -sameside(xc2,xb,xc) | -sameside(xd2,xe,xd) | -sameside(xf2,xe,xf) |  -E(xb,xa2,xe,xd2)".
		 		"| -E(xb,xc2,xe,xf2) | E(xa2,xc2,xd2,xf2)"
		 	 ),
		array(  "sameside(a1,b,a2)",
				"sameside(c1,b,c2)",
				"sameside(d1,e,d2)",
				"sameside(f1,e,f2)",
				"E3(a1,b,c1,d1,e,f1)",
				"a!=b",
				"c!=b",
				"d!=e",
				"f!=e",
				"sameside(a2,b,a)",
				"sameside(c2,b,c)",
				"sameside(d2,e,d)",
				"sameside(f2,e,f)",
				"E(b,a2,e,d2)",
				"E(b,c2,e,f2)",
				"-E(a2,c2,d2,f2)"
			 )
	),
	new Theorem( "Satz11.6",  // reflexivity of angle congruence
		array( "xa = xb | xc = xb | congruent(xa,xb,xc,xa,xb,xc)"),
		array(  "a != b", 
				"c != b",
				"-congruent(a,b,c,a,b,c)"
			 ),
		array(  "p = ext(b,a,b,a)",
				"q = ext(b,c,b,c)"
			 )
	),
	new Theorem( "Satz11.7",  // symmmetry of angle congruence
		array( "-congruent(xa,xb,xc,xd,xe,xf) | congruent(xd,xe,xf,xa,xb,xc)"),
		array(  "congruent(a,b,c,d,e,f)",
				"-congruent(d,e,f,a,b,c)"
			 ),
		array(  "a1 = ext(b,a,e,d)",
				"c1 = ext(b,c,e,f)",
				"d1 = ext(e,d,b,a)",
				"f1 = ext(e,f,b,c)"
			 )
	),
	new Theorem( "Satz11.8",  // transitivity of angle congruence
		array( "-congruent(xa1,xb1,xc1,xa2,xb2,xc2) | -congruent(xa2,xb2,xc2,xa3,xb3,xc3) | congruent(xa1,xb1,xc1,xa3,xb3,xc3)"),
		array(  "congruent(a1,b1,c1,a2,b2,c2)",
				"congruent(a2,b2,c2,a3,b3,c3)",
				"-congruent(a1,b1,c1,a3,b3,c3)"
			 ),
		array(  "p2 = insert(b1,a1,b2,a2)",
				"q2 = insert(b1,c1,b2,c2)",
				"p3 = insert(b1,a1,b3,a3)",
				"q3 = insert(b1,c1,b3,c3)"
			 )
	),
	new Theorem( "Satz11.9",  // abc is congruent to cba
		array(  "xa = xb | xc = xb | congruent(xa,xb,xc,xc,xb,xa)"),
		array(  "a != b", "c != b", "-congruent(a,b,c,c,b,a)"),
		array(  "p = ext(b,a,b,c)",
				"q = ext(b,c,b,a)"
			 )
	),
	new Theorem( "Satz11.15a",
		array(  "Col(xa,xb,xc) | Col(xd,xe,xp) | congruent(xa,xb,xc,xd,xe,constructAngle(xa,xb,xc,xd,xe,xp))",
				"Col(xa,xb,xc) | Col(xd,xe,xp) | samesideline(constructAngle(xa,xb,xc,xd,xe,xp),xp,xd,xe)"
			 ),
 		array(  "-Col(a,b,c)",
				"-Col(d,e,p)",
				"-congruent(a,b,c,d,e,x) | -samesideline(x,p,d,e)"
			 ),
 		array(  "a1 = ext(b,a,e,d)",
				"c1 = ext(b,c,e,f)",
				"d1 = ext(e,d,b,a)",
				"f1 = triangle(b,a1,c1,e,d1,p)"
			 ),
		array( "constructAngle" )
	),
	new Theorem( "Satz11.15b",
 		array( "Col(xa,xb,xc) | Col(xd,xe,xp) | -congruent(xa,xb,xc,xd,xe,xf1) | -samesideline(xf1,xp,xe,xd)".
 				" | -congruent(xa,xb,xc,xd,xe,xf2) | -samesideline(xf2,xp,xe,xd) | sameside(xf1,xe,xf2)"
			 ),
		array(  "-Col(a,b,c)",
			"-Col(d,e,p)",  
			"congruent(a,b,c,d,e,f1)",
			"samesideline(f1,p,e,d)",
			"congruent(a,b,c,d,e,f2)",
			"samesideline(f2,p,e,d)",   
			"-sameside(f1,e,f2)"
			 ),
		array(  "d2 = ext(e,d,e,d)",
				"f3 = ext(e,f1,e,f2)",
				"f4 = ext(e,f2,e,f1)"
			 )
	),  
	new Theorem( "Satz11.49a",
		array( "-congruent(xa,xb,xc,xa1,xb1,xc1) | -E(xb,xa,xb1,xa1) | -E(xb,xc,xb1,xc1) | E(xa,xc,xa1,xc1)"
 			 ),
		array(  "congruent(a,b,c,a1,b1,c1)",
			"E(b,a,b1,a1)",
			"E(b,c,b1,c1)",
			"-E(a,c,a1,c1)"
			 )
	),
	new Theorem( "Satz11.49b",
		array( "-congruent(xa,xb,xc,xa1,xb1,xc1) | -E(xb,xa,xb1,xa1) | -E(xb,xc,xb1,xc1) | xa=xc | congruent(xb,xa,xc,xb1,xa1,xc1)"
			 ),
 		array(  "congruent(a,b,c,a1,b1,c1)",
				"E(b,a,b1,a1)",
				"E(b,c,b1,c1)",
				"a != c",
				"-congruent(b,a,c,b1,a1,c1)"
 			 )
	),
	new Theorem( "ExtParallel",
 		array( "-parallel(xa1,xa2,xb1,xb2) | parallel(xa1,xa2,xb2,xb1)"
			 ),
 		array(  "parallel(a1,a2,b1,b2)",
				"-parallel(a1,a2,b2,b1)"
			 ),
		array( "c = e5(a1,a2,b2,b1)")
	),
	new Theorem( "Satz12.6",
		array( "-parallel(xa1,xa2,xb1,xb2) | -Col(xb1,xb2,xb3) | -Col(xb1,xb2,xb4) | samesideline(xb3,xb4,xa1,xa2)"
			 ),
		array(  "parallel(a1,a2,b1,b2)",
				"Col(b1,b2,b3)",
				"Col(b1,b2,b4)",
				"-samesideline(b3,b4,a1,a2)"
			 ),
		array(  "d=il(b3,b4,a1,a2)" 
			 )
	),
	new Theorem( "Lemma12.11-case1",  
		array(  "xc2 != ext(xp1,xp2,xp1,xa) | -opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
		 		"| -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
		 		"| T(c12111(xt,xq,xr,xcs,xp1,xp2,xa),b12111(xt,xq,xr,xcs,xp1,xp2,xa),xt)",
				"xc2 != ext(xp1,xp2,xp1,xa) | -opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
				"| -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
				"| Col(xp1,xp2,c12111(xt,xq,xr,xcs,xp1,xp2,xa))",
				"xc2 != ext(xp1,xp2,xp1,xa) | -opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
				" | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
				" | Col(xr,xcs,b12111(xt,xq,xr,xcs,xp1,xp2,xa))",
				"xc2 != ext(xp1,xp2,xp1,xa) | -opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
				" | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2) | xa != c12111(xt,xq,xr,xcs,xp1,xp2,xa)"
			),
		array(  "c2 = ext(p1,p2,p1,a)",
				"opposite(t,r,cs,c2)",  // this makes it Case 1
				"-Col(t,q,a)",
				"Col(r,cs,a)",
				"Col(p1,p2,a)",
				"parallel(t,q,r,cs)",
				"parallel(t,q,p1,p2)", 
				"-T(xc,xb,t) | -Col(p1,p2,xc) | -Col(r,cs,xb) | a=xc"
			),
		array(  "c = s(a,c2)", 
				"b = il(t,c2,r,cs)",
				"b2 = il(t,c,r,cs)"
			 ),
		array( "c12111", "b12111")
	),   
	new Theorem( "Lemma12.11-case2",  
		array(  "xc2 != ext(xp1,xp2,xp1,xa) | opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
		 		"| -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
		 		"| T(c12112(xt,xq,xr,xcs,xp1,xp2,xa),b12112(xt,xq,xr,xcs,xp1,xp2,xa),xt)",
				"xc2 != ext(xp1,xp2,xp1,xa) | opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
				" | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
				" | Col(xp1,xp2,c12112(xt,xq,xr,xcs,xp1,xp2,xa))",
				"xc2 != ext(xp1,xp2,xp1,xa) | opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
				" | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
				" | Col(xr,xcs,b12112(xt,xq,xr,xcs,xp1,xp2,xa))",
				"xc2 != ext(xp1,xp2,xp1,xa) | opposite(xt,xr,xcs,xc2) | Col(xt,xq,xa) | -Col(xr,xcs,xa)".
				" | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2) | xa != c12112(xt,xq,xr,xcs,xp1,xp2,xa)"
			),
		array(  "c2 = ext(p1,p2,p1,a)",
				"-opposite(t,r,cs,c2)",  // This makes it Case 2 
				"-Col(t,q,a)",
				"Col(r,cs,a)",
				"Col(p1,p2,a)",
				"parallel(t,q,r,cs)",
				"parallel(t,q,p1,p2)", 
				"-T(xc,xb,t) | -Col(p1,p2,xc) | -Col(r,cs,xb) | a=xc"
			),
		array(  "c = s(a,c2)", 
				"b = il(t,c2,r,cs)",
				"b2 = il(t,c,r,cs)"
			 ),
		array( "c12112", "b12112")
	),   
	new Theorem( "Lemma12.11",    
		array(  "Col(xt,xq,xa) | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs)".
		 		"| -parallel(xt,xq,xp1,xp2) | T(c1211(xt,xq,xr,xcs,xp1,xp2,xa),b1211(xt,xq,xr,xcs,xp1,xp2,xa),xt)",
				"Col(xt,xq,xa) | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs)".
				" | -parallel(xt,xq,xp1,xp2) | Col(xp1,xp2,c1211(xt,xq,xr,xcs,xp1,xp2,xa))",
				"Col(xt,xq,xa) | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs)".
				" | -parallel(xt,xq,xp1,xp2) | Col(xr,xcs,b1211(xt,xq,xr,xcs,xp1,xp2,xa))",
				"Col(xt,xq,xa) | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa) | -parallel(xt,xq,xr,xcs)".
				" | -parallel(xt,xq,xp1,xp2) | xa != c1211(xt,xq,xr,xcs,xp1,xp2,xa)"
			),
		array(  "-Col(t,q,a)",
				"Col(r,cs,a)",
				"Col(p1,p2,a)",
				"parallel(t,q,r,cs)",
				"parallel(t,q,p1,p2)", 
				"-T(xc,xb,t) | -Col(p1,p2,xc) | -Col(r,cs,xb) | a=xc"
			),
		array( 
				"c2 = ext(p1,p2,p1,a)",
				"c = s(a,c2)", 
				"b = il(t,c2,r,cs)",
				"b2 = il(t,c,r,cs)",
				"ca1 = c12111(t,q,r,cs,p1,p2,a)",
				"cb1 = b12111(t,q,r,cs,p1,p2,a)",
				"ca2 = c12112(t,q,r,cs,p1,p2,a)",
				"cb2= b12112(t,q,r,cs,p1,p2,a)"
			 ),
		array( "c1211", "b1211"),
		array( "opposite(t,r,cs,c2) | -opposite(t,r,cs,c2)")
	),   
	new Theorem( "Satz12.11-case1",   // case a=d of Satz12.11
		array(  "xt = xq | Col(xt,xq,xa) | xr = xcs | xp1 = xp2 | -Col(xr,xcs,xa)".
		 		"| -Col(xp1,xp2,xa) | Col(xr,xcs,xp1) | -parallel(xt,xq,xr,xcs)".
		 		"| -parallel(xt,xq,xp1,xp2) |xb!=b1211(xt,xq,xr,xcs,xp1,xp2,xa)".
		 		"| xc1!=c1211(xt,xq,xr,xcs,xp1,xp2,xa)|xc!=s(xa,xc1)|xd!=ip(xt,xb,xc1,xc,xa)|xa=xd",
				"xt = xq | Col(xt,xq,xa) | xr = xcs | xp1 = xp2 | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa)".
				" | Col(xr,xcs,xp2) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
				"| xb!=b1211(xt,xq,xr,xcs,xp1,xp2,xa) | xc1!=c1211(xt,xq,xr,xcs,xp1,xp2,xa)".
				"|xc!=s(xa,xc1)|xd!=ip(xt,xb,xc1,xc,xa)|xa=xd"
			 ),
		array(  "t != q",
				"-Col(t,q,a)",
				"r != cs",
				"p1 != p2",
				"Col(r,cs,a)",
				"Col(p1,p2,a)",
				"-Col(r,cs,p1) | -Col(r,cs,p2)",
				"parallel(t,q,r,cs)",
				"parallel(t,q,p1,p2)",
				"b = b1211(t,q,r,cs,p1,p2,a)",
				"c1 =c1211(t,q,r,cs,p1,p2,a)", 
				"c = s(a,c1)",
				"d = ip(t,b,c1,c,a)",
				"a!=d"
			 ),   
		array( 
				"cx = e1(a,b,c,d,t)",
				"cy = e2(a,b,c,d,t)"
			 )
	),
	new Theorem( "Satz12.11-case2",   // case array=d of Satz12.11
		array(  "xt = xq | Col(xt,xq,xa) | xr = xcs | xp1 = xp2 | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa)".
		 		"| Col(xr,xcs,xp1) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
				"| xb!=b1211(xt,xq,xr,xcs,xp1,xp2,xa) | xc1!=c1211(xt,xq,xr,xcs,xp1,xp2,xa)".
				" | xc!=s(xa,xc1) | xd!=ip(xt,xb,xc1,xc,xa)|xa!=xd",
				"xt = xq | Col(xt,xq,xa) | xr = xcs | xp1 = xp2 | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa)".
				" | Col(xr,xcs,xp2) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)".
				"| xb!=b1211(xt,xq,xr,xcs,xp1,xp2,xa) | xc1!=c1211(xt,xq,xr,xcs,xp1,xp2,xa)".
				" | xc!=s(xa,xc1) | xd!=ip(xt,xb,xc1,xc,xa)|xa!=xd"
			 ),
		array(  "t != q",
				"-Col(t,q,a)",
				"r != cs",
				"p1 != p2",
				"Col(r,cs,a)",
				"Col(p1,p2,a)",
				"-Col(r,cs,p1) | -Col(r,cs,p2)",
				"parallel(t,q,r,cs)",
				"parallel(t,q,p1,p2)",
				"b = b1211(t,q,r,cs,p1,p2,a)",
				"c1 =c1211(t,q,r,cs,p1,p2,a)", 
				"c = s(a,c1)",
				"d = ip(t,b,c1,c,a)",
				"a=d"
			 ),   
		array( 
				"cx = e1(a,b,c,d,t)",
				"cy = e2(a,b,c,d,t)"
			 )
	),
	new Theorem( "Satz12.11",   // so far we proved this only by dividing into two cases a=d or a!=d.
		array(  "xt = xq | Col(xt,xq,xa) | xr = xcs | xp1 = xp2 | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa)".
		 		"| Col(xr,xcs,xp1) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)",
				"xt = xq | Col(xt,xq,xa) | xr = xcs | xp1 = xp2 | -Col(xr,xcs,xa) | -Col(xp1,xp2,xa)".
				" | Col(xr,xcs,xp2) | -parallel(xt,xq,xr,xcs) | -parallel(xt,xq,xp1,xp2)"
			 ),
		array(  "t != q",
				"-Col(t,q,a)",
				"r != cs",
				"p1 != p2",
				"Col(r,cs,a)",
				"Col(p1,p2,a)",
				"-Col(r,cs,p1) | -Col(r,cs,p2)",
				"parallel(t,q,r,cs)",
				"parallel(t,q,p1,p2)"
			 ),   
		array(  "b = b1211(t,q,r,cs,p1,p2,a)",
				"c1 =c1211(t,q,r,cs,p1,p2,a)", 
				"c = s(a,c1)",
				"d = ip(t,b,c1,c,a)",
				"cx = e1(a,b,c,d,t)",
				"cy = e2(a,b,c,d,t)"
			 ),
		"",  // no Skolem symbols
		"a=d | a!=d"
	)
);  // end of theorems
 
 
$NamedTheorems = array();
foreach($TarskiTheorems as $t)
  { $NamedTheorems[$t->name] = $t;
  }  
$NamedAxioms = array();
foreach($TarskiAxioms as $t)
  { $NamedAxioms[$t->name] = $t;
  }
$NamedDefinitions = array();
foreach($TarskiDefinitions as $t)
  { $NamedDefinitions[$t->name] = $t;
  }

function axioms_needed($chapter, $theorem_name)
// given a chapter number,  return an array of axiom names 
// to be used in that chapter.  Sometimes $theorem_name is needed as well. 
{ $ans =  array("A1", "A2", "A3", "A4", "A5");
  if($chapter == 2 && $theorem_name == "Satz2.15")
      { $ans[] = "A6";
	    $ans[] = "A7";
	  } 
  if($chapter > 2)
      { $ans[] = "A6";
	    $ans[] = "A7";   // first used in Satz 3.2
		$ans[] = "A8";   // needed in Satz 3.13.a and Satz 3.13.b
	  }
  if($chapter == "9A")
      $ans[] = "A9";  // upper dimension needed only for Lemma9.13f and Lemma 9.13g.
  if($chapter >= 12)
      $ans[] = "A10";  // parallel axiom first used in Chapter 12
  return $ans;
}
//_______________________________________________________________

function definitions_needed($chapter )
// return an array of definition names to be used for the specified chapter.
// assumes chapter is not  2  or 3, where no definitions are used.
{ $ans = array("Defn2.10", "Defn4.1", "Defn4.4", "Defn4.10", "Defn4.15");
  if($chapter == "2" || $chapter == "3")
      echo "$error, called definitions_needed incorrectly.\n";
  if($chapter == 4)
     return $ans;
  $ans[] = "Defn5.4";
  if($chapter == "5" || $chapter == "5A")
     return $ans;
  $ans[] = "Defn6.1";
  if($chapter == "6")
     return $ans;
  $ans[] = "Defn7.1";
  $ans[] = "Defn7.23";  // actually only needed for Satz7.25
  if($chapter == "7")
     return $ans;
  $ans[] = "Defn8.1";
  $ans[] = "Defn8.11a";
  $ans[] = "Defn8.11b";
  if($chapter == "8" || $chapter == "8A")
     return $ans;
  $ans[] = "Defn9.1";
  $ans[] = "Defn9.7";
  if($chapter == "9" || $chapter =="9A" || $chapter = "10")
     return $ans;
  $ans[] = "Defn11.2";
  if($chapter == "11")
     return $ans;
  $ans[] = "Defn12.7";
  return $ans;
}
//_______________________________________________________________
  

function get_chapter($theorem_name)
// What chapter does this theorem belong to?  Return a string
{ if (strstr($theorem_name,"Satz"))
	  { $rest = substr($theorem_name,4);
		$x = explode(".", $rest);
		return $x[0];
	  }
  if($theorem_name == "perp1")
	  return "8";
  if($theorem_name == "SideReflect")
      return "9";
  if($theorem_name == "NarbouxLemma1")
      return "5";
  if($theorem_name == "ext1" ||  $theorem_name == "ExtCol2")
      return "8A";
  if(strstr($theorem_name, "ExtPerp"))
      return "8A";
  if (strstr($theorem_name,"Lemma9") || strstr($theorem_name,"ExtSameSide"))
	  { return "9A";
	  }
  if (strstr($theorem_name,"Lemma12") || $theorem_name == "ExtParallel")
	  { return "12";
	  }
  echo "error in get_chapter($theorem_name)\n";
}

//_______________________________________________________________

function TheoremsByChapter( $chapter)
// return an array of all theorems from the specified chapter
{ $ans = array();
  global $TarskiTheorems;
  foreach($TarskiTheorems as $t)
	{ $c = get_chapter($t->name);
	  if(!strcmp($c, $chapter))
		 $ans[] = $t;
	}
  return $ans;
}


   
?>