---

Step * 1 of Lemma sorted-seq-iff


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]])
BY
{ ((Assert ⌜∀d:ℕ. ∀i:ℕ||s||.  (i + d + 1 < ||s|| ⇒ R[s[i];s[i + d + 1]])⌝⋅
   THENM (Intros THEN (InstHyp [⌜j - i - 1⌝;⌜i⌝] (-4)⋅ THENA Auto) THEN Subst' i + (j - i - 1) + 1 ~ j -1 THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto) }

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]]
6. d : ℤ
7. [%3] : 0 < d
8. ∀i:ℕ||s||. (i + (d - 1) + 1 < ||s|| ⇒ R[s[i];s[i + (d - 1) + 1]])
9. i : ℕ||s||
10. i + d + 1 < ||s||
⊢ R[s[i];s[i + d + 1]]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  s  :  sequence(T)
4.  Trans(T;x,y.R[x;y])
5.  \mforall{}i:\mBbbN{}||s||  -  1.  R[s[i];s[i  +  1]]
\mvdash{}  \mforall{}i,j:\mBbbN{}||s||.    (i  <  j  {}\mRightarrow{}  R[s[i];s[j]])


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}i:\mBbbN{}||s||.    (i  +  d  +  1  <  ||s||  {}\mRightarrow{}  R[s[i];s[i  +  d  +  1]])\mkleeneclose{}\mcdot{}
  THENM  (Intros
                THEN  (InstHyp  [\mkleeneopen{}j  -  i  -  1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
                THEN  Subst'  i  +  (j  -  i  -  1)  +  1  \msim{}  j  -1
                THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto)

---

Home Index