Nuprl Definition : goodAux

goodAux(g0;G;moves) ==
  if (||moves|| =z 2)
  then g0
  else let g = goodAux(g0;G;play-truncate(moves;||moves|| - 2)) in
           G moves[||moves|| - 4] moves[||moves|| - 3] g
  fi 


Definitions occuring in Statement :  play-truncate: play-truncate(f;m),  play-len: ||moves||,  play-item: moves[i],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  let: let,  apply: f a,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  let: let,  play-truncate: play-truncate(f;m),  apply: f a,  play-item: moves[i],  subtract: n - m,  play-len: ||moves||,  natural_number: $n
FDL editor aliases :  goodAux
Latex:
goodAux(g0;G;moves)  ==
    if  (||moves||  =\msubz{}  2)
    then  g0
    else  let  g  =  goodAux(g0;G;play-truncate(moves;||moves||  -  2))  in
                      G  moves[||moves||  -  4]  moves[||moves||  -  3]  g
    fi 


Date html generated: 2019_06_20-PM-00_53_22
Last ObjectModification: 2019_01_02-PM-01_32_19

Theory : co-recursion-2


Home Index