Step
*
2
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 [⌜a1 @ as⌝;⌜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 = (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 = (a1 @ as) ∈ Point(free-dl(X + X))
⊢ c ∨ d = (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 = (a1 @ as) ∈ Point(free-dl(X + X))
21. c ∨ d = (b1 @ bs) ∈ Point(free-dl(X + X))
⊢ flattice-order(X;a1 @ as;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 = (a1 @ as) ∈ Point(free-dl(X + X))
21. c ∨ d = (b1 @ bs) ∈ Point(free-dl(X + X))
22. flattice-order(X;a1 @ as;b1 @ bs)
⊢ flattice-order(X;b1 @ bs;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 \mvee{} b = as) \mwedge{} (c \mvee{} d = bs) \mwedge{} flattice-order(X;as;bs) \mwedge{} flattice-order(X;bs;as))
By
Latex:
(InstConcl [\mkleeneopen{}a1 @ as\mkleeneclose{};\mkleeneopen{}b1 @ bs\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index