Step
*
1
of Lemma
f-lattice_wf
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. EquivRel(Point(free-dl(X + X));x,y.↓∃as,bs:(X + X) List List
((x = as ∈ Point(free-dl(X + X)))
∧ (y = bs ∈ Point(free-dl(X + X)))
∧ flattice-order(X;as;bs)
∧ flattice-order(X;bs;as)))
4. a : Point(free-dl(X + X))
5. c : Point(free-dl(X + X))
6. b : Point(free-dl(X + X))
7. d : Point(free-dl(X + X))
8. a1 : (X + X) List List
9. b1 : (X + X) List List
10. a = a1 ∈ Point(free-dl(X + X))
11. c = b1 ∈ Point(free-dl(X + X))
12. flattice-order(X;a1;b1)
13. flattice-order(X;b1;a1)
14. as : (X + X) List List
15. bs : (X + X) List List
16. b = as ∈ Point(free-dl(X + X))
17. d = bs ∈ Point(free-dl(X + X))
18. flattice-order(X;as;bs)
19. flattice-order(X;bs;as)
⊢ ∃as,bs:(X + X) List List
((a ∧ b = as ∈ Point(free-dl(X + X)))
∧ (c ∧ d = bs ∈ Point(free-dl(X + X)))
∧ flattice-order(X;as;bs)
∧ flattice-order(X;bs;as))
BY
{ (InstConcl [⌜free-dl-meet(a1;as)⌝;⌜free-dl-meet(b1;bs)⌝]⋅ THEN Auto) }
1
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. EquivRel(Point(free-dl(X + X));x,y.↓∃as,bs:(X + X) List List
((x = as ∈ Point(free-dl(X + X)))
∧ (y = bs ∈ Point(free-dl(X + X)))
∧ flattice-order(X;as;bs)
∧ flattice-order(X;bs;as)))
4. a : Point(free-dl(X + X))
5. c : Point(free-dl(X + X))
6. b : Point(free-dl(X + X))
7. d : Point(free-dl(X + X))
8. a1 : (X + X) List List
9. b1 : (X + X) List List
10. a = a1 ∈ Point(free-dl(X + X))
11. c = b1 ∈ Point(free-dl(X + X))
12. flattice-order(X;a1;b1)
13. flattice-order(X;b1;a1)
14. as : (X + X) List List
15. bs : (X + X) List List
16. b = as ∈ Point(free-dl(X + X))
17. d = bs ∈ Point(free-dl(X + X))
18. flattice-order(X;as;bs)
19. flattice-order(X;bs;as)
⊢ a ∧ b = free-dl-meet(a1;as) ∈ Point(free-dl(X + X))
2
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. EquivRel(Point(free-dl(X + X));x,y.↓∃as,bs:(X + X) List List
((x = as ∈ Point(free-dl(X + X)))
∧ (y = bs ∈ Point(free-dl(X + X)))
∧ flattice-order(X;as;bs)
∧ flattice-order(X;bs;as)))
4. a : Point(free-dl(X + X))
5. c : Point(free-dl(X + X))
6. b : Point(free-dl(X + X))
7. d : Point(free-dl(X + X))
8. a1 : (X + X) List List
9. b1 : (X + X) List List
10. a = a1 ∈ Point(free-dl(X + X))
11. c = b1 ∈ Point(free-dl(X + X))
12. flattice-order(X;a1;b1)
13. flattice-order(X;b1;a1)
14. as : (X + X) List List
15. bs : (X + X) List List
16. b = as ∈ Point(free-dl(X + X))
17. d = bs ∈ Point(free-dl(X + X))
18. flattice-order(X;as;bs)
19. flattice-order(X;bs;as)
20. a ∧ b = free-dl-meet(a1;as) ∈ Point(free-dl(X + X))
⊢ c ∧ d = free-dl-meet(b1;bs) ∈ Point(free-dl(X + X))
3
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. EquivRel(Point(free-dl(X + X));x,y.↓∃as,bs:(X + X) List List
((x = as ∈ Point(free-dl(X + X)))
∧ (y = bs ∈ Point(free-dl(X + X)))
∧ flattice-order(X;as;bs)
∧ flattice-order(X;bs;as)))
4. a : Point(free-dl(X + X))
5. c : Point(free-dl(X + X))
6. b : Point(free-dl(X + X))
7. d : Point(free-dl(X + X))
8. a1 : (X + X) List List
9. b1 : (X + X) List List
10. a = a1 ∈ Point(free-dl(X + X))
11. c = b1 ∈ Point(free-dl(X + X))
12. flattice-order(X;a1;b1)
13. flattice-order(X;b1;a1)
14. as : (X + X) List List
15. bs : (X + X) List List
16. b = as ∈ Point(free-dl(X + X))
17. d = bs ∈ Point(free-dl(X + X))
18. flattice-order(X;as;bs)
19. flattice-order(X;bs;as)
20. a ∧ b = free-dl-meet(a1;as) ∈ Point(free-dl(X + X))
21. c ∧ d = free-dl-meet(b1;bs) ∈ Point(free-dl(X + X))
⊢ flattice-order(X;free-dl-meet(a1;as);free-dl-meet(b1;bs))
4
1. X : Type
2. ((X + X) List List) ⊆r Point(free-dl(X + X))
3. EquivRel(Point(free-dl(X + X));x,y.↓∃as,bs:(X + X) List List
((x = as ∈ Point(free-dl(X + X)))
∧ (y = bs ∈ Point(free-dl(X + X)))
∧ flattice-order(X;as;bs)
∧ flattice-order(X;bs;as)))
4. a : Point(free-dl(X + X))
5. c : Point(free-dl(X + X))
6. b : Point(free-dl(X + X))
7. d : Point(free-dl(X + X))
8. a1 : (X + X) List List
9. b1 : (X + X) List List
10. a = a1 ∈ Point(free-dl(X + X))
11. c = b1 ∈ Point(free-dl(X + X))
12. flattice-order(X;a1;b1)
13. flattice-order(X;b1;a1)
14. as : (X + X) List List
15. bs : (X + X) List List
16. b = as ∈ Point(free-dl(X + X))
17. d = bs ∈ Point(free-dl(X + X))
18. flattice-order(X;as;bs)
19. flattice-order(X;bs;as)
20. a ∧ b = free-dl-meet(a1;as) ∈ Point(free-dl(X + X))
21. c ∧ d = free-dl-meet(b1;bs) ∈ Point(free-dl(X + X))
22. flattice-order(X;free-dl-meet(a1;as);free-dl-meet(b1;bs))
⊢ flattice-order(X;free-dl-meet(b1;bs);free-dl-meet(a1;as))
Latex:
Latex:
1. X : Type
2. ((X + X) List List) \msubseteq{}r Point(free-dl(X + X))
3. EquivRel(Point(free-dl(X + X));x,y.\mdownarrow{}\mexists{}as,bs:(X + X) List List
((x = as)
\mwedge{} (y = bs)
\mwedge{} flattice-order(X;as;bs)
\mwedge{} flattice-order(X;bs;as)))
4. a : Point(free-dl(X + X))
5. c : Point(free-dl(X + X))
6. b : Point(free-dl(X + X))
7. d : Point(free-dl(X + X))
8. a1 : (X + X) List List
9. b1 : (X + X) List List
10. a = a1
11. c = b1
12. flattice-order(X;a1;b1)
13. flattice-order(X;b1;a1)
14. as : (X + X) List List
15. bs : (X + X) List List
16. b = as
17. d = bs
18. flattice-order(X;as;bs)
19. flattice-order(X;bs;as)
\mvdash{} \mexists{}as,bs:(X + X) List List
((a \mwedge{} b = as) \mwedge{} (c \mwedge{} d = bs) \mwedge{} flattice-order(X;as;bs) \mwedge{} flattice-order(X;bs;as))
By
Latex:
(InstConcl [\mkleeneopen{}free-dl-meet(a1;as)\mkleeneclose{};\mkleeneopen{}free-dl-meet(b1;bs)\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index