---

{ [M:Type  Type]. [S:System(P.M[P])].
    (system-function(S)  Id  (Process(P.M[P]) List
                                 LabeledGraph(pInTransit(P.M[P])))) }

{ Proof }

---

Definitions occuring in Statement :  system-function: system-function(S),  System: System(P.M[P]),  pInTransit: pInTransit(P.M[P]),  Process: Process(P.M[P]),  labeled-graph: LabeledGraph(T),  Id: Id,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  system-function: system-function(S),  so_lambda: x.t[x],  lg-nil: lg-nil()
Lemmas :  fpf-cap_wf,  Id_wf,  Process_wf,  labeled-graph_wf,  pInTransit_wf,  system-fpf_wf,  id-deq_wf,  lg-nil_wf,  System_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[S:System(P.M[P])].
    (system-function(S)  \mmember{}  Id  {}\mrightarrow{}  (Process(P.M[P])  List  \mtimes{}  LabeledGraph(pInTransit(P.M[P]))))


Date html generated: 2011_08_16-PM-06_52_10
Last ObjectModification: 2011_06_18-AM-11_06_50

Home Index