---

Step * of Lemma disjoint_sublists_witness

∀[T:Type]
  ∀L1,L2,L:T List.
    (disjoint_sublists(T;L1;L2;L)
    ⇒ (∃f:ℕ||L1|| + ||L2|| ⟶ ℕ||L||
         (Inj(ℕ||L1|| + ||L2||;ℕ||L||;f)
         ∧ (∀i:ℕ||L1|| + ||L2||
              (L1[i] = L[f i] ∈ T supposing i < ||L1|| ∧ L2[i - ||L1||] = L[f i] ∈ T supposing ||L1|| ≤ i)))))
BY
{ ((Auto THEN Unfold `disjoint_sublists` (-1)) THEN ExRepD) }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. f1 : ℕ||L1|| ⟶ ℕ||L||
6. f2 : ℕ||L2|| ⟶ ℕ||L||
7. increasing(f1;||L1||)
8. ∀j:ℕ||L1||. (L1[j] = L[f1 j] ∈ T)
9. increasing(f2;||L2||)
10. ∀j:ℕ||L2||. (L2[j] = L[f2 j] ∈ T)
11. ∀j1:ℕ||L1||. ∀j2:ℕ||L2||.  (¬((f1 j1) = (f2 j2) ∈ ℤ))
⊢ ∃f:ℕ||L1|| + ||L2|| ⟶ ℕ||L||
   (Inj(ℕ||L1|| + ||L2||;ℕ||L||;f)
   ∧ (∀i:ℕ||L1|| + ||L2||
        (L1[i] = L[f i] ∈ T supposing i < ||L1|| ∧ L2[i - ||L1||] = L[f i] ∈ T supposing ||L1|| ≤ i)))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L1,L2,L:T  List.
        (disjoint\_sublists(T;L1;L2;L)
        {}\mRightarrow{}  (\mexists{}f:\mBbbN{}||L1||  +  ||L2||  {}\mrightarrow{}  \mBbbN{}||L||
                  (Inj(\mBbbN{}||L1||  +  ||L2||;\mBbbN{}||L||;f)
                  \mwedge{}  (\mforall{}i:\mBbbN{}||L1||  +  ||L2||
                            (L1[i]  =  L[f  i]  supposing  i  <  ||L1||
                            \mwedge{}  L2[i  -  ||L1||]  =  L[f  i]  supposing  ||L1||  \mleq{}  i)))))


By

---

Latex:
((Auto  THEN  Unfold  `disjoint\_sublists`  (-1))  THEN  ExRepD)

---

Home Index