Nuprl Lemma : std-components-property
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.∃cause:E ─→ (E?)
(∀C∈Cs.∀e:E
let G = last(data-stream(snd(C);map(λe.info(e);≤loc(e)))) in
∀p∈G.let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e') = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
supposing Continuous+(P.M[P])
Proof
Definitions occuring in Statement :
system-strongly-realizes: system-strongly-realizes,
command-to-msg: command-to-msg(c;nmsg;lmsg),
reliable-env: reliable-env(env; r),
component: component(P.M[P]),
com-kind: com-kind(c),
pMsg: pMsg(P.M[P]),
data-stream: data-stream(P;L),
lg-all: ∀x∈G.P[x],
lg-nil: lg-nil(),
es-info: info(e),
es-le-before: ≤loc(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
l_all: (∀x∈L.P[x]),
last: last(L),
l_member: (x ∈ l),
map: map(f;as),
cons: [a / b],
nil: [],
list: T List,
strong-type-continuous: Continuous+(T.F[T]),
nat: ℕ,
let: let,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
unit: Unit,
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
spread: spread def,
pair: <a, b>,
inl: inl x,
union: left + right,
token: "$token",
atom: Atom,
universe: Type,
equal: s = t ∈ T
Lemmas :
pRun-invariant2,
nat_wf,
lg-nil_wf_dag,
pInTransit_wf,
pRun_wf2,
reliable-env-property2,
rec_select_update_lemma,
runEvents_wf,
true_wf,
run-event-loc_wf,
run-cause_wf,
subtype_rel_dep_function,
unit_wf2,
subtype_rel_sum,
set_wf,
reliable-env_wf,
pEnvType_wf,
sub-system_wf,
InitialSystem_wf,
list_wf,
component_wf,
Id_wf,
pMsg_wf,
strong-type-continuous_wf,
select_wf,
sq_stable__le,
int_seg_subtype-nat,
length_wf,
false_wf,
less_than_wf,
int_seg_wf,
sub-system_transitivity,
cons_wf,
nil_wf,
member_iff_sublist,
lg-nil_wf,
lg-contains_weakening,
map_append_sq,
map_cons_lemma,
map_nil_lemma,
data-stream-append,
map_wf,
es-E_wf,
stdEO_wf,
es-info_wf,
es-before_wf,
subtype_rel_list,
top_wf,
data-stream-cons,
data_stream_nil_lemma,
last_append,
Process-stream_wf,
pExt_wf,
null_cons_lemma,
length_of_cons_lemma,
length_of_nil_lemma,
equal_wf,
es-loc_wf,
event-ordering+_subtype,
Process_wf,
run-event-step-positive,
l_member_wf,
run-event-state-when_wf,
Process-apply_wf,
run-info_wf,
lg-size_wf,
pCom_wf,
lg-label_wf,
com-kind_wf,
equal_functionality_wrt_subtype_rel2,
and_wf,
squash_wf,
run-lt_wf,
exists_wf,
command-to-msg_wf,
subtype_rel_transitivity,
pRun_wf,
iterate-Process_wf,
es-first_wf2,
bool_wf,
eqtt_to_assert,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
iter_df_nil_lemma,
null_nil_lemma,
list_subtype_base,
set_subtype_base,
assert_wf,
is-run-event_wf,
product_subtype_base,
le_wf,
int_subtype_base,
atom2_subtype_base,
nil-iff-no-member,
run-event-history_wf,
es-locl-first,
assert_elim,
btrue_neq_bfalse,
es-locl_wf,
stdEO-event-history,
not_wf,
run-event-step_wf,
stdEO-locl,
adjacent-run-states,
decidable__le,
not-le-2,
less-iff-le,
condition-implies-le,
minus-add,
minus-one-mul,
add-swap,
add-associates,
zero-add,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel2,
l_contains_wf,
mapfilter_wf,
eq_id_wf,
nat_plus_wf,
fulpRunType_wf,
null_wf3,
assert_of_null,
equal-wf-T-base,
sublist_wf,
lg-contains_wf,
System_wf,
member_sublist,
filter_wf5,
member_filter_2,
all_wf,
member_map,
filter_cons_lemma,
filter_nil_lemma,
cons_member,
iff_weakening_equal,
eq_id_self,
btrue_wf,
bfalse_wf,
bnot_wf,
l_contains-member,
run-prior-state_wf,
stdEO-E-property,
es-init_wf,
es-pred_wf,
es-loc-init,
es-loc-pred,
es-init-le-iff,
es-pred-loc-base,
es-pred-locl,
es-causle_weakening_locl,
es-causle_wf,
stdEO-causal,
le_weakening2,
le_weakening,
es-first-init,
assert_of_tt,
assert-eq-id,
decidable__lt,
le-add-cancel,
es-locl-iff,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
es-le_weakening,
trivial-int-eq1,
run-event-state_wf,
es-le-before_wf,
run-event-msg_wf,
es-init-elim2,
es-le_wf,
es-interval_wf,
sorted-by-strict-unique,
less_than_transitivity2,
less_than_irreflexivity,
run-event-interval_wf,
es-interval_wf2,
member-run-event-interval,
member-es-interval,
stdEO-le,
l_member_subtype,
l_before_select,
lelt_wf,
l_before-es-interval,
from-upto_wf,
list_induction,
subtype_rel_sets,
zero-le-nat,
subtype_rel_self,
length-map,
map-length,
length_wf_nat,
sqequal-wf-base,
less_than_transitivity1,
le_int_wf,
assert_of_le_int,
select-cons,
select-map,
subtract_wf,
minus-zero,
minus-minus,
sorted-by-filter,
non_neg_length,
from-upto-sorted,
length-map-sq,
list-set-type2,
l_all_iff,
es-le-loc,
filter_trivial,
es-ble_wf,
assert-es-ble,
l_all_wf2,
isect_wf,
last_wf,
append_wf,
list-cases,
product_subtype_list,
append_is_nil,
list_ind_nil_lemma,
list_ind_cons_lemma,
lg-all_wf,
es-causl_wf
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.\mexists{}cause:E {}\mrightarrow{} (E?)
(\mforall{}C\mmember{}Cs.\mforall{}e:E
let G = last(data-stream(snd(C);map(\mlambda{}e.info(e);\mleq{}loc(e)))) in
\mforall{}p\mmember{}G.let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':E
((loc(e') = y)
\mwedge{} (e < e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((cause e') = (inl e))))
supposing loc(e) = (fst(C)))
supposing Continuous+(P.M[P])
Date html generated:
2015_07_23-AM-11_25_15
Last ObjectModification:
2015_02_04-PM-05_01_30
Home
Index