`∀[L1,L2:ℝ List].  radd-list(L1) = radd-list(L2) supposing (||L1|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||L1||. (L1[i] = L2[i]))`

Proof

Definitions occuring in Statement :  req: `x = y` radd-list: `radd-list(L)` real: `ℝ` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  subtract: `n - m` cons: `[a / b]` less_than: `a < b` less_than': `less_than'(a;b)` le: `A ≤ B` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` select: `L[n]` nil: `[]` list_ind: list_ind map: `map(f;as)` lelt: `i ≤ j < k` int_seg: `{i..j-}` true: `True` real: `ℝ` squash: `↓T` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` decidable: `Dec(P)` nat_plus: `ℕ+` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` nequal: `a ≠ b ∈ T ` ge: `i ≥ j ` 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 b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` implies: `P `` 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)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Rules used in proof :  functionExtensionality hyp_replacement applyLambdaEquality closedConclusion baseApply pointwiseFunctionality addEquality productEquality universeEquality baseClosed imageMemberEquality imageElimination functionEquality setEquality rename setElimination applyEquality dependent_set_memberEquality independent_pairFormation voidEquality isect_memberEquality int_eqEquality approximateComputation voidElimination independent_functionElimination cumulativity instantiate dependent_functionElimination promote_hyp dependent_pairFormation equalitySymmetry equalityTransitivity equalityElimination unionElimination lambdaFormation natural_numberEquality lambdaEquality intEquality because_Cache callbyvalueReduce hypothesisEquality independent_isectElimination hypothesis isectElimination extract_by_obid sqequalRule thin productElimination sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[L1,L2:\mBbbR{}  List].
radd-list(L1)  =  radd-list(L2)  supposing  (||L1||  =  ||L2||)  \mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  (L1[i]  =  L2[i]))

Date html generated: 2018_05_22-PM-01_20_45
Last ObjectModification: 2018_05_21-AM-00_04_41

Theory : reals

Home Index