---

{ [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
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  strong-type-continuous: Continuous+(T.F[T]),  so_apply: x[s],  nat: ,  prop: ,  all: x:A. B[x],  implies: P  Q,  so_apply: x[s1;s2],  spreadn: spread3,  pRun: pRun(S0;env;nat2msg;loc2msg),  pi2: snd(t),  guard: {T},  member: t  T,  ext-eq: A  B,  and: P  Q,  so_lambda: x.t[x],  top: Top,  nat_plus: ,  le: A  B,  not: A,  false: False,  fulpRunType: fulpRunType(T.M[T]),  ycomb: Y,  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  ge: i  j ,  System: System(P.M[P]),  int_seg: {i..j},  unit: Unit,  lelt: i  j < k,  bool: ,  iff: P  Q,  sq_type: SQType(T),  it:
Lemmas :  nat_wf,  pEnvType_wf,  System_wf,  nat_properties,  pRun_wf,  subtype_rel_function,  Id_wf,  pMsg_wf,  unit_wf,  int_seg_wf,  top_wf,  ldag_wf,  pInTransit_wf,  le_wf,  subtype_rel_simple_product,  subtype_rel_self,  fulpRunType_wf,  pi2_wf,  do-chosen-command_wf,  strong-type-continuous_wf,  eq_int_wf,  bool_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_eq_int,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff,  ge_wf,  subtype_base_sq,  int_subtype_base

---

\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: 2011_08_16-PM-06_56_58
Last ObjectModification: 2011_06_18-AM-11_10_56

Home Index