Nuprl Definition : rsc5_Halt
rsc5_Halt() == 
n.slf,m.if eqof(IntDeq) n m then {
} else {} fi @|Loc, rsc5_decided'base()|
Definitions occuring in Statement :
rsc5_decided'base: rsc5_decided'base(),
concat-lifting-loc-1: f@,
simple-loc-comb-1: F|Loc, X|,
ifthenelse: if b then t else f fi ,
it: ,
apply: f a,
lambda: x.A[x],
int-deq: IntDeq,
eqof: eqof(d),
single-bag: {x},
empty-bag: {}
FDL editor aliases :
rsc5_Halt
rsc5\_Halt() == \mlambda{}n.\mlambda{}slf,m.if eqof(IntDeq) n m then \{\mcdot{}\} else \{\} fi @|Loc, rsc5\_decided'base()|
Date html generated:
2012_02_20-PM-05_08_14
Last ObjectModification:
2012_02_02-PM-02_19_12
Home
Index