---

Step * of Lemma interleaving_singleton

No Annotations
∀[T:Type]
  ∀L:T List. ∀i:ℕ||L||.
    ∃L2:T List
     ∃f1:ℕ1 ⟶ ℕ||L||. ∃f2:ℕ||L2|| ⟶ ℕ||L||. (interleaving_occurence(T;[L[i]];L2;L;f1;f2) ∧ ((f1 0) = i ∈ ℤ))
BY
{ ((((Auto THEN InstLemma `interleaving_split` [T;L;λj.(j = i ∈ ℤ)]) THENA ((Auto THEN Reduce 0) THEN Auto))
    THEN Reduce (-1)
    )
   THEN ExRepD
   ) }

1
1. [T] : Type
2. L : T List@i
3. i : ℕ||L||@i
4. L1 : T List
5. L2 : T List
6. f1 : ℕ||L1|| ⟶ ℕ||L||
7. f2 : ℕ||L2|| ⟶ ℕ||L||
8. interleaving_occurence(T;L1;L2;L;f1;f2)
9. ∀i@0:ℕ||L1||. ((f1 i@0) = i ∈ ℤ)
10. ∀i@0:ℕ||L2||. (¬((f2 i@0) = i ∈ ℤ))
11. ∀i@0:ℕ||L||
      (((i@0 = i ∈ ℤ) ⇒ (∃j:ℕ||L1||. ((f1 j) = i@0 ∈ ℤ))) ∧ ∃j:ℕ||L2||. ((f2 j) = i@0 ∈ ℤ) supposing ¬(i@0 = i ∈ ℤ))
⊢ ∃L2:T List. ∃f1:ℕ1 ⟶ ℕ||L||. ∃f2:ℕ||L2|| ⟶ ℕ||L||. (interleaving_occurence(T;[L[i]];L2;L;f1;f2) ∧ ((f1 0) = i ∈ ℤ))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}i:\mBbbN{}||L||.
        \mexists{}L2:T  List
          \mexists{}f1:\mBbbN{}1  {}\mrightarrow{}  \mBbbN{}||L||
            \mexists{}f2:\mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L||.  (interleaving\_occurence(T;[L[i]];L2;L;f1;f2)  \mwedge{}  ((f1  0)  =  i))


By

---

Latex:
((((Auto  THEN  InstLemma  `interleaving\_split`  [T;L;\mlambda{}j.(j  =  i)])
      THENA  ((Auto  THEN  Reduce  0)  THEN  Auto)
      )
    THEN  Reduce  (-1)
    )
  THEN  ExRepD
  )

---

Home Index