Nuprl Lemma : RSC_round_increase

Nuprl Lemma : RSC_round_increase_wf

RSC_round_increase()

A:

'. (

A

)

Proof not projected

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

, member: t

T, isect:

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

B[x], product: x:A

B[x], int:

, universe: Type
Definitions : member: t

T, RSC_round_increase: RSC_round_increase(), uall:

[x:A]. B[x]
Lemmas : band_wf, eq_int_wf, lt_int_wf

RSC\_round\_increase() \mmember{} \mcap{}A:\mBbbU{}'. (\mBbbZ{} {}\mrightarrow{} \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} A {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} \mBbbB{}) Date html generated: 2012_02_20-PM-03_59_19 Last ObjectModification: 2012_02_02-PM-01_58_31 Home Index