(def-theorem sylvester-lemma-1
"forall(s:sets[points],
f_indic_q{s} and not(coll_set(s))
implies
forsome(a,b,c,p:points,
coll(a,b,c)
and
a in s
and
b in s
and
p in s
and
not(c in on%connecting%line%through(s,p))))"
(theory geometry-4)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(p));")
(unfold-single-defined-constant (0) coll_set)
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,forall(a,b,c,p:points,with(p:prop,p)));")
(cut-with-single-formula "forsome(c:points, c in le(x,y) and not c in on%connecting%line%through(s,z) inters le(x,y))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises lines-are-infinite)
(apply-macete-with-minor-premises finitely-many-on%connecting%line%through)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally le)
simplify)
(block
(script-comment "`apply-macete-with-minor-premises' at (0 1)")
(apply-macete-with-minor-premises lines-defining-axiom_geometry-2)
(apply-macete-with-minor-premises le-is-a-line)))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference-strategy (0))
(instantiate-existential ("x" "y" "c" "z"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(incorporate-antecedent "with(c,y,x:points,c in le(x,y));")
(unfold-single-defined-constant (0) le)
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
(contrapose "with(c:points,f:sets[points],not(c in f));")
(backchain "with(x,c:points,c=x);")
(weaken (1))
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(unfold-single-defined-constant (0)
on%connecting%line%through)
(unfold-single-defined-constant (0)
connecting%lines%through)
simplify-insistently
(instantiate-existential ("le(x,z)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(unfold-single-defined-constant (0) le)
simplify)
(block
(script-comment "`instantiate-existential' at (0 1)")
(unfold-single-defined-constant (0) le)
simplify)
(block
(script-comment "`instantiate-existential' at (0 2)")
(apply-macete-with-minor-premises les-are-connecting-lines)
direct-and-antecedent-inference-strategy))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(unfold-single-defined-constant (0) le)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
(contrapose "with(c:points,f:sets[points],not(c in f));")
(backchain "with(y,c:points,c=y);")
(weaken (1))
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(unfold-single-defined-constant (0)
on%connecting%line%through)
(unfold-single-defined-constant (0)
connecting%lines%through)
simplify-insistently
(instantiate-existential ("le(y,z)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(unfold-single-defined-constant (0) le)
simplify)
(block
(script-comment "`instantiate-existential' at (0 1)")
(unfold-single-defined-constant (0) le)
simplify)
(block
(script-comment "`instantiate-existential' at (0 2)")
(apply-macete-with-minor-premises les-are-connecting-lines)
direct-and-antecedent-inference-strategy))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(unfold-single-defined-constant (0) le)
simplify)))
(block
(script-comment "`instantiate-existential' at (0 4)")
(contrapose "with(c:points,f:sets[points],not(c in f));")
simplify-insistently))
))
)
(def-theorem sylvester-lemma-2
"forall(s:sets[points], a,b,c,p:points,
f_indic_q{s} and
coll(a,b,c)
and
a in s
and
b in s
and
p in s
and
not(c in on%connecting%line%through(s,p))
implies
not a=b and not a = p and not a=c and not b=p and not b=c and not p=c
and not c in s)"
(theory geometry-4)
(proof
(
(unfold-single-defined-constant-globally on%connecting%line%through)
(unfold-single-defined-constant-globally connecting%lines%through)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0)")
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
(instantiate-existential ("c")))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0)")
(contrapose "with(p:prop,not(forsome(l:sets[points],p)));")
(backchain-backwards "with(p,a:points,a=p);")
(instantiate-existential ("le(a,b)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(unfold-single-defined-constant-globally le)
simplify)
(block
(script-comment "`instantiate-existential' at (0 1 0)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises le-is-symmetric))
(block
(script-comment "`instantiate-existential' at (0 1 1)")
(apply-macete-with-minor-premises les-are-connecting-lines)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 0)")
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
(instantiate-existential ("b"))
(apply-macete-with-minor-premises collinear-flipper-2-3))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 3 0)")
(contrapose "with(p:prop,not(forsome(l:sets[points],p)));")
(backchain-backwards "with(p,b:points,b=p);")
(instantiate-existential ("le(a,b)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(unfold-single-defined-constant-globally le)
simplify)
(block
(script-comment "`instantiate-existential' at (0 1 0)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises le-is-symmetric))
(block
(script-comment "`instantiate-existential' at (0 1 1)")
(apply-macete-with-minor-premises les-are-connecting-lines)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 4 0)")
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
(instantiate-existential ("a"))
(apply-macete-with-minor-premises collinear-flipper-1-3)
(apply-macete-with-minor-premises collinear-flipper-2-3))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 5 0)")
(contrapose "with(p:prop,not(forsome(l:sets[points],p)));")
(backchain "with(c,p:points,p=c);")
(instantiate-existential ("le(a,b)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(unfold-single-defined-constant-globally le)
simplify)
(block
(script-comment "`instantiate-existential' at (0 1 1)")
(apply-macete-with-minor-premises les-are-connecting-lines)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 6 0)")
(contrapose "with(p:prop,not(forsome(l:sets[points],p)));")
(unfold-single-defined-constant (0) connecting%lines)
(instantiate-existential ("le(p,c)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises le-is-symmetric)
(apply-macete-with-minor-premises le-contains-left-point)
simplify)
(apply-macete-with-minor-premises le-contains-left-point)
(block
(script-comment "`instantiate-existential' at (0 1 1)")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce
(apply-macete-with-minor-premises le-is-a-line)
simplify
(apply-macete-with-minor-premises tr%cardinality-at-least-2)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(instantiate-existential ("p" "c"))
simplify
simplify)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
(instantiate-existential ("s"))
simplify
simplify-insistently)))
)))
(def-theorem sylvester-lemma-3
"forall(s:sets[points],
f_indic_q{s} and not(coll_set(s))
implies
forsome(a,b,p,c:points,
a in s and
b in s and
p in s and
le(p,c) inters s =singleton{p} and
forall(x:points, bet(p,x,c) implies not x in on%connecting%line(s))
and
nonempty_indic_q{le(p,c) inters le(a,b)} and
c in on%connecting%line(s) and not p=c and not c in s))"
(theory geometry-4)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula
"forsome(a,b,c,p:points,
coll(a,b,c)
and
a in s
and
b in s
and
p in s
and
not(c in on%connecting%line%through(s,p)))"
)
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises sylvester-lemma-1)
direct-and-antecedent-inference-strategy
)
(antecedent-inference "with(p:prop,forsome(a,b,c,p:points,with(p:prop,p)));")
(cut-with-single-formula
" not a=b and not a=p and not a=c and not b=p and not b=c and not p=c and not c in s"
)
(antecedent-inference "with(p:prop,p and p and p and p and p and p and p);")
(move-to-ancestor 2)
(move-to-descendent (1))
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises sylvester-lemma-2) simplify
)
(weaken (0))
(cut-with-single-formula
"forsome(x:points,
x in on%connecting%line(s) inters le(p,c) diff singleton{p}
and
forall(y:points, y in on%connecting%line(s) inters le(p,c) diff singleton{p} implies not(bet(p,y,x))))"
)
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises empty-segment-lemma)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
(instantiate-existential ("on%connecting%line(s) inters le(p,c)")) simplify-insistently
(block
(script-comment "`instantiate-existential' at (0 1)")
(apply-macete-with-minor-premises finitely-many-on%connecting%line)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(antecedent-inference "with(p:prop,p and p and p and p and p);")
(contrapose "with(c:points,f:sets[points],not(c in f));")
(unfold-single-defined-constant-globally on%connecting%line%through)
(unfold-single-defined-constant-globally connecting%lines%through)
(apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly
(instantiate-existential ("le(p,c)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises le-is-symmetric)
)
(apply-macete-with-minor-premises le-contains-point)
)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises lines-defining-axiom_geometry-2)
(apply-macete-with-minor-premises le-is-a-line)
) ) )
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(instantiate-existential ("c")) simplify-insistently
(unfold-single-defined-constant (0) on%connecting%line)
(apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(instantiate-existential ("le(a,b)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises les-are-connecting-lines) simplify
)
(block
(script-comment "`instantiate-existential' at (0 1)")
(unfold-single-defined-constant-globally le) simplify
) )
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 0)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises definedness-of-le) simplify
) ) )
(antecedent-inference-strategy (0))
(instantiate-existential ("a" "b" "p" "x"))
(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 (antecedent-inference "with(p:prop,p and p and p and p and p);")
(contrapose "with(c:points,f:sets[points],not(c in f));")
(incorporate-antecedent "with(x:points,f:sets[points],x in f diff f);") simplify-insistently
(unfold-single-defined-constant-globally le) simplify simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 1)")
(unfold-single-defined-constant-globally on%connecting%line%through)
(unfold-single-defined-constant-globally connecting%lines%through)
(unfold-single-defined-constant-globally connecting%lines)
(apply-macete-with-minor-premises tr%cardinality-at-least-2)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly
(instantiate-existential ("le(x_$2,p)"))
(block
(script-comment "`instantiate-existential' at (0 0 0)")
(antecedent-inference "with(p:prop,p and p and p);")
(incorporate-antecedent "with(x_$2,x,p:points,x_$2 in le(p,x));")
(unfold-single-defined-constant-globally le) simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises coll-disjunctive-permuter) simplify
)
(block
(script-comment "`instantiate-existential' at (0 0 1 0)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises definedness-of-le) simplify
)
(apply-macete-with-minor-premises le-is-a-line)
(block
(script-comment "`instantiate-existential' at (0 0 1 1 1)")
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
(instantiate-existential ("s")) simplify-insistently
(instantiate-existential ("x_$2" "p"))
(apply-macete-with-minor-premises le-contains-point)
) )
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(weaken (5 4 3 2 1 0 12 11 10 9 8 7 6))
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
(instantiate-existential ("s")) simplify-insistently
) )
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 2)")
(unfold-single-defined-constant-globally on%connecting%line%through)
(unfold-single-defined-constant-globally connecting%lines%through)
(unfold-single-defined-constant-globally connecting%lines)
(apply-macete-with-minor-premises tr%cardinality-at-least-2)
(apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly
(instantiate-existential ("le(p,x)"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(unfold-single-defined-constant-globally le) simplify
direct-and-antecedent-inference-strategy direct-and-antecedent-inference-strategy
direct-and-antecedent-inference-strategy simplify
(apply-macete-with-minor-premises coll-disjunctive-permuter) simplify
)
(block
(script-comment "`instantiate-existential' at (0 1 0)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises definedness-of-le)
)
(apply-macete-with-minor-premises le-is-a-line) (instantiate-existential ("x_$2" "p"))
) )
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain-backwards "with(p,x_$1:points,x_$1=p);")
(move-to-ancestor 1)
(backchain "with(p,x_$1:points,x_$1=p);")
(apply-macete-with-minor-premises le-contains-left-point)
(apply-macete-with-minor-premises definedness-of-le)
(move-to-ancestor 1)
simplify
(move-to-ancestor 1)
(weaken (15 2 0 14 13 12 10 11 9 8 7 6 5 4 3))
simplify
(incorporate-antecedent "with(p:prop,p);")
simplify-insistently
direct-and-antecedent-inference-strategy
(move-to-ancestor 1)
direct-and-antecedent-inference-strategy
(move-to-ancestor 4)
(move-to-descendent ((2 . 0)))
(block
(script-comment "`apply-macete-with-minor-premises' at ((2 . 0))")
(contrapose "with(x:points,f:sets[points],x in f diff f);")
(backchain-backwards "with(x,p:points,p=x);") simplify-insistently
)
(block
(script-comment "`instantiate-existential' at (0 4 0 0)")
(instantiate-universal-antecedent "with(p:prop,forall(y:points,p));" ("x_$3"))
(contrapose "with(x_$3:points,f:sets[points],not(x_$3 in f));") simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(cut-with-single-formula "le(p,c)=le(p,x)") (move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises two-points-determine-a-line)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises le-is-a-line) (instantiate-existential ("p" "x"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises distinctness-1-3)
(instantiate-existential ("x_$3"))
(apply-macete-with-minor-premises symmetry-of-betweeness)
)
simplify
(block
(script-comment "`instantiate-existential' at (0 3)")
(incorporate-antecedent "with(x:points,f:sets[points],x in f diff f);")
simplify-insistently
)
(block
(script-comment "`instantiate-existential' at (0 4)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises le-is-symmetric)
)
(block
(script-comment "`instantiate-existential' at (0 5)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises definedness-of-le)
)
(block
(script-comment "`instantiate-existential' at (0 6)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises definedness-of-le)
) )
(apply-macete-with-minor-premises definedness-of-le)
)
(block
(script-comment "`cut-with-single-formula' at (0)")
(backchain "with(x,c,p:points,le(p,c)=le(p,x));")
(unfold-single-defined-constant-globally le) simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises collinear-all-cases) simplify
) )
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(force-substitution "x_$3=p" "p=x_$3" (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 "`instantiate-existential' at (0 5)") (instantiate-existential ("c"))
(unfold-single-defined-constant-globally le) simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(contrapose "with(f:sets[points],f=f);") (backchain "with(x,p:points,p=x);")
(unfold-single-defined-constant-globally le) simplify
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
(contrapose "with(x,p:points,p=x);") (antecedent-inference "with(p:prop,p and p);")
(contrapose
"with(s,f:sets[points],p:points,
singleton{p} subseteq f inters s);"
)
(instantiate-existential ("p")) simplify-insistently simplify-insistently
)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0)")
(incorporate-antecedent "with(x:points,f:sets[points],x in f diff f);")
simplify-insistently
(unfold-single-defined-constant-globally le) simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises coll-disjunctive-permuter) simplify
) )
(block
(script-comment "`instantiate-existential' at (0 6)")
(incorporate-antecedent "with(x:points,f:sets[points],x in f diff f);")
simplify-insistently
)
(incorporate-antecedent "with(f:sets[points],f=f);")
(weaken (6 9 8 7 7 5 4 3 2 1 0))
(weaken (6 5 4 3 2 1 0))
simplify-insistently
beta-reduce-insistently
beta-reduce-repeatedly
(move-to-ancestor 4)
(block
(script-comment "`instantiate-existential' at (0 7)")
(contrapose "with(f:sets[points],nonempty_indic_q{f});")
(backchain "with(x,p:points,p=x);")
(weaken (17 16 15 14 13 12 11 10 9 8 7 6 5 4 3 2 1 0))
simplify-insistently
simplify-insistently
(unfold-single-defined-constant-globally le)
)
(contrapose "with(f:sets[points],f=f);")
(move-to-ancestor 1)
(cut-with-single-formula "x in le(p,x) inters s")
(move-to-sibling 1)
(apply-macete-with-minor-premises le-is-symmetric)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce
simplify
(apply-macete-with-minor-premises le-contains-left-point)
simplify
(move-to-ancestor 6)
(block
(script-comment "`instantiate-existential' at (0 8)")
(contrapose "with(f:sets[points],f=f);") (cut-with-single-formula "x in le(p,x)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises definedness-of-le) simplify
)
(block
(script-comment "`cut-with-single-formula' at (0)") simplify extensionality
beta-reduce-repeatedly (instantiate-existential ("x")) simplify
) )
)))
(def-theorem sylvester-lemma-4
"forall(l:lines, x:points, s:sets[points], x in l and
3<=f_card{s inters l} and not x in s implies
forsome(x1,x2,x3:points,
x1 in s inters l and
x2 in s inters l and
x3 in s inters l and
bet(x1,x2,x) and
(bet(x3,x1,x) or bet(x1,x,x3))))"
(theory geometry-5)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(a,b,c:points, a in s inters l and b in s inters l and c in s inters l and not(a=b) and not(a=c) and not(b=c))")
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%cardinality-at-least-3-lemma)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference-strategy (0))
(cut-with-single-formula "line(l)")
(move-to-sibling 1)
(apply-macete-with-minor-premises lines-in-quasi-sort_geometry-2)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(l:lines,line(l));")
(unfold-single-defined-constant-globally line)
(unfold-single-defined-constant-globally coll_set)
direct-and-antecedent-inference-strategy
(weaken (0))
(cut-with-single-formula "coll(a,b,x) and coll(a,c,x) and coll(b,c,x)")
(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)")
(backchain "with(p:prop,forall(x,y,z:points,p));")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(incorporate-antecedent "with(a:points,l:lines,s:sets[points],a in s inters l);")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(incorporate-antecedent "with(b:points,l:lines,s:sets[points],b in s inters l);")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (4)")
(contrapose "with(x:points,s:sets[points],not(x in s));")
(incorporate-antecedent "with(a:points,l:lines,s:sets[points],a in s inters l);")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (5)")
(contrapose "with(x:points,s:sets[points],not(x in s));")
(incorporate-antecedent "with(b:points,l:lines,s:sets[points],b in s inters l);")
simplify-insistently))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(backchain "with(p:prop,forall(x,y,z:points,p));")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(incorporate-antecedent "with(c:points,l:lines,s:sets[points],c in s inters l);")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (5)")
(contrapose "with(x:points,s:sets[points],not(x in s));")
(incorporate-antecedent "with(c:points,l:lines,s:sets[points],c in s inters l);")
simplify-insistently))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2)")
(backchain "with(p:prop,forall(x,y,z:points,p));")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(incorporate-antecedent "with(c:points,l:lines,s:sets[points],c in s inters l);")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (5)")
(contrapose "with(x:points,s:sets[points],not(x in s));")
(incorporate-antecedent "with(c:points,l:lines,s:sets[points],c in s inters l);")
simplify-insistently)))
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(p:prop,p and p and p);")
(unfold-single-defined-constant-globally coll)
direct-and-antecedent-inference-strategy
(instantiate-existential ("b" "c" "a"))
(instantiate-existential ("b" "c" "a"))
(instantiate-existential ("b" "c" "a"))
(instantiate-existential ("a" "c" "b"))
(instantiate-existential ("c" "a" "b"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 1 2)")
(instantiate-existential ("b" "a" "c"))
(apply-macete-with-minor-premises extending)
(instantiate-existential ("a")))
(instantiate-existential ("a" "c" "b"))
(instantiate-existential ("c" "a" "b"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 2 2)")
(instantiate-existential ("b" "c" "a"))
(apply-macete-with-minor-premises extending)
(instantiate-existential ("c"))
simplify
(apply-macete-with-minor-premises symmetry-of-betweeness))
(instantiate-existential ("c" "b" "a"))
(instantiate-existential ("a" "b" "c"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 2)")
(instantiate-existential ("c" "b" "a"))
(apply-macete-with-minor-premises symmetry-of-betweeness))
(instantiate-existential ("c" "b" "a"))
(instantiate-existential ("b" "a" "c"))
(instantiate-existential ("b" "a" "c"))
(instantiate-existential ("c" "b" "a"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 2 1)")
(instantiate-existential ("c" "a" "b"))
(apply-macete-with-minor-premises extending)
(instantiate-existential ("a"))
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 2 2)")
(instantiate-existential ("c" "b" "a"))
(apply-macete-with-minor-premises symmetry-of-betweeness))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 0 0)")
(instantiate-existential ("a" "b" "c"))
(apply-macete-with-minor-premises extending)
(instantiate-existential ("b")))
(instantiate-existential ("a" "b" "c"))
(instantiate-existential ("a" "b" "c"))
(instantiate-existential ("a" "c" "b"))
(instantiate-existential ("b" "a" "c"))
(instantiate-existential ("b" "a" "c"))
(instantiate-existential ("a" "c" "b"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 2 1)")
(instantiate-existential ("c" "a" "b"))
(apply-macete-with-minor-premises symmetry-of-betweeness))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 2 2)")
(cut-with-single-formula "coll(a,b,c)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(backchain "with(p:prop,forall(x,y,z:points,p));")
(incorporate-antecedent "with(c:points,l:lines,s:sets[points],c in s inters l);")
(incorporate-antecedent "with(a:points,l:lines,s:sets[points],a in s inters l);")
(incorporate-antecedent "with(b:points,l:lines,s:sets[points],b in s inters l);")
simplify-insistently)
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(c,b,a:points,coll(a,b,c));")
(unfold-single-defined-constant-globally coll)
(contrapose "with(p:prop,forall(x1,x2,x3:points,p or p or p or p or p));")
(antecedent-inference "with(p:prop,p or p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(cut-with-single-formula "bet(a,b,x)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises nesting-2)
(apply-macete-with-minor-premises symmetry-of-betweeness)
(instantiate-existential ("c"))
(force-substitution "x=a"
"a=x"
(0))
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(x,b,a:points,bet(a,b,x));")
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises anti-cyclic)
(apply-macete-with-minor-premises symmetry-of-betweeness)))
(block
(script-comment "`antecedent-inference' at (1)")
(cut-with-single-formula "bet(x,a,b)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises nesting-2)
(instantiate-existential ("c"))
(move-to-ancestor 2)
(apply-macete-with-minor-premises symmetry-of-betweeness)
(instantiate-existential ("c"))
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential)
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(b,a,x:points,bet(x,a,b));")
(apply-macete-with-minor-premises anti-cyclic)))
(block
(script-comment "`antecedent-inference' at (2)")
(cut-with-single-formula "bet(x,c,b)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises nesting-2)
(instantiate-existential ("a"))
(apply-macete-with-minor-premises distinctness-2-3)
auto-instantiate-existential)
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(c,x,b:points,bet(b,x,c));")
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises anti-cyclic)))))))))))
(def-theorem connecting-line-sufficient-condition
"forall(s:sets[points],x:points,
f_indic_q{s} and
forsome(a,b:points, a in s and b in s and x in le(a,b))
implies
x in on%connecting%line(s))"
(theory geometry-4)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally on%connecting%line)
(unfold-single-defined-constant-globally connecting%lines)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
auto-instantiate-existential
(block
(script-comment "`auto-instantiate-existential' at (0 0 0)")
(apply-macete-with-minor-premises le-is-a-line)
(cut-with-single-formula "#(le(a,b))")
(incorporate-antecedent "with(f:sets[points],#(f));")
(unfold-single-defined-constant-globally le)
simplify)
(block
(script-comment "`auto-instantiate-existential' at (0 0 1)")
(apply-macete-with-minor-premises tr%cardinality-at-least-2)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(instantiate-existential ("a" "b"))
(block
(script-comment "`instantiate-existential' at (0 0)")
simplify-insistently
(apply-macete-with-minor-premises le-contains-left-point))
(block
(script-comment "`instantiate-existential' at (0 1)")
simplify-insistently
(apply-macete-with-minor-premises le-contains-point)
(apply-macete-with-minor-premises le-is-symmetric)))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
auto-instantiate-existential
simplify-insistently))
)))
(def-theorem sylvester
"forall(s:sets[points], f_indic_q{s} and not coll_set(s)
implies
forsome(l:lines, f_card{s inters l}=2))"
(theory geometry-5)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem sylvester-lemma-3 ("s"))
(incorporate-antecedent "with(c:points,s:sets[points],c in on%connecting%line(s));")
(unfold-single-defined-constant (0) on%connecting%line)
(unfold-single-defined-constant (0) connecting%lines)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(case-split ("2=f_card{s inters l}"))
(block
(script-comment "`case-split' at (1)")
(instantiate-existential ("l"))
simplify)
(cut-with-single-formula "3<=f_card{s inters l}")
(move-to-sibling 1)
simplify
(weaken (1 2))
(instantiate-theorem sylvester-lemma-4 ("l" "c" "s"))
(move-to-ancestor 1)
(cut-with-single-formula "not x1=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)
(cut-with-single-formula "not x1=p and not coll(x1,c,p)")
(move-to-sibling 1)
(incorporate-antecedent "with(f:sets[points],f=f);")
simplify-insistently
(move-to-ancestor 1)
(apply-macete-with-minor-premises tr%singletons-have-a-unique-member)
(apply-macete-with-minor-premises eliminate-iota-macete)
(unfold-single-defined-constant (1) le)
simplify
direct-and-antecedent-inference-strategy
(contrapose "forall(b_$0:points,
with(p:prop,p and p) implies with(p:points,b_$0=p));")
(backchain-backwards "with(p,x1:points,x1=p);")
(backchain-backwards "with(p,x1:points,x1=p);")
(instantiate-existential ("x2"))
(block
(script-comment "`instantiate-existential' at (0 0 0)")
(antecedent-inference "with(p:prop,p or p);")
(move-to-ancestor 1)
(apply-macete-with-minor-premises collinear-all-cases)
simplify)
(block
(script-comment "`instantiate-existential' at (0 1)")
simplify
(incorporate-antecedent "with(x2:points,l,s:sets[points],x2 in s inters l);")
simplify-insistently)
(backchain-backwards "with(p,x1:points,x1=p);")
(apply-macete-with-minor-premises distinctness-1-2)
(instantiate-existential ("c"))
(move-to-ancestor 2)
(block
(script-comment "`backchain-backwards' at (0)")
(force-substitution "x2=x1" "x1=x2" (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 "`direct-and-antecedent-inference-strategy' at (0 1 0)")
(apply-macete-with-minor-premises collinear-flipper-1-3)
(contrapose "forall(b_$0:points,
with(p:prop,p and p) implies with(p:points,b_$0=p));")
(instantiate-existential ("x1"))
(incorporate-antecedent "with(x1:points,l,s:sets[points],x1 in s inters l);")
simplify-insistently)
(instantiate-existential ("le(x1,p)"))
(move-to-sibling 1)
(block
(script-comment "`instantiate-existential' at (1)")
(apply-macete-with-minor-premises lines-defining-axiom_geometry-2)
(apply-macete-with-minor-premises le-is-a-line))
(contrapose "with(p:prop,forall(x:points,p));")
(cut-with-single-formula "3<=f_card{s inters le(x1,p)}")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(cut-with-single-formula "2<=f_card{s inters le(x1,p)}")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%cardinality-at-least-2)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(instantiate-existential ("x1" "p"))
(block
(script-comment "`instantiate-existential' at (0 0)")
simplify
(apply-macete-with-minor-premises le-contains-left-point)
(incorporate-antecedent "with(x1:points,l,s:sets[points],x1 in s inters l);")
simplify-insistently)
(block
(script-comment "`instantiate-existential' at (0 1)")
simplify
(apply-macete-with-minor-premises le-is-symmetric)
(apply-macete-with-minor-premises le-contains-left-point)
simplify))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
simplify
simplify-insistently
(move-to-ancestor 1)
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
auto-instantiate-existential
simplify
simplify-insistently)))
(cut-with-single-formula "forsome(q,y1,y2:points,q in s inters le(x1,p) and y1 in s inters le(x1,p) and y2 in s inters le(x1,p) and not q=y1 and not q=y2 and not y1=y2)")
(move-to-sibling 1)
(apply-macete-with-minor-premises tr%cardinality-at-least-3-lemma)
(cut-with-single-formula "forsome(z:points, z in s inters le(x1,p) and not z=p and not z=x1)")
(move-to-sibling 1)
(incorporate-antecedent "with(p:prop,forsome(q,y1,y2:points,p));")
simplify
(move-to-ancestor 1)
simplify-insistently
(move-to-ancestor 2)
(antecedent-inference "with(p:prop,forsome(q,y1,y2:points,p));")
(cut-with-single-formula "not q=p and not q=x1 or not y1=p and not y1=x1 or not y2=p and not y2=x1")
(move-to-sibling 1)
simplify
(incorporate-antecedent "with(p:prop,p and p and p and p and p and p);")
simplify
(move-to-ancestor 2)
(block
(script-comment "`cut-with-single-formula' at (1)")
(antecedent-inference "with(p:prop,p and p and p and p and p and p);")
simplify
(weaken (3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25))
(weaken (0))
simplify
(prove-by-logic-and-simplification 0))
(weaken (22 20 19 18 17 15 14 16 21 13 12 11 10 9 8 7 6 4 5 3 2))
(prove-by-logic-and-simplification 0)
(move-to-ancestor 4)
(prove-by-logic-and-simplification 3)
(move-to-ancestor 4)
(antecedent-inference "with(p:prop,p or p or p);")
(move-to-ancestor 4)
(antecedent-inference "with(p:prop,p or p or p);")
(move-to-ancestor 2)
(move-to-descendent (0))
auto-instantiate-existential
(move-to-ancestor 1)
(antecedent-inference-strategy (0))
(move-to-ancestor 5)
(move-to-descendent (0 (1 . 0)))
(instantiate-existential ("q"))
(instantiate-existential ("y1"))
(instantiate-existential ("y2"))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(z:points,p));")
(antecedent-inference "with(p:prop,p and p and p);")
(incorporate-antecedent "with(z,p,x1:points,s:sets[points],z in s inters le(x1,p));")
simplify
(apply-macete-with-minor-premises connecting-line-sufficient-condition)
(unfold-single-defined-constant (0) le)
simplify
(unfold-single-defined-constant (0) coll)
(force-substitution "forsome(x:points,
bet(p,x,c)
and
forsome(b,a:points,a in s and b in s and x in le(a,b)))"
"forsome (a,b:points,forsome(x:points,
a in s and b in s and x in le(a,b) and bet(p,x,c)))"
(0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
(weaken (0 1 2 3 4 5 6 7 8 9))
(weaken (0 1 2 3 4 5 6 7 8 9))
(weaken (0 1 2 3 4))
(prove-by-logic-and-simplification 3)
auto-instantiate-existential
auto-instantiate-existential)
(block
(script-comment "`force-substitution' at (0)")
direct-inference
(antecedent-inference "with(p:prop,z:points,s:sets[points],
z in s and (p or p or p));")
(antecedent-inference "with(p:prop,p or p or p);")
(move-to-sibling 1)
(block
(script-comment "`antecedent-inference' at (1)")
(instantiate-existential ("z" "x2"))
simplify
(incorporate-antecedent "with(x2:points,l,s:sets[points],x2 in s inters l);")
simplify
direct-inference
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises weak-pasch)
(instantiate-existential ("x1"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
simplify
(apply-macete-with-minor-premises symmetry-of-betweeness))
(block
(script-comment "`antecedent-inference' at (0)")
(instantiate-existential ("z" "x2"))
(force-substitution "x in le(z,x2)" "coll(z,x,x2)" (0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
(unfold-single-defined-constant (0) le)
(force-substitution "coll(z,x,x2)"
"coll(z,x2,x)"
(0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
direct-inference
(apply-macete-with-minor-premises collinear-flipper-2-3))
(block
(script-comment "`force-substitution' at (0)")
(weaken (0 1
2
3
4
5
6
7
8
9
10
11
12
13
14
15))
(weaken (0 1 2 3 4 5 6 7 8 9 10))
simplify
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
direct-inference
auto-instantiate-existential))
(block
(script-comment "`force-substitution' at (0)")
(incorporate-antecedent "with(x2:points,l,s:sets[points],x2 in s inters l);")
simplify
direct-inference
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises weak-pasch-other)
(instantiate-existential ("x1"))
(apply-macete-with-minor-premises collinear-flipper-1-2)
simplify
(apply-macete-with-minor-premises symmetry-of-betweeness)))
(block
(script-comment "`antecedent-inference' at (2)")
(antecedent-inference "with(p:prop,p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(instantiate-existential ("x3" "z"))
(incorporate-antecedent "with(x3:points,l,s:sets[points],x3 in s inters l);")
simplify
direct-inference
(apply-macete-with-minor-premises weak-pasch)
(instantiate-existential ("x1"))
(apply-macete-with-minor-premises collinear-flipper-1-3)
(apply-macete-with-minor-premises symmetry-of-betweeness)
(apply-macete-with-minor-premises symmetry-of-betweeness))
(block
(script-comment "`antecedent-inference' at (1)")
(instantiate-existential ("x3" "z"))
(force-substitution "x in le(x3,z)"
"coll(x3,x,z)"
(0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
(unfold-single-defined-constant (0) le)
(apply-macete-locally-with-minor-premises collinear-flipper-2-3
(0)
"coll(x3,x,z)")
simplify
(apply-macete-with-minor-premises collinear-implies-distinct-lemma)
direct-inference
auto-instantiate-existential)
(block
(script-comment "`force-substitution' at (0)")
(incorporate-antecedent "with(x3:points,l,s:sets[points],x3 in s inters l);")
simplify
direct-inference
(apply-macete-with-minor-premises weak-pasch-other)
(instantiate-existential ("x1"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises coll-conjunctive-permuter)
simplify)
(apply-macete-with-minor-premises symmetry-of-betweeness))))))
)))