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]))


Definitions occuring in Statement :  combine-list: combine-list(x,y.f[x; y];L) cons: [a b] list: List comm: Comm(T;op) assoc: Assoc(T;op) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a combine-list: combine-list(x,y.f[x; y];L) all: x:A. B[x] top: Top so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] prop: comm: Comm(T;op) infix_ap: 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

\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