### Nuprl Lemma : list_accum_functionality

`∀[T,A:Type]. ∀[f,g:T ⟶ A ⟶ T]. ∀[L:A List]. ∀[y,z:T].`
`  (accumulate (with value x and list item a):`
`    f[x;a]`
`   over list:`
`     L`
`   with starting value:`
`    y)`
`     = accumulate (with value x and list item a):`
`        g[x;a]`
`       over list:`
`         L`
`       with starting value:`
`        z)`
`     ∈ T) supposing `
`     ((y = z ∈ T) and `
`     (∀L':A List. ∀a:A.`
`        (L' @ [a] ≤ L`
`        `` (f[accumulate (with value x and list item a):`
`               f[x;a]`
`              over list:`
`                L'`
`              with starting value:`
`               y);a]`
`           = g[accumulate (with value x and list item a):`
`                f[x;a]`
`               over list:`
`                 L'`
`               with starting value:`
`                y);a]`
`           ∈ T))))`

Proof

Definitions occuring in Statement :  iseg: `l1 ≤ l2` append: `as @ bs` list_accum: list_accum cons: `[a / b]` nil: `[]` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` 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` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` so_apply: `x[s]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` so_lambda: `λ2x y.t[x; y]` guard: `{T}` top: `Top` subtype_rel: `A ⊆r B` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  last_induction all_wf equal_wf list_accum_wf list_wf iseg_wf append_wf cons_wf nil_wf list_accum_nil_lemma subtype_rel_list top_wf list_accum_cons_lemma list_accum_append squash_wf true_wf iseg_weakening iff_weakening_equal iseg_append
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity because_Cache functionEquality hypothesis applyEquality functionExtensionality independent_functionElimination dependent_functionElimination isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry voidElimination voidEquality lambdaFormation independent_isectElimination imageElimination natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T,A:Type].  \mforall{}[f,g:T  {}\mrightarrow{}  A  {}\mrightarrow{}  T].  \mforall{}[L:A  List].  \mforall{}[y,z:T].
(accumulate  (with  value  x  and  list  item  a):
f[x;a]
over  list:
L
with  starting  value:
y)
=  accumulate  (with  value  x  and  list  item  a):
g[x;a]
over  list:
L
with  starting  value:
z))  supposing
((y  =  z)  and
(\mforall{}L':A  List.  \mforall{}a:A.
(L'  @  [a]  \mleq{}  L
{}\mRightarrow{}  (f[accumulate  (with  value  x  and  list  item  a):
f[x;a]
over  list:
L'
with  starting  value:
y);a]
=  g[accumulate  (with  value  x  and  list  item  a):
f[x;a]
over  list:
L'
with  starting  value:
y);a]))))

Date html generated: 2017_04_17-AM-07_37_35
Last ObjectModification: 2017_02_27-PM-04_11_59

Theory : list_1

Home Index