Nuprl Lemma : pv11_p1_leq_bnum_max

ldrs_uid:Id ─→ ℤ. ∀b,b':pv11_p1_Ballot_Num().  (↑(pv11_p1_leq_bnum(ldrs_uid) (pv11_p1_max_bnum(ldrs_uid) b' b)))


Proof




Definitions occuring in Statement :  pv11_p1_max_bnum: pv11_p1_max_bnum(ldrs_uid) pv11_p1_leq_bnum: pv11_p1_leq_bnum(ldrs_uid) pv11_p1_Ballot_Num: pv11_p1_Ballot_Num() Id: Id assert: b all: x:A. B[x] apply: a function: x:A ─→ B[x] int:
Lemmas :  pv11_p1_leq_bnum'_wf bool_wf eqtt_to_assert assert_of_bor lt_int_wf eq_int_wf assert_of_eq_int le_int_wf assert_of_lt_int iff_transitivity assert_wf equal-wf-base int_subtype_base le_wf iff_weakening_uiff assert_of_band assert_of_le_int less_than_wf or_wf le_weakening eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot not_over_or not_over_and decidable__int_equal Id_wf unit_wf2

Latex:
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b,b':pv11\_p1\_Ballot\_Num().
    (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  b  (pv11\_p1\_max\_bnum(ldrs$_{uid\mbackslash{}f\000Cf7d$)  b'  b)))



Date html generated: 2015_07_23-PM-04_44_09
Last ObjectModification: 2015_01_29-AM-11_20_59

Home Index