Nuprl Lemma : add-remove-nth

∀[T:Type]. ∀[L:T List]. ∀[n:ℕ||L||]. (let x,L' = remove-nth(n;L) in add-nth(n;x;L') ~ L)

Proof

Definitions occuring in Statement : add-nth: add-nth(n;x;L), remove-nth: remove-nth(n;L), length: ||as||, list: T List, int_seg: {i..j^-}, uall: ∀[x:A]. B[x], spread: spread def, natural_number: $n, universe: Type, sqequal: s ~ t
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, all: ∀x:A. B[x], nat: ℕ, implies: P ⇒ Q, false: False, ge: i ≥ j , uimplies: b supposing a, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], top: Top, and: P ∧ Q, prop: ℙ, or: P ∨ Q, cons: [a / b], le: A ≤ B, less_than': less_than'(a;b), colength: colength(L), nil: [], it: ⋅, so_lambda: λ₂x.t[x], so_apply: x[s], sq_type: SQType(T), guard: {T}, less_than: a < b, squash: ↓T, so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], decidable: Dec(P), subtype_rel: A ⊆r B, lelt: i ≤ j < k, int_seg: {i..j^-}, remove-nth: remove-nth(n;L), add-nth: add-nth(n;x;L), firstn: firstn(n;as), nth_tl: nth_tl(n;as), so_lambda: so_lambda(x,y,z.t[x; y; z]), so_apply: x[s1;s2;s3], bool: 𝔹, unit: Unit, btrue: tt, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , append: as @ bs, bfalse: ff, bnot: ¬_bb, assert: ↑b, rev_implies: P ⇐ Q, iff: P ⇐⇒ Q, select: L[n], subtract: n - m, le_int: i ≤z j, lt_int: i <z j
Lemmas referenced : nat_properties, full-omega-unsat, intformand_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, ge_wf, less_than_wf, int_seg_wf, length_wf, list-cases, product_subtype_list, colength-cons-not-zero, colength_wf_list, le_wf, subtract-1-ge-0, subtype_base_sq, nat_wf, set_subtype_base, int_subtype_base, spread_cons_lemma, decidable__equal_int, subtract_wf, intformnot_wf, intformeq_wf, itermSubtract_wf, itermAdd_wf, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_subtract_lemma, int_term_value_add_lemma, decidable__le, list_wf, nil_wf, int_seg_properties, length_of_nil_lemma, length_of_cons_lemma, list_ind_cons_lemma, reduce_tl_cons_lemma, lt_int_wf, eqtt_to_assert, assert_of_lt_int, le_int_wf, assert_of_le_int, non_neg_length, eqff_to_assert, bool_cases_sqequal, bool_wf, bool_subtype_base, assert-bnot, iff_weakening_uiff, assert_wf, list_ind_nil_lemma, general_arith_equation1, lelt_wf, false_wf, add-is-int-iff, decidable__lt, select-cons-tl
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :isect_memberFormation_alt, introduction, cut, thin, Error :lambdaFormation_alt, extract_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, hypothesis, setElimination, rename, intWeakElimination, natural_numberEquality, independent_isectElimination, approximateComputation, independent_functionElimination, Error :dependent_pairFormation_alt, Error :lambdaEquality_alt, int_eqEquality, dependent_functionElimination, Error :isect_memberEquality_alt, voidElimination, sqequalRule, independent_pairFormation, Error :universeIsType, axiomSqEquality, Error :functionIsTypeImplies, Error :inhabitedIsType, unionElimination, promote_hyp, hypothesis_subsumption, productElimination, Error :equalityIsType1, because_Cache, Error :dependent_set_memberEquality_alt, instantiate, cumulativity, intEquality, equalityTransitivity, equalitySymmetry, imageElimination, applyLambdaEquality, Error :equalityIsType4, addEquality, applyEquality, universeEquality, voidEquality, isect_memberEquality, lambdaEquality, dependent_pairFormation, isect_memberFormation, equalityElimination, baseClosed, closedConclusion, baseApply, pointwiseFunctionality, dependent_set_memberEquality

Latex:
\mforall{}[T:Type]. \mforall{}[L:T List]. \mforall{}[n:\mBbbN{}||L||]. (let x,L' = remove-nth(n;L) in add-nth(n;x;L') \msim{} L) Date html generated: 2019_06_20-PM-01_33_04 Last ObjectModification: 2018_10_03-PM-11_01_00 Theory : list_1 Home Index