Nuprl Lemma : radd-list_functionality_wrt_permutation

[L1,L2:ℝ List].  radd-list(L1) radd-list(L2) ∈ ℝ supposing permutation(ℝ;L1;L2)


Proof




Definitions occuring in Statement :  radd-list: radd-list(L) real: permutation: permutation(T;L1;L2) list: List uimplies: supposing a uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  true: True decidable: Dec(P) nat_plus: + squash: T top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A nequal: a ≠ b ∈  ge: i ≥  false: False assert: b bnot: ¬bb guard: {T} sq_type: SQType(T) or: P ∨ Q prop: exists: x:A. B[x] bfalse: ff ifthenelse: if then else fi  and: P ∧ Q uiff: uiff(P;Q) btrue: tt it: unit: Unit bool: 𝔹 implies:  Q all: x:A. B[x] so_apply: x[s] so_lambda: λ2x.t[x] nat: has-valueall: has-valueall(a) has-value: (a)↓ callbyvalueall: callbyvalueall radd-list: radd-list(L) uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  reg-seq-list-add_functionality_wrt_permutation less_than_wf int_formula_prop_le_lemma int_formula_prop_less_lemma intformle_wf intformless_wf decidable__lt decidable__equal_int regular-int-seq_wf nat_plus_wf true_wf squash_wf accelerate_wf permutation_wf int-to-real_wf int_formula_prop_wf int_formula_prop_not_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformnot_wf itermConstant_wf itermVar_wf intformeq_wf intformand_wf full-omega-unsat non_neg_length neg_assert_of_eq_int assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal equal_wf eqff_to_assert assert_of_eq_int eqtt_to_assert bool_wf length_wf eq_int_wf permutation-length length_wf_nat int-value-type le_wf set-value-type nat_wf value-type-has-value valueall-type-real-list evalall-reduce real-valueall-type list-valueall-type real_wf list_wf valueall-type-has-valueall
Rules used in proof :  baseClosed imageMemberEquality dependent_set_memberEquality rename setElimination functionEquality setEquality imageElimination applyEquality axiomEquality independent_pairFormation voidEquality isect_memberEquality int_eqEquality approximateComputation voidElimination independent_functionElimination cumulativity instantiate dependent_functionElimination promote_hyp dependent_pairFormation productElimination equalitySymmetry equalityTransitivity equalityElimination unionElimination lambdaFormation natural_numberEquality lambdaEquality intEquality because_Cache callbyvalueReduce hypothesisEquality independent_isectElimination hypothesis thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[L1,L2:\mBbbR{}  List].    radd-list(L1)  =  radd-list(L2)  supposing  permutation(\mBbbR{};L1;L2)



Date html generated: 2018_05_22-PM-01_20_36
Last ObjectModification: 2018_05_21-AM-00_02_22

Theory : reals


Home Index