---

Step * 1 of Lemma append_interleaving


1. [T] : Type
2. L1 : T List
3. L2 : T List
4. ||L1 @ L2|| = (||L1|| + ||L2||) ∈ ℕ
⊢ disjoint_sublists(T;L1;L2;L1 @ L2)
BY
{ (Assert increasing(λx.(x + ||L1||);||L2||) BY
         ((Unfold `increasing` 0 THEN Reduce 0) THEN Auto)) }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. ||L1 @ L2|| = (||L1|| + ||L2||) ∈ ℕ
5. increasing(λx.(x + ||L1||);||L2||)
⊢ disjoint_sublists(T;L1;L2;L1 @ L2)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  ||L1  @  L2||  =  (||L1||  +  ||L2||)
\mvdash{}  disjoint\_sublists(T;L1;L2;L1  @  L2)


By

---

Latex:
(Assert  increasing(\mlambda{}x.(x  +  ||L1||);||L2||)  BY
              ((Unfold  `increasing`  0  THEN  Reduce  0)  THEN  Auto))

---

Home Index