Nuprl Lemma : ler2_new_conf

Nuprl Lemma : ler2_new_conf_wf

ler2_new_conf()

Id

(

Id)

Proof not projected

Definitions occuring in Statement : Id: Id, member: t

T, function: x:A

B[x], product: x:A

B[x], int:

Definitions : ler2_new_conf: ler2_new_conf(), member: t

T, uall:

[x:A]. B[x]
Lemmas : Id_wf, lt_int_wf, ifthenelse_wf

ler2\_new\_conf() \mmember{} Id {}\mrightarrow{} \mBbbZ{} \mtimes{} Id {}\mrightarrow{} \mBbbZ{} \mtimes{} Id {}\mrightarrow{} (\mBbbZ{} \mtimes{} Id) Date html generated: 2012_02_20-PM-06_13_00 Last ObjectModification: 2012_02_02-PM-02_41_59 Home Index