---

Step * 2 of Lemma AF-uniform-induction


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 : ℕ
11. s : ℕn ⟶ (T?)
12. ∀%9:ℕn. (AF-spread-law(x,y.R[x;y]) %9 s (s %9))
13. ∀t1:{t1:T?| AF-spread-law(x,y.R[x;y]) n s t1} 
      (if (n + 1 =z 0)
       then fix(F)
       else case if (n + 1) - 1=n  then t1  else (s ((n + 1) - 1)) of inl(z) => fix(F) | inr(z) => Ax
       fi  ∈ if (n + 1 =z 0)
       then Q[t]
       else case if (n + 1) - 1=n  then t1  else (s ((n + 1) - 1)) of inl(z) => Q[z] | inr(z) => True
       fi )
⊢ if (n =z 0) then fix(F) else case s (n - 1) of inl(z) => fix(F) | inr(z) => Ax fi  ∈ if (n =z 0)
  then Q[t]
  else case s (n - 1) of inl(z) => Q[z] | inr(z) => True
  fi 
BY
{ ((Assert ∀t1:{t1:T?| AF-spread-law(x,y.R[x;y]) n s t1} 
             (case t1 of inl(z) => fix(F) | inr(z) => Ax ∈ case t1 of inl(z) => Q[z] | inr(z) => True) BY
          (ParallelLast THEN NthHypSq (-1) THEN AutoSplit))
   THEN Thin (-2)
   ) }

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 : ℕ
11. s : ℕn ⟶ (T?)
12. ∀%9:ℕn. (AF-spread-law(x,y.R[x;y]) %9 s (s %9))
13. ∀t1:{t1:T?| AF-spread-law(x,y.R[x;y]) n s t1} 
      (case t1 of inl(z) => fix(F) | inr(z) => Ax ∈ case t1 of inl(z) => Q[z] | inr(z) => True)
⊢ if (n =z 0) then fix(F) else case s (n - 1) of inl(z) => fix(F) | inr(z) => Ax fi  ∈ if (n =z 0)
  then Q[t]
  else case s (n - 1) of inl(z) => Q[z] | inr(z) => True
  fi 

---

Latex:

---

Latex:

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  :  \mBbbN{}
11.  s  :  \mBbbN{}n  {}\mrightarrow{}  (T?)
12.  \mforall{}\%9:\mBbbN{}n.  (AF-spread-law(x,y.R[x;y])  \%9  s  (s  \%9))
13.  \mforall{}t1:\{t1:T?|  AF-spread-law(x,y.R[x;y])  n  s  t1\} 
            (if  (n  +  1  =\msubz{}  0)
              then  fix(F)
              else  case  if  (n  +  1)  -  1=n    then  t1    else  (s  ((n  +  1)  -  1))
                          of  inl(z)  =>
                          fix(F)
                          |  inr(z)  =>
                          Ax
              fi    \mmember{}  if  (n  +  1  =\msubz{}  0)
              then  Q[t]
              else  case  if  (n  +  1)  -  1=n    then  t1    else  (s  ((n  +  1)  -  1))
                          of  inl(z)  =>
                          Q[z]
                          |  inr(z)  =>
                          True
              fi  )
\mvdash{}  if  (n  =\msubz{}  0)  then  fix(F)  else  case  s  (n  -  1)  of  inl(z)  =>  fix(F)  |  inr(z)  =>  Ax  fi    \mmember{}  if  (n  =\msubz{}  0)
    then  Q[t]
    else  case  s  (n  -  1)  of  inl(z)  =>  Q[z]  |  inr(z)  =>  True
    fi 


By

---

Latex:
((Assert  \mforall{}t1:\{t1:T?|  AF-spread-law(x,y.R[x;y])  n  s  t1\} 
                      (case  t1  of  inl(z)  =>  fix(F)  |  inr(z)  =>  Ax  \mmember{}  case  t1
                          of  inl(z)  =>
                          Q[z]
                          |  inr(z)  =>
                          True)  BY
                (ParallelLast  THEN  NthHypSq  (-1)  THEN  AutoSplit))
  THEN  Thin  (-2)
  )

---

Home Index