---

Step * of Lemma sorted-seq-iff

No Annotations
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀s:sequence(T). (Trans(T;x,y.R[x;y]) ⇒ (sorted-seq(x,y.R[x;y];s) ⇐⇒ ∀i:ℕ||s|| - 1. R[s[i];s[i + 1]]))
BY
{ (Auto THEN UnfoldTopAb 0) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. s : sequence(T)
4. Trans(T;x,y.R[x;y])
5. ∀i:ℕ||s|| - 1. R[s[i];s[i + 1]]
⊢ ∀i,j:ℕ||s||.  (i < j ⇒ R[s[i];s[j]])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}s:sequence(T)
        (Trans(T;x,y.R[x;y])  {}\mRightarrow{}  (sorted-seq(x,y.R[x;y];s)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}||s||  -  1.  R[s[i];s[i  +  1]]))


By

---

Latex:
(Auto  THEN  UnfoldTopAb  0)

---

Home Index