---

Step * of Lemma fl-morph-id

∀I:fset(ℕ). (<1> = (λx.x) ∈ (Point(face_lattice(I)) ⟶ Point(face_lattice(I))))
BY
{ ((Auto
    THEN (InstLemma `fl-lift-unique` [names(I);⌜NamesDeq⌝;⌜face-lattice(names(I);NamesDeq)⌝;⌜face_lattice-deq()⌝;
          ⌜λj.dM-to-FL(I;¬(1 j))⌝;⌜λj.dM-to-FL(I;1 j)⌝;⌜λx.x⌝]⋅
          THENA (Auto THEN Try ((Fold `face_lattice` 0 THEN Auto)))
          )
    )
   THEN Try ((Fold `face_lattice` (-1) THEN Fold `fl-morph` (-1) THEN Auto))
   THEN RepUR ``nh-id`` 0) }

1
1. I : fset(ℕ)
2. x : names(I)
⊢ (x=0) = dM-to-FL(I;¬(<x>)) ∈ Point(face_lattice(I))

2
1. I : fset(ℕ)
2. x : names(I)
3. ((λx.x) (x=0)) = ((λj.dM-to-FL(I;¬(1 j))) x) ∈ Point(face-lattice(names(I);NamesDeq))
⊢ (x=1) = dM-to-FL(I;<x>) ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{}).  (ə>  =  (\mlambda{}x.x))


By

---

Latex:
((Auto
    THEN  (InstLemma  `fl-lift-unique`  [names(I);\mkleeneopen{}NamesDeq\mkleeneclose{};\mkleeneopen{}face-lattice(names(I);NamesDeq)\mkleeneclose{};
                \mkleeneopen{}face\_lattice-deq()\mkleeneclose{};\mkleeneopen{}\mlambda{}j.dM-to-FL(I;\mneg{}(1  j))\mkleeneclose{};\mkleeneopen{}\mlambda{}j.dM-to-FL(I;1  j)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]\mcdot{}
                THENA  (Auto  THEN  Try  ((Fold  `face\_lattice`  0  THEN  Auto)))
                )
    )
  THEN  Try  ((Fold  `face\_lattice`  (-1)  THEN  Fold  `fl-morph`  (-1)  THEN  Auto))
  THEN  RepUR  ``nh-id``  0)

---

Home Index