---

Step * 1 1 of Lemma append_interleaving


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)
BY
{ (Unfold `disjoint_sublists` 0 THEN (InstConcl [λx.x; λx.(x + ||L1||)] THEN Reduce 0) THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `disjoint\_sublists`  0  THEN  (InstConcl  [\mlambda{}x.x;  \mlambda{}x.(x  +  ||L1||)]  THEN  Reduce  0)  THEN  Auto')

---

Home Index