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