---

Step * of Lemma geo-orientation_wf

∀[g:EuclideanPlaneStructure]. ∀[a,b:Point]. ∀[c:{c:Point| a # bc} ].
  (geo-orientation(g;a;b;c) ∈ a leftof bc ∨ a leftof cb)
BY
{ (Auto THEN DSetVars THEN (Assert g ∈ EuclideanPlaneStructure BY Auto) THEN (D 1 THENA Auto) THEN ProveWfLemma) }

1
1. g : self:GeometryPrimitives
       "Bstable":∀[a,b,c:Point].  Stable{a_b_c}
       "Estable":∀[a,b,c,d:Point].  Stable{ab ≅ cd}
       "Ssquashstable":∀a,b:Point.  SqStable(a ≠ b)
       "Lsquashstable":∀a,b,c:Point.  SqStable(a leftof bc)
       "Lorsquashstable":∀a,b,c:Point.  SqStable(a leftof bc ∨ a leftof cb)
       "SepOr":∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point.  (a ≠ c ∨ b ≠ c)
       "nontrivial":∃a:Point. (∃b:{Point| a ≠ b})
       "SS":∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} .  (∃x:{Point| (Colinear(a;b;x) ∧ u_x_v)})
       "SC":∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point.  (∃x:{Point| (a_b_x ∧ bx ≅ bc)}) ⋂ x:Atom
       ⟶ if x =a "CC"
          then ∀a,b:Point. ∀c:{c:Point| a ≠ c} . ∀d:Point.
                 ∀[p:{p:Point| ab ≅ ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd ≅ cq ∧ ab ≥ aq} ].
                   ∃u:{u:Point| ab ≅ au ∧ cd ≅ cu} 
                    (∃v:{Point| ((ab ≅ av ∧ cd ≅ cv) ∧ ((ab > aq ∧ cd > cp) ⇒ (u leftof ac ∧ v leftof ca)))})
          else Top
          fi 
2. g ∈ GeometryPrimitives
3. a : Point
4. b : Point
5. c : Point
6. a # bc
7. g ∈ EuclideanPlaneStructure
8. g."Bstable" ∈ ∀[a,b,c:Point].  Stable{a_b_c}
9. g."Estable" ∈ ∀[a,b,c,d:Point].  Stable{ab ≅ cd}
10. g."Ssquashstable" ∈ ∀a,b:Point.  SqStable(a ≠ b)
11. g."Lsquashstable" ∈ ∀a,b,c:Point.  SqStable(a leftof bc)
12. g."Lorsquashstable" ∈ ∀a,b,c:Point.  SqStable(a leftof bc ∨ a leftof cb)
13. g."SepOr" ∈ ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point.  (a ≠ c ∨ b ≠ c)
14. g."nontrivial" ∈ ∃a:Point. (∃b:{Point| a ≠ b})
15. g."SS" ∈ ∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} .  (∃x:{Point| (Colinear(a;b;x) ∧ u_x_v)}\000C)
16. g."SC" ∈ ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point.  (∃x:{Point| (a_b_x ∧ bx ≅ bc)})
17. g."CC" ∈ ∀a,b:Point. ∀c:{c:Point| a ≠ c} . ∀d:Point.
               ∀[p:{p:Point| ab ≅ ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd ≅ cq ∧ ab ≥ aq} ].
                 ∃u:{u:Point| ab ≅ au ∧ cd ≅ cu} 
                  (∃v:{Point| ((ab ≅ av ∧ cd ≅ cv) ∧ ((ab > aq ∧ cd > cp) ⇒ (u leftof ac ∧ v leftof ca)))})
⊢ ⋅ ∈ ↓a leftof bc ∨ a leftof cb

---

Latex:

---

Latex:
\mforall{}[g:EuclideanPlaneStructure].  \mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  a  \#  bc\}  ].
    (geo-orientation(g;a;b;c)  \mmember{}  a  leftof  bc  \mvee{}  a  leftof  cb)


By

---

Latex:
(Auto
  THEN  DSetVars
  THEN  (Assert  g  \mmember{}  EuclideanPlaneStructure  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  ProveWfLemma)

---

Home Index