(def-language language-for-geometry (base-types points ) (constants (bet"[points,points,points,prop]")))

(def-theory geometry-1Remark: This entry is multiply defined. See: [1] [2](language language-for-geometry) (axioms (at-least-two-points"forsome(a,b:points, not(a=b))") (distinctness-1-2"forall(x,y,z:points, bet(x,y,z) implies not(x=y))") (distinctness-1-3"forall(x,y,z:points, bet(x,y,z) implies not(x=z))") (symmetry-of-betweeness"forall(x,y,z:points, bet(x,y,z) iff bet(z,y,x))") (anti-cyclic"forall(x,y,z:points, bet(x,y,z) implies not(bet(y,x,z)))") (existence-left"forall(x,y:points, not x=y implies forsome(b:points, bet(b,x,y)))") (existence-middle"forall(x,y:points, not x=y implies forsome(a:points, bet(x,a,y)))") ))

(def-theorem distinctness-2-3Remark: This entry is multiply defined. See: [1] [2]"forall(x,y,z:points, bet(x,y,z) implies not(y=z))"(theory geometry-1) (proof ( (apply-macete-with-minor-premises symmetry-of-betweeness) direct-inference (instantiate-theorem distinctness-1-2 ("z""y""x")) simplify simplify )))

(def-theorem existence-rightRemark: This entry is multiply defined. See: [1] [2]"forall(x,y:points, not x=y implies forsome(c:points, bet(x,y,c)))"(theory geometry-1) (proof ( (apply-macete-with-minor-premises symmetry-of-betweeness) (apply-macete-with-minor-premises existence-left) simplify )))

(def-theorem sandwichRemark: This entry is multiply defined. See: [1] [2]"forall(m:points, forsome(x,y:points, bet(x,m,y)))"(theory geometry-1) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem at-least-two-points ()) (antecedent-inference"with(p:prop,p);") (cut-with-single-formula"(not m=a) or (not m=b)") (move-to-sibling 1) simplify (block (script-comment"node added by `cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,p or p);") (block (script-comment"node added by `antecedent-inference' at (0)") (instantiate-theorem existence-right ("a""m")) auto-instantiate-existential) (block (script-comment"node added by `antecedent-inference' at (1)") (instantiate-theorem existence-right ("b""m")) auto-instantiate-existential)) )))

(def-constant collRemark: This entry is multiply defined. See: [1] [2]"lambda(x,y,z:points, bet(x,y,z) or bet(y,x,z) or bet(x,z,y))"(theory geometry-1) )

(def-theorem collinear-all-casesRemark: This entry is multiply defined. See: [1] [2]"forall(x,y,z:points, coll(x,y,z) iff (bet(x,y,z) or bet (z,y,x) or bet(y,x,z) or bet(z,x,y) or bet(x,z,y) or bet(y,z,x)))"(theory geometry-1) (proof ( (unfold-single-defined-constant (0) coll) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 1)") (contrapose"with(z,y,x:points,not(bet(x,y,z)));") (apply-macete-with-minor-premises symmetry-of-betweeness)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 3)") (contrapose"with(z,x,y:points,not(bet(y,x,z)));") (apply-macete-with-minor-premises symmetry-of-betweeness)) (apply-macete-with-minor-premises symmetry-of-betweeness) )))

(def-theorem coll-disjunctive-permuterRemark: This entry is multiply defined. See: [1] [2]"forall(a,b,c:points, coll(a,b,c) iff (coll(a,b,c) or coll(a,c,b) or coll(b,a,c) or coll(b,c,a) or coll(c,a,b) or coll(c,b,a)))"(theory geometry-1) (proof ( (apply-macete-with-minor-premises collinear-all-cases) direct-and-antecedent-inference-strategy )))

(def-theorem collinear-flipper-1-2Remark: This entry is multiply defined. See: [1] [2]"forall(x,y,z:points, coll(x,y,z) iff coll(y,x,z))"(theory geometry-1) (proof( (apply-macete-with-minor-premises collinear-all-cases) direct-and-antecedent-inference-strategy ) ))

