---

Step * 1 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))))
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))
BY
{ (Thin (-1)
   THEN Unfold `free-DeMorgan-lattice` -1
   THEN (RWO "free-dl-point" (-1) THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN MoveToConcl (-1)) }

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))))
⊢ ∀x:fset(fset(names(I) + names(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))))
6.  x  :  Point(free-DeMorgan-lattice(names(I);NamesDeq))
7.  x  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(x))
\mvdash{}  dM-to-FL(I;\mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(x)))  \mwedge{}  dM-to-FL(I;\mneg{}(\mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"
                                                                                                                                          (x))))
=  0


By

---

Latex:
(Thin  (-1)
  THEN  Unfold  `free-DeMorgan-lattice`  -1
  THEN  (RWO  "free-dl-point"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1))

---

Home Index