---

Step * 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
  "Ssquashstable":∀x,y:Vec.  SqStable((x # y))
  "Pstable":∀x,y:Vec.  Stable{(x ⊥ y)}
  "SepOr":∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec.  ((z # x) ∨ (z # y))
  "cross":∀a:Vec. ∀b:{b:Vec| (a # b)} .  (∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])
  "nontrivial":∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])
BY
{ RepeatFor 5 ((RecordPlusTypeCD
                THENL [ Id
                      ; ((Unfolds``dp-vec dp-sep dp-perp`` 0 THEN Reduce 0)
                         THEN Folds ``dp-vec dp-sep dp-perp`` 0
                         THEN Try (Trivial))]
               )) }

1
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

---

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
    "Ssquashstable":\mforall{}x,y:Vec.    SqStable((x  \#  y))
    "Pstable":\mforall{}x,y:Vec.    Stable\{(x  \mbot{}  y)\}
    "SepOr":\mforall{}x:Vec.  \mforall{}y:\{y:Vec|  (x  \#  y)\}  .  \mforall{}z:Vec.    ((z  \#  x)  \mvee{}  (z  \#  y))
    "cross":\mforall{}a:Vec.  \mforall{}b:\{b:Vec|  (a  \#  b)\}  .    (\mexists{}c:Vec  [((a  \mbot{}  c)  \mwedge{}  (b  \mbot{}  c))])
    "nontrivial":\mforall{}a:Vec.  (\mexists{}c:Vec  [((a  \mbot{}  c)  \mwedge{}  (a  \#  c))])


By

---

Latex:
RepeatFor  5  ((RecordPlusTypeCD
                            THENL  [  Id
                                        ;  ((Unfolds``dp-vec  dp-sep  dp-perp``  0  THEN  Reduce  0)
                                              THEN  Folds  ``dp-vec  dp-sep  dp-perp``  0
                                              THEN  Try  (Trivial))]
                          ))

---

Home Index