{ 
[x:ClassDerivation]
cdvcomb-fun(x) 
cdvcomb-argtype(x) 
bag(cdvcomb-typ(x))
supposing 
cdvcomb?(x) }
{ Proof }
Definitions occuring in Statement :
cdvcomb-fun: cdvcomb-fun(x),
cdvcomb-argtype: cdvcomb-argtype(x),
cdvcomb-typ: cdvcomb-typ(x),
cdvcomb?: cdvcomb?(x),
classderiv: ClassDerivation,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
bag: bag(T)
Definitions :
true: True,
natural_number: $n,
classderiv_ind: classderiv_ind,
apply: f a,
it: 
,
false: False,
classderiv_ind_cdvreccomb: classderiv_ind_cdvreccomb_compseq_tag_def,
classderiv_ind_cdvcomb: classderiv_ind_cdvcomb_compseq_tag_def,
classderiv_ind_cdvdelay: classderiv_ind_cdvdelay_compseq_tag_def,
classderiv_ind_cdvpair: classderiv_ind_cdvpair_compseq_tag_def,
classderiv_ind_cdvbase: classderiv_ind_cdvbase_compseq_tag_def,
int: 
,
unit: Unit,
set: {x:A| B[x]} ,
product: x:A 
B[x],
universe: Type,
base-deriv: BaseDef,
union: left + right,
rec: rec(x.A[x]),
implies: P 
Q,
all: x:A. B[x],
cdvcomb?: cdvcomb?(x),
uall: [x:A]. B[x],
function: x:A B[x],
cdvcomb-argtype: cdvcomb-argtype(x),
bag: bag(T),
cdvcomb-typ: cdvcomb-typ(x),
cdvcomb-fun: cdvcomb-fun(x),
classderiv: ClassDerivation,
axiom: Ax,
uimplies: b supposing a,
isect: 
x:A. B[x],
assert: b,
prop: 
,
member: t T,
equal: s = t
Lemmas :
assert_wf,
cdvcomb?_wf,
classderiv_wf,
true_wf,
false_wf
\mforall{}[x:ClassDerivation]
cdvcomb-fun(x) \mmember{} cdvcomb-argtype(x) {}\mrightarrow{} bag(cdvcomb-typ(x)) supposing \muparrow{}cdvcomb?(x)
Date html generated:
2011_08_17-PM-04_25_42
Last ObjectModification:
2011_06_18-AM-11_37_51
Home
Index