Nuprl Lemma : pv11_p1_max_bnum_comm
∀[ldrs_uid:Id ─→ ℤ]. ∀[b1,b2:pv11_p1_Ballot_Num()].
(pv11_p1_max_bnum(ldrs_uid) b1 b2) = (pv11_p1_max_bnum(ldrs_uid) b2 b1) ∈ pv11_p1_Ballot_Num()
supposing Inj(Id;ℤ;ldrs_uid)
Proof
Definitions occuring in Statement :
pv11_p1_max_bnum: pv11_p1_max_bnum(ldrs_uid),
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),
Id: Id,
inject: Inj(A;B;f),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
apply: f a,
function: x:A ─→ B[x],
int: ℤ,
equal: s = t ∈ T
Lemmas :
bor_wf,
lt_int_wf,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
le_int_wf,
equal-wf-T-base,
assert_wf,
or_wf,
less_than_wf,
equal-wf-base,
int_subtype_base,
le_wf,
assert_of_le_int,
bnot_wf,
not_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_bor,
assert_of_lt_int,
assert_of_band,
uiff_transitivity,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_thru_bor,
band_wf,
squash_wf,
true_wf,
bnot_of_lt_int,
bnot_thru_band,
bnot_of_le_int,
assert_of_bnot,
le_antisymmetry,
unit_wf2
Latex:
\mforall{}[ldrs$_{uid}$:Id {}\mrightarrow{} \mBbbZ{}]. \mforall{}[b1,b2:pv11\_p1\_Ballot\_Num()].
(pv11\_p1\_max\_bnum(ldrs$_{uid}$) b1 b2) = (pv11\_p1\_max\_bnum(ldrs$_{\000Cuid}$) b2 b1) supposing Inj(Id;\mBbbZ{};ldrs$_{uid}$)
Date html generated:
2015_07_23-PM-04_44_25
Last ObjectModification:
2015_01_29-AM-11_20_57
Home
Index