---

Step * of Lemma face-lattice-induction

∀T:Type. ∀eq:EqDecider(T).
  ∀[P:Point(face-lattice(T;eq)) ⟶ ℙ]
    ((∀x:Point(face-lattice(T;eq)). SqStable(P[x]))
    ⇒ P[0]
    ⇒ P[1]
    ⇒ (∀x,y:Point(face-lattice(T;eq)).  (P[x] ⇒ P[y] ⇒ P[x ∨ y]))
    ⇒ (∀x:Point(face-lattice(T;eq)). (P[x] ⇒ (∀i:T. (P[(i=0) ∧ x] ∧ P[(i=1) ∧ x]))))
    ⇒ (∀x:Point(face-lattice(T;eq)). P[x]))
BY
{ (InstLemma `face-lattice-basis` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN (InstHyp [⌜x⌝] 3⋅ THENA Auto)
   THEN (HypSubst' -1 0 THENA Auto)
   THEN Thin (-1)
   THEN (Assert deq-fset(deq-fset(union-deq(T;T;eq;eq))) ∈ EqDecider(Point(face-lattice(T;eq))) BY
               (RWO  "fl-point-sq" 0 THEN Auto))) }

1
1. T : Type
2. eq : EqDecider(T)
3. ∀[x:Point(face-lattice(T;eq))]. (x = \/(λs./\(λu.{{u}}"(s))"(x)) ∈ Point(face-lattice(T;eq)))
4. [P] : Point(face-lattice(T;eq)) ⟶ ℙ
5. ∀x:Point(face-lattice(T;eq)). SqStable(P[x])
6. P[0]
7. P[1]
8. ∀x,y:Point(face-lattice(T;eq)).  (P[x] ⇒ P[y] ⇒ P[x ∨ y])
9. ∀x:Point(face-lattice(T;eq)). (P[x] ⇒ (∀i:T. (P[(i=0) ∧ x] ∧ P[(i=1) ∧ x])))
10. x : Point(face-lattice(T;eq))
11. deq-fset(deq-fset(union-deq(T;T;eq;eq))) ∈ EqDecider(Point(face-lattice(T;eq)))
⊢ P[\/(λs./\(λu.{{u}}"(s))"(x))]

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).
    \mforall{}[P:Point(face-lattice(T;eq))  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}x:Point(face-lattice(T;eq)).  SqStable(P[x]))
        {}\mRightarrow{}  P[0]
        {}\mRightarrow{}  P[1]
        {}\mRightarrow{}  (\mforall{}x,y:Point(face-lattice(T;eq)).    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[x  \mvee{}  y]))
        {}\mRightarrow{}  (\mforall{}x:Point(face-lattice(T;eq)).  (P[x]  {}\mRightarrow{}  (\mforall{}i:T.  (P[(i=0)  \mwedge{}  x]  \mwedge{}  P[(i=1)  \mwedge{}  x]))))
        {}\mRightarrow{}  (\mforall{}x:Point(face-lattice(T;eq)).  P[x]))


By

---

Latex:
(InstLemma  `face-lattice-basis`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  -1  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (Assert  deq-fset(deq-fset(union-deq(T;T;eq;eq)))  \mmember{}  EqDecider(Point(face-lattice(T;eq)))  BY
                          (RWO    "fl-point-sq"  0  THEN  Auto)))

---

Home Index