---

Step * of Lemma comparison-sort-permutation

∀T:Type. (valueall-type(T) ⇒ (∀cmp:comparison(T). ∀L:T List.  permutation(T;comparison-sort(cmp;L);L)))
BY
{ (Auto
   THEN Unfold `comparison-sort` 0
   THEN (Assert ⌜∀L,A,B:T List.
                   (permutation(T;A;B) ⇒ permutation(T;eager-accum(srtd,x.insert-no-combine(cmp;x;srtd);A;L);B @ L))⌝⋅
   THENM (InstHyp [⌜L⌝;⌜[]⌝;⌜[]⌝] (-1)⋅ THEN Auto)
   )
   THEN InductionOnList
   THEN Auto
   THEN RWW "append-nil" 0
   THEN Auto
   THEN (RecUnfold `eager-accum` 0 THEN Reduce 0)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstHyp [⌜insert-no-combine(cmp;u;A)⌝;⌜[u] @ A⌝] (-4)⋅ THENM RWO "-1" 0)
   THEN Auto) }

1
1. T : Type@i'
2. valueall-type(T)@i
3. cmp : comparison(T)@i
4. L : T List@i
5. u : T@i
6. v : T List@i
7. ∀A,B:T List.  (permutation(T;A;B) ⇒ permutation(T;eager-accum(srtd,x.insert-no-combine(cmp;x;srtd);A;v);B @ v))@i
8. A : T List@i
9. B : T List@i
10. permutation(T;A;B)@i
11. permutation(T;eager-accum(srtd,x.insert-no-combine(cmp;x;srtd);insert-no-combine(cmp;u;A);v);([u] @ A) @ v)
⊢ permutation(T;([u] @ A) @ v;B @ [u / v])

---

Latex:

---

Latex:
\mforall{}T:Type
    (valueall-type(T)  {}\mRightarrow{}  (\mforall{}cmp:comparison(T).  \mforall{}L:T  List.    permutation(T;comparison-sort(cmp;L);L)))


By

---

Latex:
(Auto
  THEN  Unfold  `comparison-sort`  0
  THEN  (Assert  \mkleeneopen{}\mforall{}L,A,B:T  List.
                                  (permutation(T;A;B)
                                  {}\mRightarrow{}  permutation(T;eager-accum(srtd,x.insert-no-combine(cmp;x;srtd);A;L);B  @  L))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnList
  THEN  Auto
  THEN  RWW  "append-nil"  0
  THEN  Auto
  THEN  (RecUnfold  `eager-accum`  0  THEN  Reduce  0)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}insert-no-combine(cmp;u;A)\mkleeneclose{};\mkleeneopen{}[u]  @  A\mkleeneclose{}]  (-4)\mcdot{}  THENM  RWO  "-1"  0)
  THEN  Auto)

---

Home Index