---

Step * 1 of Lemma assert-isdM1


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)))
BY
{ (FoldTop `guard` (-2) THEN (RWO "-1" 0 THENA Try (Complete (Auto)))) }

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(x = {{}} ∈ fset(fset(names(I) + names(I)));x = 1 ∈ Point(dM(I)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(dM(I))
3.  x  \mmember{}  fset(fset(names(I)  +  names(I)))
4.  uiff(\muparrow{}isdM1(x);x  =  \{\{\}\})
\mvdash{}  uiff(\muparrow{}isdM1(x);x  =  1)


By

---

Latex:
(FoldTop  `guard`  (-2)  THEN  (RWO  "-1"  0  THENA  Try  (Complete  (Auto))))

---

Home Index