---

WF(dv) ==
  case(dv)
  Base(a)=> True
  pair(d1,d2) => wf1,wf2.wf1  wf2
  (d)'=> wf.wf
  f(d:P):T=> wf.wf  (P = cdv-argtype(d))  ((f (k.{})) = {})
  f(d:P, self'):T=> wf.wf  (P = cdv-argtype(d))  ((f (k.{}) {}) = {})

---

Definitions occuring in Statement :  cdv-argtype: cdv-argtype(dv),  classderiv_ind: classderiv_ind,  and: P  Q,  true: True,  apply: f a,  lambda: x.A[x],  universe: Type,  equal: s = t,  empty-bag: {},  bag: bag(T)
Definitions :  classderiv_ind: classderiv_ind,  true: True,  and: P  Q,  universe: Type,  cdv-argtype: cdv-argtype(dv),  equal: s = t,  bag: bag(T),  apply: f a,  lambda: x.A[x],  empty-bag: {}
FDL editor aliases :  cdv-wf

---

WF(dv)  ==
    case(dv)
    Base(a)=>  True
    pair(d1,d2)  =>  wf1,wf2.wf1  \mwedge{}  wf2
    (d)'=>  wf.wf
    f(d:P):T=>  wf.wf  \mwedge{}  (P  =  cdv-argtype(d))  \mwedge{}  ((f  (\mlambda{}k.\{\}))  =  \{\})
    f(d:P,  self'):T=>  wf.wf  \mwedge{}  (P  =  cdv-argtype(d))  \mwedge{}  ((f  (\mlambda{}k.\{\})  \{\})  =  \{\})


Date html generated: 2011_08_17-PM-04_27_25
Last ObjectModification: 2011_01_18-PM-04_38_54

Home Index