---

Step * 1 2 1 1 1 2 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 : x,y:Point(l)//(eq x y)
20. b : x,y:Point(l)//(eq x y)
⊢ a ∨ b = b ∨ a ∈ (x,y:Point(l)//(eq x y))
BY
{ (OnVar `a' QuotientElimForEquality THEN OnVar `b' QuotientElimForEquality) }

1
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
⊢ a ∨ b = b1 ∨ a1 ∈ (x,y:Point(l)//(eq x y))

---

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  :  x,y:Point(l)//(eq  x  y)
20.  b  :  x,y:Point(l)//(eq  x  y)
\mvdash{}  a  \mvee{}  b  =  b  \mvee{}  a


By

---

Latex:
(OnVar  `a'  QuotientElimForEquality  THEN  OnVar  `b'  QuotientElimForEquality)

---

Home Index