Nuprl Definition : genFAN

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


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


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

Theory : bar-induction


Home Index