---

Step * of Lemma append_overlapping_sublists

No Annotations
∀[T:Type]. ∀L1,L2,L:T List. ∀x:T.  L1 @ [x] ⊆ L ⇒ [x / L2] ⊆ L ⇒ L1 @ [x / L2] ⊆ L supposing no_repeats(T;L)
BY
{ (((Auto THEN All (Unfolds ``sublist no_repeats``)) THEN All Reduce) THEN ExRepD) }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
7. f1 : ℕ||L1 @ [x]|| ⟶ ℕ||L||
8. increasing(f1;||L1 @ [x]||)
9. ∀j:ℕ||L1 @ [x]||. (L1 @ [x][j] = L[f1 j] ∈ T)
10. f : ℕ||L2|| + 1 ⟶ ℕ||L||
11. increasing(f;||L2|| + 1)
12. ∀j:ℕ||L2|| + 1. ([x / L2][j] = L[f j] ∈ T)
⊢ ∃f:ℕ||L1 @ [x / L2]|| ⟶ ℕ||L||
   (increasing(f;||L1 @ [x / L2]||) ∧ (∀j:ℕ||L1 @ [x / L2]||. (L1 @ [x / L2][j] = L[f j] ∈ T)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}L1,L2,L:T  List.  \mforall{}x:T.
        L1  @  [x]  \msubseteq{}  L  {}\mRightarrow{}  [x  /  L2]  \msubseteq{}  L  {}\mRightarrow{}  L1  @  [x  /  L2]  \msubseteq{}  L  supposing  no\_repeats(T;L)


By

---

Latex:
(((Auto  THEN  All  (Unfolds  ``sublist  no\_repeats``))  THEN  All  Reduce)  THEN  ExRepD)

---

Home Index