Nuprl Lemma : concat-lifting-loc-gen

{

[B:Type].

[n:

].

[A:

n

Type].

[f:Id

funtype(n;A;bag(B))].
(concat-lifting-loc-gen(n;f)

Id

k:

n

bag(A k)

bag(B)) }

{ Proof }

Definitions occuring in Statement : concat-lifting-loc-gen: concat-lifting-loc-gen(n;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 : axiom: Ax, concat-lifting-loc-gen: concat-lifting-loc-gen(n;f), bag: bag(T), apply: f a, natural_number: $n, int_seg: {i..j

}, function: x:A

B[x], Id: Id, equal: s = t, member: t

T, isect:

x:A. B[x], funtype: funtype(n;A;T), uall:

[x:A]. B[x], universe: Type, nat:

, all:

x:A. B[x], int:

, subtype: S

T, grp_car: |g|, real:

, set: {x:A| B[x]} , lambda:

x.A[x], concat-lifting-loc: concat-lifting-loc(n;bags;loc;f)
Lemmas : bag_wf, int_seg_wf, concat-lifting-loc_wf, Id_wf, nat_wf, funtype_wf

\mforall{}[B:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[f:Id {}\mrightarrow{} funtype(n;A;bag(B))]. (concat-lifting-loc-gen(n;f) \mmember{} Id {}\mrightarrow{} k:\mBbbN{}n {}\mrightarrow{} bag(A k) {}\mrightarrow{} bag(B)) Date html generated: 2011_08_17-PM-06_12_29 Last ObjectModification: 2011_06_02-PM-06_11_53 Home Index