Nuprl Lemma : RSC_VoterState-trans
[Cmd:ValueAllType]. [es:EO'].
e1,e2:E. n,a,b:
.
((e1 <loc e2)
(
c:Cmd. <<n, a>, c> 
Base(``sc retry``; 
Cmd)(e1))
a Prior(RSC_VoterState(Cmd) n)?
z.{0}(e1)
b Prior(RSC_VoterState(Cmd) n)?z.{0}(e2)
(a < b))
Proof not projected
Definitions occuring in Statement :
RSC_VoterState: RSC_VoterState(Cmd),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
primed-class-opt: Prior(X)?b,
classrel: v X(e),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-E: E,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
less_than: a < b,
apply: f a,
lambda: x.A[x],
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
natural_number: $n,
int: ,
token: "$token",
single-bag: {x},
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
all: x:A. B[x],
implies: P Q,
exists: x:A. B[x],
RSC_VoterState: Error :RSC_VoterState,
member: t T,
nat: 
,
ge: i 
j ,
le: A 
B,
not: 
A,
false: False,
prop: 
,
squash: 
T,
true: True,
Accum-class: Accum-class(f;init;X),
RSC_new_retry: Error :RSC_new_retry,
top: Top,
and: P 
Q,
ifthenelse: if b then t else f fi ,
band: p 
q,
cand: A c B,
name: Name,
btrue: tt,
or: P 
Q,
guard: {T},
bfalse: ff,
es-locl: (e <loc e'),
strongwellfounded: SWellFounded(R[x; y]),
sq_stable: SqStable(P),
rev_uimplies: rev_uimplies(P;Q),
uiff: uiff(P;Q),
uimplies: b supposing a,
es-p-local-pred: es-p-local-pred(es;P),
iff: P 
Q,
single-valued-classrel: single-valued-classrel(es;X;T),
sq_type: SQType(T),
bool: 
,
unit: Unit,
subtype: S 
T,
it: 
,
RSC_Retry: Error :RSC_Retry
Lemmas :
es-causl-swellfnd,
event-ordering+_inc,
Message_wf,
nat_properties,
ge_wf,
nat_wf,
le_wf,
es-causl_wf,
rec-combined-class-opt-1-classrel,
Accum-class_wf,
Error :RSC_new_retry_wf,
Error :RSC_Retry_wf,
sq_stable__valueall-type,
valueall-type_wf,
simple-comb-2-classrel,
primed-class-opt_wf,
Error :RSC_VoterState_wf,
classrel_wf,
simple-comb-2_wf,
lifting-2_wf,
primed-class-opt-classrel,
es-locl-trichotomy,
single-bag_wf,
Id_wf,
base-headers-msg-val_wf,
es-locl_wf,
es-E_wf,
event-ordering+_wf,
eq_int_eq_true,
eq_int_wf,
bool_wf,
band_wf,
ifthenelse_wf,
RSC_VoterState-single-val,
subtype_base_sq,
int_subtype_base,
assert_wf,
bor_wf,
bnot_wf,
not_wf,
uiff_transitivity,
eqtt_to_assert,
assert_of_band,
and_functionality_wrt_uiff,
assert_of_eq_int,
iff_transitivity,
iff_weakening_uiff,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_thru_band,
assert_of_bor,
or_functionality_wrt_uiff,
assert_of_bnot,
not_functionality_wrt_uiff
\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO'].
\mforall{}e1,e2:E. \mforall{}n,a,b:\mBbbZ{}.
((e1 <loc e2)
{}\mRightarrow{} (\mexists{}c:Cmd. <<n, a>, c> \mmember{} Base(``sc retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e1))
{}\mRightarrow{} a \mmember{} Prior(RSC\_VoterState(Cmd) n)?\mlambda{}z.\{0\}(e1)
{}\mRightarrow{} b \mmember{} Prior(RSC\_VoterState(Cmd) n)?\mlambda{}z.\{0\}(e2)
{}\mRightarrow{} (a < b))
Date html generated:
2012_02_20-PM-04_02_55
Last ObjectModification:
2012_02_02-PM-01_59_41
Home
Index