Nuprl Lemma : temp-lifting-gen-list-rev_wf
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));B)].
(lifting-gen-list-rev(n;bags) m g ∈ bag(B))
Proof
Definitions occuring in Statement :
lifting-gen-list-rev: lifting-gen-list-rev(n;bags),
bag: bag(T),
funtype: funtype(n;A;T),
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
subtract: n - m,
add: n + m,
natural_number: $n,
universe: Type
Lemmas referenced :
lifting-gen-list-rev_wf
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}[B:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[m:\mBbbN{}n + 1]. \mforall{}[A:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[bags:k:\mBbbN{}n {}\mrightarrow{} bag(A k)].
\mforall{}[g:funtype(n - m;\mlambda{}x.(A (x + m));B)].
(lifting-gen-list-rev(n;bags) m g \mmember{} bag(B))
Date html generated:
2016_05_15-PM-02_59_38
Last ObjectModification:
2015_12_27-AM-09_29_18
Theory : bags
Home
Index