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