Nuprl Definition : spector-bar-rec

spector-bar-rec(Y;G;H;n;s)==r if Y n s ≤z n then G n s else H n s (λt.spector-bar-rec(Y;G;H;n + 1;s.t@n)) fi

spector-bar-rec(Y;G;H;n;s) ==

  fix((λspector-bar-rec,n,s. if Y n s ≤z n then G n s else H n s (λt.(spector-bar-rec (n + 1) s.t@n)) fi )) n s

Definitions occuring in Statement : le_int: i ≤z j, seq-add: s.x@n, ifthenelse: if b then t else f fi , apply: f a, fix: fix(F), lambda: λx.A[x], add: n + m, natural_number: $n
Definitions occuring in definition : seq-add: s.x@n, natural_number: $n, add: n + m, apply: f a, lambda: λx.A[x], le_int: i ≤z j, ifthenelse: if b then t else f fi , fix: fix(F)
FDL editor aliases : spector-bar-rec

Latex:
spector-bar-rec(Y;G;H;n;s) ==r if Y n s \mleq{}z n then G n s else H n s (\mlambda{}t.spector-bar-rec(Y;G;H;n + 1;s.t@n)) fi

Latex:
spector-bar-rec(Y;G;H;n;s) == fix((\mlambda{}spector-bar-rec,n,s. if Y n s \mleq{}z n then G n s else H n s (\mlambda{}t.(spector-bar-rec (n + 1) s.t@n)) fi )) n s Date html generated: 2016_05_14-PM-09_58_24 Last ObjectModification: 2016_05_13-AM-09_27_02 Theory : continuity Home Index