---

Step * 4 2 1 of Lemma sorted-by-append


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. as : T List
4. bs : T List
5. ∀i:ℕ||as||. ∀j:ℕi.  (R as[j] as[i])
6. ∀i:ℕ||bs||. ∀j:ℕi.  (R bs[j] bs[i])
7. (∀a∈as.(∀b∈bs.R a b))
8. i : ℕ||as @ bs||
9. j : ℕi
10. ¬i < ||as||
11. j < ||as||
⊢ R as @ bs[j] as @ bs[i]
BY
{ ((RW (AddrC [1;2] (LemmaC `select_append_front`)) 0 THEN Auto') THEN RWO  "select_append_back" 0 THEN Auto') }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  as  :  T  List
4.  bs  :  T  List
5.  \mforall{}i:\mBbbN{}||as||.  \mforall{}j:\mBbbN{}i.    (R  as[j]  as[i])
6.  \mforall{}i:\mBbbN{}||bs||.  \mforall{}j:\mBbbN{}i.    (R  bs[j]  bs[i])
7.  (\mforall{}a\mmember{}as.(\mforall{}b\mmember{}bs.R  a  b))
8.  i  :  \mBbbN{}||as  @  bs||
9.  j  :  \mBbbN{}i
10.  \mneg{}i  <  ||as||
11.  j  <  ||as||
\mvdash{}  R  as  @  bs[j]  as  @  bs[i]


By

---

Latex:
((RW  (AddrC  [1;2]  (LemmaC  `select\_append\_front`))  0  THEN  Auto')
  THEN  RWO    "select\_append\_back"  0
  THEN  Auto')

---

Home Index