---

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

.....wf..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x,y,z:T.  ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))
4. AFx,y:T.R[x;y]
5. Q : T ⟶ ℙ
6. F : ∀[t:T]. ((∀[s:{s:T| ¬R[t;s]} ]. Q[s]) ⇒ Q[t])
7. t : T
8. AF-spread-law(x,y.R[x;y]) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ
9. AFbar() ∈ n:ℕ ⟶ AF-spread-law(x,y.R[x;y])-consistent-seq(n) ⟶ ℙ
10. n : {1...}
11. s : ℕn ⟶ (T?)
12. ∀%9:ℕn. ((↑isl(s %9)) ⇒ (∀i:ℕ%9. ((↑isl(s i)) ∧ (¬R[outl(s i);outl(s %9)]))))
13. ∀t1:{t1:T?| (↑isl(t1)) ⇒ (∀i:ℕn. ((↑isl(s i)) ∧ (¬R[outl(s i);outl(t1)])))} 
      (case t1 of inl(z) => fix(F) | inr(z) => Ax ∈ case t1 of inl(z) => Q[z] | inr(z) => True)
14. x : T
15. (s (n - 1)) = (inl x) ∈ (T?)
16. s1 : T
17. ¬R[x;s1]
⊢ inl s1 ∈ {t1:T?| (↑isl(t1)) ⇒ (∀i:ℕn. ((↑isl(s i)) ∧ (¬R[outl(s i);outl(t1)])))} 
BY
{ (InstHyp [⌜n - 1⌝] (-6)⋅ THENA (Auto THEN HypSubst' (-3) 0 THEN Reduce 0 THEN Auto)) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x,y,z:T.  ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))
4. AFx,y:T.R[x;y]
5. Q : T ⟶ ℙ
6. F : ∀[t:T]. ((∀[s:{s:T| ¬R[t;s]} ]. Q[s]) ⇒ Q[t])
7. t : T
8. AF-spread-law(x,y.R[x;y]) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ
9. AFbar() ∈ n:ℕ ⟶ AF-spread-law(x,y.R[x;y])-consistent-seq(n) ⟶ ℙ
10. n : {1...}
11. s : ℕn ⟶ (T?)
12. ∀%9:ℕn. ((↑isl(s %9)) ⇒ (∀i:ℕ%9. ((↑isl(s i)) ∧ (¬R[outl(s i);outl(s %9)]))))
13. ∀t1:{t1:T?| (↑isl(t1)) ⇒ (∀i:ℕn. ((↑isl(s i)) ∧ (¬R[outl(s i);outl(t1)])))} 
      (case t1 of inl(z) => fix(F) | inr(z) => Ax ∈ case t1 of inl(z) => Q[z] | inr(z) => True)
14. x : T
15. (s (n - 1)) = (inl x) ∈ (T?)
16. s1 : T
17. ¬R[x;s1]
18. ∀i:ℕn - 1. ((↑isl(s i)) ∧ (¬R[outl(s i);outl(s (n - 1))]))
⊢ inl s1 ∈ {t1:T?| (↑isl(t1)) ⇒ (∀i:ℕn. ((↑isl(s i)) ∧ (¬R[outl(s i);outl(t1)])))} 

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x,y,z:T.    ((\mneg{}R[x;y])  {}\mRightarrow{}  (\mneg{}R[y;z])  {}\mRightarrow{}  (\mneg{}R[x;z]))
4.  AFx,y:T.R[x;y]
5.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
6.  F  :  \mforall{}[t:T].  ((\mforall{}[s:\{s:T|  \mneg{}R[t;s]\}  ].  Q[s])  {}\mRightarrow{}  Q[t])
7.  t  :  T
8.  AF-spread-law(x,y.R[x;y])  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  (T?))  {}\mrightarrow{}  (T?)  {}\mrightarrow{}  \mBbbP{}
9.  AFbar()  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  AF-spread-law(x,y.R[x;y])-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}
10.  n  :  \{1...\}
11.  s  :  \mBbbN{}n  {}\mrightarrow{}  (T?)
12.  \mforall{}\%9:\mBbbN{}n.  ((\muparrow{}isl(s  \%9))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\%9.  ((\muparrow{}isl(s  i))  \mwedge{}  (\mneg{}R[outl(s  i);outl(s  \%9)]))))
13.  \mforall{}t1:\{t1:T?|  (\muparrow{}isl(t1))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  ((\muparrow{}isl(s  i))  \mwedge{}  (\mneg{}R[outl(s  i);outl(t1)])))\} 
            (case  t1  of  inl(z)  =>  fix(F)  |  inr(z)  =>  Ax  \mmember{}  case  t1  of  inl(z)  =>  Q[z]  |  inr(z)  =>  True)
14.  x  :  T
15.  (s  (n  -  1))  =  (inl  x)
16.  s1  :  T
17.  \mneg{}R[x;s1]
\mvdash{}  inl  s1  \mmember{}  \{t1:T?|  (\muparrow{}isl(t1))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  ((\muparrow{}isl(s  i))  \mwedge{}  (\mneg{}R[outl(s  i);outl(t1)])))\} 


By

---

Latex:
(InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  (-6)\mcdot{}  THENA  (Auto  THEN  HypSubst'  (-3)  0  THEN  Reduce  0  THEN  Auto))

---

Home Index