Proof of Nuprl Lemma : type-lattice

Step * of Lemma type-lattice_wf

type-lattice{i:l}() ∈ bdd-lattice{i':l}
BY
{ (ProveWfLemma
   THEN Try (D -3)
   THEN Try (D -2)
   THEN D -1
   THEN Unfolds ``e-union e-isect`` 0
   THEN Unfold `e-type` 0
   THEN BLemma `quotient-member-eq`
   THEN Auto
   THEN ∀h:hyp. (UnfoldTop `ext-eq` h THEN D h)
   THEN D 0
   THEN (D 0 THENA Auto)
   THEN ∀h:hyp. D_b_union h
   THEN ∀h:hyp. Isect2HD h
   THEN Try (Isect2CD)
   THEN Try ((DoSubsume THEN Trivial))
   THEN Try (QuickAuto)
   THEN Try ((BUnionRight THEN QuickAuto))
   THEN Try ((BUnionLeft THEN QuickAuto))) }

1
1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. a : Base
4. a1 : Base
5. a = a1 ∈ (A,B:Type//A ≡ B)
6. a ∈ Type
7. a1 ∈ Type
8. a ⊆r a1
9. a1 ⊆r a
10. b : Base
11. b1 : Base
12. b = b1 ∈ (A,B:Type//A ≡ B)
13. b ∈ Type
14. b1 ∈ Type
15. b ⊆r b1
16. b1 ⊆r b
17. c : Base
18. c1 : Base
19. c = c1 ∈ (A,B:Type//A ≡ B)
20. c ∈ Type
21. c1 ∈ Type
22. c ⊆r c1
23. c1 ⊆r c
24. x : a ⋂ b ⋂ c
25. x ∈ b ⋂ c
26. x ∈ a
27. x ∈ c
28. x ∈ b
⊢ x ∈ a1 ⋂ b1

2
1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. a : Base
4. a1 : Base
5. a = a1 ∈ (A,B:Type//A ≡ B)
6. a ∈ Type
7. a1 ∈ Type
8. a ⊆r a1
9. a1 ⊆r a
10. b : Base
11. b1 : Base
12. b = b1 ∈ (A,B:Type//A ≡ B)
13. b ∈ Type
14. b1 ∈ Type
15. b ⊆r b1
16. b1 ⊆r b
17. c : Base
18. c1 : Base
19. c = c1 ∈ (A,B:Type//A ≡ B)
20. c ∈ Type
21. c1 ∈ Type
22. c ⊆r c1
23. c1 ⊆r c
24. x : a ⋂ b ⋂ c
25. x ∈ b ⋂ c
26. x ∈ a
27. x ∈ c
28. x ∈ b
⊢ x ∈ c1

3
1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. a : Base
4. a1 : Base
5. a = a1 ∈ (A,B:Type//A ≡ B)
6. a ∈ Type
7. a1 ∈ Type
8. a ⊆r a1
9. a1 ⊆r a
10. b : Base
11. b1 : Base
12. b = b1 ∈ (A,B:Type//A ≡ B)
13. b ∈ Type
14. b1 ∈ Type
15. b ⊆r b1
16. b1 ⊆r b
17. c : Base
18. c1 : Base
19. c = c1 ∈ (A,B:Type//A ≡ B)
20. c ∈ Type
21. c1 ∈ Type
22. c ⊆r c1
23. c1 ⊆r c
24. x : a1 ⋂ b1 ⋂ c1
25. x ∈ c1
26. x ∈ a1 ⋂ b1
27. x ∈ b1
28. x ∈ a1
⊢ x ∈ b ⋂ c

4
1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. ∀[a,b,c:EType].  (e-isect(a;e-isect(b;c)) = e-isect(e-isect(a;b);c) ∈ EType)
4. a : Base
5. a1 : Base
6. a = a1 ∈ (A,B:Type//A ≡ B)
7. a ∈ Type
8. a1 ∈ Type
9. a ⊆r a1
10. a1 ⊆r a
11. b : Base
12. b1 : Base
13. b = b1 ∈ (A,B:Type//A ≡ B)
14. b ∈ Type
15. b1 ∈ Type
16. b ⊆r b1
17. b1 ⊆r b
18. c : Base
19. c1 : Base
20. c = c1 ∈ (A,B:Type//A ≡ B)
21. c ∈ Type
22. c1 ∈ Type
23. c ⊆r c1
24. c1 ⊆r c
25. a3 : a
⊢ a3 ∈ a1 ⋃ b1 ⋃ c1

5
1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. ∀[a,b,c:EType].  (e-isect(a;e-isect(b;c)) = e-isect(e-isect(a;b);c) ∈ EType)
4. a : Base
5. a1 : Base
6. a = a1 ∈ (A,B:Type//A ≡ B)
7. a ∈ Type
8. a1 ∈ Type
9. a ⊆r a1
10. a1 ⊆r a
11. b : Base
12. b1 : Base
13. b = b1 ∈ (A,B:Type//A ≡ B)
14. b ∈ Type
15. b1 ∈ Type
16. b ⊆r b1
17. b1 ⊆r b
18. c : Base
19. c1 : Base
20. c = c1 ∈ (A,B:Type//A ≡ B)
21. c ∈ Type
22. c1 ∈ Type
23. c ⊆r c1
24. c1 ⊆r c
25. a3 : b ⋃ c
⊢ a3 ∈ a1 ⋃ b1 ⋃ c1

6
1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. ∀[a,b,c:EType].  (e-isect(a;e-isect(b;c)) = e-isect(e-isect(a;b);c) ∈ EType)
4. a : Base
5. a1 : Base
6. a = a1 ∈ (A,B:Type//A ≡ B)
7. a ∈ Type
8. a1 ∈ Type
9. a ⊆r a1
10. a1 ⊆r a
11. b : Base
12. b1 : Base
13. b = b1 ∈ (A,B:Type//A ≡ B)
14. b ∈ Type
15. b1 ∈ Type
16. b ⊆r b1
17. b1 ⊆r b
18. c : Base
19. c1 : Base
20. c = c1 ∈ (A,B:Type//A ≡ B)
21. c ∈ Type
22. c1 ∈ Type
23. c ⊆r c1
24. c1 ⊆r c
25. a3 : a1 ⋃ b1
⊢ a3 ∈ a ⋃ b ⋃ c

7
1. ∀[a,b:EType].  (e-isect(a;b) = e-isect(b;a) ∈ EType)
2. ∀[a,b:EType].  (e-union(a;b) = e-union(b;a) ∈ EType)
3. ∀[a,b,c:EType].  (e-isect(a;e-isect(b;c)) = e-isect(e-isect(a;b);c) ∈ EType)
4. a : Base
5. a1 : Base
6. a = a1 ∈ (A,B:Type//A ≡ B)
7. a ∈ Type
8. a1 ∈ Type
9. a ⊆r a1
10. a1 ⊆r a
11. b : Base
12. b1 : Base
13. b = b1 ∈ (A,B:Type//A ≡ B)
14. b ∈ Type
15. b1 ∈ Type
16. b ⊆r b1
17. b1 ⊆r b
18. c : Base
19. c1 : Base
20. c = c1 ∈ (A,B:Type//A ≡ B)
21. c ∈ Type
22. c1 ∈ Type
23. c ⊆r c1
24. c1 ⊆r c
25. a3 : c1
⊢ a3 ∈ a ⋃ b ⋃ c

Latex:

Latex:
type-lattice\{i:l\}() \mmember{} bdd-lattice\{i':l\} By Latex: (ProveWfLemma THEN Try (D -3) THEN Try (D -2) THEN D -1 THEN Unfolds ``e-union e-isect`` 0 THEN Unfold `e-type` 0 THEN BLemma `quotient-member-eq` THEN Auto THEN \mforall{}h:hyp. (UnfoldTop `ext-eq` h THEN D h) THEN D 0 THEN (D 0 THENA Auto) THEN \mforall{}h:hyp. D\_b\_union h THEN \mforall{}h:hyp. Isect2HD h THEN Try (Isect2CD) THEN Try ((DoSubsume THEN Trivial)) THEN Try (QuickAuto) THEN Try ((BUnionRight THEN QuickAuto)) THEN Try ((BUnionLeft THEN QuickAuto))) Home Index