---

Step * of Lemma dM-to-FL-neg

∀[I:fset(ℕ)]
  ∀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 (Assert ⌜∀a,b:Point(free-DeMorgan-lattice(names(I);NamesDeq)).
                   Dec(a = b ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))⌝⋅
         THENA (BLemma `deq-implies` THEN Auto THEN UseWitness ⌜free-dml-deq(names(I);NamesDeq)⌝⋅ THEN Auto)
         )
   THEN (Assert deq-fset(deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq)))
                ∈ EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq))) BY
               (Fold `free-dml-deq` 0 THEN Auto))
   THEN (Assert ⌜λs./\(λx.free-dl-inc(x)"(s)) ∈ fset(names(I) + names(I))
                 ⟶ Point(free-DeMorgan-lattice(names(I);NamesDeq))⌝⋅
         THENA (RepeatFor 2 (MemCD')
                THEN Try (Trivial)
                THEN Try ((Unfold `free-DeMorgan-lattice` 0 THEN Complete (Auto)))
                THEN Auto)
         )
   THEN (Assert ⌜∀v:fset(fset(names(I) + names(I)))
                   (λs./\(λx.free-dl-inc(x)"(s))"(v) ∈ fset(Point(free-DeMorgan-lattice(names(I);NamesDeq))))⌝⋅
         THENA 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))))
⊢ ∀x:Point(free-DeMorgan-lattice(names(I);NamesDeq)). (dM-to-FL(I;x) ∧ dM-to-FL(I;¬(x)) = 0 ∈ Point(face_lattice(I)))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})]
    \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  (Assert  \mkleeneopen{}\mforall{}a,b:Point(free-DeMorgan-lattice(names(I);NamesDeq)).    Dec(a  =  b)\mkleeneclose{}\mcdot{}
              THENA  (BLemma  `deq-implies`
                            THEN  Auto
                            THEN  UseWitness  \mkleeneopen{}free-dml-deq(names(I);NamesDeq)\mkleeneclose{}\mcdot{}
                            THEN  Auto)
              )
  THEN  (Assert  deq-fset(deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq)))
                            \mmember{}  EqDecider(Point(free-DeMorgan-lattice(names(I);NamesDeq)))  BY
                          (Fold  `free-dml-deq`  0  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))  \mmember{}  fset(names(I)  +  names(I))
                              {}\mrightarrow{}  Point(free-DeMorgan-lattice(names(I);NamesDeq))\mkleeneclose{}\mcdot{}
              THENA  (RepeatFor  2  (MemCD')
                            THEN  Try  (Trivial)
                            THEN  Try  ((Unfold  `free-DeMorgan-lattice`  0  THEN  Complete  (Auto)))
                            THEN  Auto)
              )
  THEN  (Assert  \mkleeneopen{}\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))))\mkleeneclose{}\mcdot{}
              THENA  Auto
              ))

---

Home Index