Nuprl Lemma : select-rev-append

∀[T:Type]. ∀[L,bs:T List]. ∀[i:ℕ||L|| + ||bs||].
(rev(L) + bs[i] = if i <z ||L|| then L[||L|| - 1 - i] else bs[i - ||L||] fi ∈ T)

Proof

Definitions occuring in Statement : select: L[n], length: ||as||, rev-append: rev(as) + bs, list: T List, int_seg: {i..j^-}, ifthenelse: if b then t else f fi , lt_int: i <z j, uall: ∀[x:A]. B[x], subtract: n - m, add: n + m, natural_number: $n, universe: Type, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, so_lambda: λ₂x.t[x], int_seg: {i..j^-}, uimplies: b supposing a, sq_stable: SqStable(P), implies: P ⇒ Q, lelt: i ≤ j < k, and: P ∧ Q, squash: ↓T, top: Top, all: ∀x:A. B[x], bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, ifthenelse: if b then t else f fi , uiff: uiff(P;Q), exists: ∃x:A. B[x], subtype_rel: A ⊆r B, nat: ℕ, so_apply: x[s], prop: ℙ, bfalse: ff, or: P ∨ Q, sq_type: SQType(T), guard: {T}, bnot: ¬_bb, assert: ↑b, false: False, not: ¬A, select: L[n], nil: [], so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], subtract: n - m, cand: A c∧ B, gt: i > j, le: A ≤ B, decidable: Dec(P), iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, less_than': less_than'(a;b), true: True, less_than: a < b, nat_plus: ℕ⁺
Lemmas referenced : list_induction, uall_wf, list_wf, int_seg_wf, length_wf, equal_wf, select_wf, rev-append_wf, sq_stable__le, length-rev-append, lt_int_wf, bool_wf, eqtt_to_assert, assert_of_lt_int, subtract_wf, non_neg_length, length_wf_nat, nat_wf, set_subtype_base, le_wf, int_subtype_base, eqff_to_assert, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, less_than_wf, length_of_nil_lemma, rev_app_nil_lemma, stuck-spread, base_wf, less_than_transitivity1, less_than_irreflexivity, squash_wf, minus-zero, add-zero, not-gt-2, decidable__lt, false_wf, not-lt-2, less-iff-le, condition-implies-le, minus-add, minus-one-mul, add-swap, minus-one-mul-top, add-commutes, add-associates, zero-add, add_functionality_wrt_le, le-add-cancel, length_of_cons_lemma, rev_app_cons_lemma, true_wf, cons_wf, lelt_wf, iff_weakening_equal, select_cons_tl, le_reflexive, one-mul, add-mul-special, two-mul, mul-distributes-right, zero-mul, not-le-2, omega-shadow, mul-distributes, mul-associates, minus-minus, mul-swap, mul-commutes, le-add-cancel-alt, add-is-int-iff, int_seg_properties, nat_properties, decidable__le, select_cons_hd
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, isect_memberFormation, introduction, cut, thin, extract_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, sqequalRule, lambdaEquality, cumulativity, hypothesis, natural_numberEquality, addEquality, because_Cache, setElimination, rename, independent_isectElimination, independent_functionElimination, productElimination, imageMemberEquality, baseClosed, imageElimination, isect_memberEquality, voidElimination, voidEquality, lambdaFormation, unionElimination, equalityElimination, dependent_pairFormation, sqequalIntensionalEquality, applyEquality, intEquality, equalityTransitivity, equalitySymmetry, dependent_functionElimination, promote_hyp, instantiate, productEquality, independent_pairFormation, minusEquality, axiomEquality, dependent_set_memberEquality, universeEquality, multiplyEquality, baseApply, closedConclusion

Latex:
\mforall{}[T:Type]. \mforall{}[L,bs:T List]. \mforall{}[i:\mBbbN{}||L|| + ||bs||]. (rev(L) + bs[i] = if i <z ||L|| then L[||L|| - 1 - i] else bs[i - ||L||] fi ) Date html generated: 2017_04_14-AM-08_38_42 Last ObjectModification: 2017_02_27-PM-03_31_19 Theory : list_0 Home Index