Proof of Nuprl Lemma : free-dl

Step * 11 of Lemma free-dl_wf

1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. ∀[a,b:free-dl-type(X)]. (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)]. (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))

5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))

6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))

5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))

6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))

7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X))
9. ∀[a:free-dl-type(X)]. (free-dl-meet(a;[[]]) = a ∈ free-dl-type(X))
10. ∀[a:free-dl-type(X)]. (free-dl-join(a;[]) = a ∈ free-dl-type(X))
11. X List List ∈ Type
12. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
13. ∀as:X List List
      ((∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))))
14. X List List ∈ Type
15. ∀a1,b1:X List List.  (dlattice-eq(X;a1;b1) ∈ Type)
16. ∀a1:X List List
      ((∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))))
17. X List List ∈ Type
18. ∀a2,b2:X List List.  (dlattice-eq(X;a2;b2) ∈ Type)
19. ∀a2:X List List
      ((∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))))
20. as : X List List
21. bs : X List List
22. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
23. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
24. free-dl-type(X) = free-dl-type(X) ∈ Type
25. a1 : X List List
26. b1 : X List List
27. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
28. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
29. free-dl-type(X) = free-dl-type(X) ∈ Type
30. a2 : X List List
31. b2 : X List List
32. ∀x:X List. ((x ∈ b2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))
33. ∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ b2) ∧ l_subset(X;y;x))))
34. free-dl-type(X) = free-dl-type(X) ∈ Type
35. x : X List
36. u : X List
37. v : X List
38. (u ∈ bs)
39. (v ∈ b1)
40. x = (u @ v) ∈ (X List)

⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ ((v ∈ a1) ∨ (v ∈ a2)) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))

2
1. X : Type
2. EquivRel(X List List;as,bs.(∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))))
3. ∀[a,b:free-dl-type(X)]. (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)]. (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))

5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))

6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))

⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ ((v ∈ a1) ∨ (v ∈ a2)) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))

3
1. X : Type
2. EquivRel(X List List;as,bs.(∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))))
3. ∀[a,b:free-dl-type(X)]. (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)]. (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))

5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))

6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))

7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X))
9. ∀[a:free-dl-type(X)]. (free-dl-meet(a;[[]]) = a ∈ free-dl-type(X))
10. ∀[a:free-dl-type(X)]. (free-dl-join(a;[]) = a ∈ free-dl-type(X))
11. X List List ∈ Type
12. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
13. ∀as:X List List
      ((∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))))
14. X List List ∈ Type
15. ∀a1,b1:X List List.  (dlattice-eq(X;a1;b1) ∈ Type)
16. ∀a1:X List List
      ((∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))))
17. X List List ∈ Type
18. ∀a2,b2:X List List.  (dlattice-eq(X;a2;b2) ∈ Type)
19. ∀a2:X List List
      ((∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))))
20. as : X List List
21. bs : X List List
22. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
23. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
24. free-dl-type(X) = free-dl-type(X) ∈ Type
25. a1 : X List List
26. b1 : X List List
27. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
28. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
29. free-dl-type(X) = free-dl-type(X) ∈ Type
30. a2 : X List List
31. b2 : X List List
32. ∀x:X List. ((x ∈ b2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))
33. ∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ b2) ∧ l_subset(X;y;x))))
34. free-dl-type(X) = free-dl-type(X) ∈ Type
35. x : X List
36. u : X List
37. v : X List
38. (u ∈ as)
39. (v ∈ a1)
40. x = (u @ v) ∈ (X List)
⊢ ∃y:X List
   (((∃u,v:X List. ((u ∈ bs) ∧ (v ∈ b1) ∧ (y = (u @ v) ∈ (X List))))
   ∨ (∃u,v:X List. ((u ∈ bs) ∧ (v ∈ b2) ∧ (y = (u @ v) ∈ (X List)))))
   ∧ l_subset(X;y;x))

4
1. X : Type
2. EquivRel(X List List;as,bs.(∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))

5. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))

6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))

7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X))
9. ∀[a:free-dl-type(X)]. (free-dl-meet(a;[[]]) = a ∈ free-dl-type(X))
10. ∀[a:free-dl-type(X)]. (free-dl-join(a;[]) = a ∈ free-dl-type(X))
11. X List List ∈ Type
12. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
13. ∀as:X List List
      ((∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))))
14. X List List ∈ Type
15. ∀a1,b1:X List List.  (dlattice-eq(X;a1;b1) ∈ Type)
16. ∀a1:X List List
      ((∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))))
17. X List List ∈ Type
18. ∀a2,b2:X List List.  (dlattice-eq(X;a2;b2) ∈ Type)
19. ∀a2:X List List
      ((∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))))
20. as : X List List
21. bs : X List List
22. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
23. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
24. free-dl-type(X) = free-dl-type(X) ∈ Type
25. a1 : X List List
26. b1 : X List List
27. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
28. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
29. free-dl-type(X) = free-dl-type(X) ∈ Type
30. a2 : X List List
31. b2 : X List List
32. ∀x:X List. ((x ∈ b2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))
33. ∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ b2) ∧ l_subset(X;y;x))))
34. free-dl-type(X) = free-dl-type(X) ∈ Type
35. x : X List
36. u : X List
37. v : X List
38. (u ∈ as)
39. (v ∈ a2)
40. x = (u @ v) ∈ (X List)
⊢ ∃y:X List
   (((∃u,v:X List. ((u ∈ bs) ∧ (v ∈ b1) ∧ (y = (u @ v) ∈ (X List))))
   ∨ (∃u,v:X List. ((u ∈ bs) ∧ (v ∈ b2) ∧ (y = (u @ v) ∈ (X List)))))
   ∧ l_subset(X;y;x))

Latex:

Latex:
1. X : Type 2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs)) 3. \mforall{}[a,b:free-dl-type(X)]. (free-dl-meet(a;b) = free-dl-meet(b;a)) 4. \mforall{}[a,b:free-dl-type(X)]. (free-dl-join(a;b) = free-dl-join(b;a)) 5. \mforall{}[a,b,c:free-dl-type(X)]. (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c)) 6. \mforall{}[a,b,c:free-dl-type(X)]. (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c)) 7. \mforall{}[a,b:free-dl-type(X)]. (free-dl-join(a;free-dl-meet(a;b)) = a) 8. \mforall{}[a,b:free-dl-type(X)]. (free-dl-meet(a;free-dl-join(a;b)) = a) 9. \mforall{}[a:free-dl-type(X)]. (free-dl-meet(a;[[]]) = a) 10. \mforall{}[a:free-dl-type(X)]. (free-dl-join(a;[]) = a) 11. a : free-dl-type(X) 12. b : free-dl-type(X) 13. c : free-dl-type(X) \mvdash{} free-dl-meet(a;free-dl-join(b;c)) = free-dl-join(free-dl-meet(a;b);free-dl-meet(a;c)) By Latex: ((OnVar `a' newQuotientElim THENA Auto) THEN (OnVar `b' newQuotientElim THENA Auto) THEN (OnVar `c' newQuotientElim THENA Auto) THEN RepUR ``free-dl-join`` 0 THEN EqTypeCD THEN Auto THEN RepUR ``dlattice-eq`` 0 THEN (RWO "dlattice-order-iff" 0 THENA Auto) THEN (RWW "member-free-dl-meet member\_append" 0 THENA Auto) THEN \mforall{}h:hyp. (RepUR ``dlattice-eq`` h THEN (RWO "dlattice-order-iff" h THENA Auto)) THEN D 0 THEN (UnivCD THENA Auto) THEN ExRepD THEN SplitOrHyps THEN ExRepD) Home Index