---

Step * 1 of Lemma comparison-sort-permutation


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])
BY
{ (InstLemma `permutation-rotate` [⌜T⌝;⌜[u]⌝;⌜A⌝]⋅ THENA 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)
12. permutation(T;[u] @ A;A @ [u])
⊢ permutation(T;([u] @ A) @ v;B @ [u / v])

---

Latex:

---

Latex:

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.  \mforall{}A,B:T  List.
          (permutation(T;A;B)
          {}\mRightarrow{}  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)
\mvdash{}  permutation(T;([u]  @  A)  @  v;B  @  [u  /  v])


By

---

Latex:
(InstLemma  `permutation-rotate`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}[u]\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index