Nuprl Lemma : l_all_eager_product-map
∀T:Type
∀A,B:Type. ∀Pa:A ⟶ ℙ. ∀Pb:B ⟶ ℙ. ∀Pt:T ⟶ ℙ. ∀f:A ⟶ B ⟶ T.
((∀a:A. ∀b:B. (Pa[a] ⇒ Pb[b] ⇒ Pt[f a b]))
⇒ (∀as:A List. ∀bs:B List. ((∀a∈as.Pa[a]) ⇒ (∀b∈bs.Pb[b]) ⇒ (∀t∈eager-product-map(f;as;bs).Pt[t]))))
supposing value-type(T)
Proof
Definitions occuring in Statement :
l_all: (∀x∈L.P[x]),
eager-product-map: eager-product-map(f;as;bs),
list: T List,
value-type: value-type(T),
uimplies: b supposing a,
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
value-type: value-type(T),
uall: ∀[x:A]. B[x],
has-value: (a)↓,
prop: ℙ,
implies: P ⇒ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
top: Top,
subtype_rel: A ⊆r B,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
cand: A c∧ B,
guard: {T}
Lemmas referenced :
equal-wf-base,
base_wf,
list_induction,
all_wf,
list_wf,
l_all_wf,
l_member_wf,
eager-product-map_wf,
value-type_wf,
eager_product_map_nil_lemma,
l_all_nil,
l_all_wf_nil,
cons_wf,
eager-product-map-nil,
subtype_rel_list,
top_wf,
l_all_cons,
eager_product_map_cons_lemma,
equal_wf,
eager-map-append-sq,
l_all_append,
map_wf,
reverse_wf,
l_all_map,
l_all_reverse
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
introduction,
sqequalRule,
sqequalHypSubstitution,
isect_memberEquality,
isectElimination,
thin,
hypothesisEquality,
axiomSqleEquality,
hypothesis,
extract_by_obid,
because_Cache,
equalityTransitivity,
equalitySymmetry,
rename,
lambdaEquality,
cumulativity,
functionEquality,
setElimination,
applyEquality,
functionExtensionality,
setEquality,
independent_isectElimination,
independent_functionElimination,
dependent_functionElimination,
universeEquality,
voidElimination,
voidEquality,
productElimination,
independent_pairFormation,
productEquality,
addLevel,
impliesFunctionality
Latex:
\mforall{}T:Type
\mforall{}A,B:Type. \mforall{}Pa:A {}\mrightarrow{} \mBbbP{}. \mforall{}Pb:B {}\mrightarrow{} \mBbbP{}. \mforall{}Pt:T {}\mrightarrow{} \mBbbP{}. \mforall{}f:A {}\mrightarrow{} B {}\mrightarrow{} T.
((\mforall{}a:A. \mforall{}b:B. (Pa[a] {}\mRightarrow{} Pb[b] {}\mRightarrow{} Pt[f a b]))
{}\mRightarrow{} (\mforall{}as:A List. \mforall{}bs:B List.
((\mforall{}a\mmember{}as.Pa[a]) {}\mRightarrow{} (\mforall{}b\mmember{}bs.Pb[b]) {}\mRightarrow{} (\mforall{}t\mmember{}eager-product-map(f;as;bs).Pt[t]))))
supposing value-type(T)
Date html generated:
2017_04_14-AM-08_55_23
Last ObjectModification:
2017_02_27-PM-03_39_33
Theory : omega
Home
Index