---

Step * 3 1 1 1 of Lemma free-dl_wf


1. X : Type@i'
2. as : X List List@i
3. bs : X List List@i
4. a1 : X List List@i
5. b1 : X List List@i
6. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
7. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
8. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
9. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
10. x : X List@i
11. u : X List@i
12. v : X List@i
13. (u ∈ b1)
14. (v ∈ bs)
15. x = (u @ v) ∈ (X List)
16. y1 : X List
17. (y1 ∈ a1)
18. l_subset(X;y1;u)
19. y : X List
20. (y ∈ as)
21. l_subset(X;y;v)
⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))
BY
{ (D 0 With ⌜y @ y1⌝  THEN Auto) }

1
1. X : Type@i'
2. as : X List List@i
3. bs : X List List@i
4. a1 : X List List@i
5. b1 : X List List@i
6. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
7. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
8. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
9. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
10. x : X List@i
11. u : X List@i
12. v : X List@i
13. (u ∈ b1)
14. (v ∈ bs)
15. x = (u @ v) ∈ (X List)
16. y1 : X List
17. (y1 ∈ a1)
18. l_subset(X;y1;u)
19. y : X List
20. (y ∈ as)
21. l_subset(X;y;v)
22. ∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ ((y @ y1) = (u @ v) ∈ (X List)))
⊢ l_subset(X;y @ y1;x)

---

Latex:

---

Latex:

1.  X  :  Type@i'
2.  as  :  X  List  List@i
3.  bs  :  X  List  List@i
4.  a1  :  X  List  List@i
5.  b1  :  X  List  List@i
6.  \mforall{}x:X  List.  ((x  \mmember{}  bs)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x))))
7.  \mforall{}x:X  List.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  bs)  \mwedge{}  l\_subset(X;y;x))))
8.  \mforall{}x:X  List.  ((x  \mmember{}  b1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a1)  \mwedge{}  l\_subset(X;y;x))))
9.  \mforall{}x:X  List.  ((x  \mmember{}  a1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  b1)  \mwedge{}  l\_subset(X;y;x))))
10.  x  :  X  List@i
11.  u  :  X  List@i
12.  v  :  X  List@i
13.  (u  \mmember{}  b1)
14.  (v  \mmember{}  bs)
15.  x  =  (u  @  v)
16.  y1  :  X  List
17.  (y1  \mmember{}  a1)
18.  l\_subset(X;y1;u)
19.  y  :  X  List
20.  (y  \mmember{}  as)
21.  l\_subset(X;y;v)
\mvdash{}  \mexists{}y:X  List.  ((\mexists{}u,v:X  List.  ((u  \mmember{}  as)  \mwedge{}  (v  \mmember{}  a1)  \mwedge{}  (y  =  (u  @  v))))  \mwedge{}  l\_subset(X;y;x))


By

---

Latex:
(D  0  With  \mkleeneopen{}y  @  y1\mkleeneclose{}    THEN  Auto)

---

Home Index