Nuprl Lemma : RSC_new_proposal

Nuprl Lemma : RSC_new_proposal_wf

RSC_new_proposal()

A:

'. (

A

(

List)

)

Proof not projected

Definitions occuring in Statement : RSC_new_proposal: RSC_new_proposal(), bool:

, member: t

T, isect:

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

B[x], product: x:A

B[x], list: type List, int:

, universe: Type
Definitions : member: t

T, RSC_new_proposal: RSC_new_proposal(), uall:

[x:A]. B[x]
Lemmas : bor_wf, lt_int_wf, deq-member_wf, int-deq_wf

RSC\_new\_proposal() \mmember{} \mcap{}A:\mBbbU{}'. (\mBbbZ{} \mtimes{} A {}\mrightarrow{} \mBbbZ{} \mtimes{} (\mBbbZ{} List) {}\mrightarrow{} \mBbbB{}) Date html generated: 2012_02_20-PM-04_00_25 Last ObjectModification: 2012_02_02-PM-01_58_52 Home Index