---

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


1. T : Type
2. T
3. R : T ⟶ T ⟶ ℙ
4. ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
5. ∀f:ℕ ⟶ T. (↓∃m:ℕ. ∃n:ℕm. (¬R[f n;f m]))
6. alpha : {f:ℕ ⟶ (T?)| ∀x:ℕ. ((0 < x ∧ (↑isl(f x))) ⇒ ((↑isl(f (x - 1))) ∧ (R outl(f (x - 1)) outl(f x))))} @i
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))
BY
{ TACTIC:(RenameVar `t' 2
          THEN D -1
          THEN (With ⌜λn.case alpha n of inl(x) => x | inr(x) => t⌝ (D 5)⋅ THENA Auto)
          THEN Reduce (-1)
          THEN RepeatFor 2 (D -1)) }

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. (¬R[case alpha n of inl(x) => x | inr(x) => t;case alpha m of inl(x) => x | inr(x) => t])
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  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.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}m.  (\mneg{}R[f  n;f  m]))
6.  alpha  :  \{f:\mBbbN{}  {}\mrightarrow{}  (T?)| 
                        \mforall{}x:\mBbbN{}.  ((0  <  x  \mwedge{}  (\muparrow{}isl(f  x)))  {}\mRightarrow{}  ((\muparrow{}isl(f  (x  -  1)))  \mwedge{}  (R  outl(f  (x  -  1))  outl(f  x))))\}  @i
\mvdash{}  \mdownarrow{}\mexists{}m:\mBbbN{}.  (0  <  m  \mwedge{}  (\muparrow{}isr(alpha  (m  -  1))))


By

---

Latex:
TACTIC:(RenameVar  `t'  2
                THEN  D  -1
                THEN  (With  \mkleeneopen{}\mlambda{}n.case  alpha  n  of  inl(x)  =>  x  |  inr(x)  =>  t\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto)
                THEN  Reduce  (-1)
                THEN  RepeatFor  2  (D  -1))

---

Home Index