Step
*
1
2
1
1
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))
⊢ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∧ b = b ∧ a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∨ b = b ∨ a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b,c:x,y:Point(l)//(eq x y)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b,c:x,y:Point(l)//(eq x y)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∨ a ∧ b = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b:x,y:Point(l)//(eq x y)]. (a ∧ a ∨ b = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a:x,y:Point(l)//(eq x y)]. (a ∧ 1 = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a:x,y:Point(l)//(eq x y)]. (a ∨ 0 = a ∈ (x,y:Point(l)//(eq x y))))
∧ (∀[a,b,c:x,y:Point(l)//(eq x y)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ (x,y:Point(l)//(eq x y))))
BY
{ (SplitAndConcl THEN (UnivCD THENA Auto)) }
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 : 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))
2
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))
3
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)
21. c : x,y:Point(l)//(eq x y)
⊢ a ∧ b ∧ c = a ∧ b ∧ c ∈ (x,y:Point(l)//(eq x y))
4
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)
21. c : x,y:Point(l)//(eq x y)
⊢ a ∨ b ∨ c = a ∨ b ∨ c ∈ (x,y:Point(l)//(eq x y))
5
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 ∨ a ∧ b = a ∈ (x,y:Point(l)//(eq x y))
6
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 ∧ a ∨ b = a ∈ (x,y:Point(l)//(eq x y))
7
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)
⊢ a ∧ 1 = a ∈ (x,y:Point(l)//(eq x y))
8
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)
⊢ a ∨ 0 = a ∈ (x,y:Point(l)//(eq x y))
9
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)
21. c : x,y:Point(l)//(eq x y)
⊢ a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ (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))
\mvdash{} (\mforall{}[a,b:x,y:Point(l)//(eq x y)]. (a \mwedge{} b = b \mwedge{} a))
\mwedge{} (\mforall{}[a,b:x,y:Point(l)//(eq x y)]. (a \mvee{} b = b \mvee{} a))
\mwedge{} (\mforall{}[a,b,c:x,y:Point(l)//(eq x y)]. (a \mwedge{} b \mwedge{} c = a \mwedge{} b \mwedge{} c))
\mwedge{} (\mforall{}[a,b,c:x,y:Point(l)//(eq x y)]. (a \mvee{} b \mvee{} c = a \mvee{} b \mvee{} c))
\mwedge{} (\mforall{}[a,b:x,y:Point(l)//(eq x y)]. (a \mvee{} a \mwedge{} b = a))
\mwedge{} (\mforall{}[a,b:x,y:Point(l)//(eq x y)]. (a \mwedge{} a \mvee{} b = a))
\mwedge{} (\mforall{}[a:x,y:Point(l)//(eq x y)]. (a \mwedge{} 1 = a))
\mwedge{} (\mforall{}[a:x,y:Point(l)//(eq x y)]. (a \mvee{} 0 = a))
\mwedge{} (\mforall{}[a,b,c:x,y:Point(l)//(eq x y)]. (a \mwedge{} b \mvee{} c = a \mwedge{} b \mvee{} a \mwedge{} c))
By
Latex:
(SplitAndConcl THEN (UnivCD THENA Auto))
Home
Index