---

Step * of Lemma sorted-by-append

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀as,bs:T List.  (sorted-by(R;as @ bs) ⇐⇒ sorted-by(R;as) ∧ sorted-by(R;bs) ∧ (∀a∈as.(∀b∈bs.R a b)))
BY
{ (Unfold `sorted-by` 0 THEN Reduce 0 THEN Auto THEN Reduce 0 THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. as : T List
4. bs : T List
5. ∀i:ℕ||as @ bs||. ∀j:ℕi.  (R as @ bs[j] as @ bs[i])
6. i : ℕ||as||
7. j : ℕi
⊢ R as[j] as[i]

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. as : T List
4. bs : T List
5. ∀i:ℕ||as @ bs||. ∀j:ℕi.  (R as @ bs[j] as @ bs[i])
6. i : ℕ||bs||
7. j : ℕi
⊢ R bs[j] bs[i]

3
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. as : T List
4. bs : T List
5. ∀i:ℕ||as @ bs||. ∀j:ℕi.  (R as @ bs[j] as @ bs[i])
⊢ (∀a∈as.(∀b∈bs.R a b))

4
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]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}as,bs:T  List.
        (sorted-by(R;as  @  bs)  \mLeftarrow{}{}\mRightarrow{}  sorted-by(R;as)  \mwedge{}  sorted-by(R;bs)  \mwedge{}  (\mforall{}a\mmember{}as.(\mforall{}b\mmember{}bs.R  a  b)))


By

---

Latex:
(Unfold  `sorted-by`  0  THEN  Reduce  0  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index