(def-language language-for-geometry
(base-types points )
(constants (bet "[points,points,points,prop]")))
(def-theory geometry-1
Remark: 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 implication-equivalent
"forall(p:[points,points,points->prop],
forall(x,y,z:points,
p(x,y,z) implies p(z,y,x)) iff
forall(x,y,z:points, p(x,y,z) iff p(z,y,x)))"
(theory geometry-1)
(proof
(
(prove-by-logic-and-simplification 0)
)))
(def-theorem distinctness-2-3
Remark: 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-right
Remark: 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 sandwich
Remark: 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 coll
Remark: 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 between-implies-collinear-contra
"forall(a,b,c:points, not(coll(a,b,c)) implies not(bet(a,b,c)))"
(theory geometry-1)
(proof
(
(unfold-single-defined-constant (0) coll)
simplify
)))
(def-theorem collinear-all-cases
Remark: 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-permuter
Remark: 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 coll-conjunctive-permuter
"forall(a,b,c:points,
coll(a,b,c) iff
(coll(a,b,c) and
coll(a,c,b) and
coll(b,a,c) and
coll(b,c,a) and
coll(c,a,b) and
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-2
Remark: 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-3
Remark: 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-3
Remark: 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-theorem collinear-implies-distinct-lemma
"forall(x,y,z:points,coll(x,y,z) implies not x=y)"
(theory geometry-1)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(apply-macete-with-minor-premises distinctness-1-2)
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1)")
(force-substitution "x=y" "y=x" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises distinctness-1-2)
auto-instantiate-existential)
simplify)
(block
(script-comment "direct-and-antecedent-inference-strategy' at (0 0 2)")
(apply-macete-with-minor-premises distinctness-1-3)
auto-instantiate-existential)
)))
(def-theorem collinear-implies-distinct
"forall(x,y,z:points,coll(x,y,z) implies not x=y and not y=z and not x=z)"
(theory geometry-1)
(proof
(
direct-and-antecedent-inference-strategy
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
auto-instantiate-existential)
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 1)")
(incorporate-antecedent "with(z,y,x:points,coll(x,y,z));")
(apply-macete-with-minor-premises collinear-flipper-1-2)
(apply-macete-with-minor-premises collinear-flipper-2-3)
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
direct-inference
auto-instantiate-existential)
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 2)")
(incorporate-antecedent "with(z,y,x:points,coll(x,y,z));")
(apply-macete-with-minor-premises collinear-flipper-2-3)
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
direct-inference
auto-instantiate-existential)
)) )
(def-theory geometry-2
Remark: 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-switching
Remark: 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-cases
Remark: 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-script bet-replacer 0
(
(while (matches? "with(p:prop, p)"
"with(x,y,z:points, bet(x,y,z))")
(block
(contrapose "with(x,y,z:points, bet(x,y,z))")
(apply-macete-with-minor-premises between-implies-collinear-contra)
(apply-macete-with-minor-premises coll-conjunctive-permuter)
(contrapose 0))
(skip))
))
(def-script coll-replacer 0
(
(while (matches? "with(p:prop, p)"
"with(x,y,z:points, coll(x,y,z))")
(block
(contrapose "with(x,y,z:points, coll(x,y,z))")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
(contrapose 0))
(skip))
))
(def-script inequality-killer 0
(
bet-replacer
coll-replacer
(label-node here)
(antecedent-inference-strategy (* "with(p:prop, p)"))
direct-and-antecedent-inference-strategy
(jump-to-node here)
(for-nodes
(unsupported-descendents)
(if (matches? "with(x,y:points, not x=y)"
"with(x,y,z:points, coll(x,y,z))")
(block
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
auto-instantiate-existential)
(skip)))))
(def-script collinear-killer 1
( (let-script inequality-killer 0
(
(label-node here)
(antecedent-inference-strategy (* "with(p:prop, p)"))
direct-and-antecedent-inference-strategy
(jump-to-node here)
(for-nodes
(unsupported-descendents)
(if (matches? "with(x,y:points, not x=y)"
"with(x,y,z:points, coll(x,y,z))")
(block
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
auto-instantiate-existential)
(skip)))))
(cut-with-single-formula "with(tt:points,tt=tt)")
(antecedent-inference-strategy (* "with(p:prop, p)"))
bet-replacer
coll-replacer
(antecedent-inference-strategy (* "with(p:prop, p)"))
(apply-macete-with-minor-premises switching-all-cases)
(label-node here)
(instantiate-existential ($1))
(jump-to-node here)
(move-to-descendent (0 0))
(label-node there-2)
(for-nodes (unsupported-descendents) $inequality-killer)
(jump-to-node there-2)
(contrapose 0)
(for-nodes (unsupported-descendents) $inequality-killer)
(jump-to-node there-2)
(contrapose 1)
(for-nodes (unsupported-descendents) $inequality-killer)
(jump-to-node here)
(prove-by-logic-and-simplification 0)
))
(def-theorem triple-switching
Remark: 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-script collinear-triple-killer 2
(
(let-script
bet-replacer 0
(
(while (matches? "with(p:prop, p)"
"with(x,y,z:points, bet(x,y,z))")
(block
(contrapose "with(x,y,z:points, bet(x,y,z))")
(apply-macete-with-minor-premises between-implies-collinear-contra)
(apply-macete-with-minor-premises coll-conjunctive-permuter)
(contrapose 0))
(skip))
))
(let-script
coll-replacer 0
(
(while (matches? "with(p:prop, p)"
"with(x,y,z:points, coll(x,y,z))")
(block
(contrapose "with(x,y,z:points, coll(x,y,z))")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
(contrapose 0))
(skip))
))
(antecedent-inference-strategy (* "with(p:prop, p)"))
$bet-replacer
$coll-replacer
(antecedent-inference-strategy (* "with(p:prop, p)"))
(apply-macete-with-minor-premises triple-switching)
(label-node here)
(instantiate-existential ($2)
(label-node there)
(prove-by-logic-and-simplification 0)
(jump-to-node there)
(for-nodes (unsupported-descendents) inequality-killer)
(jump-to-node here)
(prove-by-logic-and-simplification 0))))
(def-constant coll_set
Remark: 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))
(def-theorem singletons-are-collinear
"forall(x:points, coll_set(singleton{x}))"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant-globally coll_set)
simplify
)))
(def-theorem pairs-are-collinear
"forall(x,y:points, coll_set(indic{z:points,z=x or z=y}))"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant-globally coll_set)
(prove-by-logic-and-simplification 0)
)))
(def-constant seg
"lambda(a,b:points,if( not a=b,indic{p:points,bet(a,p,b)},?sets[points]))"
(theory geometry-2)
)
(def-theorem segments-are-collinear
"forall(a,b:points,not a=b implies coll_set(seg(a,b)))"
(theory geometry-2)
(proof
(
unfold-defined-constants
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises triple-switching)
(apply-macete-with-minor-premises collinear-all-cases)
(instantiate-existential ("b" "a"))
)
))
(def-constant line
"lambda(l:sets[points],
coll_set(l) and
forall(s:sets[points],
coll_set(s) and l subseteq s implies l = s))"
(theory geometry-2))
(def-constant le
"lambda (x,y:points,
if(not x=y, indic{p:points, p=x or p=y or coll(x,y,p)} ,?sets[points]))"
(theory geometry-1)
)
(def-theorem definedness-of-le
"forall(a,b:points,not a=b implies #(le(a,b)))"
(theory geometry-2)
(usages d-r-convergence)
(proof
(
unfold-defined-constants
simplify
)))
(def-theorem other-point-lemma
"forall(x:points, forsome(y:points,not x=y))"
(theory geometry-1)
(proof
(
(instantiate-theorem at-least-two-points ())
(antecedent-inference "with(p:prop,p);")
direct-and-antecedent-inference-strategy
(case-split ("x=a"))
(block
(script-comment "node added by `case-split' at (1)")
(instantiate-existential ("b"))
simplify)
(instantiate-existential ("a"))
)))
(def-theorem lines-contain-two-points
"forall(l:sets[points],
line(l)
implies
forsome(a,b:points, a in l and b in l and not(a=b)))"
(theory geometry-2)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(case-split ("forall(p:points, not p in l)"))
(block
(script-comment "`case-split' at (1)")
(instantiate-theorem at-least-two-points ())
(cut-with-single-formula "coll_set(indic{z:points,z=a or z=b})")
(move-to-sibling 1)
(apply-macete-with-minor-premises pairs-are-collinear)
(block
(script-comment "`cut-with-single-formula' at (0)")
(auto-instantiate-universal-antecedent "with(l:sets[points],
forall(s:sets[points],
coll_set(s) and l subseteq s implies l=s));")
empty-set-handler
empty-set-handler))
(block
(script-comment "`case-split' at (2)")
pick-an-element
(case-split ("forsome(q:points, not p = q and q in l)"))
(block
(script-comment "`case-split' at (1)")
(antecedent-inference "with(p:prop,forsome(q:points,p));")
auto-instantiate-existential)
(block
(script-comment "`case-split' at (2)")
(cut-with-single-formula "forsome(r:points, not(p=r))")
(move-to-sibling 1)
(apply-macete-with-minor-premises other-point-lemma)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(r:points,p));")
(cut-with-single-formula "coll_set(indic{x:points, x=p or x=r})")
(move-to-sibling 1)
(apply-macete-with-minor-premises pairs-are-collinear)
(block
(script-comment "`cut-with-single-formula' at (0)")
(auto-instantiate-universal-antecedent "with(l:sets[points],
forall(s:sets[points],
coll_set(s) and l subseteq s implies l=s));")
(block
(script-comment "`auto-instantiate-universal-antecedent' at (0 0 0 1 0 0)")
indic-removal
(contrapose "with(p:prop,not(forsome(q:points,p)));")
(instantiate-existential ("x_$0"))
simplify)
(block
(script-comment "`auto-instantiate-universal-antecedent' at (0 0 1)")
(instantiate-existential ("p " "r"))
indic-handler))))))))
(def-theorem le-is-symmetric
"forall(a,b:points, le(a,b)==le(b,a))"
(theory geometry-1)
(proof
(
(unfold-single-defined-constant-globally le)
direct-and-antecedent-inference-strategy
(case-split ("a=b"))
simplify
(block
(script-comment "node added by `case-split' at (2)")
simplify
(apply-macete-locally collinear-flipper-1-2 (0) "coll(a,b,p)")
indic-equality
))))
(def-theorem le-is-collinear
"forall(a,b:points, not a=b implies coll_set(le(a,b)))"
(theory geometry-2)
(proof
(
unfold-defined-constants
simplify
big-d-with-simplification
(apply-macete-with-minor-premises collinear-flipper-1-3)
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 0 2 1 0)")
(apply-macete-with-minor-premises collinear-flipper-1-3)
(apply-macete-with-minor-premises collinear-flipper-2-3))
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 0 2 2 0)")
(apply-macete-with-minor-premises switching)
auto-instantiate-existential)
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 1 0 2 0)")
(apply-macete-with-minor-premises collinear-flipper-1-3)
(apply-macete-with-minor-premises collinear-flipper-1-2))
(apply-macete-with-minor-premises collinear-flipper-2-3)
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 1 2 2 0)")
(apply-macete-with-minor-premises other-switching)
auto-instantiate-existential)
(apply-macete-with-minor-premises collinear-flipper-1-2)
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 2 0 2 0)")
(apply-macete-with-minor-premises collinear-flipper-2-3)
(apply-macete-with-minor-premises switching)
(instantiate-existential ("b")))
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 2 1 2 0)")
(apply-macete-with-minor-premises collinear-flipper-2-3)
(apply-macete-with-minor-premises other-switching)
auto-instantiate-existential)
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 2 2 0 0)")
(apply-macete-with-minor-premises collinear-flipper-1-3)
(apply-macete-with-minor-premises switching)
auto-instantiate-existential
simplify)
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 2 2 1 0)")
(apply-macete-with-minor-premises collinear-flipper-1-3)
(apply-macete-with-minor-premises other-switching)
(instantiate-existential ("a"))
simplify)
(block
(script-comment "node added by `big-d-with-simplification' at (0 0 0 0 0 2 2 2)")
(apply-macete-with-minor-premises triple-switching)
auto-instantiate-existential)
)))
(def-theorem le-is-a-line
"forall(a,b:points, not a=b implies line(le(a,b)))"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant (0) line)
(apply-macete-with-minor-premises le-is-collinear)
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
(unfold-single-defined-constant-globally coll_set)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(s,f:sets[points],f subseteq s);")
simplify-insistently
(unfold-single-defined-constant-globally le)
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(x,y,z:points,p));")
simplify
)))
(def-theorem extending-collinear-sets
forall(x:points,s:sets[points], coll_set(s) and
forsome(a,b:points, a in s and b in s and coll(a,b,x))
implies coll_set(s union singleton{x}))
(theory geometry-2)
this theorem says that if you start with a collinear set s and if some
element x (outside the set is the interesting case) is collinear with any two
particular elements of s, then it is collinear with any two elements of s
and thus if it is added to s, the resulting set is still collinear.
using this result, we can obtain the collinearity of of le(a,b) by adding
one at a time to {a,b} all the elements collinear with a and b. this
argument is intuitively clear, but requires some set theoretic apparatus
that we do not want to develop at this point.")
(def-theorem lines-are-le
"forall(s:sets[points],a,b:points,
line(s) and a in s and b in s and not(a=b)
implies
s = le(a,b))"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant (0) line)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(s:sets[points],coll_set(s));")
unfold-defined-constants
simplify
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
simplify-insistently
big-d-with-simplification
(instantiate-universal-antecedent "with(p:prop,forall(s_$0:sets[points],p));"
("le(a,b)"))
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 0 0)")
(contrapose "with(f:sets[points],not(coll_set(f)));")
(apply-macete-with-minor-premises le-is-collinear))
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 0 1 0 0)")
(contrapose "with(x_$0:points,f:sets[points],not(x_$0 in f));")
(unfold-single-defined-constant (0) le)
simplify)
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 1)")
(incorporate-antecedent "with(f,s:sets[points],s=f);")
(unfold-single-defined-constant (0) le)
simplify
direct-and-antecedent-inference-strategy
(backchain "with(f,s:sets[points],s=f);")
(weaken (0))
simplify-insistently)
(block
(script-comment "node added by `instantiate-universal-antecedent' at (1 1 0)")
(unfold-single-defined-constant (0) le)
simplify)
)))
(def-constant coll%closed
"lambda(s:sets[points], forall(a,b,x:points,
a in s and b in s and coll(a,b,x)
implies
x in s))"
(theory geometry-2))
(def-theorem coll%closed-closed-under-le
"forall(b,a:points,u:sets[points],
a in u and b in u and coll%closed(u) and not a=b
implies
le(a,b) subseteq u)"
(theory geometry-2)
(proof
(
unfold-defined-constants
simplify-insistently
big-d-with-simplification
(backchain "with(p:prop,forall(x:points,p));")
(instantiate-existential ("b" "a"))
)))
(def-constant coll%closure
"lambda(s:sets[points],
iota(t:sets[points],
coll%closed(t) and s subseteq t and
forall(u:sets[points],
coll%closed(u) and s subseteq u implies t subseteq u)))"
(theory geometry-2))
(def-theorem coll%closed-iff-fixed-under-coll%closure
"forall(s:sets[points],coll%closed(s) iff coll%closure(s)=s)"
(theory geometry-2)
reverse
(proof
(
(unfold-single-defined-constant (0) coll%closure)
direct-and-antecedent-inference-strategy
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0)")
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
simplify)
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 1)")
(contrapose "with(p:prop,p);")
(apply-macete-with-minor-premises eliminate-iota-macete)
simplify))))
(def-theorem emptyset-is-coll%closed
"coll%closed(empty_indic{points})"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant (0) coll%closed)
simplify
)))
(def-theorem emptyset-equals-its-coll%closure
"coll%closure(empty_indic{points})=empty_indic{points}"
(theory geometry-2)
(proof
(
(apply-macete-with-minor-premises
rev%coll%closed-iff-fixed-under-coll%closure)
(apply-macete-with-minor-premises emptyset-is-coll%closed)
)))
(def-theorem universe-is-coll%closed
"coll%closed(sort_to_indic{points})"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant (0) coll%closed)
simplify
)))
(def-theorem universe-equals-its-coll%closure
"coll%closure(sort_to_indic{points})=sort_to_indic{points}"
(theory geometry-2)
(proof
(
(apply-macete-with-minor-premises
rev%coll%closed-iff-fixed-under-coll%closure)
(apply-macete-with-minor-premises universe-is-coll%closed)
)))
(def-theorem singleton-is-coll%closed
"forall(x:points, coll%closed(singleton{x}))"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant (0) coll%closed)
simplify
direct-and-antecedent-inference-strategy
(instantiate-theorem collinear-implies-distinct ("x" "x" "x_$0"))
)))
(def-theorem singleton-equals-its-coll%closure
"forall(x:points,coll%closure(singleton{x})=singleton{x})"
(theory geometry-2)
(proof
(
(apply-macete-with-minor-premises
rev%coll%closed-iff-fixed-under-coll%closure)
(apply-macete-with-minor-premises singleton-is-coll%closed)
)))
(def-theorem le-is-coll%closed
"forall(a,b:points, not(a=b) implies coll%closed(le(a,b)))"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant (0) coll%closed)
direct-and-antecedent-inference-strategy
(instantiate-theorem lines-are-le ("le(a,b)" "a_$0" "b_$0"))
(block
(script-comment "node added by `instantiate-theorem' at (0 0 0 0)")
(contrapose "with(f:sets[points],not(line(f)));")
(apply-macete-with-minor-premises le-is-a-line))
(instantiate-theorem collinear-implies-distinct ("a_$0" "b_$0" "x_$0"))
(block
(script-comment "node added by `instantiate-theorem' at (0 1)")
(backchain "with(f:sets[points],f=f);")
(unfold-single-defined-constant (0) le)
simplify
(instantiate-theorem collinear-implies-distinct ("a_$0" "b_$0" "x_$0")))
)))
(def-theorem le-equals-its-coll%closure
"forall(a,b:points, not(a=b) implies coll%closure(le(a,b))=le(a,b))"
(theory geometry-2)
(proof
(
(apply-macete-with-minor-premises
rev%coll%closed-iff-fixed-under-coll%closure)
(apply-macete-with-minor-premises le-is-coll%closed)
)))
(def-theorem monotonicity-of-coll%closure
"forall(s,t:sets[points], s subseteq t implies
coll%closure(s) subseteq coll%closure(t))"
(theory geometry-2)
(proof
(
)))
(def-theorem sandwich-lemma
"forall(s,t:sets[points], s subseteq t and t subseteq coll%closure(s)
implies
coll%closure(s)=coll%closure(t))"
(theory geometry-2)
(proof
(
)))
)
(def-theorem coll%closure-of-pair
"forall(a,b:points, not(a = b) implies
coll%closure(indic{x:points, x=a or x=b})=le(a,b))"
(theory geometry-2)
(proof
(
(unfold-single-defined-constant (0) coll%closure)
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises le-is-coll%closed)
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 1)")
(unfold-single-defined-constant (0) le)
simplify-insistently)
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 2 0
0 0)")
(incorporate-antecedent "with(u_$1:sets[points],coll%closed(u_$1));")
(apply-macete-with-minor-premises coll%closed-closed-under-le)
direct-inference
(incorporate-antecedent "with(u_$1:sets[points],b,a:points,
indic{x_$1:points, x_$1=a or x_$1=b} subseteq u_$1);")
simplify-insistently)
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (1 0 0
0 0)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
simplify
simplify)
)))
(def-theorem two-points-determine-a-line
"forall(s,t:sets[points],a,b:points, not a=b and line(s) and line(t) and
a in s and b in s and a in t and b in t
implies
s=t)"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem lines-are-le ("s" "a" "b"))
(instantiate-theorem lines-are-le ("t" "a" "b"))
)))
(def-theorem intersection-of-two-lines
"forall(s,t:sets[points],
line(s) and line(t) and not s=t
and
nonempty_indic_q{s inters t}
implies
forsome(x:points, s inters t=singleton{x}))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-existential ("x_$0"))
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises two-points-determine-a-line)
(cut-with-single-formula "forsome(y:points, not y=x_$0 and y in s inters t)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(y:points,p));")
auto-instantiate-existential
(simplify-antecedent "with(p:prop,p and p);")
(block
(script-comment "`auto-instantiate-existential' at (0 4)")
(simplify-antecedent "with(x_$0:points,t,s:sets[points],x_$0 in s inters t);"))
(simplify-antecedent "with(p:prop,p and p);")
(simplify-antecedent "with(x_$0:points,t,s:sets[points],x_$0 in s inters t);"))
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
simplify-insistently
direct-and-antecedent-inference-strategy
(simplify-antecedent "with(x_$0:points,f:sets[points],x_$0 in f);")
(simplify-antecedent "with(x_$0:points,t,s:sets[points],x_$0 in s inters t);")))
)))
(def-theorem le-equality-condition
"forall(x,y,z:points, coll(x,y,z) implies le(x,y)=le(x,z))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not x=y and not y=z and not x=z")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises collinear-implies-distinct))
(block
(script-comment "`cut-with-single-formula' at (0)")
(unfold-single-defined-constant-globally le)
simplify
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 1)")
(apply-macete-with-minor-premises collinear-flipper-2-3)
simplify)
(collinear-killer "y")
simplify
(collinear-killer "z"))
)))
(def-theorem intersection-of-two-les
"forall(a,b,c,d:points, not a=b and not c=d and
not le(a,b)=le(c,d)
and
nonempty_indic_q{le(a,b) inters le(c,d)}
implies
forsome(x:points, le(a,b) inters le(c,d)=singleton{x}))"
(theory geometry-2)
(proof
(
(apply-macete-with-minor-premises intersection-of-two-lines)
(apply-macete-with-minor-premises le-is-a-line)
)))
(def-theorem a-singleton-containing-a-particular-element
"forall(s:sets[ind_1],a,b:ind_1,s=singleton{a} and b in s implies
s=singleton{b})"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(b:ind_1,s:sets[ind_1],b in s);")
(backchain-repeatedly ("with(a:ind_1,s:sets[ind_1],s=singleton{a});"))
(weaken (0))
simplify-insistently
)))
(def-theorem intersection-of-les-with-common-first-point
"forall(a,b,c:points, not a=b and not a=c and not b=c and
not coll(a,b,c) implies le(b,a) inters le(b,c)=singleton{b})"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "b in le(b,a) inters le(b,c)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(unfold-single-defined-constant-globally le)
simplify)
(cut-with-single-formula
" forsome(x:points, le(b,a) inters le(b,c)=singleton{x})")
(move-to-sibling 1)
(apply-macete-with-minor-premises intersection-of-two-les)
direct-and-antecedent-inference-strategy
(contrapose "with(c,b,a:points,not(coll(a,b,c)));")
(cut-with-single-formula "c in le(b,a)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(backchain "with(f:sets[points],f=f);")
(unfold-single-defined-constant (0) le)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(c,a,b:points,c in le(b,a));")
(unfold-single-defined-constant (0) le)
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises coll-disjunctive-permuter)
simplify)
(instantiate-existential ("b"))
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-with-minor-premises tr%a-singleton-containing-a-particular-element)
simplify)
)))
(def-theorem non-collinear-between
"forall(x,y,z,p:points,not x=y and not x=z and not y=z and not coll(x,y,z) and
bet(x,p,y) implies not coll(p,y,z))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(z,y,x:points,not(coll(x,y,z)));")
(collinear-killer "p")
)))
(def-theorem non-collinear-right
"forall(x,y,z,p:points,not x=y and not x=z and not y=z and
not coll(x,y,z) and
bet(x,y,p) implies not coll(p,y,z))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(z,y,x:points,not(coll(x,y,z)));")
(collinear-killer "p")
)))
(def-theorem non-collinear-left
"forall(x,y,z,p:points,not x=y and not x=z and not y=z and
not coll(x,y,z) and
bet(y,x,p) implies not coll(p,y,z))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(z,y,x:points,not(coll(x,y,z)));")
(collinear-killer "p")
)))
(def-theorem non-collinear
"forall(x,y,z,p:points,not x=y and not x=z and not y=z and
not coll(x,y,z) and
coll(x,y,p) implies not coll(p,y,z))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(p,y,x:points,coll(x,y,p));")
unfold-defined-constants
(contrapose "with(z,y,p:points,coll(p,y,z));")
(antecedent-inference "with(p:prop,p or p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(apply-macete-with-minor-premises non-collinear-right)
auto-instantiate-existential)
(block
(script-comment "`antecedent-inference' at (1)")
(apply-macete-with-minor-premises non-collinear-left)
auto-instantiate-existential)
(block
(script-comment "`antecedent-inference' at (2)")
(apply-macete-with-minor-premises non-collinear-between)
auto-instantiate-existential)
)))
(def-theorem non-equality-1
"forall(x,y,z,p:points,not x=y and not x=z and not y=z and
not coll(x,y,z) and
coll(x,y,p) implies not p=z)"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(z,y,x:points,not(coll(x,y,z)));")
(backchain-backwards "with(z,p:points,p=z);")
)))
(def-theorem inequality-2
"forall(x,y,z,p,q:points,not x=y and not x=z and not y=z and
not coll(x,y,z) and
coll(x,y,p) and coll(x,z,q) implies not p=q)"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(z,y,x:points,not(coll(x,y,z)));")
(incorporate-antecedent "with(q,z,x:points,coll(x,z,q));")
(backchain-backwards "with(q,p:points,p=q);")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises switching-all-cases)
(instantiate-existential ("p"))
(block
(script-comment "`instantiate-existential' at (0 0 1)")
(apply-macete-with-minor-premises collinear-flipper-1-3)
(move-to-ancestor 1)
(apply-macete-with-minor-premises coll-disjunctive-permuter)
simplify)
(block
(script-comment "`instantiate-existential' at (0 0 2)")
(apply-macete-with-minor-premises switching-all-cases)
(instantiate-existential ("x"))
(block
(script-comment "`instantiate-existential' at (0 0 0)")
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
auto-instantiate-existential)
(collinear-killer "p"))
)))
(def-theorem non-collinear-2
"forall(x,y,z,p,q:points,not x=y and not x=z and not y=z and
not coll(x,y,z) and
coll(x,y,p) and coll(x,z,q) implies not coll(p,q,x))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not p=q and not q=y and not p=z")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(apply-macete-with-minor-premises inequality-2)
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(apply-macete-with-minor-premises non-equality-1)
(instantiate-existential ("z" "x"))
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(contrapose "with(z,y,x:points,not(coll(x,y,z)));")
(apply-macete-with-minor-premises collinear-flipper-2-3)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2)")
(apply-macete-with-minor-premises non-equality-1)
(instantiate-existential ("y" "x"))))
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(z,y,x:points,not(coll(x,y,z)));")
(cut-with-single-formula "coll(p,q,y) and coll(p,q,z)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-with-minor-premises triple-switching)
auto-instantiate-existential)
(block
(script-comment "`cut-with-single-formula' at (1)")
direct-and-antecedent-inference-strategy
(collinear-killer "x")
(collinear-killer "x")))
)))
(def-theorem non-collinear-2-other
"forall(x,y,z,p,q:points,not x=y and not x=z and not y=z and
not coll(x,y,z) and
coll(x,y,p) and coll(x,z,q) implies not coll(p,q,y))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not coll(q,x,y)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-collinear)
(instantiate-existential ("z"))
simplify
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(apply-macete-with-minor-premises collinear-flipper-1-2))
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-with-minor-premises collinear-flipper-2-3)
(apply-macete-with-minor-premises non-collinear)
(instantiate-existential ("x"))
(block
(script-comment "`instantiate-existential' at (0 1)")
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
(apply-macete-with-minor-premises collinear-flipper-2-3)
auto-instantiate-existential)
(block
(script-comment "`instantiate-existential' at (0 2)")
(force-substitution "y=q" "q=y" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises non-equality-1)
(instantiate-existential ("y" "x"))
(move-to-ancestor 2)
(instantiate-existential ("z" "x"))
(apply-macete-with-minor-premises collinear-flipper-2-3))
simplify)
(block
(script-comment "`instantiate-existential' at (0 3)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify))
)))
(def-theory geometry-3
(component-theories geometry-2 h-o-real-arithmetic)
)
(def-translation rel-to-coll
(source three-place-predicate-theory)
(target geometry-3)
(sort-pairs (ind_1 points))
(constant-pairs (rel coll))
(fixed-theories h-o-real-arithmetic)
(theory-interpretation-check using-simplification))
(def-theorem coll%closure-exists
"forall(s:sets[points],#(coll%closure(s)))"
(theory geometry-3)
(proof
(
(apply-macete-with-minor-premises tr%rel%closure-exists)
)))
(def-theory geometry-4
(component-theories geometry-3)
(axioms
(a-point-separates-a-line-or
"forall(a,b,m,p:points, bet(a,m,b) and coll(a,b,p) and not p=m
implies
(bet(a,m,p) or bet(p,m,b)))")
(a-point-separates-a-line-not-both "forall(a,b,m,p:points, bet(a,m,b) and
coll(a,b,p) and bet(a,m,p) implies not( bet(p,m,b)))")
)
)
(def-theorem nesting
"forall(a,b,c,d:points, bet(a,b,d) and bet(b,c,d) implies bet(a,c,d))"
(theory geometry-4)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not a=c")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(d,c,b:points,bet(b,c,d));")
(backchain-backwards "with(c,a:points,a=c);")
(apply-macete-with-minor-premises anti-cyclic))
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "(bet(b,c,a) or bet(a,c,d))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises a-point-separates-a-line-or)
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "bet(a,b,c) or bet(c,b,d)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises a-point-separates-a-line-or)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(apply-macete-with-minor-premises collinear-flipper-2-3)
(apply-macete-with-minor-premises switching)
(instantiate-existential ("b"))
(block
(script-comment "`instantiate-existential' at (0 1)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`instantiate-existential' at (0 2)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2)")
(force-substitution "c=b" "b=c" (0))
(move-to-sibling 1)
simplify
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises distinctness-1-2)
auto-instantiate-existential)))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference-strategy (0 1))
(block
(script-comment "`antecedent-inference-strategy' at (0 0)")
(contrapose "with(c,b,a:points,bet(a,b,c));")
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises anti-cyclic))
(block
(script-comment "`antecedent-inference-strategy' at (1 0)")
(contrapose "with(d,b,c:points,bet(c,b,d));")
(apply-macete-with-minor-premises anti-cyclic)))))
)))
(def-theorem other-nesting
"forall(a,b,c,d:points, bet(d,b,a) and bet(d,a,c) implies bet(d,b,c))"
(theory geometry-4)
(proof
(
(apply-macete-with-minor-premises symmetry-of-betweeness)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises nesting)
auto-instantiate-existential
)))
(def-theorem nesting-2
"forall(a,b,c,d:points, not b=d and bet(a,b,c) and bet(a,c,d) implies bet(b,c,d))"
(theory geometry-4)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "bet(d,c,b) or bet(b,c,a)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises a-point-separates-a-line-or)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises symmetry-of-betweeness)
(collinear-killer "c")
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2)")
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p);")
(apply-macete-with-minor-premises symmetry-of-betweeness)
(block
(script-comment "`antecedent-inference' at (1)")
(contrapose "with(a,c,b:points,bet(b,c,a));")
(apply-macete-with-minor-premises anti-cyclic)
(apply-macete-with-minor-premises symmetry-of-betweeness)))
)))
(def-theorem extending
"forall(a,b,c,d:points, not a=d and bet(a,b,c) and
bet(b,c,d) implies bet(a,c,d))"
(theory geometry-4)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not a=c")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises distinctness-1-3)
auto-instantiate-existential)
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "bet(b,c,a) or bet(a,c,d)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises a-point-separates-a-line-or)
simplify
(collinear-killer "c"))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p);")
(contrapose "with(a,c,b:points,bet(b,c,a));")
(apply-macete-with-minor-premises anti-cyclic)
(apply-macete-with-minor-premises symmetry-of-betweeness)))
)))
(def-theorem other-extending
"forall(a,b,c,d:points, not a=d and bet(a,b,c) and
bet(b,c,d) implies bet(a,b,d))"
(theory geometry-4)
(proof
(
(apply-macete-with-minor-premises symmetry-of-betweeness)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises extending)
auto-instantiate-existential
simplify
)))
(def-theorem f_card_difference
Remark: This entry is multiply defined. See: [1] [2]
f_card_difference
(theory generic-theory-1)
(usages transportable-macete)
(proof existing-theorem))
(def-theorem empty-segment-lemma
"forall(p:points, s:sets[points], f_indic_q{s} and nonempty_indic_q{s}
implies
forsome(x:points, x in s and
forall(y:points, y in s implies not(bet(p,y,x)))))"
(theory geometry-4)
(proof
(
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "1<=n")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(backchain-backwards "with(n:nn,n=n);")
(cut-with-single-formula "0<=f_card{s} and not(f_card{s}=0)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%empty-indic-has-f-card-zero)
simplify
(contrapose "with(x:points,s:sets[points],x in s);")
(backchain "with(f,s:sets[points],s=f);")
(weaken (0 1))
simplify))
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "forall(n:zz, 1<=n implies forall(s:sets[points],
f_card{s}=n implies forsome(x:points,
x in s
and
forall(y:points,y in s implies not(bet(p,y,x))))))")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(weaken (0 1 2))
(induction trivial-integer-inductor ("n"))
(block
(script-comment "`induction' at (0 0)")
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%singleton-has-f-card-one)
direct-and-antecedent-inference-strategy
(instantiate-existential ("y"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(backchain "with(p:prop,p);")
(apply-macete-with-minor-premises tr%singleton-equality-conversion))
(block
(script-comment "`instantiate-existential' at (0 1 0 0)")
(cut-with-single-formula "y=y_$0")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(y_$0:points,s:sets[points],y_$0 in s);")
(backchain "with(f,s:sets[points],s=f);")
(apply-macete-with-minor-premises tr%singleton-equality-conversion)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(y_$0,y:points,y=y_$0);")
(force-substitution "y=y_$0" "y_$0=y" (0))
(move-to-sibling 1)
simplify
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential))))
(block
(script-comment "`induction' at (0 1 0 0 0 0 0 0)")
(cut-with-single-formula "forsome(x:points, x in s)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%rev%positive-f-card-iff-nonempty)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(s:sets[points],nonempty_indic_q{s});")
(instantiate-universal-antecedent "with(p:prop,forall(s:sets[points],p));"
("s diff singleton{x}"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises tr%f_card_difference)
(move-to-sibling 1)
simplify-insistently
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises tr%singleton-has-f-card-one-rewrite)
simplify))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1 0 0)")
(incorporate-antecedent "with(p:prop,forall(y_$1:points,p));")
(apply-macete-with-minor-premises indicator-facts-macete)
simplify
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(x_$4:points,f,s:sets[points],x_$4 in s diff f);")
(apply-macete-with-minor-premises indicator-facts-macete)
simplify
direct-and-antecedent-inference-strategy
(case-split ("bet(p,x,x_$4)"))
(move-to-sibling 2)
(block
(script-comment "`case-split' at (2)")
(instantiate-existential ("x_$4"))
simplify
(case-split ("y=x"))
simplify
simplify)
(block
(script-comment "`case-split' at (1)")
(instantiate-existential ("x"))
(case-split ("y=x"))
(block
(script-comment "`case-split' at (1)")
(contrapose "with(x,y:points,y=x);")
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential)
(block
(script-comment "`case-split' at (2)")
(contrapose "with(p:prop,forall(y_$1:points,p));")
(instantiate-existential ("y"))
(apply-macete-with-minor-premises other-nesting)
auto-instantiate-existential)))))))
)))
(def-theory geometry-5
(component-theories geometry-4)
(axioms
(weak-pasch
"forall(a,b,c,d,e:points,
not coll(a,b,c) and
not a=b and
bet(b,c,d) and
bet(a,e,c)
implies
forsome(f:points, f in le(d,e) and bet(a,f,b)))")))
(def-theorem weak-pasch-ordered-lemma
"forall(d,c,e,b,f,a:points,
bet(a,f,b)
and
bet(a,e,c)
and
bet(b,c,d)
and
not(coll(a,b,c))
implies
not(bet(d,f,e)))"
(theory geometry-5)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not a=c and not b=c and not b=d and not c=d and not b=f and not f=a and not b=a and not a=f and not e=c")
(move-to-sibling 1)
inequality-killer
(cut-with-single-formula "not coll(d,e,c)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-collinear-2)
(instantiate-existential ("a" "b"))
simplify
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(contrapose "with(c,b,a:points,not(coll(a,b,c)));")
(apply-macete-with-minor-premises collinear-flipper-1-3))
(block
(script-comment "`instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`instantiate-existential' at (0 5)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify))
(contrapose "with(c,b,a:points,not(coll(a,b,c)));")
(cut-with-single-formula "forsome(x:points, x in le(a,f) and bet(d,x,c))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises weak-pasch)
auto-instantiate-existential
(block
(script-comment "`auto-instantiate-existential' at (0 0)")
(contrapose "with(c,e,d:points,not(coll(d,e,c)));")
(apply-macete-with-minor-premises collinear-flipper-2-3))
simplify
(apply-macete-with-minor-premises symmetry-of-betweeness))
(antecedent-inference "with(p:prop,forsome(x:points,p));")
(cut-with-single-formula "x in le(b,c) inters le(b,a)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(unfold-single-defined-constant-globally le)
simplify
direct-and-antecedent-inference-strategy
(collinear-killer "d")
(move-to-sibling 2)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 2)")
(cut-with-single-formula "le(a,b)=le(a,f)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises le-equality-condition)
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p and p);")
(incorporate-antecedent "with(x:points,f:sets[points],x in f);")
(backchain-backwards "with(f:sets[points],f=f);")
(unfold-single-defined-constant (0) le)
simplify
(apply-macete-with-minor-premises collinear-all-cases)
direct-and-antecedent-inference-strategy))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 1)")
(contrapose "with(c,x:points,x=c);")
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential))
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(c,e,d:points,not(coll(d,e,c)));")
(cut-with-single-formula "le(b,c) inters le(b,a)=singleton{b}")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises intersection-of-les-with-common-first-point)
(apply-macete-with-minor-premises collinear-flipper-1-3))
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(x:points,f:sets[points],x in f);")
(backchain "with(f:sets[points],f=f);")
simplify-insistently
direct-and-antecedent-inference-strategy
(antecedent-inference "with(p:prop,p and p);")
(contrapose "with(c,x,d:points,bet(d,x,c));")
(backchain "with(b,x:points,x=b);")
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises anti-cyclic))))))
(def-theorem weak-pasch-ordered
"forall(a,b,c,d,e,f:points,
not coll(a,b,c) and
bet(b,c,d) and
bet(a,e,c) and
f in le(d,e) and
bet(a,f,b)
implies
bet(d,e,f))"
(theory geometry-5)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not a=c and not b=c and not b=d and not c=d and not b=f and not f=a and not b=a and not a=f and not a=e")
(move-to-sibling 1)
inequality-killer
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(f:points,f) in with(f:sets[points],f);")
(unfold-single-defined-constant-globally le)
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(contrapose "with(d,f:points,f=d);")
(weaken (0))
(cut-with-single-formula " le(b,a) inters le(b,c)=singleton{b}")
(move-to-sibling 1)
(apply-macete-with-minor-premises intersection-of-les-with-common-first-point)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(f:sets[points],f=f);")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(b:points,f:sets[points],
f inters f subseteq singleton{b});")
unfold-defined-constants
simplify-insistently
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(b:points,p:prop,
forall(x_$2:points,p and p implies x_$2=b));"
("d"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0 0 0)")
(contrapose "with(d,a,b:points,not(coll(b,a,d)));")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0 1 0)")
(contrapose "with(d,c,b:points,not(coll(b,c,d)));")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1)")
(contrapose "with(e,f:points,f=e);")
(weaken (0))
(cut-with-single-formula " le(a,b) inters le(a,c)=singleton{a}")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises intersection-of-les-with-common-first-point)
(contrapose "with(c,b,a:points,not(coll(a,b,c)));")
(apply-macete-with-minor-premises collinear-flipper-1-2))
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(f:sets[points],f=f);")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(a:points,f:sets[points],
f inters f subseteq singleton{a});")
unfold-defined-constants
simplify-insistently
direct-and-antecedent-inference-strategy
(auto-instantiate-universal-antecedent "with(c,b,a:points,
forall(x_$2:points,
(x_$2=a or x_$2=b or coll(a,b,x_$2))
and
(x_$2=a or x_$2=c or coll(a,c,x_$2))
implies
x_$2=a));")
(block
(script-comment "`auto-instantiate-universal-antecedent' at (0 0 0 0 0)")
(contrapose "with(f,b,a:points,not(coll(a,b,f)));")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`auto-instantiate-universal-antecedent' at (0 0 0 1 0)")
(contrapose "with(f,c,a:points,not(coll(a,c,f)));")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2)")
(incorporate-antecedent "with(f,e,d:points,coll(d,e,f));")
(unfold-single-defined-constant (0) coll)
direct-and-antecedent-inference-strategy
(move-to-sibling 2)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 2)")
(contrapose "with(e,f,d:points,bet(d,f,e));")
(apply-macete-with-minor-premises weak-pasch-ordered-lemma)
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
(cut-with-single-formula "not coll(f,e,a)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-collinear-2)
(instantiate-existential ("c" "b"))
(block
(script-comment "`instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`instantiate-existential' at (0 5)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify))
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "forsome(x:points, x in le(b,d) and bet(e,x,a))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises weak-pasch)
(instantiate-existential ("f"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(contrapose "with(a,e,f:points,not(coll(f,e,a)));")
(apply-macete-with-minor-premises coll-disjunctive-permuter)
simplify)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(x:points,p));")
(cut-with-single-formula "x in le(c,a) inters le(c,b)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(unfold-single-defined-constant-globally le)
simplify
direct-and-antecedent-inference-strategy
(collinear-killer "e")
(move-to-sibling 2)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 2)")
(cut-with-single-formula "le(b,c)=le(b,d)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises le-equality-condition)
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p and p);")
(incorporate-antecedent "with(x:points,f:sets[points],x in f);")
(backchain-backwards "with(f:sets[points],f=f);")
(unfold-single-defined-constant (0)
le)
simplify
(apply-macete-with-minor-premises collinear-all-cases)
direct-and-antecedent-inference-strategy))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 1)")
(contrapose "with(a,x:points,x=a);")
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential))
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(a,e,f:points,not(coll(f,e,a)));")
(cut-with-single-formula "le(c,a) inters le(c,b)=singleton{c}")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises intersection-of-les-with-common-first-point)
(apply-macete-with-minor-premises collinear-flipper-2-3))
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(x:points,f:sets[points],x in f);")
(backchain "with(f:sets[points],f=f);")
simplify-insistently
direct-and-antecedent-inference-strategy
(antecedent-inference "with(p:prop,p and p);")
(contrapose "with(a,x,e:points,bet(e,x,a));")
(backchain "with(c,x:points,x=c);")
(apply-macete-with-minor-premises anti-cyclic)
(apply-macete-with-minor-premises symmetry-of-betweeness))))))))
)))
(def-theorem weak-pasch-other
"forall(a,b,c,d,f:points,
not coll(a,b,c) and
not a=c and
bet(b,c,d) and
bet(a,f,b)
implies
forsome(e:points, coll(d,e,f) and bet(a,e,c)))"
(theory geometry-5)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not b=c and not b=d and not c=d and not b=f and not f=a and not b=a and not a=f")
(move-to-sibling 1)
inequality-killer
(cut-with-single-formula "not d=f")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises inequality-2)
(instantiate-existential ("a" "c" "b"))
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
(prove-by-logic-and-simplification 3))
(block
(script-comment "`instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`instantiate-existential' at (0 5)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify))
(cut-with-single-formula "not d=a")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-equality-1)
(instantiate-existential ("b" "c"))
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(block
(script-comment "`instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises coll-disjunctive-permuter)
simplify))
(cut-with-single-formula "not coll(d,c,a)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-collinear)
auto-instantiate-existential)
(cut-with-single-formula "forsome(h:points,bet(h,b,f))")
(move-to-sibling 1)
(apply-macete-with-minor-premises existence-left)
(antecedent-inference "with(p:prop,forsome(h:points,p));")
(cut-with-single-formula "not coll(f,d,b)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-collinear-2)
(instantiate-existential ("c" "a"))
(apply-macete-with-minor-premises collinear-flipper-1-2))
(cut-with-single-formula " forsome(r:points, r in le(h,c) and bet(d,r,f))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises weak-pasch)
(instantiate-existential ("b"))
(apply-macete-with-minor-premises collinear-flipper-1-2)
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises symmetry-of-betweeness))
(antecedent-inference "with(p:prop,forsome(r:points,p));")
(cut-with-single-formula "bet(h,c,r)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises weak-pasch-ordered)
(instantiate-existential ("b" "f" "d")))
(cut-with-single-formula "bet(a,f,h)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises other-extending)
(instantiate-existential ("b"))
(contrapose "with(b,f,a:points,bet(a,f,b));")
(backchain "with(h,a:points,a=h);")
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises anti-cyclic)
(apply-macete-with-minor-premises symmetry-of-betweeness))
(cut-with-single-formula "not coll(f,d,a)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-collinear-2-other)
(instantiate-existential ("c" "b")))
(cut-with-single-formula "forsome(l:points, l in le(h,r) and bet(d,l,a))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises weak-pasch)
(instantiate-existential ("f"))
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(antecedent-inference "with(p:prop,forsome(l:points,p));")
(cut-with-single-formula "bet(h,r,l)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises weak-pasch-ordered)
(instantiate-existential ("f" "a" "d")))
(cut-with-single-formula "bet(c,r,l)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises nesting-2)
(instantiate-existential ("h"))
(force-substitution "c=l" "l=c" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises non-equality-1)
(instantiate-existential ("d" "a"))
simplify
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(block
(script-comment "`instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises collinear-flipper-1-2)
(move-to-ancestor 1)
(apply-macete-with-minor-premises collinear-all-cases)
simplify))
simplify)
(cut-with-single-formula "not coll(l,c,a)")
(move-to-sibling 1)
(apply-macete-with-minor-premises non-collinear)
(instantiate-existential ("d"))
(move-to-ancestor 4)
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "not coll(l,a,c)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises non-collinear)
auto-instantiate-existential
(block
(script-comment "`auto-instantiate-existential' at (0 3)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(block
(script-comment "`auto-instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify))
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "not l=c and not l=a")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential)
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "forsome(e:points,e in le(d,r) and bet(c,e,a))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises weak-pasch)
auto-instantiate-existential
(block
(script-comment "`auto-instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(apply-macete-with-minor-premises symmetry-of-betweeness))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(e:points,p));")
(cut-with-single-formula "le(d,r)=le(d,f)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises le-equality-condition)
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference-strategy (10 6 2 1))
(incorporate-antecedent "with(e,r,d:points,e in le(d,r));")
(backchain "with(f:sets[points],f=f);")
direct-and-antecedent-inference-strategy
(instantiate-existential ("e"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(cut-with-single-formula "bet(d,e,f)")
(move-to-ancestor 1)
(cut-with-single-formula "not d=e")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises inequality-2)
(instantiate-existential ("a" "b"
"c"))
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(e,f,d:points,e in le(d,f));")
(unfold-single-defined-constant (0)
le)
(cut-with-single-formula "not d=f")
simplify
(cut-with-single-formula "not e=f")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises inequality-2)
(instantiate-existential ("b" "c"
"a"))
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(block
(script-comment "`instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`instantiate-existential' at (0 5)")
(apply-macete-with-minor-premises collinear-all-cases)
simplify))
(block
(script-comment "`cut-with-single-formula' at (0)")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises coll-disjunctive-permuter)
simplify)))
(apply-macete-with-minor-premises symmetry-of-betweeness))))))
)))
"we next show that a line can intersect at most two sides of a triangle."
(def-theorem line-intersects-at-most-two-sides-of-a-triangle-lemma-1
"forall(a,b,c,x,y,z:points,
not(coll(a,b,c)) and bet(a,x,b) and bet(b,y,c) and bet(c,z,a) implies not(x=y))"
(theory geometry-2)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(b,x,a:points,bet(a,x,b));")
(backchain "with(y,x:points,x=y);")
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises switching)
(instantiate-existential ("y"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises distinctness-1-3)
auto-instantiate-existential)
(block
(script-comment "`instantiate-existential' at (0 1)")
(apply-macete-with-minor-premises collinear-flipper-2-3)
(apply-macete-with-minor-premises switching)
(instantiate-existential ("b"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises distinctness-1-3)
auto-instantiate-existential
(instantiate-existential ("b"))
(move-to-ancestor 1)
(instantiate-existential ("z")))
(block
(script-comment "`instantiate-existential' at (0 1)")
(apply-macete-with-minor-premises collinear-all-cases)
direct-and-antecedent-inference-strategy)
(block
(script-comment "`instantiate-existential' at (0 2)")
(apply-macete-with-minor-premises collinear-all-cases)
direct-and-antecedent-inference-strategy))
(block
(script-comment "`instantiate-existential' at (0 2)")
(apply-macete-with-minor-premises collinear-all-cases)
direct-and-antecedent-inference-strategy)
)))