---

Step * 1 1 of Lemma mk-dp_wf


1. self : DualPlanePrimitives
2. sqs : ∀x,y:Vec.  SqStable((x # y))
3. st : ∀x,y:Vec.  Stable{(x ⊥ y)}
4. sor : ∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec.  ((z # x) ∨ (z # y))
5. crs : ∀a:Vec. ∀b:{b:Vec| (a # b)} .  (∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])
6. nt : ∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])
⊢ self["Ssquashstable" := sqs]["Pstable" := st]["SepOr" := sor]["cross" := crs]["nontrivial" := nt]
  ∈ DualPlanePrimitives
BY
{ (((Assert self ∈ DualPlanePrimitives BY
           Auto)
    THEN (D 1 THENA Auto)
    THEN Unfold `dual-plane-primitives` 0
    THEN RepeatFor 3 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Trivial ⋅)])))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  self  :  DualPlanePrimitives
2.  sqs  :  \mforall{}x,y:Vec.    SqStable((x  \#  y))
3.  st  :  \mforall{}x,y:Vec.    Stable\{(x  \mbot{}  y)\}
4.  sor  :  \mforall{}x:Vec.  \mforall{}y:\{y:Vec|  (x  \#  y)\}  .  \mforall{}z:Vec.    ((z  \#  x)  \mvee{}  (z  \#  y))
5.  crs  :  \mforall{}a:Vec.  \mforall{}b:\{b:Vec|  (a  \#  b)\}  .    (\mexists{}c:Vec  [((a  \mbot{}  c)  \mwedge{}  (b  \mbot{}  c))])
6.  nt  :  \mforall{}a:Vec.  (\mexists{}c:Vec  [((a  \mbot{}  c)  \mwedge{}  (a  \#  c))])
\mvdash{}  self["Ssquashstable"  :=  sqs]["Pstable"  :=  st]["SepOr"  :=  sor]["cross"  :=  crs]["nontrivial"  :=  nt]
    \mmember{}  DualPlanePrimitives


By

---

Latex:
(((Assert  self  \mmember{}  DualPlanePrimitives  BY
                  Auto)
    THEN  (D  1  THENA  Auto)
    THEN  Unfold  `dual-plane-primitives`  0
    THEN  RepeatFor  3  ((RecordPlusTypeCD  THENL  [  Id;  (Reduce  0  THEN  Trivial  \mcdot{})])))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index