Nuprl Lemma : run-event-state-next

[M:Type  Type]
  n2m:  pMsg(P.M[P]). l2m:Id  pMsg(P.M[P]). S0:System(P.M[P]). env:pEnvType(P.M[P]).
    let r = pRun(S0;env;n2m;l2m) in
        e:runEvents(r)
          sub-mset(Process(P.M[P]); map(P.(fst(Process-apply(P;run-event-msg(r;e))));run-prior-state(S0;r;e));
                   run-event-state(r;e)) 
  supposing Continuous+(P.M[P])


Proof not projected



Definitions occuring in Statement :  run-prior-state: run-prior-state(S0;r;e),  run-event-state: run-event-state(r;e),  run-event-msg: run-event-msg(r;e),  runEvents: runEvents(r),  pRun: pRun(S0;env;nat2msg;loc2msg),  pEnvType: pEnvType(T.M[T]),  System: System(P.M[P]),  Process-apply: Process-apply(P;m),  pMsg: pMsg(P.M[P]),  Process: Process(P.M[P]),  Id: Id,  strong-type-continuous: Continuous+(T.F[T]),  map: map(f;as),  nat: ,  let: let,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  pi1: fst(t),  all: x:A. B[x],  lambda: x.A[x],  function: x:A  B[x],  universe: Type,  sub-mset: sub-mset(T; L1; L2)
Definitions :  int_seg: {i..j},  guard: {T},  bfalse: ff,  btrue: tt,  exposed-bfalse: exposed-bfalse,  ycomb: Y,  ifthenelse: if b then t else f fi ,  run-info: run-info(r;e),  outl: outl(x),  isl: isl(x),  band: p  q,  spreadn: spread3,  true: True,  squash: T,  implies: P  Q,  pi2: snd(t),  is-run-event: is-run-event(r;t;x),  assert: b,  so_lambda: x.t[x],  fulpRunType: fulpRunType(T.M[T]),  pRunType: pRunType(T.M[T]),  and: P  Q,  ext-eq: A  B,  member: t  T,  run-event-state: run-event-state(r;e),  run-event-msg: run-event-msg(r;e),  pRun: pRun(S0;env;nat2msg;loc2msg),  let: let,  Id: Id,  nat: ,  all: x:A. B[x],  so_apply: x[s],  strong-type-continuous: Continuous+(T.F[T]),  uimplies: b supposing a,  uall: [x:A]. B[x],  pi1: fst(t),  do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm),  cand: A c B,  subtype: S  T,  top: Top,  prop: ,  false: False,  le: A  B,  lelt: i  j < k,  exists: x:A. B[x],  not: A,  System: System(P.M[P]),  list_accum: list_accum(x,a.f[x; a];y;l),  reduce: reduce(f;k;as),  filter: filter(P;l),  map: map(f;as),  append: as @ bs,  reverse: rev(as),  deliver-msg: deliver-msg(t;m;x;Cs;L),  mapfilter: mapfilter(f;P;L),  deliver-msg-to-comp: deliver-msg-to-comp(t;m;x;S;C),  iff: P  Q,  rev_implies: P  Q,  component: component(P.M[P]),  eq_int: (i = j),  compose: f o g,  ge: i  j ,  suptype: suptype(S; T),  exposed-it: exposed-it,  so_lambda: x y.t[x; y],  unit: Unit,  sub-mset: sub-mset(T; L1; L2),  sq_type: SQType(T),  uiff: uiff(P;Q),  bool: ,  sq_stable: SqStable(P),  runEvents: runEvents(r),  or: P  Q,  lg-is-source: lg-is-source(g;i),  pInTransit: pInTransit(P.M[P]),  decidable: Dec(P),  so_apply: x[s1;s2],  create-component: create-component(t;P;x;Cs;L),  it:
Lemmas :  strong-type-continuous_wf,  pEnvType_wf,  runEvents_wf,  eq_id_wf,  atom2_subtype_base,  subtype_base_sq,  assert-eq-id,  System_wf,  pi2_wf,  do-chosen-command_wf,  subtype_rel_self,  le_wf,  lelt_wf,  subtype_rel_sets,  int_seg_wf,  pInTransit_wf,  ldag_wf,  top_wf,  unit_wf2,  pMsg_wf,  Id_wf,  subtype_rel_dep_function,  not_functionality_wrt_uiff,  assert_of_bnot,  eqff_to_assert,  not_wf,  bnot_wf,  false_wf,  assert_of_eq_int,  eqtt_to_assert,  assert_wf,  equal_wf,  uiff_transitivity,  bool_wf,  eq_int_wf,  is-run-event_wf,  sq_stable__assert,  pRunType_wf,  fulpRunType_wf,  fulpRunType-subtype,  pRun_wf,  nat_wf,  lg-is-source_wf_dag,  true_wf,  squash_wf,  and_wf,  assert_of_le_int,  bnot_of_lt_int,  assert_functionality_wrt_uiff,  assert_of_lt_int,  bool_subtype_base,  bool_cases,  member_wf,  bfalse_wf,  assert_elim,  btrue_neq_bfalse,  le_int_wf,  less_than_wf,  lt_int_wf,  comm-create_wf,  create-component_wf,  it_wf,  comm-msg_wf,  deliver-msg_wf,  component_wf,  lg-remove_wf_dag,  isl_wf,  outl_wf,  pi1_wf_top,  assert_of_eq_atom,  com-kind_wf,  eq_atom_wf,  lg-size_wf_dag,  lg-label_wf_dag,  subtype_rel_list,  reverse_wf,  filter_type,  map-is-top-list,  append-nil,  Process_wf,  mapfilter_wf,  reverse-reverse,  mapfilter-reverse,  append_wf,  add-cause_wf,  lg-append_wf_dag,  pExt_wf,  Process-apply_wf,  mapfilter-singleton,  mapfilter-append,  l_member_wf,  append_assoc_sq,  subtype_rel_simple_product,  run-prior-state_wf,  map_wf,  sub-mset_transitivity,  run-prior-state-property,  sub-mset_wf,  length_wf_nat,  map-map,  filter_wf,  sub-mset-map,  Error :pi2_wf,  unit_wf,  all_wf,  ge_wf,  nat_properties,  decidable__equal_int,  permutation_weakening,  sub-mset_weakening,  int_subtype_base,  list_accum_append,  filter_append_sq,  deliver-msg-to-comp_wf,  list_accum_wf,  permutation_wf,  last_induction,  permutation-cons2,  permutation-rotate,  permutation_transitivity,  int_seg_properties,  exists_wf,  permutation-reverse
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S0:System(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
        let  r  =  pRun(S0;env;n2m;l2m)  in
                \mforall{}e:runEvents(r)
                    sub-mset(Process(P.M[P]);  map(\mlambda{}P.(fst(Process-apply(P;run-event-msg(r;e))));
                                                                                run-prior-state(S0;r;e));  run-event-state(r;e)) 
    supposing  Continuous+(P.M[P])


Date html generated: 2012_01_23-PM-12_43_34
Last ObjectModification: 2011_12_13-PM-08_13_11

Home Index