Nuprl Lemma : concat-lifting-gen_wf

[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;bag(B))].  (concat-lifting-gen(n;f) ∈ (k:ℕn ⟶ bag(A k)) ⟶ bag(B))


Proof




Definitions occuring in Statement :  concat-lifting-gen: concat-lifting-gen(n;f) bag: bag(T) funtype: funtype(n;A;T) int_seg: {i..j-} nat: uall: [x:A]. B[x] member: t ∈ T apply: a function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T concat-lifting-gen: concat-lifting-gen(n;f) nat:
Lemmas referenced :  concat-lifting_wf int_seg_wf bag_wf funtype_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis functionEquality natural_numberEquality setElimination rename applyEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache cumulativity universeEquality

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[f:funtype(n;A;bag(B))].
    (concat-lifting-gen(n;f)  \mmember{}  (k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k))  {}\mrightarrow{}  bag(B))



Date html generated: 2016_05_15-PM-03_07_01
Last ObjectModification: 2015_12_27-AM-09_27_02

Theory : bags


Home Index