Nuprl Lemma : rsc5_Halt_wf
rsc5_Halt() 
EClass'(Unit)
Proof not projected
Definitions occuring in Statement :
rsc5_Halt: rsc5_Halt(),
Message: Message,
eclass: EClass(A[eo; e]),
unit: Unit,
member: t T,
function: x:A B[x],
int:
Definitions :
rsc5_Halt: rsc5_Halt(),
member: t T,
all: 
x:A. B[x],
uall: [x:A]. B[x]
Lemmas :
rsc5_decided'base_wf,
Id_wf,
empty-bag_wf,
it_wf,
single-bag_wf,
bag_wf,
int-deq_wf,
eqof_wf,
ifthenelse_wf,
concat-lifting-loc-1_wf,
unit_wf2,
Message_wf,
simple-loc-comb-1_wf
rsc5\_Halt() \mmember{} \mBbbZ{} {}\mrightarrow{} EClass'(Unit)
Date html generated:
2012_02_20-PM-05_08_18
Last ObjectModification:
2012_02_02-PM-02_19_14
Home
Index