---

Step * 3 1 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)
22. ∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ ((y @ y1) = (u @ v) ∈ (X List)))
⊢ l_subset(X;y @ y1;x)
BY
{ (SubstFor ⌜x⌝ 0⋅ 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;u @ v)

---

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)
22.  \mexists{}u,v:X  List.  ((u  \mmember{}  as)  \mwedge{}  (v  \mmember{}  a1)  \mwedge{}  ((y  @  y1)  =  (u  @  v)))
\mvdash{}  l\_subset(X;y  @  y1;x)


By

---

Latex:
(SubstFor  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index