---

{ [M:Type  Type]. [r:fulpRunType(P.M[P])]. [t:].
    (run-system(r;t)  System(P.M[P])) }

{ Proof }

---

Definitions occuring in Statement :  run-system: run-system(r;t),  fulpRunType: fulpRunType(T.M[T]),  System: System(P.M[P]),  nat_plus: ,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  fulpRunType: fulpRunType(T.M[T]),  so_apply: x[s],  member: t  T,  run-system: run-system(r;t),  nat: ,  so_lambda: x.t[x],  le: A  B,  not: A,  implies: P  Q,  false: False,  nat_plus: ,  prop:
Lemmas :  pi2_wf,  Id_wf,  pMsg_wf,  unit_wf,  System_wf,  nat_plus_properties,  le_wf,  nat_plus_wf,  nat_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:fulpRunType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].    (run-system(r;t)  \mmember{}  System(P.M[P]))


Date html generated: 2011_08_16-PM-06_56_38
Last ObjectModification: 2011_06_18-AM-11_10_35

Home Index