Nuprl Definition : prank

prank(x) ==
  formula_ind(x;
              pvar(v)⇒ 0;
              pnot(a)⇒ r.r + 1;
              pand(a,b)⇒ r1,r2.imax(r1;r2) + 1;
              por(a,b)⇒ r1,r2.imax(r1;r2) + 1;
              pimp(a,b)⇒ r1,r2.imax(r1;r2) + 1)

Definitions occuring in Statement : formula_ind: formula_ind, imax: imax(a;b), add: n + m, natural_number: $n
Definitions occuring in definition : formula_ind: formula_ind, add: n + m, imax: imax(a;b), natural_number: $n
FDL editor aliases : prank

Latex:
prank(x) == formula\_ind(x; pvar(v){}\mRightarrow{} 0; pnot(a){}\mRightarrow{} r.r + 1; pand(a,b){}\mRightarrow{} r1,r2.imax(r1;r2) + 1; por(a,b){}\mRightarrow{} r1,r2.imax(r1;r2) + 1; pimp(a,b){}\mRightarrow{} r1,r2.imax(r1;r2) + 1) Date html generated: 2016_05_15-PM-07_12_37 Last ObjectModification: 2015_09_23-AM-08_13_05 Theory : general Home Index