---

Step * of Lemma insert-no-combine-permutation

∀T:Type. ∀cmp:comparison(T). ∀L:T List. ∀u:T.  permutation(T;insert-no-combine(cmp;u;L);[u] @ L)
BY
{ (InductionOnList
   THEN Auto
   THEN Unfold `insert-no-combine` 0
   THEN Reduce 0
   THEN Try (Fold `insert-no-combine` 0)
   THEN Auto
   THEN AutoSplit
   THEN RWO "-3" 0
   THEN Auto
   THEN Reduce 0) }

1
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]])

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}cmp:comparison(T).  \mforall{}L:T  List.  \mforall{}u:T.    permutation(T;insert-no-combine(cmp;u;L);[u]  @  L)


By

---

Latex:
(InductionOnList
  THEN  Auto
  THEN  Unfold  `insert-no-combine`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `insert-no-combine`  0)
  THEN  Auto
  THEN  AutoSplit
  THEN  RWO  "-3"  0
  THEN  Auto
  THEN  Reduce  0)

---

Home Index