---

Step * of Lemma one-dimensional-dM

∀i:ℕ. ∀v:Point(dM({i})).
  ((v = 0 ∈ Point(dM({i})))
  ∨ (v = 1 ∈ Point(dM({i})))
  ∨ (v = <i> ∈ Point(dM({i})))
  ∨ (v = <1-i> ∈ Point(dM({i})))
  ∨ (v = <i> ∧ <1-i> ∈ Point(dM({i})))
  ∨ (v = <i> ∨ <1-i> ∈ Point(dM({i}))))
BY
{ (Auto
   THEN (Assert Point(dM({i})) ⊆r fset(fset(names({i}) + names({i}))) BY
               (RWO "dM-point" 0 THEN Auto))
   THEN (Assert ∀x,y:Point(dM({i})).  (x = y ∈ Point(dM({i})) ⇐⇒ x = y ∈ fset(fset(names({i}) + names({i})))) BY
               ((UnivCD THENA Auto)
                THEN (RepeatFor 2 ((D 0 THENA Auto))
                      THENL [(RWO "-1" 0 THENA Auto)
                            ; ((InstLemma `assert-deq` [Point(dM({i}));⌜dM-deq({i})⌝]⋅ THENA Auto)
                               THEN (BHyp -1 THENA Auto)
                               )]
                )
                THEN RepUR ``dM-deq free-dml-deq`` 0
                THEN RWO "assert-deq-fset" 0
                THEN Auto))) }

1
1. i : ℕ
2. v : Point(dM({i}))
3. Point(dM({i})) ⊆r fset(fset(names({i}) + names({i})))
4. ∀x,y:Point(dM({i})).  (x = y ∈ Point(dM({i})) ⇐⇒ x = y ∈ fset(fset(names({i}) + names({i}))))
⊢ (v = 0 ∈ Point(dM({i})))
∨ (v = 1 ∈ Point(dM({i})))
∨ (v = <i> ∈ Point(dM({i})))
∨ (v = <1-i> ∈ Point(dM({i})))
∨ (v = <i> ∧ <1-i> ∈ Point(dM({i})))
∨ (v = <i> ∨ <1-i> ∈ Point(dM({i})))

---

Latex:

---

Latex:
\mforall{}i:\mBbbN{}.  \mforall{}v:Point(dM(\{i\})).
    ((v  =  0)  \mvee{}  (v  =  1)  \mvee{}  (v  =  <i>)  \mvee{}  (v  =  ə-i>)  \mvee{}  (v  =  <i>  \mwedge{}  ə-i>)  \mvee{}  (v  =  <i>  \mvee{}  ə-i>))


By

---

Latex:
(Auto
  THEN  (Assert  Point(dM(\{i\}))  \msubseteq{}r  fset(fset(names(\{i\})  +  names(\{i\})))  BY
                          (RWO  "dM-point"  0  THEN  Auto))
  THEN  (Assert  \mforall{}x,y:Point(dM(\{i\})).    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  x  =  y)  BY
                          ((UnivCD  THENA  Auto)
                            THEN  (RepeatFor  2  ((D  0  THENA  Auto))
                                        THENL  [(RWO  "-1"  0  THENA  Auto)
                                                    ;  ((InstLemma  `assert-deq`  [Point(dM(\{i\}));\mkleeneopen{}dM-deq(\{i\})\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                          THEN  (BHyp  -1  THENA  Auto)
                                                          )]
                            )
                            THEN  RepUR  ``dM-deq  free-dml-deq``  0
                            THEN  RWO  "assert-deq-fset"  0
                            THEN  Auto)))

---

Home Index