---

{ [x:ClassDerivation]. cdvbase-args(x)  BaseDef supposing cdvbase?(x) }

{ Proof }

---

Definitions occuring in Statement :  cdvbase-args: cdvbase-args(x),  cdvbase?: cdvbase?(x),  classderiv: ClassDerivation,  base-deriv: BaseDef,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  assert: b,  cdvbase?: cdvbase?(x),  member: t  T,  cdvbase-args: cdvbase-args(x),  implies: P  Q,  btrue: tt,  bfalse: ff,  ifthenelse: if b then t else f fi ,  classderiv: ClassDerivation,  unit: Unit,  false: False,  it: ,  cdvbase: cdvbase(args),  prop: ,  cdvpair: cdvpair(fst;snd),  cdvdelay: cdvdelay(X;dummy),  cdvcomb: cdvcomb(typ;argtype;arg;fun),  cdvreccomb: cdvreccomb(typ;argtype;arg;fun)
Lemmas :  classderiv_wf,  true_wf,  false_wf,  assert_wf,  cdvbase?_wf

---

\mforall{}[x:ClassDerivation].  cdvbase-args(x)  \mmember{}  BaseDef  supposing  \muparrow{}cdvbase?(x)


Date html generated: 2011_08_17-PM-04_23_57
Last ObjectModification: 2011_06_18-AM-11_35_50

Home Index