#!/usr/bin/php 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; } ?>