Nuprl Lemma : int-dot-reduce-dim
∀[as,bs:ℤ List]. ∀[i:ℕ].
∀[cs:ℤ List]. (as ⋅ bs ~ as[i] * cs + as\i ⋅ bs\i) supposing ((bs[i] = cs ⋅ bs\i ∈ ℤ) and (||cs|| = (||as|| - 1) ∈ ℤ))\000C
supposing i < ||as|| ∧ i < ||bs||
Proof
Definitions occuring in Statement :
int-vec-add: as + bs,
int-vec-mul: a * as,
list-delete: as\i,
integer-dot-product: as ⋅ bs,
select: L[n],
length: ||as||,
list: T List,
nat: ℕ,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
subtract: n - m,
natural_number: $n,
int: ℤ,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
sq_type: SQType(T),
all: ∀x:A. B[x],
implies: P ⇒ Q,
guard: {T},
prop: ℙ,
nat: ℕ,
sq_stable: SqStable(P),
squash: ↓T,
subtype_rel: A ⊆r B,
top: Top,
true: True,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
int-dot-select,
subtype_base_sq,
int_subtype_base,
equal_wf,
select_wf,
sq_stable__le,
integer-dot-product_wf,
list-delete_wf,
equal-wf-base,
list_subtype_base,
list_wf,
less_than_wf,
length_wf,
nat_wf,
int-vec-mul_wf,
squash_wf,
true_wf,
length-int-vec-mul,
length-list-delete,
iff_weakening_equal,
int-dot-mul-left,
int-dot-add-left
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
independent_isectElimination,
productElimination,
instantiate,
cumulativity,
intEquality,
sqequalRule,
because_Cache,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
sqequalAxiom,
setElimination,
rename,
natural_numberEquality,
imageMemberEquality,
baseClosed,
imageElimination,
isect_memberEquality,
baseApply,
closedConclusion,
applyEquality,
productEquality,
lambdaEquality,
voidElimination,
voidEquality,
universeEquality,
addEquality
Latex:
\mforall{}[as,bs:\mBbbZ{} List]. \mforall{}[i:\mBbbN{}].
\mforall{}[cs:\mBbbZ{} List]
(as \mcdot{} bs \msim{} as[i] * cs + as\mbackslash{}i \mcdot{} bs\mbackslash{}i) supposing ((bs[i] = cs \mcdot{} bs\mbackslash{}i) and (||cs|| = (||as|| - 1)))\000C
supposing i < ||as|| \mwedge{} i < ||bs||
Date html generated:
2017_04_14-AM-08_55_59
Last ObjectModification:
2017_02_27-PM-03_39_44
Theory : omega
Home
Index