### Nuprl Lemma : combine-list-flip

`∀[A:Type]. ∀[f:A ⟶ A ⟶ A].`
`  (∀[as:A List]. ∀[a1,a2:A].`
`     (combine-list(x,y.f[x;y];[a1; [a2 / as]]) = combine-list(x,y.f[x;y];[a2; [a1 / as]]) ∈ A)) supposing `
`     (Comm(A;λx,y. f[x;y]) and `
`     Assoc(A;λx,y. f[x;y]))`

Proof

Definitions occuring in Statement :  combine-list: `combine-list(x,y.f[x; y];L)` cons: `[a / b]` list: `T List` comm: `Comm(T;op)` assoc: `Assoc(T;op)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` lambda: `λx.A[x]` 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` combine-list: `combine-list(x,y.f[x; y];L)` all: `∀x:A. B[x]` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` prop: `ℙ` comm: `Comm(T;op)` infix_ap: `x f y` true: `True` squash: `↓T`
Lemmas referenced :  list_wf true_wf squash_wf list_accum_wf assoc_wf comm_wf list_accum_cons_lemma reduce_tl_cons_lemma reduce_hd_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis because_Cache isectElimination hypothesisEquality axiomEquality lambdaEquality applyEquality equalityTransitivity equalitySymmetry natural_numberEquality imageElimination functionEquality universeEquality imageMemberEquality baseClosed

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
(\mforall{}[as:A  List].  \mforall{}[a1,a2:A].
(combine-list(x,y.f[x;y];[a1;  [a2  /  as]])
=  combine-list(x,y.f[x;y];[a2;  [a1  /  as]])))  supposing
(Comm(A;\mlambda{}x,y.  f[x;y])  and
Assoc(A;\mlambda{}x,y.  f[x;y]))

Date html generated: 2016_05_14-PM-01_40_59
Last ObjectModification: 2016_01_15-AM-08_23_58

Theory : list_1

Home Index