```(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 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 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 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-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-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-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))
```