---

Step * 1 1 1 1 2 1 1 of Lemma AF-induction-iff


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t]) supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R+[x;y] ⇒ (¬R'[x;y]))))
4. ∀x,y:T.  Dec(R+[x;y])
5. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t])
6. f : ℕ ⟶ T
7. t : T
8. ∀s:{s:T| R[t;s]} . ∀f:ℕ ⟶ T.  (((f 0) = s ∈ T) ⇒ (↓∃n:ℕ. (¬(R+ (f n) (f (n + 1))))))
9. f1 : ℕ ⟶ T
10. (f1 0) = t ∈ T
11. y : T
12. (f1 0) R y
13. y (R^*) (f1 1)
⊢ ↓∃n:ℕ. (¬(R+ (f1 n) (f1 (n + 1))))
BY
{ ((InstHyp [⌜y⌝;⌜λi.if (i =z 0) then y else f1 i fi ⌝] (-6)⋅ THENA Auto) THENM (Reduce (-1) THEN SqExRepD)) }

1
.....wf..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t]) supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R+[x;y] ⇒ (¬R'[x;y]))))
4. ∀x,y:T.  Dec(R+[x;y])
5. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t])
6. f : ℕ ⟶ T
7. t : T
8. ∀s:{s:T| R[t;s]} . ∀f:ℕ ⟶ T.  (((f 0) = s ∈ T) ⇒ (↓∃n:ℕ. (¬(R+ (f n) (f (n + 1))))))
9. f1 : ℕ ⟶ T
10. (f1 0) = t ∈ T
11. y : T
12. (f1 0) R y
13. y (R^*) (f1 1)
⊢ y ∈ {s:T| R[t;s]} 

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t]) supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R+[x;y] ⇒ (¬R'[x;y]))))
4. ∀x,y:T.  Dec(R+[x;y])
5. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t])
6. f : ℕ ⟶ T
7. t : T
8. ∀s:{s:T| R[t;s]} . ∀f:ℕ ⟶ T.  (((f 0) = s ∈ T) ⇒ (↓∃n:ℕ. (¬(R+ (f n) (f (n + 1))))))
9. f1 : ℕ ⟶ T
10. (f1 0) = t ∈ T
11. y : T
12. (f1 0) R y
13. y (R^*) (f1 1)
14. n : ℕ
15. ¬(R+ if (n =z 0) then y else f1 n fi  if (n + 1 =z 0) then y else f1 (n + 1) fi )
⊢ ↓∃n:ℕ. (¬(R+ (f1 n) (f1 (n + 1))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  TI(T;x,y.R[x;y];t.Q[t]) 
      supposing  \mexists{}R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (AFx,y:T.R'[x;y]  \mwedge{}  (\mforall{}x,y:T.    (R\msupplus{}[x;y]  {}\mRightarrow{}  (\mneg{}R'[x;y]))))
4.  \mforall{}x,y:T.    Dec(R\msupplus{}[x;y])
5.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  TI(T;x,y.R[x;y];t.Q[t])
6.  f  :  \mBbbN{}  {}\mrightarrow{}  T
7.  t  :  T
8.  \mforall{}s:\{s:T|  R[t;s]\}  .  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.    (((f  0)  =  s)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  (\mneg{}(R\msupplus{}  (f  n)  (f  (n  +  1))))))
9.  f1  :  \mBbbN{}  {}\mrightarrow{}  T
10.  (f1  0)  =  t
11.  y  :  T
12.  (f1  0)  R  y
13.  y  rel\_star(T;  R)  (f1  1)
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  (\mneg{}(R\msupplus{}  (f1  n)  (f1  (n  +  1))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  0)  then  y  else  f1  i  fi  \mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
THENM  (Reduce  (-1)  THEN  SqExRepD)
)

---

Home Index