Nuprl Lemma : l_mul_permute

[L1,L2:ℤ List].  l_mul(L1) l_mul(L2) ∈ ℤ supposing permutation(ℤ;L1;L2)


Proof




Definitions occuring in Statement :  l_mul: l_mul(L) permutation: permutation(T;L1;L2) list: List uimplies: supposing a uall: [x:A]. B[x] int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a l_mul: l_mul(L) assoc: Assoc(T;op) so_apply: x[s1;s2] infix_ap: y all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top prop: comm: Comm(T;op)
Lemmas referenced :  list_wf permutation_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_mul_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermVar_wf itermMultiply_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int reduce-permutation
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality lambdaEquality multiplyEquality hypothesisEquality natural_numberEquality independent_isectElimination sqequalRule dependent_functionElimination because_Cache hypothesis unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[L1,L2:\mBbbZ{}  List].    l\_mul(L1)  =  l\_mul(L2)  supposing  permutation(\mBbbZ{};L1;L2)



Date html generated: 2016_05_14-PM-02_54_26
Last ObjectModification: 2016_01_15-AM-07_29_05

Theory : list_1


Home Index