---

Step * 1 1 1 1 2 1 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. increasing(f;||L2||)
17. ∀j:ℕ||L2||. (L2[j] = L[f j] ∈ T)
18. L1 : T List
19. ||L1|| = k ∈ ℤ
20. increasing(g;||L1||)
21. ∀j:ℕ||L1||. (L1[j] = L[g j] ∈ T)
22. ∀j1:ℕ||L2||. ∀j2:ℕ||L1||.  (¬((f j1) = (g j2) ∈ ℤ))
⊢ ||L|| = (||L2|| + ||L1||) ∈ ℕ
BY
{ (Using [`f',f;`g',g] (BackThruLemma `disjoint_increasing_onto`) 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. increasing(f;||L2||)
17. ∀j:ℕ||L2||. (L2[j] = L[f j] ∈ T)
18. L1 : T List
19. ||L1|| = k ∈ ℤ
20. increasing(g;||L1||)
21. ∀j:ℕ||L1||. (L1[j] = L[g j] ∈ T)
22. ∀j1:ℕ||L2||. ∀j2:ℕ||L1||.  (¬((f j1) = (g j2) ∈ ℤ))
23. i : ℕ||L||
⊢ (∃j:ℕ||L2||. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕ||L1||. (i = (g j) ∈ ℤ))

---

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.  increasing(f;||L2||)
17.  \mforall{}j:\mBbbN{}||L2||.  (L2[j]  =  L[f  j])
18.  L1  :  T  List
19.  ||L1||  =  k
20.  increasing(g;||L1||)
21.  \mforall{}j:\mBbbN{}||L1||.  (L1[j]  =  L[g  j])
22.  \mforall{}j1:\mBbbN{}||L2||.  \mforall{}j2:\mBbbN{}||L1||.    (\mneg{}((f  j1)  =  (g  j2)))
\mvdash{}  ||L||  =  (||L2||  +  ||L1||)


By

---

Latex:
(Using  [`f',f;`g',g]  (BackThruLemma  `disjoint\_increasing\_onto`)  THEN  Auto')

---

Home Index