---

Step * of Lemma interleaving_occurence_onto

∀[A:Type]
  ∀L,L1,L2:A List. ∀f1:ℕ||L1|| ⟶ ℕ||L||. ∀f2:ℕ||L2|| ⟶ ℕ||L||.
    ∀j:ℕ||L||. ((∃k:ℕ||L1||. (j = (f1 k) ∈ ℤ)) ∨ (∃k:ℕ||L2||. (j = (f2 k) ∈ ℤ))) 
    supposing interleaving_occurence(A;L1;L2;L;f1;f2)
BY
{ ((Auto THEN AllHyps (Unfold `interleaving_occurence`)) THEN ExRepD) }

1
1. [A] : Type
2. L : A List
3. L1 : A List
4. L2 : A List
5. f1 : ℕ||L1|| ⟶ ℕ||L||
6. f2 : ℕ||L2|| ⟶ ℕ||L||
7. ||L|| = (||L1|| + ||L2||) ∈ ℕ
8. increasing(f1;||L1||)
9. ∀j:ℕ||L1||. (L1[j] = L[f1 j] ∈ A)
10. increasing(f2;||L2||)
11. ∀j:ℕ||L2||. (L2[j] = L[f2 j] ∈ A)
12. ∀j1:ℕ||L1||. ∀j2:ℕ||L2||.  (¬((f1 j1) = (f2 j2) ∈ ℤ))
13. j : ℕ||L||
⊢ (∃k:ℕ||L1||. (j = (f1 k) ∈ ℤ)) ∨ (∃k:ℕ||L2||. (j = (f2 k) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}L,L1,L2:A  List.  \mforall{}f1:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L||.  \mforall{}f2:\mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L||.
        \mforall{}j:\mBbbN{}||L||.  ((\mexists{}k:\mBbbN{}||L1||.  (j  =  (f1  k)))  \mvee{}  (\mexists{}k:\mBbbN{}||L2||.  (j  =  (f2  k)))) 
        supposing  interleaving\_occurence(A;L1;L2;L;f1;f2)


By

---

Latex:
((Auto  THEN  AllHyps  (Unfold  `interleaving\_occurence`))  THEN  ExRepD)

---

Home Index