Nuprl Definition : bbar-recursion
bbar-recursion(d;b;i;s) == fix((λbbar-recursion,s. if d s then b s else i s (λt.(bbar-recursion (s @ [t]))) fi )) s
Definitions occuring in Statement :
append: as @ bs
,
cons: [a / b]
,
nil: []
,
ifthenelse: if b then t else f fi
,
apply: f a
,
fix: fix(F)
,
lambda: λx.A[x]
Definitions occuring in definition :
fix: fix(F)
,
ifthenelse: if b then t else f fi
,
lambda: λx.A[x]
,
apply: f a
,
append: as @ bs
,
cons: [a / b]
,
nil: []
FDL editor aliases :
bbar-recursion
Latex:
bbar-recursion(d;
b;
i;
s) ==
fix((\mlambda{}bbar-recursion,s. if d s then b s else i s (\mlambda{}t.(bbar-recursion (s @ [t]))) fi )) s
Date html generated:
2016_05_15-PM-10_05_02
Last ObjectModification:
2015_09_23-AM-08_22_09
Theory : bar!induction
Home
Index