---

{ [L:{dv:ClassDerivation| WF(dv)}  List]
    (list-to-cdv(L)  {dv:ClassDerivation| WF(dv)} ) }

{ Proof }

---

Definitions occuring in Statement :  list-to-cdv: list-to-cdv(L),  cdv-wf: WF(dv),  classderiv: ClassDerivation,  uall: [x:A]. B[x],  member: t  T,  set: {x:A| B[x]} ,  listp: A List
Definitions :  uall: [x:A]. B[x],  member: t  T,  list-to-cdv: list-to-cdv(L),  ycomb: Y,  list_accum: list_accum(x,a.f[x; a];y;l),  hd: hd(l),  tl: tl(l),  all: x:A. B[x],  cdv-wf: WF(dv),  and: P  Q,  listp: A List,  ge: i  j ,  length: ||as||,  prop: ,  le: A  B,  not: A,  implies: P  Q,  false: False
Lemmas :  listp_properties,  classderiv_wf,  cdv-wf_wf,  listp_wf,  cdvpair_wf

---

\mforall{}[L:\{dv:ClassDerivation|  WF(dv)\}    List\msupplus{}].  (list-to-cdv(L)  \mmember{}  \{dv:ClassDerivation|  WF(dv)\}  )


Date html generated: 2011_08_17-PM-04_27_43
Last ObjectModification: 2011_06_18-AM-11_40_50

Home Index