---

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


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])
9. ¬(∃m:ℕm + 2. (0 < m ∧ (↑isr(alpha (m - 1)))))
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))
BY
{ TACTIC:(Assert ∀i:ℕm + 2. (0 < i ⇒ (↑isl(alpha (i - 1)))) BY
                TACTIC:(Auto
                        THEN SupposeNot
                        THEN D -4
                        THEN With ⌜i⌝ (D 0)⋅
                        THEN Auto
                        THEN MoveToConcl (-2)
                        THEN (GenConclTerm ⌜alpha (i - 1)⌝⋅ THENA Auto)
                        THEN D -2
                        THEN Reduce 0
                        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. (¬R[case alpha n of inl(x) => x | inr(x) => t;case alpha m of inl(x) => x | inr(x) => t])
9. ¬(∃m:ℕm + 2. (0 < m ∧ (↑isr(alpha (m - 1)))))
10. ∀i:ℕm + 2. (0 < i ⇒ (↑isl(alpha (i - 1))))
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))

---

Latex:

---

Latex:

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.  \mexists{}n:\mBbbN{}m.  (\mneg{}R[case  alpha  n  of  inl(x)  =>  x  |  inr(x)  =>  t;case  alpha  m  of  inl(x)  =>  x  |  inr(x)  =>  t])
9.  \mneg{}(\mexists{}m:\mBbbN{}m  +  2.  (0  <  m  \mwedge{}  (\muparrow{}isr(alpha  (m  -  1)))))
\mvdash{}  \mdownarrow{}\mexists{}m:\mBbbN{}.  (0  <  m  \mwedge{}  (\muparrow{}isr(alpha  (m  -  1))))


By

---

Latex:
TACTIC:(Assert  \mforall{}i:\mBbbN{}m  +  2.  (0  <  i  {}\mRightarrow{}  (\muparrow{}isl(alpha  (i  -  1))))  BY
                            TACTIC:(Auto
                                            THEN  SupposeNot
                                            THEN  D  -4
                                            THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}
                                            THEN  Auto
                                            THEN  MoveToConcl  (-2)
                                            THEN  (GenConclTerm  \mkleeneopen{}alpha  (i  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                            THEN  D  -2
                                            THEN  Reduce  0
                                            THEN  Auto))

---

Home Index