---

Step * 1 2 1 1 1 1 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. ∀x:ℕj + 2. (0 < x ⇒ (↑isl(alpha (x - 1))))
10. x : T@i
11. (alpha j) = (inl x) ∈ (T?)
12. ↑isl(alpha i)
13. x1 : T@i
14. (alpha i) = (inl x1) ∈ (T?)
⊢ R[x1;x] ⇒ R[x1;outl(alpha j)]
BY
{ TACTIC:((D 0 THENA Auto) THEN NthHypEq (-1) THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
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. ∀x:ℕj + 2. (0 < x ⇒ (↑isl(alpha (x - 1))))
10. x : T@i
11. (alpha j) = (inl x) ∈ (T?)
12. ↑isl(alpha i)
13. x1 : T@i
14. (alpha i) = (inl x1) ∈ (T?)
15. R[x1;x]
⊢ outl(alpha j) = x ∈ T

---

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.  \mforall{}x:\mBbbN{}j  +  2.  (0  <  x  {}\mRightarrow{}  (\muparrow{}isl(alpha  (x  -  1))))
10.  x  :  T@i
11.  (alpha  j)  =  (inl  x)
12.  \muparrow{}isl(alpha  i)
13.  x1  :  T@i
14.  (alpha  i)  =  (inl  x1)
\mvdash{}  R[x1;x]  {}\mRightarrow{}  R[x1;outl(alpha  j)]


By

---

Latex:
TACTIC:((D  0  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCD  THEN  Auto)

---

Home Index