---

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


1. I : fset(ℕ)
2. x : Point(dM(I))
3. dM-to-FL(I;x) = 1 ∈ Point(face_lattice(I))
4. dM-to-FL(I;x) = \/(λs./\(λx.dM-to-FL(I;free-dl-inc(x))"(s))"(x)) ∈ Point(face_lattice(I))
5. \/(λs./\(λx.dM-to-FL(I;free-dl-inc(x))"(s))"(x)) = 1 ∈ Point(face_lattice(I))
⊢ x = 1 ∈ Point(dM(I))
BY
{ ((Assert ⌜\/(λs./\(λx.free-dl-inc(x)"(s))"(x)) = 1 ∈ Point(dM(I))⌝⋅ THENM (InstLemma `dM-basis` [⌜I⌝;⌜x⌝]⋅ THEN Auto))
   THEN RepeatFor 2 (Thin (-2))
   ) }

1
1. I : fset(ℕ)
2. x : Point(dM(I))
3. \/(λs./\(λx.dM-to-FL(I;free-dl-inc(x))"(s))"(x)) = 1 ∈ Point(face_lattice(I))
⊢ \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) = 1 ∈ Point(dM(I))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(dM(I))
3.  dM-to-FL(I;x)  =  1
4.  dM-to-FL(I;x)  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.dM-to-FL(I;free-dl-inc(x))"(s))"(x))
5.  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.dM-to-FL(I;free-dl-inc(x))"(s))"(x))  =  1
\mvdash{}  x  =  1


By

---

Latex:
((Assert  \mkleeneopen{}\mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(s))"(x))  =  1\mkleeneclose{}\mcdot{}
  THENM  (InstLemma  `dM-basis`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  )
  THEN  RepeatFor  2  (Thin  (-2))
  )

---

Home Index