Nuprl Lemma : RSC_vote2retry

Nuprl Lemma : RSC_vote2retry_wf

RSC_vote2retry()

B,A:

'. (Id

B

A

bag(B))

Proof not projected

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

T, isect:

x:A. B[x], function: x:A

B[x], product: x:A

B[x], universe: Type, bag: bag(T)
Definitions : member: t

T, RSC_vote2retry: RSC_vote2retry(), all:

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

RSC\_vote2retry() \mmember{} \mcap{}B,A:\mBbbU{}'. (Id {}\mrightarrow{} B \mtimes{} A {}\mrightarrow{} bag(B)) Date html generated: 2012_02_20-PM-03_59_07 Last ObjectModification: 2012_02_02-PM-01_58_26 Home Index