---

Step * 1 2 1 1 1 of Lemma face-lattice-induction


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)))
12. v : fset(Point(face-lattice(T;eq)))
13. λs./\(λu.{{u}}"(s))"(x) = v ∈ fset(Point(face-lattice(T;eq)))
14. x1 : Point(face-lattice(T;eq))
15. x1 ∈ v
⊢ P[x1]
BY
{ ((RevHypSubst' (-3) (-1) THENA Auto) THEN RWO "member-fset-image-iff" (-1) THEN Try (QuickAuto)) }

1
.....wf..... 
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)))
12. v : fset(Point(face-lattice(T;eq)))
13. λs./\(λu.{{u}}"(s))"(x) = v ∈ fset(Point(face-lattice(T;eq)))
14. x1 : Point(face-lattice(T;eq))
15. x1 ∈ λs./\(λu.{{u}}"(s))"(x)
⊢ λs./\(λu.{{u}}"(s)) ∈ fset(T + T) ⟶ Point(face-lattice(T;eq))

2
.....wf..... 
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)))
12. v : fset(Point(face-lattice(T;eq)))
13. λs./\(λu.{{u}}"(s))"(x) = v ∈ fset(Point(face-lattice(T;eq)))
14. x1 : Point(face-lattice(T;eq))
15. x1 ∈ λs./\(λu.{{u}}"(s))"(x)
⊢ x ∈ fset(fset(T + T))

3
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)))
12. v : fset(Point(face-lattice(T;eq)))
13. λs./\(λu.{{u}}"(s))"(x) = v ∈ fset(Point(face-lattice(T;eq)))
14. x1 : Point(face-lattice(T;eq))
15. ↓∃x2:fset(T + T). (x2 ∈ x ∧ (x1 = ((λs./\(λu.{{u}}"(s))) x2) ∈ Point(face-lattice(T;eq))))
⊢ P[x1]

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  \mforall{}[x:Point(face-lattice(T;eq))].  (x  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}u.\{\{u\}\}"(s))"(x)))
4.  P  :  Point(face-lattice(T;eq))  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x:Point(face-lattice(T;eq)).  SqStable(P[x])
6.  P[0]
7.  P[1]
8.  \mforall{}x,y:Point(face-lattice(T;eq)).    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[x  \mvee{}  y])
9.  \mforall{}x:Point(face-lattice(T;eq)).  (P[x]  {}\mRightarrow{}  (\mforall{}i:T.  (P[(i=0)  \mwedge{}  x]  \mwedge{}  P[(i=1)  \mwedge{}  x])))
10.  x  :  Point(face-lattice(T;eq))
11.  deq-fset(deq-fset(union-deq(T;T;eq;eq)))  \mmember{}  EqDecider(Point(face-lattice(T;eq)))
12.  v  :  fset(Point(face-lattice(T;eq)))
13.  \mlambda{}s./\mbackslash{}(\mlambda{}u.\{\{u\}\}"(s))"(x)  =  v
14.  x1  :  Point(face-lattice(T;eq))
15.  x1  \mmember{}  v
\mvdash{}  P[x1]


By

---

Latex:
((RevHypSubst'  (-3)  (-1)  THENA  Auto)  THEN  RWO  "member-fset-image-iff"  (-1)  THEN  Try  (QuickAuto))

---

Home Index