---

{ [ds:z:Id fp-> Type]. (timedState(ds)  Type) }

{ Proof }

---

Definitions occuring in Statement :  ma-tstate: timedState(ds),  fpf: a:A fp-> B[a],  Id: Id,  uall: [x:A]. B[x],  member: t  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  ma-tstate: timedState(ds),  so_lambda: x.t[x],  so_apply: x[s]
Lemmas :  Id_wf,  rationals_wf,  fpf-cap_wf,  id-deq_wf,  top_wf,  fpf_wf

---

\mforall{}[ds:z:Id  fp->  Type].  (timedState(ds)  \mmember{}  Type)


Date html generated: 2011_08_10-AM-08_12_02
Last ObjectModification: 2011_06_18-AM-08_27_17

Home Index