(def-theorem collinear-flipper-2-3Remark: This entry is multiply defined. See: [1] [2]"forall(x,y,z:points, coll(x,y,z) iff coll(x,z,y))"(theory geometry-1) (proof ( (apply-macete-with-minor-premises collinear-all-cases) direct-and-antecedent-inference-strategy ) ))

(def-theorem collinear-flipper-1-3Remark: This entry is multiply defined. See: [1] [2]"forall(x,y,z:points, coll(x,y,z) iff coll(z,y,x))"(theory geometry-1) (proof ( (apply-macete-with-minor-premises collinear-all-cases) direct-and-antecedent-inference-strategy )))

(def-theory geometry-2Remark: This entry is multiply defined. See: [1] [2](language geometry-1) (component-theories geometry-1) (axioms (switching"forall(x,y,a,b:points, not a=b and coll(x,y,a) and coll(x,y,b) implies coll(a,b,x))") ))

(def-theorem other-switchingRemark: This entry is multiply defined. See: [1] [2]"forall(x,y,a,b:points, not a=b and coll(x,y,a) and coll(x,y,b) implies coll(a,b,y))"(theory geometry-2) (proof ( (apply-macete-locally-with-minor-premises collinear-flipper-1-2 (0)"coll(x,y,a)") (apply-macete-locally-with-minor-premises collinear-flipper-1-2 (0)"coll(x,y,b)") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises switching) auto-instantiate-existential )))

(def-theorem switching-all-casesRemark: This entry is multiply defined. See: [1] [2]"forall(a,b,c:points, forsome(x:points, not b=c and coll(a,x,b) and coll(a,x,c) or not c=a and coll(b,x,c) and coll(b,x,a) or not a=b and coll(c,x,a) and coll(c,x,b)) implies coll(a,b,c))"(theory geometry-2) (proof ( direct-inference direct-inference (contrapose"with(p:prop,p);") (apply-macete-with-minor-premises coll-disjunctive-permuter) (contrapose"with(p:prop,p);") (antecedent-inference"with(p:prop,p);") (antecedent-inference"with(p:prop,p);") (block (script-comment"`antecedent-inference' at (0)") (apply-macete-with-minor-premises collinear-flipper-1-3) (apply-macete-with-minor-premises switching) (instantiate-existential ("x")) simplify (apply-macete-with-minor-premises coll-disjunctive-permuter) (apply-macete-with-minor-premises coll-disjunctive-permuter)) (block (script-comment"`antecedent-inference' at (1)") (apply-macete-with-minor-premises collinear-flipper-2-3) (apply-macete-with-minor-premises switching) (instantiate-existential ("x")) simplify (apply-macete-with-minor-premises coll-disjunctive-permuter) (apply-macete-with-minor-premises coll-disjunctive-permuter)) (block (script-comment"`antecedent-inference' at (2)") (apply-macete-with-minor-premises switching) (instantiate-existential ("x")) (apply-macete-with-minor-premises coll-disjunctive-permuter) (apply-macete-with-minor-premises coll-disjunctive-permuter)) )))

(def-theorem triple-switchingRemark: This entry is multiply defined. See: [1] [2]"forall(a,b,c,x,y:points, not(a=b) and not a=c and not b=c implies coll(x,y,a) and coll(x,y,b) and coll(x,y,c) implies coll(a,b,c))"(theory geometry-2) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises switching) (apply-macete-with-minor-premises collinear-flipper-2-3) (instantiate-existential ("x")) (block (script-comment"`instantiate-existential' at (0 1)") (apply-macete-with-minor-premises switching) auto-instantiate-existential simplify) (block (script-comment"`instantiate-existential' at (0 2)") (apply-macete-with-minor-premises switching) auto-instantiate-existential simplify) )))

(def-constant coll_setRemark: This entry is multiply defined. See: [1] [2]"lambda(s:sets[points], forall(x,y,z:points,x in s and y in s and z in s and not x=y and not x=z and not y=z implies coll(x,y,z)))"(theory geometry-2))