Nuprl Lemma : reduce-permutation

[A:Type]. ∀[f:A ⟶ A ⟶ A]. ∀[e:A].
  (∀[as,bs:A List].  reduce(f;e;as) reduce(f;e;bs) ∈ supposing permutation(A;as;bs)) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))


Definitions occuring in Statement :  permutation: permutation(T;L1;L2) reduce: reduce(f;k;as) 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 prop: so_apply: x[s1;s2] true: True so_lambda: λ2y.t[x; y] all: x:A. B[x] top: Top ge: i ≥  decidable: Dec(P) or: P ∨ Q le: A ≤ B and: P ∧ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A squash: T subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3]
Lemmas referenced :  reduce-as-combine-list permutation_wf list_wf comm_wf assoc_wf combine-list-permutation cons_wf length_of_cons_lemma non_neg_length decidable__lt length_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf equal_wf squash_wf true_wf iff_weakening_equal nil_wf permutation_weakening append_functionality_wrt_permutation list_ind_cons_lemma list_ind_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality independent_isectElimination hypothesis cumulativity sqequalRule isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry lambdaEquality applyEquality functionExtensionality functionEquality natural_numberEquality dependent_functionElimination voidElimination voidEquality addEquality unionElimination productElimination dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll imageElimination imageMemberEquality baseClosed universeEquality independent_functionElimination

\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[e:A].
    (\mforall{}[as,bs:A  List].    reduce(f;e;as)  =  reduce(f;e;bs)  supposing  permutation(A;as;bs))  supposing 
          (Comm(A;\mlambda{}x,y.  f[x;y])  and 
          Assoc(A;\mlambda{}x,y.  f[x;y]))

Date html generated: 2017_04_17-AM-08_23_25
Last ObjectModification: 2017_02_27-PM-04_45_15

Theory : list_1

Home Index