{ 
[B:Type]. [n:
]. [A:n 
Type]. [bags:k:n bag(A k)]. [loc:Id].
[f:Id funtype(n;A;bag(B))].
(concat-lifting-loc(n;bags;loc;f) 
bag(B)) }
{ Proof }
Definitions occuring in Statement :
concat-lifting-loc: concat-lifting-loc(n;bags;loc;f),
Id: Id,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
member: t T,
apply: f a,
function: x:A B[x],
natural_number: $n,
universe: Type,
bag: bag(T),
funtype: funtype(n;A;T)
Definitions :
uall: [x:A]. B[x],
member: t T,
isect: 
x:A. B[x],
Id: Id,
function: x:A B[x],
int_seg: {i..j},
apply: f a,
bag: bag(T),
universe: Type,
nat: ,
equal: s = t,
funtype: funtype(n;A;T),
concat-lifting-loc: concat-lifting-loc(n;bags;loc;f),
axiom: Ax,
all: x:A. B[x],
natural_number: $n,
int: 
,
subtype: S 
T,
grp_car: |g|,
real: 
,
set: {x:A| B[x]} ,
concat-lifting: concat-lifting(n;f;bags)
Lemmas :
concat-lifting_wf,
nat_wf,
int_seg_wf,
bag_wf,
Id_wf,
funtype_wf
\mforall{}[B:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[bags:k:\mBbbN{}n {}\mrightarrow{} bag(A k)]. \mforall{}[loc:Id].
\mforall{}[f:Id {}\mrightarrow{} funtype(n;A;bag(B))].
(concat-lifting-loc(n;bags;loc;f) \mmember{} bag(B))
Date html generated:
2011_08_17-PM-06_12_00
Last ObjectModification:
2011_06_01-PM-07_34_20
Home
Index