---

Step * of Lemma face_lattice-induction

∀I:fset(ℕ)
  ∀[P:Point(face_lattice(I)) ⟶ ℙ]
    ((∀x:Point(face_lattice(I)). SqStable(P[x]))
    ⇒ P[0]
    ⇒ P[1]
    ⇒ (∀x,y:Point(face_lattice(I)).  (P[x] ⇒ P[y] ⇒ P[x ∨ y]))
    ⇒ (∀x:Point(face_lattice(I)). (P[x] ⇒ (∀i:names(I). (P[(i=0) ∧ x] ∧ P[(i=1) ∧ x]))))
    ⇒ {∀x:Point(face_lattice(I)). P[x]})
BY
{ ((D 0 THENA Auto)
   THEN RepUR ``fl0 fl1 face_lattice guard`` 0
   THEN (InstLemma `face-lattice-induction` [names(I);⌜NamesDeq⌝]⋅ THENA Auto)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{})
    \mforall{}[P:Point(face\_lattice(I))  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}x:Point(face\_lattice(I)).  SqStable(P[x]))
        {}\mRightarrow{}  P[0]
        {}\mRightarrow{}  P[1]
        {}\mRightarrow{}  (\mforall{}x,y:Point(face\_lattice(I)).    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[x  \mvee{}  y]))
        {}\mRightarrow{}  (\mforall{}x:Point(face\_lattice(I)).  (P[x]  {}\mRightarrow{}  (\mforall{}i:names(I).  (P[(i=0)  \mwedge{}  x]  \mwedge{}  P[(i=1)  \mwedge{}  x]))))
        {}\mRightarrow{}  \{\mforall{}x:Point(face\_lattice(I)).  P[x]\})


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepUR  ``fl0  fl1  face\_lattice  guard``  0
  THEN  (InstLemma  `face-lattice-induction`  [names(I);\mkleeneopen{}NamesDeq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Trivial)

---

Home Index