---

Step * of Lemma dM-basis

∀[I:fset(ℕ)]. ∀[x:Point(dM(I))].  (x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(dM(I)))
BY
{ (Auto
   THEN (InstLemma `free-dl-basis` [⌜names(I) + names(I)⌝;⌜union-deq(names(I);names(I);NamesDeq;NamesDeq)⌝]⋅ THENA Auto)
   THEN Fold `free-DeMorgan-lattice` (-1)) }

1
1. I : fset(ℕ)
2. x : Point(dM(I))
3. ∀[x:Point(free-DeMorgan-lattice(names(I);NamesDeq))]
     (x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))
⊢ x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(dM(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:Point(dM(I))].    (x  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(x)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `free-dl-basis`  [\mkleeneopen{}names(I)  +  names(I)\mkleeneclose{};
              \mkleeneopen{}union-deq(names(I);names(I);NamesDeq;NamesDeq)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `free-DeMorgan-lattice`  (-1))

---

Home Index