Nuprl Lemma : pv11_p1_ldr_state_eq2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
uiff(v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e);if first(e)
then v
= (pv11_p1_init_leader(Cmd) loc(e))
∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
if pred(e) ∈b pv11_p1_propose'base(Cmd;f)
then ∃x:ℤ × Cmd
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v = (pv11_p1_on_propose(Cmd) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
if pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
then ∃x:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
if pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
then ∃x:pv11_p1_Ballot_Num()
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
else v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
fi )
Proof
Definitions occuring in Statement :
pv11_p1_LeaderState: pv11_p1_LeaderState(Cmd;ldrs_uid;mf),
pv11_p1_when_preempted: pv11_p1_when_preempted(Cmd;ldrs_uid),
pv11_p1_when_adopted: pv11_p1_when_adopted(Cmd;ldrs_uid),
pv11_p1_on_propose: pv11_p1_on_propose(Cmd),
pv11_p1_init_leader: pv11_p1_init_leader(Cmd),
pv11_p1_propose'base: pv11_p1_propose'base(Cmd;mf),
pv11_p1_adopted'base: pv11_p1_adopted'base(Cmd;mf),
pv11_p1_preempted'base: pv11_p1_preempted'base(Cmd;mf),
pv11_p1_headers_type: pv11_p1_headers_type{i:l}(Cmd),
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),
Message: Message(f),
classrel: v ∈ X(e),
member-eclass: e ∈b X,
event-ordering+: EO+(Info),
es-first: first(e),
es-pred: pred(e),
es-loc: loc(e),
es-E: E,
Id: Id,
list: T List,
vatype: ValueAllType,
ifthenelse: if b then t else f fi ,
bool: 𝔹,
uiff: uiff(P;Q),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
product: x:A × B[x],
int: ℤ,
equal: s = t ∈ T
Lemmas :
es-first_wf2,
event-ordering+_subtype,
Message_wf,
eqtt_to_assert,
equal_wf,
pv11_p1_init_leader_wf,
es-loc_wf,
eqff_to_assert,
bool_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
member-eclass_wf,
es-pred_wf,
classfun-res_wf,
base-headers-msg-val-single-val,
cons_wf_listp,
nil_wf,
listp_wf,
subtype_rel_weakening,
ext-eq_weakening,
pv11_p1_LeaderStateFun_wf,
cons_wf,
pv11_p1_Ballot_Num_wf,
list_wf,
pv11_p1_ldr_state_fun_eq,
iff_weakening_equal,
pv11_p1_propose'base_wf,
exists_wf,
classrel_wf,
pv11_p1_LeaderState_wf,
pv11_p1_on_propose_wf,
pv11_p1_adopted'base_wf,
pv11_p1_when_adopted_wf,
pv11_p1_preempted'base_wf,
pv11_p1_when_preempted_wf,
uiff_wf,
es-E_wf,
pv11_p1_LeaderState-classrel,
classrel-classfun-res
Latex:
\mforall{}Cmd:ValueAllType. \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd). \mforall{}es:EO+(Message(f)). \mforall{}e:E. \mforall{}ldrs$_\mbackslash{}ff7\000Cbuid}$:Id {}\mrightarrow{} \mBbbZ{}.
\mforall{}v:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List).
uiff(v \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e);if first(e)
then v = (pv11\_p1\_init\_leader(Cmd) loc(e))
if pred(e) \mmember{}\msubb{} pv11\_p1\_propose'base(Cmd;f)
then \mexists{}x:\mBbbZ{} \mtimes{} Cmd
\mexists{}s:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List)
(x \mmember{} pv11\_p1\_propose'base(Cmd;f)(pred(e))
\mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e))
\mwedge{} (v = (pv11\_p1\_on\_propose(Cmd) loc(e) x s)))
if pred(e) \mmember{}\msubb{} pv11\_p1\_adopted'base(Cmd;f)
then \mexists{}x:pv11\_p1\_Ballot\_Num() \mtimes{} ((pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List)
\mexists{}s:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List)
(x \mmember{} pv11\_p1\_adopted'base(Cmd;f)(pred(e))
\mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e))
\mwedge{} (v = (pv11\_p1\_when\_adopted(Cmd;ldrs$_{uid}$) loc(e) x s)))
if pred(e) \mmember{}\msubb{} pv11\_p1\_preempted'base(Cmd;f)
then \mexists{}x:pv11\_p1\_Ballot\_Num()
\mexists{}s:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List)
(x \mmember{} pv11\_p1\_preempted'base(Cmd;f)(pred(e))
\mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e))
\mwedge{} (v = (pv11\_p1\_when\_preempted(Cmd;ldrs$_{uid}$) loc(e) x s)))
else v \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(pred(e))
fi )
Date html generated:
2015_07_23-PM-04_46_54
Last ObjectModification:
2015_02_04-AM-08_24_05
Home
Index