Step
*
3
1
2
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
((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
⇒ (∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))))
11. x : X List@i
12. u : X List@i
13. v : X List@i
14. (u ∈ as)
15. (v ∈ a1)
16. x = (u @ v) ∈ (X List)
17. y1 : X List
18. (y1 ∈ bs)
19. l_subset(X;y1;u)
20. y : X List
21. (y ∈ b1)
22. l_subset(X;y;v)
23. ∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ ((y @ y1) = (u @ v) ∈ (X List)))
⊢ l_subset(X;y @ y1;u @ v)
BY
{ (BLemma `l_subset_append` 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
((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
⇒ (∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))))
11. x : X List@i
12. u : X List@i
13. v : X List@i
14. (u ∈ as)
15. (v ∈ a1)
16. x = (u @ v) ∈ (X List)
17. y1 : X List
18. (y1 ∈ bs)
19. l_subset(X;y1;u)
20. y : X List
21. (y ∈ b1)
22. l_subset(X;y;v)
23. ∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ ((y @ y1) = (u @ v) ∈ (X List)))
⊢ l_subset(X;y;u @ v)
2
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
((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
⇒ (∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))))
11. x : X List@i
12. u : X List@i
13. v : X List@i
14. (u ∈ as)
15. (v ∈ a1)
16. x = (u @ v) ∈ (X List)
17. y1 : X List
18. (y1 ∈ bs)
19. l_subset(X;y1;u)
20. y : X List
21. (y ∈ b1)
22. l_subset(X;y;v)
23. ∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ ((y @ y1) = (u @ v) ∈ (X List)))
24. l_subset(X;y;u @ v)
⊢ l_subset(X;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. \mforall{}x:X List
((\mexists{}u,v:X List. ((u \mmember{} b1) \mwedge{} (v \mmember{} bs) \mwedge{} (x = (u @ v))))
{}\mRightarrow{} (\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))))
11. x : X List@i
12. u : X List@i
13. v : X List@i
14. (u \mmember{} as)
15. (v \mmember{} a1)
16. x = (u @ v)
17. y1 : X List
18. (y1 \mmember{} bs)
19. l\_subset(X;y1;u)
20. y : X List
21. (y \mmember{} b1)
22. l\_subset(X;y;v)
23. \mexists{}u,v:X List. ((u \mmember{} b1) \mwedge{} (v \mmember{} bs) \mwedge{} ((y @ y1) = (u @ v)))
\mvdash{} l\_subset(X;y @ y1;u @ v)
By
Latex:
(BLemma `l\_subset\_append` THEN Auto)
Home
Index