Step
*
1
1
1
1
2
1
of Lemma
face-lattice-hom-unique
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f0 : T ⟶ Point(L)
6. f1 : T ⟶ Point(L)
7. g : Point(face-lattice(T;eq)) ⟶ Point(L)
8. ∀[a,b:Point(face-lattice(T;eq))]. ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
9. (g 0) = 0 ∈ Point(L)
10. (g 1) = 1 ∈ Point(L)
11. h : Point(face-lattice(T;eq)) ⟶ Point(L)
12. ∀[a,b:Point(face-lattice(T;eq))]. ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
13. (h 0) = 0 ∈ Point(L)
14. (h 1) = 1 ∈ Point(L)
15. ∀x:T. (g (x=0) ∧ g (x=1) = 0 ∈ Point(L))
16. ∀x:T. ((g (x=0)) = (h (x=0)) ∈ Point(L))
17. ∀x:T. ((g (x=1)) = (h (x=1)) ∈ Point(L))
18. y : fset(fset(T + T))
19. (↑fset-antichain(union-deq(T;T;eq;eq);y)) ∧ (∀a:fset(T + T). (a ∈ y ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z ∈ a)))))
20. y ∈ Point(face-lattice(T;eq))
21. y
= \/(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
∈ Point(face-lattice(T;eq))
22. BoundedDistributiveLattice ⊆r BoundedLattice
23. ∀x,y:Point(face-lattice(T;eq)). Dec(x = y ∈ Point(face-lattice(T;eq)))
⊢ (g \/(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y)))
= (h \/(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y)))
∈ Point(L)
BY
{ (Fold `fl-deq` 0
THEN (InstLemma `lattice-hom-fset-join` [⌜face-lattice(T;eq)⌝;⌜L⌝;⌜fl-deq(T;eq)⌝;⌜eqL⌝]⋅ THENA Auto)
THEN ((RWO "-1" 0 THENM EqCD) THENA Auto)) }
1
.....subterm..... T:t
1:n
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f0 : T ⟶ Point(L)
6. f1 : T ⟶ Point(L)
7. g : Point(face-lattice(T;eq)) ⟶ Point(L)
8. ∀[a,b:Point(face-lattice(T;eq))]. ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
9. (g 0) = 0 ∈ Point(L)
10. (g 1) = 1 ∈ Point(L)
11. h : Point(face-lattice(T;eq)) ⟶ Point(L)
12. ∀[a,b:Point(face-lattice(T;eq))]. ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
13. (h 0) = 0 ∈ Point(L)
14. (h 1) = 1 ∈ Point(L)
15. ∀x:T. (g (x=0) ∧ g (x=1) = 0 ∈ Point(L))
16. ∀x:T. ((g (x=0)) = (h (x=0)) ∈ Point(L))
17. ∀x:T. ((g (x=1)) = (h (x=1)) ∈ Point(L))
18. y : fset(fset(T + T))
19. (↑fset-antichain(union-deq(T;T;eq;eq);y)) ∧ (∀a:fset(T + T). (a ∈ y ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z ∈ a)))))
20. y ∈ Point(face-lattice(T;eq))
21. y
= \/(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
∈ Point(face-lattice(T;eq))
22. BoundedDistributiveLattice ⊆r BoundedLattice
23. ∀x,y:Point(face-lattice(T;eq)). Dec(x = y ∈ Point(face-lattice(T;eq)))
24. ∀[f:Hom(face-lattice(T;eq);L)]. ∀[s:fset(Point(face-lattice(T;eq)))]. ((f \/(s)) = \/(f"(s)) ∈ Point(L))
⊢ L = L ∈ BoundedLattice
2
.....subterm..... T:t
2:n
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f0 : T ⟶ Point(L)
6. f1 : T ⟶ Point(L)
7. g : Point(face-lattice(T;eq)) ⟶ Point(L)
8. ∀[a,b:Point(face-lattice(T;eq))]. ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
9. (g 0) = 0 ∈ Point(L)
10. (g 1) = 1 ∈ Point(L)
11. h : Point(face-lattice(T;eq)) ⟶ Point(L)
12. ∀[a,b:Point(face-lattice(T;eq))]. ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
13. (h 0) = 0 ∈ Point(L)
14. (h 1) = 1 ∈ Point(L)
15. ∀x:T. (g (x=0) ∧ g (x=1) = 0 ∈ Point(L))
16. ∀x:T. ((g (x=0)) = (h (x=0)) ∈ Point(L))
17. ∀x:T. ((g (x=1)) = (h (x=1)) ∈ Point(L))
18. y : fset(fset(T + T))
19. (↑fset-antichain(union-deq(T;T;eq;eq);y)) ∧ (∀a:fset(T + T). (a ∈ y ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z ∈ a)))))
20. y ∈ Point(face-lattice(T;eq))
21. y
= \/(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
∈ Point(face-lattice(T;eq))
22. BoundedDistributiveLattice ⊆r BoundedLattice
23. ∀x,y:Point(face-lattice(T;eq)). Dec(x = y ∈ Point(face-lattice(T;eq)))
24. ∀[f:Hom(face-lattice(T;eq);L)]. ∀[s:fset(Point(face-lattice(T;eq)))]. ((f \/(s)) = \/(f"(s)) ∈ Point(L))
⊢ g"(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
= h"(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
∈ fset(Point(L))
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f0 : T {}\mrightarrow{} Point(L)
6. f1 : T {}\mrightarrow{} Point(L)
7. g : Point(face-lattice(T;eq)) {}\mrightarrow{} Point(L)
8. \mforall{}[a,b:Point(face-lattice(T;eq))]. ((g a \mwedge{} g b = (g a \mwedge{} b)) \mwedge{} (g a \mvee{} g b = (g a \mvee{} b)))
9. (g 0) = 0
10. (g 1) = 1
11. h : Point(face-lattice(T;eq)) {}\mrightarrow{} Point(L)
12. \mforall{}[a,b:Point(face-lattice(T;eq))]. ((h a \mwedge{} h b = (h a \mwedge{} b)) \mwedge{} (h a \mvee{} h b = (h a \mvee{} b)))
13. (h 0) = 0
14. (h 1) = 1
15. \mforall{}x:T. (g (x=0) \mwedge{} g (x=1) = 0)
16. \mforall{}x:T. ((g (x=0)) = (h (x=0)))
17. \mforall{}x:T. ((g (x=1)) = (h (x=1)))
18. y : fset(fset(T + T))
19. (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);y))
\mwedge{} (\mforall{}a:fset(T + T). (a \mmember{} y {}\mRightarrow{} (\mforall{}z:T. (\mneg{}(inl z \mmember{} a \mwedge{} inr z \mmember{} a)))))
20. y \mmember{} Point(face-lattice(T;eq))
21. y = \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
22. BoundedDistributiveLattice \msubseteq{}r BoundedLattice
23. \mforall{}x,y:Point(face-lattice(T;eq)). Dec(x = y)
\mvdash{} (g \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y)))
= (h \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y)))
By
Latex:
(Fold `fl-deq` 0
THEN (InstLemma `lattice-hom-fset-join` [\mkleeneopen{}face-lattice(T;eq)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}fl-deq(T;eq)\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN ((RWO "-1" 0 THENM EqCD) THENA Auto))
Home
Index