Nuprl Lemma : rsc4-ilf-hide
HIDDEN 
HIDDEN HIDDEN HIDDEN HIDDEN HIDDEN HIDDEN
Proof
Definitions occuring in Statement :
rsc4_main: rsc4_Main,
rsc4_update_replica: rsc4_update_replica(Cmd),
rsc4_Proposal: rsc4_Proposal(Cmd),
rsc4_Notify: rsc4_Notify(Cmd;clients),
rsc4_decision: rsc4_decision(Cmd;clients),
rsc4_update_round: rsc4_update_round(Cmd),
rsc4_RoundInfo: rsc4_RoundInfo(Cmd),
rsc4_Quorum: rsc4_Quorum(Cmd;cmdeq;coeff;flrs),
rsc4_add_to_quorum: rsc4_add_to_quorum(Cmd),
rsc4_newvote: rsc4_newvote(Cmd),
rsc4_init: rsc4_init(),
rsc4_decided'base: rsc4_decided'base(Cmd),
rsc4_vote'base: rsc4_vote'base(Cmd),
Memory-class: Memory-class(f;init;X),
concat-lifting-loc-1: f@,
make-Msg: make-Msg(hdr;typ;val),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
simple-loc-comb-1: F|Loc, X|,
no-classrel-in-interval: (no X between start and e),
no-prior-classrel: (no X prior to e),
classrel: v 
X(e),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e 
loc e' ,
es-loc: loc(e),
es-E: E,
Id: Id,
length: ||as||,
assert: 
b,
sq_or: a 
b,
uall: 
[x:A]. B[x],
guard: {T},
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
exists: 
x:A. B[x],
iff: P 
Q,
not: 
A,
squash: T,
or: P Q,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
cons: [car / cdr],
nil: [],
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: 
,
token: "$token",
equal: s = t,
l_member: (x l),
hide: HIDDEN,
poss-maj: poss-maj(eq;L;x),
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
vatype: ValueAllType
Definitions :
rsc4_main: rsc4_Main,
rsc4_Replica: rsc4_Replica(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc4_Voter: rsc4_Voter(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc4_NewVoters: rsc4_NewVoters(Cmd),
so_lambda: 
x y.t[x; y],
rsc4_NewRounds: rsc4_NewRounds(Cmd),
rsc4_Round: rsc4_Round(Cmd;cmdeq;coeff;flrs;locs),
rsc4_NewRoundsState: rsc4_NewRoundsState(Cmd),
rsc4_when_new_round: rsc4_when_new_round(Cmd),
uiff: uiff(P;Q),
rsc4_vote'broadcast: rsc4_vote'broadcast(Cmd),
rsc4_ReplicaState: rsc4_ReplicaState(Cmd),
rsc4_when_new_proposal: rsc4_when_new_proposal(Cmd),
rsc4_Proposal: rsc4_Proposal(Cmd),
rsc4_vote2prop: rsc4_vote2prop(Cmd),
rsc4_propose'base: rsc4_propose'base(Cmd),
rsc4_RoundInfo: rsc4_RoundInfo(Cmd),
rsc4_vote2retry: rsc4_vote2retry(Cmd),
rsc4_retry'base: rsc4_retry'base(Cmd),
sq_or: a b,
rsc4_Quorum: rsc4_Quorum(Cmd;cmdeq;coeff;flrs),
rsc4_QuorumState: rsc4_QuorumState(Cmd),
rsc4_when_quorum: rsc4_when_quorum(Cmd;cmdeq;coeff;flrs),
band: p 
q,
rsc4_roundout: rsc4_roundout(Cmd;cmdeq;coeff;flrs),
rsc4_newvote: rsc4_newvote(Cmd),
rsc4_retry'send: rsc4_retry'send(Cmd),
rsc4_decided'send: rsc4_decided'send(Cmd),
rsc4_Notify: rsc4_Notify(Cmd;clients),
false: False,
not: A,
alle-lt: e<e'.P[e],
no-prior-classrel: (no X prior to e),
rsc4_decided'base: rsc4_decided'base(Cmd),
rsc4_decision: rsc4_decision(Cmd;clients),
rsc4_notify'broadcast: rsc4_notify'broadcast(Cmd),
subtype: S 
T,
top: Top,
nequal: a 
b T ,
or: P Q,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
so_lambda: x.t[x],
cand: A c B,
prop: 
,
exists: x:A. B[x],
rsc4_vote'base: rsc4_vote'base(Cmd),
true: True,
squash: T,
bag-member: x bs,
rev_implies: P Q,
implies: P Q,
name: Name,
member: t T,
classrel: v X(e),
iff: P Q,
guard: {T},
all: x:A. B[x],
vatype: ValueAllType,
uall: [x:A]. B[x],
hide: HIDDEN,
and: P Q,
so_apply: x[s1;s2],
deq: EqDecider(T),
nat: 
,
pi2: snd(t),
pi1: fst(t),
unit: Unit,
bool: 
,
uimplies: b supposing a,
rev_uimplies: rev_uimplies(P;Q),
sq_stable: SqStable(P),
so_apply: x[s],
it: 
Lemmas :
classrel-at,
eo-forward-forward2,
eclass_wf,
eo-forward-le,
subtype_rel_self,
subtype_rel_sets,
bind-class-rel-weak,
until-classrel,
es-le-loc,
eo-forward-no-prior-classrel,
eo-forward-first2,
eo-forward-loc,
send-once-loc-classrel,
sq_or_sq_or,
or_functionality_wrt_uiff,
bnot_thru_band,
and_functionality_wrt_uiff,
eo-forward-base-classrel,
assert_of_le_int,
assert_of_band,
bnot_of_lt_int,
bnot_thru_bor,
assert_functionality_wrt_uiff,
le_wf,
le_int_wf,
not_functionality_wrt_iff,
assert-deq-member,
assert_of_lt_int,
assert_of_bor,
iff_weakening_uiff,
and_functionality_wrt_iff,
squash_sq_or,
rsc4_main_wf,
rsc4_Replica_wf,
class-at_wf,
rsc4_Voter_wf,
rsc4_NewVoters_wf,
top_wf,
es-interface-subtype_rel,
rsc4_NewRounds_wf,
bind-class_wf,
until-class_wf,
rsc4_Round_wf,
rsc4_NewRoundsState_wf,
rsc4_when_new_round_wf,
send-once-loc-class_wf,
subtype_rel_set,
rsc4_vote'broadcast_wf,
rsc4_ReplicaState_wf,
rsc4_when_new_proposal_wf,
lt_int_wf,
bor_wf,
l_member_wf,
less_than_wf,
rsc4_update_replica_wf,
rsc4_update_round_wf,
decidable__es-le,
es-le_wf,
sq_stable_from_decidable,
member-eo-forward-E,
no-classrel-in-interval_wf,
eo-forward_wf,
eo-forward-E-subtype,
Id-valueall-type,
rsc4_Proposal_wf,
rsc4_vote2prop_wf,
rsc4_propose'base_wf,
parallel-classrel-weak,
sq_or_squash3,
rsc4_RoundInfo_wf,
rsc4_vote2retry_wf,
rsc4_retry'base_wf,
parallel-class_wf,
sq_or_wf,
simple-loc-comb-2-concat-classrel-weak,
bfalse_wf,
int-deq_wf,
product-deq_wf,
id-deq_wf,
deq-member_wf,
band_wf,
pair-eta,
bag-member-single-weak,
deq_wf,
rsc4_Quorum_wf,
rsc4_QuorumState_wf,
rsc4_when_quorum_wf,
concat-lifting-loc-2_wf,
simple-loc-comb-2_wf,
rsc4_roundout_wf,
single-bag_wf,
rsc4_retry'send_wf,
rsc4_decided'send_wf,
length_wf,
poss-maj_wf,
nat_wf,
rsc4_newvote_wf,
rsc4_init_wf,
rsc4_add_to_quorum_wf,
Memory-class_wf,
once-classrel-weak,
es-locl_wf,
rsc4_Notify_wf,
once-class_wf,
no-prior-classrel_wf,
es-loc_wf,
exists-product1,
simple-loc-comb-1-concat-classrel-weak,
bag-member-empty-weak,
bag-member-ifthenelse,
and_false_r,
and_wf,
pi2_wf,
pi1_wf_top,
bag-member-map,
neg_assert_of_eq_int,
and_functionality_wrt_uiff2,
nequal_wf,
or_functionality_wrt_iff,
ifthenelse-prop,
iff_transitivity,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
bag-map_wf,
assert_of_eq_int,
eqtt_to_assert,
assert_wf,
uiff_transitivity,
bool_wf,
or_false_r,
squash_equal,
equal_wf,
trivial-eq,
exists-elim,
and_true_r,
squash-bag-member,
squash_true,
squash_and,
and_true_l,
rsc4_decided'base_wf,
rsc4_decision_wf,
concat-lifting-loc-1_wf,
simple-loc-comb-1_wf,
empty-bag_wf,
rsc4_notify'broadcast_wf,
bag_wf,
eq_int_wf,
ifthenelse_wf,
false_wf,
or_wf,
make-Msg_wf,
exists_wf,
squash_wf,
sq_stable__valueall-type,
int-valueall-type,
product-valueall-type,
true_wf,
bag-member_wf,
valueall-type_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
Message_wf,
Id_wf,
rsc4_vote'base_wf,
base-headers-msg-val_wf,
classrel_wf
HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN
Date html generated:
2012_02_20-PM-04_56_13
Last ObjectModification:
2012_02_02-PM-02_16_11
Home
Index