Nuprl Lemma : map_is_cons
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[L:A List]. ∀[L2:B List]. ∀[b:B].
{((f hd(L)) = b ∈ B) ∧ (map(f;tl(L)) = L2 ∈ (B List))} supposing map(f;L) = [b / L2] ∈ (B List)
Proof
Definitions occuring in Statement :
hd: hd(l),
map: map(f;as),
tl: tl(l),
cons: [a / b],
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
guard: {T},
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
guard: {T},
append: as @ bs,
all: ∀x:A. B[x],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
top: Top,
so_apply: x[s1;s2;s3],
and: P ∧ Q,
cand: A c∧ B,
tl: tl(l),
nth_tl: nth_tl(n;as),
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
bnot: ¬bb,
lt_int: i <z j,
btrue: tt,
bfalse: ff,
subtract: n - m,
prop: ℙ,
firstn: firstn(n;as),
or: P ∨ Q,
cons: [a / b],
pi2: snd(t),
subtype_rel: A ⊆r B,
not: ¬A,
implies: P ⇒ Q,
false: False,
squash: ↓T,
ge: i ≥ j
Lemmas referenced :
length_cons_ge_one,
length_wf,
ge_wf,
squash_wf,
hd_wf,
btrue_neq_bfalse,
bfalse_wf,
null_cons_lemma,
top_wf,
subtype_rel_list,
null_wf3,
and_wf,
btrue_wf,
null_nil_lemma,
reduce_hd_cons_lemma,
map_cons_lemma,
product_subtype_list,
map_nil_lemma,
nth_tl_nil,
list-cases,
map_wf,
list_wf,
equal_wf,
length_of_nil_lemma,
length_of_cons_lemma,
list_ind_nil_lemma,
list_ind_cons_lemma,
nil_wf,
cons_wf,
map_is_append
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
because_Cache,
hypothesis,
independent_isectElimination,
sqequalRule,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
productElimination,
independent_pairFormation,
independent_pairEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
functionEquality,
universeEquality,
unionElimination,
promote_hyp,
hypothesis_subsumption,
natural_numberEquality,
dependent_set_memberEquality,
applyEquality,
lambdaEquality,
setElimination,
rename,
setEquality,
independent_functionElimination,
imageElimination,
imageMemberEquality,
baseClosed
Latex:
\mforall{}[A,B:Type]. \mforall{}[f:A {}\mrightarrow{} B]. \mforall{}[L:A List]. \mforall{}[L2:B List]. \mforall{}[b:B].
\{((f hd(L)) = b) \mwedge{} (map(f;tl(L)) = L2)\} supposing map(f;L) = [b / L2]
Date html generated:
2016_05_15-PM-04_19_41
Last ObjectModification:
2016_01_16-AM-11_09_33
Theory : general
Home
Index