---

Step * 1 of Lemma insert-no-combine-permutation


1. T : Type
2. cmp : comparison(T)
3. u : T
4. v : T List
5. ∀u:T. permutation(T;insert-no-combine(cmp;u;v);[u] @ v)
6. u@0 : T
7. ¬(0 ≤ (cmp u@0 u))
⊢ permutation(T;[u; [u@0 / v]];[u@0; [u / v]])
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}u:T.  permutation(T;insert-no-combine(cmp;u;v);[u]  @  v)
6.  u@0  :  T
7.  \mneg{}(0  \mleq{}  (cmp  u@0  u))
\mvdash{}  permutation(T;[u;  [u@0  /  v]];[u@0;  [u  /  v]])


By

---

Latex:
Auto

---

Home Index