---

Step * of Lemma interleaving_implies_occurence

∀[T:Type]
  ∀L1,L2,L:T List.
    (interleaving(T;L1;L2;L) ⇒ (∃f1:ℕ||L1|| ⟶ ℕ||L||. ∃f2:ℕ||L2|| ⟶ ℕ||L||. interleaving_occurence(T;L1;L2;L;f1;f2)))
BY
{ ((((((Auto THEN All (Unfolds ``interleaving interleaving_occurence``)) THEN All (Unfold `disjoint_sublists`))
      THEN ExRepD
      )
     THEN InstConcl [f1;f2]
     )
    THENA Auto'
    )
   THEN SimpConcl
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L1,L2,L:T  List.
        (interleaving(T;L1;L2;L)
        {}\mRightarrow{}  (\mexists{}f1:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L||.  \mexists{}f2:\mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L||.  interleaving\_occurence(T;L1;L2;L;f1;f2)))


By

---

Latex:
((((((Auto  THEN  All  (Unfolds  ``interleaving  interleaving\_occurence``))
          THEN  All  (Unfold  `disjoint\_sublists`)
          )
        THEN  ExRepD
        )
      THEN  InstConcl  [f1;f2]
      )
    THENA  Auto'
    )
  THEN  SimpConcl
  )

---

Home Index