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