---

Step * 1 of Lemma mk-eu_wf


1. self : GeometryPrimitives
2. Sstab : ∀a,b,c,d:Point.  SqStable(ab>cd)
3. Lstab : ∀a,b,c:Point.  SqStable(a # bc)
4. Sepor : ∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point.  (a # c ∨ b # c)
5. nontriv : ∃a:Point. (∃b:Point [a # b])
6. SS : ∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} .  (∃x:Point [(Colinear(a;b;x) ∧ B(uxv))])
7. SC : ∀c,d,a:Point. ∀b:{b:Point| b # a ∧ B(cbd)} .  (∃u:Point [(cu ≅ cd ∧ B(abu) ∧ (b # d ⇒ b # u))])
8. CC : ∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:{d:Point| StrictOverlap(a;b;c;d)} .
          (∃u:Point [(ab ≅ au ∧ cd ≅ cu ∧ u leftof ac)])
⊢ self["Ssquashstable" := Sstab]["Lorsquashstable" := Lstab]["SepOr" := Sepor]["nontrivial" := nontriv]["SS" := SS]
  ["SS" := SS]["SC" := SC]["CC" := CC] ∈ GeometryPrimitives
BY
{ ((Assert self ∈ GeometryPrimitives BY
          Auto)
   THEN (D 1 THENA Auto)
   THEN Unfold `geo-primitives` 0
   THEN RepeatFor 2
   ((RecordPlusTypeCD THENL [ Id; (UnfoldGeoAbbreviations 0 THEN FoldGeoAbbreviations 0 THEN Trivial)]))) }

1
1. self : self:"Point":Type
          "O":Point ⟶ Point ⟶ Point ⟶ Point ⟶ ℙ ⋂ x:Atom ⟶ if x =a "L"
                                                                then Point ⟶ Point ⟶ Point ⟶ ℙ
                                                                else Top
                                                                fi 
2. self ∈ record(x.Top)
3. Sstab : ∀a,b,c,d:Point.  SqStable(ab>cd)
4. Lstab : ∀a,b,c:Point.  SqStable(a # bc)
5. Sepor : ∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point.  (a # c ∨ b # c)
6. nontriv : ∃a:Point. (∃b:Point [a # b])
7. SS : ∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} .  (∃x:Point [(Colinear(a;b;x) ∧ B(uxv))])
8. SC : ∀c,d,a:Point. ∀b:{b:Point| b # a ∧ B(cbd)} .  (∃u:Point [(cu ≅ cd ∧ B(abu) ∧ (b # d ⇒ b # u))])
9. CC : ∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:{d:Point| StrictOverlap(a;b;c;d)} .
          (∃u:Point [(ab ≅ au ∧ cd ≅ cu ∧ u leftof ac)])
10. self ∈ GeometryPrimitives
11. self."Point" ∈ Type
12. self."O" ∈ Point ⟶ Point ⟶ Point ⟶ Point ⟶ ℙ
13. self."L" ∈ Point ⟶ Point ⟶ Point ⟶ ℙ
⊢ self["Ssquashstable" := Sstab]["Lorsquashstable" := Lstab]["SepOr" := Sepor]["nontrivial" := nontriv]["SS" := SS]
  ["SS" := SS]["SC" := SC]["CC" := CC] ∈ "Point":Type

---

Latex:

---

Latex:

1.  self  :  GeometryPrimitives
2.  Sstab  :  \mforall{}a,b,c,d:Point.    SqStable(ab>cd)
3.  Lstab  :  \mforall{}a,b,c:Point.    SqStable(a  \#  bc)
4.  Sepor  :  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c:Point.    (a  \#  c  \mvee{}  b  \#  c)
5.  nontriv  :  \mexists{}a:Point.  (\mexists{}b:Point  [a  \#  b])
6.  SS  :  \mforall{}a,b:Point.  \mforall{}u:\{u:Point|  u  leftof  ab\}  .  \mforall{}v:\{v:Point|  v  leftof  ba\}  .
                    (\mexists{}x:Point  [(Colinear(a;b;x)  \mwedge{}  B(uxv))])
7.  SC  :  \mforall{}c,d,a:Point.  \mforall{}b:\{b:Point|  b  \#  a  \mwedge{}  B(cbd)\}  .
                    (\mexists{}u:Point  [(cu  \mcong{}  cd  \mwedge{}  B(abu)  \mwedge{}  (b  \#  d  {}\mRightarrow{}  b  \#  u))])
8.  CC  :  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a  \#  c\}  .  \mforall{}d:\{d:Point|  StrictOverlap(a;b;c;d)\}  .
                    (\mexists{}u:Point  [(ab  \mcong{}  au  \mwedge{}  cd  \mcong{}  cu  \mwedge{}  u  leftof  ac)])
\mvdash{}  self["Ssquashstable"  :=  Sstab]["Lorsquashstable"  :=  Lstab]["SepOr"  :=  Sepor]
    ["nontrivial"  :=  nontriv]["SS"  :=  SS]["SS"  :=  SS]["SC"  :=  SC]["CC"  :=  CC]  \mmember{}  GeometryPrimitives


By

---

Latex:
((Assert  self  \mmember{}  GeometryPrimitives  BY
                Auto)
  THEN  (D  1  THENA  Auto)
  THEN  Unfold  `geo-primitives`  0
  THEN  RepeatFor  2  ((RecordPlusTypeCD
                                        THENL  [  Id;  (UnfoldGeoAbbreviations  0  THEN  FoldGeoAbbreviations  0  THEN  Trivial)]
                                      )))

---

Home Index