Nuprl Definition : genFAN

genFAN(max;d) ==
  bar_recursion(λn,s. eval in
                      if int_seg_decide(λk.if fst((s k))=k then inr _.Ax)  else (inl _.Ax));0;x)
                      then inl Ax
                      else case i.(snd((s i)))) of inl(z) => inl inr(_) => inr _.Ax) 
                      fi ;
                λn,s,f. 1;
                λn,s,f. ((max t.(f <n, t>))) 1);
                0;λm.eval in

Definitions occuring in Statement :  bar_recursion: bar_recursion int_seg_decide: int_seg_decide(d;i;j) callbyvalue: callbyvalue bottom: ifthenelse: if then else fi  pi1: fst(t) pi2: snd(t) int_eq: if a=b then else d apply: a lambda: λx.A[x] pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x add: m natural_number: $n axiom: Ax
Definitions occuring in definition :  bottom: callbyvalue: callbyvalue lambda: λx.A[x] natural_number: $n pair: <a, b> apply: a add: m axiom: Ax inr: inr  inl: inl x pi2: snd(t) decide: case of inl(x) => s[x] inr(y) => t[y] pi1: fst(t) int_eq: if a=b then else d int_seg_decide: int_seg_decide(d;i;j) ifthenelse: if then else fi  bar_recursion: bar_recursion
FDL editor aliases :  genFAN

genFAN(max;d)  ==
    bar\_recursion(\mlambda{}n,s.  eval  x  =  n  in
                                            if  int\_seg\_decide(\mlambda{}k.if  fst((s  k))=k  then  inr  (\mlambda{}$_{}$.Ax)  \000C  else  (inl  (\mlambda{}$_{}$.Ax));0;x)
                                            then  inl  Ax
                                            else  case  d  n  (\mlambda{}i.(snd((s  i))))  of  inl(z)  =>  inl  z  |  inr($_{}\mbackslash{}\000Cff24)  =>  inr  (\mlambda{}$_{}$.Ax) 
                                            fi  ;
                                \mlambda{}n,s,f.  1;
                                \mlambda{}n,s,f.  ((max  n  (\mlambda{}t.(f  <n,  t>)))  +  1);
                                0;\mlambda{}m.eval  x  =  m  in

Date html generated: 2019_10_15-AM-10_20_17
Last ObjectModification: 2019_10_07-PM-04_08_19

Theory : bar-induction

Home Index