---

{ input(lp.piM(lp);0)  PiDataVal() }

{ Proof }

---

Definitions occuring in Statement :  piM: piM(T),  PiDataVal: PiDataVal(),  process-input: input(lp.M[lp];n),  ext-eq: A  B,  natural_number: $n
Definitions :  ext-eq: A  B,  process-input: input(lp.M[lp];n),  piM: piM(T),  and: P  Q,  member: t  T,  uall: [x:A]. B[x]
Lemmas :  subtype_rel_self,  PiDataVal_wf

---

input(lp.piM(lp);0)  \mequiv{}  PiDataVal()


Date html generated: 2011_08_17-PM-07_05_27
Last ObjectModification: 2011_06_18-PM-12_47_57

Home Index