---

Step * 1 1 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)
12. permutation(T;[u] @ A;A @ [u])
⊢ permutation(T;(A @ [u]) @ v;B @ [u / v])
BY
{ ((RWO "append_assoc" 0 THENA Auto) THEN Reduce 0) }

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


By

---

Latex:
((RWO  "append\_assoc"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index