Nuprl Lemma : norep2_okfor

Nuprl Lemma : norep2_okfor_wf

norep2_okfor()

Id

bag(

)

Proof not projected

Definitions occuring in Statement : norep2_okfor: norep2_okfor(), Id: Id, member: t

T, function: x:A

B[x], int:

, bag: bag(T)
Definitions : norep2_okfor: norep2_okfor(), member: t

T, all:

x:A. B[x], uall:

[x:A]. B[x]
Lemmas : Id_wf, empty-bag_wf, single-bag_wf, bag_wf, eq_int_wf, ifthenelse_wf

norep2\_okfor() \mmember{} \mBbbZ{} {}\mrightarrow{} Id {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} bag(\mBbbZ{}) Date html generated: 2012_02_20-PM-03_37_07 Last ObjectModification: 2012_02_02-PM-01_56_58 Home Index