---

Step * 1 2 1 1 1 9 1 of Lemma quotient-dl_wf


1. l : BoundedDistributiveLattice
2. eq : Point(l) ⟶ Point(l) ⟶ ℙ
3. EquivRel(Point(l);x,y.eq[x;y])
4. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∧ b;c ∧ d])
5. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∨ b;c ∨ d])
6. l."meet" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
7. l."join" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
8. ∀[a,b:Point(l)].  (a ∧ b = b ∧ a ∈ Point(l))
9. ∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l))
10. ∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
11. ∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
12. ∀[a,b:Point(l)].  (a ∨ a ∧ b = a ∈ Point(l))
13. ∀[a,b:Point(l)].  (a ∧ a ∨ b = a ∈ Point(l))
14. ∀[a:Point(l)]. (a ∨ 0 = a ∈ Point(l))
15. ∀[a:Point(l)]. (a ∧ 1 = a ∈ Point(l))
16. ∀[a,b,c:Point(l)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l))
17. ∀[a,b:x,y:Point(l)//(eq x y)].  (a ∧ b ∈ x,y:Point(l)//(eq x y))
18. ∀[a,b:x,y:Point(l)//(eq x y)].  (a ∨ b ∈ x,y:Point(l)//(eq x y))
19. a : Base
20. a1 : Base
21. a = a1 ∈ pertype(λx,y. ((x ∈ Point(l)) ∧ (y ∈ Point(l)) ∧ (eq x y)))
22. a ∈ Point(l)
23. a1 ∈ Point(l)
24. eq a a1
25. b : Base
26. b1 : Base
27. b = b1 ∈ pertype(λx,y. ((x ∈ Point(l)) ∧ (y ∈ Point(l)) ∧ (eq x y)))
28. b ∈ Point(l)
29. b1 ∈ Point(l)
30. eq b b1
31. c : Base
32. c1 : Base
33. c = c1 ∈ pertype(λx,y. ((x ∈ Point(l)) ∧ (y ∈ Point(l)) ∧ (eq x y)))
34. c ∈ Point(l)
35. c1 ∈ Point(l)
36. eq c c1
⊢ a ∧ b ∨ c = a1 ∧ b1 ∨ a1 ∧ c1 ∈ (x,y:Point(l)//(eq x y))
BY
{ ((Assert a ∧ b ∨ c = a1 ∧ b1 ∨ c1 ∈ (x,y:Point(l)//(eq x y)) BY
          (RepUR ``lattice-join lattice-meet`` 0
           THEN RepeatFor 2 (EqCDA)
           THEN Try ((EqTypeCD THEN Auto))
           THEN EqCDA
           THEN EqTypeCD
           THEN Auto))
   THEN (Assert a1 ∧ b1 ∨ c1 = a1 ∧ b1 ∨ a1 ∧ c1 ∈ (x,y:Point(l)//(eq x y)) BY
               BackThruSomeHyp)
   THEN Eq) }

---

Latex:

---

Latex:

1.  l  :  BoundedDistributiveLattice
2.  eq  :  Point(l)  {}\mrightarrow{}  Point(l)  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(Point(l);x,y.eq[x;y])
4.  \mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mwedge{}  b;c  \mwedge{}  d])
5.  \mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mvee{}  b;c  \mvee{}  d])
6.  l."meet"  \mmember{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])
7.  l."join"  \mmember{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])
8.  \mforall{}[a,b:Point(l)].    (a  \mwedge{}  b  =  b  \mwedge{}  a)
9.  \mforall{}[a,b:Point(l)].    (a  \mvee{}  b  =  b  \mvee{}  a)
10.  \mforall{}[a,b,c:Point(l)].    (a  \mwedge{}  b  \mwedge{}  c  =  a  \mwedge{}  b  \mwedge{}  c)
11.  \mforall{}[a,b,c:Point(l)].    (a  \mvee{}  b  \mvee{}  c  =  a  \mvee{}  b  \mvee{}  c)
12.  \mforall{}[a,b:Point(l)].    (a  \mvee{}  a  \mwedge{}  b  =  a)
13.  \mforall{}[a,b:Point(l)].    (a  \mwedge{}  a  \mvee{}  b  =  a)
14.  \mforall{}[a:Point(l)].  (a  \mvee{}  0  =  a)
15.  \mforall{}[a:Point(l)].  (a  \mwedge{}  1  =  a)
16.  \mforall{}[a,b,c:Point(l)].    (a  \mwedge{}  b  \mvee{}  c  =  a  \mwedge{}  b  \mvee{}  a  \mwedge{}  c)
17.  \mforall{}[a,b:x,y:Point(l)//(eq  x  y)].    (a  \mwedge{}  b  \mmember{}  x,y:Point(l)//(eq  x  y))
18.  \mforall{}[a,b:x,y:Point(l)//(eq  x  y)].    (a  \mvee{}  b  \mmember{}  x,y:Point(l)//(eq  x  y))
19.  a  :  Base
20.  a1  :  Base
21.  a  =  a1
22.  a  \mmember{}  Point(l)
23.  a1  \mmember{}  Point(l)
24.  eq  a  a1
25.  b  :  Base
26.  b1  :  Base
27.  b  =  b1
28.  b  \mmember{}  Point(l)
29.  b1  \mmember{}  Point(l)
30.  eq  b  b1
31.  c  :  Base
32.  c1  :  Base
33.  c  =  c1
34.  c  \mmember{}  Point(l)
35.  c1  \mmember{}  Point(l)
36.  eq  c  c1
\mvdash{}  a  \mwedge{}  b  \mvee{}  c  =  a1  \mwedge{}  b1  \mvee{}  a1  \mwedge{}  c1


By

---

Latex:
((Assert  a  \mwedge{}  b  \mvee{}  c  =  a1  \mwedge{}  b1  \mvee{}  c1  BY
                (RepUR  ``lattice-join  lattice-meet``  0
                  THEN  RepeatFor  2  (EqCDA)
                  THEN  Try  ((EqTypeCD  THEN  Auto))
                  THEN  EqCDA
                  THEN  EqTypeCD
                  THEN  Auto))
  THEN  (Assert  a1  \mwedge{}  b1  \mvee{}  c1  =  a1  \mwedge{}  b1  \mvee{}  a1  \mwedge{}  c1  BY
                          BackThruSomeHyp)
  THEN  Eq)

---

Home Index