---

Step * 1 of Lemma AF-path-barred


1. T : Type
2. t : T
3. R : T ⟶ T ⟶ ℙ
4. alpha : ℕ ⟶ (T?)@i
5. ∀x:ℕ. ((↑isl(alpha x)) ⇒ (∀i:ℕx. ((↑isl(alpha i)) ∧ (¬R[outl(alpha i);outl(alpha x)]))))
6. i : ℕ@i
7. j : ℕ@i
8. i < j
9. R[case alpha i of inl(x) => x | inr(x) => t;case alpha j of inl(x) => x | inr(x) => t]
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))
BY
{ TACTIC:(Decide ⌜∃m:ℕj + 2. (0 < m ∧ (↑isr(alpha (m - 1))))⌝⋅ THENA Auto) }

1
1. T : Type
2. t : T
3. R : T ⟶ T ⟶ ℙ
4. alpha : ℕ ⟶ (T?)@i
5. ∀x:ℕ. ((↑isl(alpha x)) ⇒ (∀i:ℕx. ((↑isl(alpha i)) ∧ (¬R[outl(alpha i);outl(alpha x)]))))
6. i : ℕ@i
7. j : ℕ@i
8. i < j
9. R[case alpha i of inl(x) => x | inr(x) => t;case alpha j of inl(x) => x | inr(x) => t]
10. ∃m:ℕj + 2. (0 < m ∧ (↑isr(alpha (m - 1))))
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))

2
1. T : Type
2. t : T
3. R : T ⟶ T ⟶ ℙ
4. alpha : ℕ ⟶ (T?)@i
5. ∀x:ℕ. ((↑isl(alpha x)) ⇒ (∀i:ℕx. ((↑isl(alpha i)) ∧ (¬R[outl(alpha i);outl(alpha x)]))))
6. i : ℕ@i
7. j : ℕ@i
8. i < j
9. R[case alpha i of inl(x) => x | inr(x) => t;case alpha j of inl(x) => x | inr(x) => t]
10. ¬(∃m:ℕj + 2. (0 < m ∧ (↑isr(alpha (m - 1)))))
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  t  :  T
3.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  alpha  :  \mBbbN{}  {}\mrightarrow{}  (T?)@i
5.  \mforall{}x:\mBbbN{}.  ((\muparrow{}isl(alpha  x))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}x.  ((\muparrow{}isl(alpha  i))  \mwedge{}  (\mneg{}R[outl(alpha  i);outl(alpha  x)]))))
6.  i  :  \mBbbN{}@i
7.  j  :  \mBbbN{}@i
8.  i  <  j
9.  R[case  alpha  i  of  inl(x)  =>  x  |  inr(x)  =>  t;case  alpha  j  of  inl(x)  =>  x  |  inr(x)  =>  t]
\mvdash{}  \mdownarrow{}\mexists{}m:\mBbbN{}.  (0  <  m  \mwedge{}  (\muparrow{}isr(alpha  (m  -  1))))


By

---

Latex:
TACTIC:(Decide  \mkleeneopen{}\mexists{}m:\mBbbN{}j  +  2.  (0  <  m  \mwedge{}  (\muparrow{}isr(alpha  (m  -  1))))\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index