### Nuprl Lemma : new_23_sig_when_new_round_wf

`∀[Cmd:ValueAllType]. (new_23_sig_when_new_round(Cmd) ∈ ℤ ─→ Id ─→ (ℤ × ℤ × Cmd) ─→ ℤ ─→ bag(ℤ × ℤ × Cmd))`

Proof

Definitions occuring in Statement :  new_23_sig_when_new_round: `new_23_sig_when_new_round(Cmd)` Id: `Id` vatype: `ValueAllType` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ─→ B[x]` product: `x:A × B[x]` int: `ℤ` bag: `bag(T)`
Lemmas :  eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int lt_int_wf equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert_of_lt_int single-bag_wf eqff_to_assert assert-bnot iff_transitivity assert_wf equal-wf-base int_subtype_base less_than_wf iff_weakening_uiff assert_of_band empty-bag_wf Id_wf set_wf valueall-type_wf

Latex:
\mforall{}[Cmd:ValueAllType]
(new\_23\_sig\_when\_new\_round(Cmd)  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  Id  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  bag(\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd))

Date html generated: 2015_07_23-PM-03_51_09
Last ObjectModification: 2015_01_29-AM-08_51_23

Home Index