Nuprl Lemma : new_23_sig_assert_newvote
∀[Cmd:ValueAllType]
∀ni:ℤ × ℤ. ∀vote:ℤ × ℤ × Cmd × Id. ∀quorum:Cmd List × (Id List).
(↑(new_23_sig_newvote(Cmd) ni vote quorum) ⇐⇒ (ni = (fst(fst(vote))) ∈ (ℤ × ℤ)) ∧ (¬(snd(vote) ∈ snd(quorum))))
Proof
Definitions occuring in Statement :
new_23_sig_newvote: new_23_sig_newvote(Cmd),
Id: Id,
l_member: (x ∈ l),
list: T List,
vatype: ValueAllType,
assert: ↑b,
uall: ∀[x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
and: P ∧ Q,
apply: f a,
product: x:A × B[x],
int: ℤ,
equal: s = t ∈ T
Lemmas :
productdeq_reduce_lemma,
intdeq_reduce_lemma,
subtype_base_sq,
int_subtype_base,
l_member_wf,
Id_wf,
equal-wf-base,
not_wf,
and_wf,
equal_wf,
pi1_wf_top,
subtype_rel_product,
top_wf,
subtype_top,
pi2_wf,
iff_transitivity,
assert_wf,
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
bool_cases_sqequal,
bool_subtype_base,
bnot_wf,
deq-member_wf,
id-deq_wf,
iff_weakening_uiff,
assert_of_band,
assert_of_bnot,
assert-deq-member,
iff_wf,
list_wf,
new_23_sig_newvote_wf,
assert_witness,
valueall-type_wf
Latex:
\mforall{}[Cmd:ValueAllType]
\mforall{}ni:\mBbbZ{} \mtimes{} \mBbbZ{}. \mforall{}vote:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id. \mforall{}quorum:Cmd List \mtimes{} (Id List).
(\muparrow{}(new\_23\_sig\_newvote(Cmd) ni vote quorum)
\mLeftarrow{}{}\mRightarrow{} (ni = (fst(fst(vote)))) \mwedge{} (\mneg{}(snd(vote) \mmember{} snd(quorum))))
Date html generated:
2015_07_23-PM-03_57_43
Last ObjectModification:
2015_01_29-AM-08_49_18
Home
Index