Nuprl Lemma : mu_ex_v5_ZigZag
es:EO'. m1,m2,init,p1,p2:Id.
(strong-message-constraint-no-rep-large{i:l}(es;mu_ex_v5_main(init;m1;m2;p1;p2);mu_ex_v5_headers_no_inputs())
mu_ex_v5_cs-constraint{i:l}(es;m1;m2;init;p1;p2)
(e:E. p:Id.
((
mu_ex_v5_Token()(e) 
<p, make-Msg([token];Unit;)> mu_ex_v5_main(init;m1;m2;p1;p2)(e))
(
L:E List
((last(L) = e)
<mu_ex_v5_getOtherProc(p1;p2) init, make-Msg([token];Unit;)> mu_ex_v5_main(init;m1;m2;p1;p2)(hd(L))
(e':E
((e' L)
(( mu_ex_v5_Token()(e')
(p:Id. <p, make-Msg([token];Unit;)> mu_ex_v5_main(init;m1;m2;p1;p2)(e')))
e' c
e)))
(e':E
(( mu_ex_v5_Token()(e')
(p:Id. <p, make-Msg([token];Unit;)> mu_ex_v5_main(init;m1;m2;p1;p2)(e')))
(e' <loc e)
(e' L)))
(i:
||L|| - 1
(( mu_ex_v5_Token()(L[i])
(<mu_ex_v5_getOtherProc(p1;p2) loc(L[i + 1]), make-Msg([token];Unit;)>
mu_ex_v5_main(init;m1;m2;p1;p2)(L[i + 1])
(L[i] <loc L[i + 1])))
(p:Id
(<p, make-Msg([token];Unit;)> mu_ex_v5_main(init;m1;m2;p1;p2)(L[i])
( mu_ex_v5_Token()(L[i + 1]) (p = loc(L[i + 1])) (L[i] < L[i + 1])))))))))))
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_cs-constraint: mu_ex_v5_cs-constraint{i:l}(es;m1;m2;init;p1;p2),
mu_ex_v5_headers_no_inputs: mu_ex_v5_headers_no_inputs(),
mu_ex_v5_main: mu_ex_v5_main(initial_token;m1;m2;proc1;proc2),
mu_ex_v5_getOtherProc: mu_ex_v5_getOtherProc(proc1;proc2),
mu_ex_v5_Token: mu_ex_v5_Token(),
make-Msg: make-Msg(hdr;typ;val),
strong-message-constraint-no-rep-large: strong-message-constraint-no-rep-large{i:l}(es;X;hdrs),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-causle: e c e',
es-locl: (e <loc e'),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
select: l[i],
hd: hd(l),
length: ||as||,
int_seg: {i..j
},
it: ,
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
or: P Q,
and: P Q,
unit: Unit,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
cons: [car / cdr],
nil: [],
subtract: n - m,
add: n + m,
natural_number: $n,
token: "$token",
equal: s = t,
listp: A List,
last: last(L),
l_member: (x l)
Definitions :
all: x:A. B[x],
implies: P Q,
or: P Q,
unit: Unit,
squash: T,
member: t T,
nat: ,
ge: i 
j ,
le: A B,
not: 
A,
false: False,
prop: 
,
true: True,
mu_ex_v5_headers_no_inputs: mu_ex_v5_headers_no_inputs(),
and: P Q,
int_seg: {i..j},
length: ||as||,
select: l[i],
name: Name,
lelt: i j < k,
ycomb: Y,
ifthenelse: if b then t else f fi ,
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
btrue: tt,
bfalse: ff,
bag: bag(T),
top: Top,
guard: {T},
exists: x:A. B[x],
so_lambda: 
x.t[x],
listp: A List,
subtype: S 
T,
last: last(L),
assert: 
b,
null: null(as),
rev_implies: P 
Q,
iff: P Q,
so_lambda: x y.t[x; y],
label: ...$L... t,
single-bag: {x},
pi2: snd(t),
name_eq: name_eq(x;y),
so_apply: x[s],
name-deq: NameDeq,
list-deq: list-deq(eq),
band: p q,
atom-deq: AtomDeq,
eq_atom: x =a y,
sub-bag: sub-bag(T;as;bs),
pi1: fst(t),
bag-member: x bs,
uimplies: b supposing a,
uiff: uiff(P;Q),
cand: A c B,
class-output: class-output(X;es;bg),
Id: Id,
hd: hd(l),
append: as @ bs,
filter: filter(P;l),
reduce: reduce(f;k;as),
gt: i > j,
bag-append: as + bs,
mapfilter: mapfilter(f;P;L),
map: map(f;as),
mu_ex_v5_Token: mu_ex_v5_Token(),
es-header: es-header(es;e),
msg-has-type: msg-has-type(m;T),
make-Msg: make-Msg(hdr;typ;val),
msg-header: msg-header(m),
mu_ex_v5_getOtherProc: mu_ex_v5_getOtherProc(proc1;proc2),
class-le-before: class-le-before(X;es;e),
bag-filter: [xb|p[x]],
empty-bag: {},
classrel: v X(e),
l_disjoint: l_disjoint(T;l1;l2),
bag-no-repeats: bag-no-repeats(T;bs),
es-locl: (e <loc e'),
uall: [x:A]. B[x],
Accum-loc-class: Accum-loc-class(f;init;X),
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
mu_ex_v5_State: mu_ex_v5_State(initial_token),
disjoint-union-tr: tr1 + tr2,
mu_ex_v5_onRequest: mu_ex_v5_onRequest(),
isl: isl(x),
spreadn: spread3,
mu_ex_v5_onLeaveCS: mu_ex_v5_onLeaveCS(),
outr: outr(x),
eq_id: a = b,
eqof: eqof(d),
strongwellfounded: SWellFounded(R[x; y]),
strong-message-constraint-no-rep-large: strong-message-constraint-no-rep-large{i:l}(es;X;hdrs),
delivered-with-headers: delivered-with-headers(hdrs;es;e),
deq-member: deq-member(eq;x;L),
es-le-before: loc(e),
bor: p q,
rev_uimplies: rev_uimplies(P;Q),
sq_type: SQType(T),
sq_stable: SqStable(P),
so_apply: x[s1;s2],
bool: 
,
sq_or: a b,
deq: EqDecider(T),
l_member: (x l),
decidable: Dec(P),
es-sv-class: es-sv-class(es;X),
es-le: e loc e' ,
message-constraint: message-constraint{i:l}(es;X;hdrs),
es-p-local-pred: es-p-local-pred(es;P),
mu_ex_v5_LeaveCS: mu_ex_v5_LeaveCS(),
mu_ex_v5_UseSR: mu_ex_v5_UseSR(),
mu_ex_v5_Request: mu_ex_v5_Request(),
mu_ex_v5_initState: mu_ex_v5_initState(initial_token),
it: ,
cons-bag: x.b,
eclass: EClass(A[eo; e]),
bag-map: bag-map(f;bs),
!hyp_hide: x
Lemmas :
es-causl-swellfnd,
event-ordering+_inc,
Message_wf,
nat_properties,
ge_wf,
less_than_wf,
nat_wf,
le_wf,
es-causl_wf,
or_wf,
classrel_wf,
unit_wf2,
mu_ex_v5_Token_wf,
it_wf,
Id_wf,
mu_ex_v5_main_wf,
make-Msg_wf,
equal-valueall-type,
valueall-type_wf,
equal_wf,
es-E_wf,
mu_ex_v5_cs-constraint_wf,
strong-message-constraint-no-rep-large_wf,
mu_ex_v5_headers_no_inputs_wf,
event-ordering+_wf,
mu_ex_v5_no_repeats_headers_no_inputs,
strong-message-constraint-no-rep-large-1hdr,
select_member,
name_wf,
mapfilter-append,
es-before_wf,
top_wf,
bor_wf,
eqof_wf,
name-deq_wf,
es-header_wf,
bfalse_wf,
l_member_wf,
mapfilter-singleton,
assert-name_eq,
base-noloc-classrel,
subtype_base_sq,
bool_wf,
bool_subtype_base,
sub-bag-append-left2,
bag_wf,
mapfilter_wf,
name_eq_wf,
es-loc_wf,
es-info_wf,
assert_wf,
bag_qinc,
class-output_wf,
sub-bag-singleton-left,
member-class-output,
member-class-le-before,
assert_elim,
sq_stable__equal,
mu_ex_v5_getOtherProc_wf,
sq_stable__and,
es-info-make-Msg,
mu_ex_v5_Token-ilf,
es-le_wf,
and_wf,
es-locl-trichotomy,
bag-member_wf,
es-le-loc,
mu_ex_v5_closest-send-token2,
es-causle_weakening_locl,
es-causl_transitivity1,
append_wf,
es-locl_wf,
exists_wf,
select_wf,
length_wf,
int_seg_wf,
last_wf,
hd_wf,
all_wf,
es-causle_wf,
length-append,
assert_of_lt_int,
non_neg_length,
length_wf_nat,
lt_int_wf,
last_append,
false_wf,
select-as-hd,
squash_wf,
true_wf,
eclass_wf,
select_append,
length_nil,
length_wf_nil,
length_cons,
lelt_wf,
listp_properties,
iff_imp_equal_bool,
btrue_wf,
iff_functionality_wrt_iff,
iff_weakening_uiff,
member_append,
cons_member,
nil_member,
es-causle_weakening,
es-causle_weakening_eq,
sub-bag_wf,
bag-append_wf,
bag-filter_wf,
msg-header_wf,
pi2_wf,
subtype_rel_bag,
bag-filter-append,
bag-filter-singleton,
eqtt_to_assert,
uiff_transitivity,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
empty-bag_wf,
bag-filter-trivial2,
filter_wf,
bag-member-map,
sq_stable__assert,
pi1_wf_top,
bag-member-filter,
assert_of_bor,
assert_functionality_wrt_uiff,
btrue_neq_bfalse,
eq_id_wf,
eq_id_self,
bag-member-list,
decidable__es-E-equal,
member-es-before,
sub-bag-filter2,
bag-split,
es-eq-E_wf,
bag-extensionality-no-repeats,
single-bag_wf,
bag-filter-no-repeats,
bag-no-repeats-single,
bag-member-single,
assert-es-eq-E-2,
assert-es-eq-E,
bag-combine-append-left,
class-le-before_wf,
band_wf,
bag-combine_wf,
bag-combine-single-left,
bag-filter-empty-iff,
assert_of_band,
assert-bag-null,
subtype_rel_set_simple,
bag-member-combine,
not_functionality_wrt_uiff,
mu_ex_v5_send-token-unit,
assert-eq-id,
atom2_subtype_base,
mu_ex_v5_send-token-from-same-loc,
bag-member-filter-set,
bag-append-empty,
bag-filter-equal,
mu_ex_v5_send-token-to-same-loc2,
length_zero,
eq_term_wf,
msg-type_wf,
type-valueall-type,
list-subtype-bag,
subtype_rel_self,
mu_ex_v5_tok-dec_wf,
iff_wf,
cons-bag_wf,
member_wf,
null_wf3,
assert_of_null,
listp-not-nil,
cons_wf_listp,
mu_ex_v5_send-token-not-token,
select-cons,
le_int_wf,
assert_of_le_int,
int_subtype_base,
select0,
last_cons,
pos_length2,
member_singleton,
bag-map_wf,
or_functionality_wrt_uiff,
or_functionality_wrt_iff,
bnot_thru_band,
and_functionality_wrt_uiff3,
and_functionality_wrt_iff,
iff_transitivity,
assert-eq_term,
assert-deq,
bool_cases,
id-deq_wf,
deq_wf,
ifthenelse_wf,
equal-unit,
msg-body_wf2,
map_wf_bag,
mu_ex_v5_send-single,
not_functionality_wrt_iff,
mapfilter-cons,
eq_term_comm,
not_over_and,
decidable__classrel,
decidable__equal_unit,
not_over_or,
set_subtype_base,
mu_ex_v5_main-single-val,
decidable__equal_Id,
bag-filter-combine,
es-le-before_wf2,
bag-combine-filter,
bag-combine-eq-right,
bag-size_wf,
mu_ex_v5_send-at-most-one,
bag-size-zero,
bag-size-one,
bag-only_wf,
mu_ex_v5_not-send-token,
bag-member-list-member,
es-le-before_wf,
member-es-le-before,
implies-filter-equal,
no_repeats_append_iff,
es-causl_transitivity2,
es-causl_irreflexivity,
no_repeats_cons,
no_repeats_nil,
no_repeats_wf,
int_seg_properties,
es-causl_weakening,
no_repeats_singleton,
l_before_wf,
member_filter_2,
mu_ex_v5_assert-tok-dec,
last_member,
es-causle-le,
es-le_transitivity,
l_before_filter,
l_before_append_iff,
l_before-es-le-before-iff,
es-locl_transitivity2,
es-le_weakening,
l_before_select,
event_ordering_wf,
es-locl_irreflexivity,
permutation_weakening,
list_subtype_base,
atom_subtype_base,
sub-bag-cancel-right,
filter-sq,
name_eq_symmetry,
map_wf,
strong-message-constraint-no-rep-large-implies,
sub-bag-map-equal,
filter_type,
sub-bag-no-repeats-iff,
es-eq_wf,
no_repeats_filter,
decidable__l_member,
sq_stable_from_decidable,
mu_ex_v5_send-token-received-or-born,
and_functionality_wrt_uiff2,
list-member-bag-member,
mu_ex_v5_token-between-2sends,
es-le_weakening_eq,
es-locl_transitivity1,
mu_ex_v5_send-token-state,
decidable__or,
pos_length,
es-first-le,
hd_member,
es-first_wf,
mu_ex_v5_decidable-prior-token,
mu_ex_v5_initial-send,
select-append,
mu_ex_v5_send-token-to-same-loc,
mu_ex_v5_send-token-had-token,
primed-class-opt-classrel,
mu_ex_v5_State_wf,
mu_ex_v5_initState_wf,
mu_ex_v5_State-token,
length_append,
es-causle_transitivity,
decidable__es-le,
decidable__es-locl,
es-le-not-locl,
lifting-loc-2_wf,
rec-combined-loc-class-opt-1_wf,
primed-class-opt_wf,
mu_ex_v5_LeaveCS_wf,
mu_ex_v5_UseSR_wf,
mu_ex_v5_Request_wf,
disjoint-union-class_wf,
uall_wf,
disjoint-union-tr_wf,
simple-loc-comb-2-classrel,
rec-combined-loc-class-opt-1-classrel,
mu_ex_v5_onRequest_wf,
mu_ex_v5_onLeaveCS_wf,
mu_ex_v5_onUseSR_wf,
mu_ex_v5_onToken_wf,
disjoint-union-classrel,
not_assert_elim,
mu_ex_v5_State-exists
\mforall{}es:EO'. \mforall{}m1,m2,init,p1,p2:Id.
(strong-message-constraint-no-rep-large\{i:l\}(es;mu\_ex\_v5\_main(init;m1;m2;p1;p2);...)
{}\mRightarrow{} mu\_ex\_v5\_cs-constraint\{i:l\}(es;m1;m2;init;p1;p2)
{}\mRightarrow{} (\mforall{}e:E. \mforall{}p:Id.
((\mcdot{} \mmember{} mu\_ex\_v5\_Token()(e)
\mvee{} <p, make-Msg([token];Unit;\mcdot{})> \mmember{} mu\_ex\_v5\_main(init;m1;m2;p1;p2)(e))
{}\mRightarrow{} (\mdownarrow{}\mexists{}L:E List\msupplus{}
((last(L) = e)
\mwedge{} <mu\_ex\_v5\_getOtherProc(p1;p2) init, make-Msg([token];Unit;\mcdot{})> \mmember{}
mu\_ex\_v5\_main(init;m1;m2;p1;p2)(hd(L))
\mwedge{} (\mforall{}e':E
((e' \mmember{} L)
{}\mRightarrow{} ((\mcdot{} \mmember{} mu\_ex\_v5\_Token()(e')
\mvee{} (\mexists{}p:Id
<p, make-Msg([token];Unit;\mcdot{})> \mmember{} mu\_ex\_v5\_main(init;m1;m2;p1;p2)(e')))
\mwedge{} e' c\mleq{} e)))
\mwedge{} (\mforall{}e':E
((\mcdot{} \mmember{} mu\_ex\_v5\_Token()(e')
\mvee{} (\mexists{}p:Id. <p, make-Msg([token];Unit;\mcdot{})> \mmember{} mu\_ex\_v5\_main(init;m1;m2;p1;p2)(e')))
{}\mRightarrow{} (e' <loc e)
{}\mRightarrow{} (e' \mmember{} L)))
\mwedge{} (\mforall{}i:\mBbbN{}||L|| - 1
((\mcdot{} \mmember{} mu\_ex\_v5\_Token()(L[i])
{}\mRightarrow{} (<mu\_ex\_v5\_getOtherProc(p1;p2) loc(L[i + 1]), make-Msg([token];Unit;\mcdot{})> \mmember{}
mu\_ex\_v5\_main(init;m1;m2;p1;p2)(L[i + 1])
\mwedge{} (L[i] <loc L[i + 1])))
\mwedge{} (\mforall{}p:Id
(<p, make-Msg([token];Unit;\mcdot{})> \mmember{} mu\_ex\_v5\_main(init;m1;m2;p1;p2)(L[i])
{}\mRightarrow{} (\mcdot{} \mmember{} mu\_ex\_v5\_Token()(L[i + 1])
\mwedge{} (p = loc(L[i + 1]))
\mwedge{} (L[i] < L[i + 1])))))))))))
Date html generated:
2012_02_20-PM-07_05_44
Last ObjectModification:
2012_02_02-PM-03_03_36
Home
Index