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