---

Step * 1 of Lemma dM-to-FL-neg


1. I : fset(ℕ)
2. ∀a,b:Point(free-DeMorgan-lattice(names(I);NamesDeq)).  Dec(a = b ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))
3. deq-fset(deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq)))
   ∈ EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))
4. λs./\(λx.free-dl-inc(x)"(s)) ∈ fset(names(I) + names(I)) ⟶ Point(free-DeMorgan-lattice(names(I);NamesDeq))
5. ∀v:fset(fset(names(I) + names(I)))
     (λs./\(λx.free-dl-inc(x)"(s))"(v) ∈ fset(Point(free-DeMorgan-lattice(names(I);NamesDeq))))
⊢ ∀x:Point(free-DeMorgan-lattice(names(I);NamesDeq)). (dM-to-FL(I;x) ∧ dM-to-FL(I;¬(x)) = 0 ∈ Point(face_lattice(I)))
BY
{ ((D 0 THENA Auto) THEN (InstLemma `dM-basis` [⌜I⌝;⌜x⌝]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Auto) }

1
1. I : fset(ℕ)
2. ∀a,b:Point(free-DeMorgan-lattice(names(I);NamesDeq)).  Dec(a = b ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))
3. deq-fset(deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq)))
   ∈ EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))
4. λs./\(λx.free-dl-inc(x)"(s)) ∈ fset(names(I) + names(I)) ⟶ Point(free-DeMorgan-lattice(names(I);NamesDeq))
5. ∀v:fset(fset(names(I) + names(I)))
     (λs./\(λx.free-dl-inc(x)"(s))"(v) ∈ fset(Point(free-DeMorgan-lattice(names(I);NamesDeq))))
6. x : Point(free-DeMorgan-lattice(names(I);NamesDeq))
7. x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(dM(I))
⊢ dM-to-FL(I;\/(λs./\(λx.free-dl-inc(x)"(s))"(x))) ∧ dM-to-FL(I;¬(\/(λs./\(λx.free-dl-inc(x)"(s))"(x))))
= 0
∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  \mforall{}a,b:Point(free-DeMorgan-lattice(names(I);NamesDeq)).    Dec(a  =  b)
3.  deq-fset(deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq)))
      \mmember{}  EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))
4.  \mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))  \mmember{}  fset(names(I)  +  names(I))
      {}\mrightarrow{}  Point(free-DeMorgan-lattice(names(I);NamesDeq))
5.  \mforall{}v:fset(fset(names(I)  +  names(I)))
          (\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(v)  \mmember{}  fset(Point(free-DeMorgan-lattice(names(I);NamesDeq))))
\mvdash{}  \mforall{}x:Point(free-DeMorgan-lattice(names(I);NamesDeq)).  (dM-to-FL(I;x)  \mwedge{}  dM-to-FL(I;\mneg{}(x))  =  0)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (InstLemma  `dM-basis`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index