---

Step * of Lemma AF-uniform-induction4-ext

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  ∀Q:T ⟶ ℙ. uniform-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]))))
BY
{ xxxExtract of Obid: AF-uniform-induction4
     not unfolding  
     finishing with Auto
     normalizes to:
     
     λT,R,Q,F. fix((λx.(F x)))xxx }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  uniform-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]))))


By

---

Latex:
xxxExtract  of  Obid:  AF-uniform-induction4
      not  unfolding   
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}T,R,Q,F.  fix((\mlambda{}x.(F  x)))xxx

---

Home Index