Nuprl Lemma : pRun-System-invariant

∀[M:Type ─→ Type]
  ∀[Q:ℕ ─→ System(P.M[P]) ─→ ℙ]
    ∀nat2msg:ℕ ─→ pMsg(P.M[P]). ∀loc2msg:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]).
      (Q[0;S0]
      ⇒ (∀t:ℕ. ∀S:System(P.M[P]).
            (Q[t;S]
            ⇒ (∀env:pEnvType(P.M[P])
                  let n,m,nm = env (t + 1) pRun(S0;env;nat2msg;loc2msg) in 
                  Q[t + 1;snd(do-chosen-command(nat2msg;loc2msg;t + 1;S;n;m;nm))])))
      ⇒ {∀env:pEnvType(P.M[P]). ∀t:ℕ.  Q[t;snd((pRun(S0;env;nat2msg;loc2msg) t))]}) 
  supposing Continuous+(P.M[P])


Proof



Definitions occuring in Statement :  pRun: pRun(S0;env;nat2msg;loc2msg),  pEnvType: pEnvType(T.M[T]),  do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm),  System: System(P.M[P]),  pMsg: pMsg(P.M[P]),  Id: Id,  strong-type-continuous: Continuous+(T.F[T]),  nat: ℕ,  spreadn: spread3,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  prop: ℙ,  guard: {T},  so_apply: x[s1;s2],  so_apply: x[s],  pi2: snd(t),  all: ∀x:A. B[x],  implies: P ⇒ Q,  apply: f a,  function: x:A ─→ B[x],  add: n + m,  natural_number: $n,  universe: Type
Lemmas :  nat_wf,  less_than_transitivity1,  less_than_irreflexivity,  int_seg_wf,  decidable__equal_int,  subtype_rel-int_seg,  false_wf,  le_weakening,  subtract_wf,  int_seg_properties,  le_wf,  eq_int_wf,  bool_wf,  eqtt_to_assert,  assert_of_eq_int,  System_wf,  subtype_base_sq,  int_subtype_base,  iff_weakening_equal,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_int,  int_upper_subtype_nat,  nat_properties,  nequal-le-implies,  zero-add,  all_wf,  int_seg_subtype-nat,  pRun_wf,  fulpRunType_wf,  pMsg_wf,  unit_wf2,  decidable__lt,  not-equal-2,  condition-implies-le,  minus-add,  minus-minus,  minus-one-mul,  add-swap,  add-commutes,  add-associates,  add_functionality_wrt_le,  le-add-cancel-alt,  less-iff-le,  le-add-cancel,  lelt_wf,  set_wf,  less_than_wf,  primrec-wf2,  decidable__le,  not-le-2,  sq_stable__le,  add-zero,  add-mul-special,  zero-mul,  pEnvType_wf,  pRun_wf2,  subtype_rel_dep_function,  top_wf,  ldag_wf,  pInTransit_wf,  subtype_rel_self,  do-chosen-command_wf,  Id_wf,  strong-type-continuous_wf,  subtract-is-less,  trivial-int-eq1
Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[Q:\mBbbN{}  {}\mrightarrow{}  System(P.M[P])  {}\mrightarrow{}  \mBbbP{}]
        \mforall{}nat2msg:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}loc2msg:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S0:System(P.M[P]).
            (Q[0;S0]
            {}\mRightarrow{}  (\mforall{}t:\mBbbN{}.  \mforall{}S:System(P.M[P]).
                        (Q[t;S]
                        {}\mRightarrow{}  (\mforall{}env:pEnvType(P.M[P])
                                    let  n,m,nm  =  env  (t  +  1)  pRun(S0;env;nat2msg;loc2msg)  in 
                                    Q[t  +  1;snd(do-chosen-command(nat2msg;loc2msg;t  +  1;S;n;m;nm))])))
            {}\mRightarrow{}  \{\mforall{}env:pEnvType(P.M[P]).  \mforall{}t:\mBbbN{}.    Q[t;snd((pRun(S0;env;nat2msg;loc2msg)  t))]\}) 
    supposing  Continuous+(P.M[P])


Date html generated: 2015_07_23-AM-11_10_23
Last ObjectModification: 2015_02_04-PM-04_48_11

Home Index