Nuprl Definition : subgame

subgame(g;p;n)
==r if (n =z 0)
    then inl g
    else let a,f = g 
         in case p 0 a of inl(m) => subgame(f m;λi.(p (i + 1));n - 1) | inr(z) => inr z 
    fi 
subgame(g;p;n) ==
  fix((λsubgame,g,p,n. if (n =z 0)
                      then inl g
                      else let a,f = g 
                           in case p 0 a of inl(m) => subgame (f m) (λi.(p (i + 1))) (n - 1) | inr(z) => inr z 
                      fi )) 
  g 
  p 
  n


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  inr: inr x ,  natural_number: $n,  subtract: n - m,  add: n + m,  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  inl: inl x,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  fix: fix(F)
FDL editor aliases :  subgame subgame
Latex:
subgame(g;p;n)
==r  if  (n  =\msubz{}  0)
        then  inl  g
        else  let  a,f  =  g 
                  in  case  p  0  a  of  inl(m)  =>  subgame(f  m;\mlambda{}i.(p  (i  +  1));n  -  1)  |  inr(z)  =>  inr  z 
        fi 

Latex:
subgame(g;p;n)  ==
    fix((\mlambda{}subgame,g,p,n.  if  (n  =\msubz{}  0)
                                            then  inl  g
                                            else  let  a,f  =  g 
                                                      in  case  p  0  a
                                                              of  inl(m)  =>
                                                              subgame  (f  m)  (\mlambda{}i.(p  (i  +  1)))  (n  -  1)
                                                              |  inr(z)  =>
                                                              inr  z 
                                            fi  )) 
    g 
    p 
    n


Date html generated: 2016_05_14-PM-03_56_24
Last ObjectModification: 2016_05_04-PM-03_40_19

Theory : spread


Home Index