Nuprl Lemma : rsc3_update_round_wf

[Cmd:ValueAllType]. (rsc3_update_round(Cmd)        Cmd    )


Proof not projected



Definitions occuring in Statement :  rsc3_update_round: rsc3_update_round(Cmd),  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  int: ,  vatype: ValueAllType
Definitions :  rsc3_update_round: rsc3_update_round(Cmd),  member: t  T,  vatype: ValueAllType,  uall: [x:A]. B[x]
Lemmas :  valueall-type_wf,  lt_int_wf,  eq_int_wf,  band_wf,  ifthenelse_wf
\mforall{}[Cmd:ValueAllType].  (rsc3\_update\_round(Cmd)  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})


Date html generated: 2012_02_20-PM-04_13_00
Last ObjectModification: 2012_02_02-PM-02_03_51

Home Index