---

Step * 1 1 2 of Lemma interleaving_split


1. [T] : Type
2. L : T List
3. [P] : ℕ||L|| ⟶ ℙ
4. ∀x:ℕ||L||. Dec(P x)
5. n : ℕ
6. k : ℕ
7. f : ℕn ⟶ ℕ||L||
8. g : ℕk ⟶ ℕ||L||
9. increasing(f;n)
10. increasing(g;k)
11. ∀i:ℕn. (P (f i))
12. ∀j:ℕk. (¬(P (g j)))
13. ∀i:ℕ||L||. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
14. L2 : T List
15. ||L2|| = n ∈ ℤ
16. sublist_occurence(T;L2;L;f)
17. L1 : T List
18. ||L1|| = k ∈ ℤ
19. sublist_occurence(T;L1;L;g)
20. interleaving_occurence(T;L2;L1;L;f;g)
⊢ interleaving_occurence(T;L2;L1;L;f;g)
∧ ((∀i:ℕ||L2||. (P (f i))) ∧ (∀i:ℕ||L1||. (¬(P (g i)))))
∧ (∀i:ℕ||L||. (((P i) ⇒ (∃j:ℕ||L2||. ((f j) = i ∈ ℤ))) ∧ ∃j:ℕ||L1||. ((g j) = i ∈ ℤ) supposing ¬(P i)))
BY
{ TACTIC:(D 0 THEN Auto) }

1
1. [T] : Type
2. L : T List
3. [P] : ℕ||L|| ⟶ ℙ
4. ∀x:ℕ||L||. Dec(P x)
5. n : ℕ
6. k : ℕ
7. f : ℕn ⟶ ℕ||L||
8. g : ℕk ⟶ ℕ||L||
9. increasing(f;n)
10. increasing(g;k)
11. ∀i:ℕn. (P (f i))
12. ∀j:ℕk. (¬(P (g j)))
13. ∀i:ℕ||L||. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
14. L2 : T List
15. ||L2|| = n ∈ ℤ
16. sublist_occurence(T;L2;L;f)
17. L1 : T List
18. ||L1|| = k ∈ ℤ
19. sublist_occurence(T;L1;L;g)
20. interleaving_occurence(T;L2;L1;L;f;g)
21. ∀i:ℕ||L2||. (P (f i))
22. ∀i:ℕ||L1||. (¬(P (g i)))
23. i : ℕ||L||
24. P i
⊢ ∃j:ℕ||L2||. ((f j) = i ∈ ℤ)

2
1. [T] : Type
2. L : T List
3. [P] : ℕ||L|| ⟶ ℙ
4. ∀x:ℕ||L||. Dec(P x)
5. n : ℕ
6. k : ℕ
7. f : ℕn ⟶ ℕ||L||
8. g : ℕk ⟶ ℕ||L||
9. increasing(f;n)
10. increasing(g;k)
11. ∀i:ℕn. (P (f i))
12. ∀j:ℕk. (¬(P (g j)))
13. ∀i:ℕ||L||. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
14. L2 : T List
15. ||L2|| = n ∈ ℤ
16. sublist_occurence(T;L2;L;f)
17. L1 : T List
18. ||L1|| = k ∈ ℤ
19. sublist_occurence(T;L1;L;g)
20. interleaving_occurence(T;L2;L1;L;f;g)
21. ∀i:ℕ||L2||. (P (f i))
22. ∀i:ℕ||L1||. (¬(P (g i)))
23. i : ℕ||L||
24. (P i) ⇒ (∃j:ℕ||L2||. ((f j) = i ∈ ℤ))
25. ¬(P i)
⊢ ∃j:ℕ||L1||. ((g j) = i ∈ ℤ)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  [P]  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:\mBbbN{}||L||.  Dec(P  x)
5.  n  :  \mBbbN{}
6.  k  :  \mBbbN{}
7.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}||L||
8.  g  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}||L||
9.  increasing(f;n)
10.  increasing(g;k)
11.  \mforall{}i:\mBbbN{}n.  (P  (f  i))
12.  \mforall{}j:\mBbbN{}k.  (\mneg{}(P  (g  j)))
13.  \mforall{}i:\mBbbN{}||L||.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j))))
14.  L2  :  T  List
15.  ||L2||  =  n
16.  sublist\_occurence(T;L2;L;f)
17.  L1  :  T  List
18.  ||L1||  =  k
19.  sublist\_occurence(T;L1;L;g)
20.  interleaving\_occurence(T;L2;L1;L;f;g)
\mvdash{}  interleaving\_occurence(T;L2;L1;L;f;g)
\mwedge{}  ((\mforall{}i:\mBbbN{}||L2||.  (P  (f  i)))  \mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  (\mneg{}(P  (g  i)))))
\mwedge{}  (\mforall{}i:\mBbbN{}||L||.  (((P  i)  {}\mRightarrow{}  (\mexists{}j:\mBbbN{}||L2||.  ((f  j)  =  i)))  \mwedge{}  \mexists{}j:\mBbbN{}||L1||.  ((g  j)  =  i)  supposing  \mneg{}(P  i)))


By

---

Latex:
TACTIC:(D  0  THEN  Auto)

---

Home Index