Nuprl Definition : proof_tree_ind

proof_tree_ind(effect;abort;progress;pf) ==
  W_ind(λa,f,q. let s,r = a in case effect <s, r> of inl(x) => progress s r mklist(||x||;f) (λi.(q i)) | inr(x) => abort\000C s r;pf)


Definitions occuring in Statement :  mklist: mklist(n;f),  length: ||as||,  W_ind: W_ind(F;w),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  W_ind: W_ind(F;w),  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  pair: <a, b>,  mklist: mklist(n;f),  length: ||as||,  lambda: λx.A[x],  apply: f a
FDL editor aliases :  proof_tree_ind
Latex:
proof\_tree\_ind(effect;abort;progress;pf)  ==
    W\_ind(\mlambda{}a,f,q.  let  s,r  =  a 
                                in  case  effect  <s,  r>
                                        of  inl(x)  =>
                                        progress  s  r  mklist(||x||;f)  (\mlambda{}i.(q  i))
                                        |  inr(x)  =>
                                        abort  s  r;pf)


Date html generated: 2018_05_21-PM-06_28_46
Last ObjectModification: 2018_01_11-AM-09_45_13

Theory : general


Home Index