---

Step * 4 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
⊢ R as @ bs[j] as @ bs[i]
BY
{ (Decide ⌜i < ||as||⌝⋅ THENA Auto) }

1
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||
⊢ R as @ bs[j] as @ bs[i]

2
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||
⊢ R as @ bs[j] as @ bs[i]

---

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
\mvdash{}  R  as  @  bs[j]  as  @  bs[i]


By

---

Latex:
(Decide  \mkleeneopen{}i  <  ||as||\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index