{ 
[x:ClassDerivation]
cdvreccomb-fun(x) 
cdvreccomb-argtype(x)
bag(cdvreccomb-typ(x))
bag(cdvreccomb-typ(x))
supposing 
cdvreccomb?(x) }
{ Proof }
Definitions occuring in Statement :
cdvreccomb-fun: cdvreccomb-fun(x),
cdvreccomb-argtype: cdvreccomb-argtype(x),
cdvreccomb-typ: cdvreccomb-typ(x),
cdvreccomb?: cdvreccomb?(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],
cdvreccomb?: cdvreccomb?(x),
uall: [x:A]. B[x],
cdvreccomb-argtype: cdvreccomb-argtype(x),
function: x:A B[x],
bag: bag(T),
cdvreccomb-typ: cdvreccomb-typ(x),
cdvreccomb-fun: cdvreccomb-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,
cdvreccomb?_wf,
classderiv_wf,
false_wf,
true_wf
\mforall{}[x:ClassDerivation]
cdvreccomb-fun(x) \mmember{} cdvreccomb-argtype(x) {}\mrightarrow{} bag(cdvreccomb-typ(x)) {}\mrightarrow{} bag(cdvreccomb-typ(x))
supposing \muparrow{}cdvreccomb?(x)
Date html generated:
2011_08_17-PM-04_26_31
Last ObjectModification:
2011_06_18-AM-11_38_51
Home
Index