---

{ [env:E#Env]. [x:Atom].
    esharp-base(env;x)  {dv:ClassDerivation| WF(dv)  (||cdv-types(dv)|| = 1)} \000C 
    supposing esharp-base-wf(env;x) }

{ Proof }

---

Definitions occuring in Statement :  esharp-base: esharp-base(env;x),  esharp-base-wf: esharp-base-wf(env;x),  esharp-env: E#Env,  cdv-wf: WF(dv),  cdv-types: cdv-types(dv),  classderiv: ClassDerivation,  length: ||as||,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  and: P  Q,  member: t  T,  set: {x:A| B[x]} ,  natural_number: $n,  int: ,  atom: Atom,  equal: s = t
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  assert: b,  esharp-base-wf: esharp-base-wf(env;x),  member: t  T,  and: P  Q,  cdv-wf: WF(dv),  length: ||as||,  cdv-types: cdv-types(dv),  esharp-base: esharp-base(env;x),  btrue: tt,  bfalse: ff,  outl: outl(x),  outr: outr(x),  all: x:A. B[x],  implies: P  Q,  ifthenelse: if b then t else f fi ,  true: True,  ycomb: Y,  esharp-env: E#Env,  prop: ,  false: False
Lemmas :  apply-alist_wf,  atom-deq_wf,  base-deriv_wf,  combinator-def_wf,  classderiv_wf,  cdv-wf_wf,  length_wf1,  cdv-types_wf,  unit_wf,  cdvbase_wf,  true_wf,  false_wf,  assert_wf,  esharp-base-wf_wf,  esharp-env_wf

---

\mforall{}[env:E\#Env].  \mforall{}[x:Atom].
    esharp-base(env;x)  \mmember{}  \{dv:ClassDerivation|  WF(dv)  \mwedge{}  (||cdv-types(dv)||  =  1)\}   
    supposing  \muparrow{}esharp-base-wf(env;x)


Date html generated: 2011_08_17-PM-04_31_45
Last ObjectModification: 2011_06_18-AM-11_43_04

Home Index