---

Step * 1 1 2 1 1 1 1 1 1 of Lemma cWO-rel-path-barred

.....assertion..... 
1. T : Type
2. t : T
3. R : T ⟶ T ⟶ ℙ
4. ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
5. alpha : ℕ ⟶ (T?)@i
6. ∀x:ℕ. ((0 < x ∧ (↑isl(alpha x))) ⇒ ((↑isl(alpha (x - 1))) ∧ (R outl(alpha (x - 1)) outl(alpha x))))
7. m : ℕ@i
8. n : ℕm@i
9. ∀i:ℕm + 2. (0 < i ⇒ (↑isl(alpha (i - 1))))
10. x : T@i
11. (alpha n) = (inl x) ∈ (T?)
12. x1 : T@i
13. (alpha m) = (inl x1) ∈ (T?)
⊢ ∀d,n:ℕ.  (n < m ⇒ ((m - n) ≤ d) ⇒ (R outl(alpha n) outl(alpha m)))
BY
{ (Assert ∀i:ℕm + 1. (↑isl(alpha i)) BY
         ((D 0 THENA Auto) THEN InstHyp [⌜i + 1⌝] 9⋅ THEN Auto THEN RW IntNormC (-1) THEN Auto)) }

1
1. T : Type
2. t : T
3. R : T ⟶ T ⟶ ℙ
4. ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
5. alpha : ℕ ⟶ (T?)@i
6. ∀x:ℕ. ((0 < x ∧ (↑isl(alpha x))) ⇒ ((↑isl(alpha (x - 1))) ∧ (R outl(alpha (x - 1)) outl(alpha x))))
7. m : ℕ@i
8. n : ℕm@i
9. ∀i:ℕm + 2. (0 < i ⇒ (↑isl(alpha (i - 1))))
10. x : T@i
11. (alpha n) = (inl x) ∈ (T?)
12. x1 : T@i
13. (alpha m) = (inl x1) ∈ (T?)
14. ∀i:ℕm + 1. (↑isl(alpha i))
⊢ ∀d,n:ℕ.  (n < m ⇒ ((m - n) ≤ d) ⇒ (R outl(alpha n) outl(alpha m)))

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  t  :  T
3.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}a,b,c:T.    (R[a;b]  {}\mRightarrow{}  R[b;c]  {}\mRightarrow{}  R[a;c])
5.  alpha  :  \mBbbN{}  {}\mrightarrow{}  (T?)@i
6.  \mforall{}x:\mBbbN{}
          ((0  <  x  \mwedge{}  (\muparrow{}isl(alpha  x)))  {}\mRightarrow{}  ((\muparrow{}isl(alpha  (x  -  1)))  \mwedge{}  (R  outl(alpha  (x  -  1))  outl(alpha  x))))
7.  m  :  \mBbbN{}@i
8.  n  :  \mBbbN{}m@i
9.  \mforall{}i:\mBbbN{}m  +  2.  (0  <  i  {}\mRightarrow{}  (\muparrow{}isl(alpha  (i  -  1))))
10.  x  :  T@i
11.  (alpha  n)  =  (inl  x)
12.  x1  :  T@i
13.  (alpha  m)  =  (inl  x1)
\mvdash{}  \mforall{}d,n:\mBbbN{}.    (n  <  m  {}\mRightarrow{}  ((m  -  n)  \mleq{}  d)  {}\mRightarrow{}  (R  outl(alpha  n)  outl(alpha  m)))


By

---

Latex:
(Assert  \mforall{}i:\mBbbN{}m  +  1.  (\muparrow{}isl(alpha  i))  BY
              ((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  9\mcdot{}  THEN  Auto  THEN  RW  IntNormC  (-1)  THEN  Auto))

---

Home Index