---

Step * 1 1 1 1 2 2 1 of Lemma free-dist-lattice-hom-unique2


1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. g : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
6. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
7. (g 0) = 0 ∈ Point(L)
8. (g 1) = 1 ∈ Point(L)
9. h : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
10. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
11. (h 0) = 0 ∈ Point(L)
12. (h 1) = 1 ∈ Point(L)
13. ∀x:T. ((g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L))
14. x : fset(fset(T))
15. ↑fset-antichain(eq;x)
16. x ∈ Point(free-dist-lattice(T; eq))
17. BoundedDistributiveLattice ⊆r BoundedLattice
18. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice(T; eq)))
19. ∀[f:Hom(free-dist-lattice(T; eq);L)]. ∀[s:fset(Point(free-dist-lattice(T; eq)))].
      ((f \/(s)) = \/(f"(s)) ∈ Point(L))
20. x1 : fset(T)
⊢ (g /\(λx.free-dl-inc(x)"(x1))) = (h /\(λx.free-dl-inc(x)"(x1))) ∈ Point(L)
BY
{ ((InstLemma `lattice-hom-fset-meet` [⌜free-dist-lattice(T; eq)⌝;⌜L⌝;⌜deq-fset(deq-fset(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. g : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
6. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
7. (g 0) = 0 ∈ Point(L)
8. (g 1) = 1 ∈ Point(L)
9. h : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
10. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
11. (h 0) = 0 ∈ Point(L)
12. (h 1) = 1 ∈ Point(L)
13. ∀x:T. ((g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L))
14. x : fset(fset(T))
15. ↑fset-antichain(eq;x)
16. x ∈ Point(free-dist-lattice(T; eq))
17. BoundedDistributiveLattice ⊆r BoundedLattice
18. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice(T; eq)))
19. ∀[f:Hom(free-dist-lattice(T; eq);L)]. ∀[s:fset(Point(free-dist-lattice(T; eq)))].
      ((f \/(s)) = \/(f"(s)) ∈ Point(L))
20. x1 : fset(T)
21. ∀[f:Hom(free-dist-lattice(T; eq);L)]. ∀[s:fset(Point(free-dist-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. g : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
6. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
7. (g 0) = 0 ∈ Point(L)
8. (g 1) = 1 ∈ Point(L)
9. h : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
10. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
11. (h 0) = 0 ∈ Point(L)
12. (h 1) = 1 ∈ Point(L)
13. ∀x:T. ((g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L))
14. x : fset(fset(T))
15. ↑fset-antichain(eq;x)
16. x ∈ Point(free-dist-lattice(T; eq))
17. BoundedDistributiveLattice ⊆r BoundedLattice
18. deq-fset(deq-fset(eq)) ∈ EqDecider(Point(free-dist-lattice(T; eq)))
19. ∀[f:Hom(free-dist-lattice(T; eq);L)]. ∀[s:fset(Point(free-dist-lattice(T; eq)))].
      ((f \/(s)) = \/(f"(s)) ∈ Point(L))
20. x1 : fset(T)
21. ∀[f:Hom(free-dist-lattice(T; eq);L)]. ∀[s:fset(Point(free-dist-lattice(T; eq)))].
      ((f /\(s)) = /\(f"(s)) ∈ Point(L))
⊢ g"(λx.free-dl-inc(x)"(x1)) = h"(λx.free-dl-inc(x)"(x1)) ∈ fset(Point(L))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  BoundedDistributiveLattice
4.  eqL  :  EqDecider(Point(L))
5.  g  :  Point(free-dist-lattice(T;  eq))  {}\mrightarrow{}  Point(L)
6.  \mforall{}[a,b:Point(free-dist-lattice(T;  eq))].    ((g  a  \mwedge{}  g  b  =  (g  a  \mwedge{}  b))  \mwedge{}  (g  a  \mvee{}  g  b  =  (g  a  \mvee{}  b)))
7.  (g  0)  =  0
8.  (g  1)  =  1
9.  h  :  Point(free-dist-lattice(T;  eq))  {}\mrightarrow{}  Point(L)
10.  \mforall{}[a,b:Point(free-dist-lattice(T;  eq))].    ((h  a  \mwedge{}  h  b  =  (h  a  \mwedge{}  b))  \mwedge{}  (h  a  \mvee{}  h  b  =  (h  a  \mvee{}  b)))
11.  (h  0)  =  0
12.  (h  1)  =  1
13.  \mforall{}x:T.  ((g  free-dl-inc(x))  =  (h  free-dl-inc(x)))
14.  x  :  fset(fset(T))
15.  \muparrow{}fset-antichain(eq;x)
16.  x  \mmember{}  Point(free-dist-lattice(T;  eq))
17.  BoundedDistributiveLattice  \msubseteq{}r  BoundedLattice
18.  deq-fset(deq-fset(eq))  \mmember{}  EqDecider(Point(free-dist-lattice(T;  eq)))
19.  \mforall{}[f:Hom(free-dist-lattice(T;  eq);L)].  \mforall{}[s:fset(Point(free-dist-lattice(T;  eq)))].
            ((f  \mbackslash{}/(s))  =  \mbackslash{}/(f"(s)))
20.  x1  :  fset(T)
\mvdash{}  (g  /\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(x1)))  =  (h  /\mbackslash{}(\mlambda{}x.free-dl-inc(x)"(x1)))


By

---

Latex:
((InstLemma  `lattice-hom-fset-meet`  [\mkleeneopen{}free-dist-lattice(T;  eq)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}deq-fset(deq-fset(eq))\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  ((RWO    "-1"  0  THENM  EqCD)  THENA  Auto)
  )

---

Home Index