---

Step * of Lemma assert-isdM1

No Annotations
∀[I:fset(ℕ)]. ∀[x:Point(dM(I))].  uiff(↑isdM1(x);x = 1 ∈ Point(dM(I)))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert x ∈ fset(fset(names(I) + names(I))) BY
               ((RWO "dM-point" (-1) THENA Auto) THEN D -1 THEN Auto))
   THEN (InstLemma `assert-deq-fset` [⌜fset(names(I) + names(I))⌝;
         ⌜deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq))⌝;⌜x⌝;⌜{{}}⌝]⋅
         THENA Auto
         )
   THEN Fold `isdM1` (-1)) }

1
1. I : fset(ℕ)
2. x : Point(dM(I))
3. x ∈ fset(fset(names(I) + names(I)))
4. uiff(↑isdM1(x);x = {{}} ∈ fset(fset(names(I) + names(I))))
⊢ uiff(↑isdM1(x);x = 1 ∈ Point(dM(I)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:Point(dM(I))].    uiff(\muparrow{}isdM1(x);x  =  1)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  x  \mmember{}  fset(fset(names(I)  +  names(I)))  BY
                          ((RWO  "dM-point"  (-1)  THENA  Auto)  THEN  D  -1  THEN  Auto))
  THEN  (InstLemma  `assert-deq-fset`  [\mkleeneopen{}fset(names(I)  +  names(I))\mkleeneclose{};
              \mkleeneopen{}deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq))\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\{\{\}\}\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `isdM1`  (-1))

---

Home Index