### Nuprl Lemma : seq-append1

[n:ℕ]. ∀[s,t:Top].  (seq-append(n;1;s;λi.t) seq-normalize(n 1;λm.if m=n  then t  else (s m)))

Proof

Definitions occuring in Statement :  seq-normalize: seq-normalize(n;s) seq-append: seq-append(n;m;s1;s2) nat: uall: [x:A]. B[x] top: Top int_eq: if a=b  then c  else d apply: a lambda: λx.A[x] add: m natural_number: \$n sqequal: t
Definitions unfolded in proof :  seq-normalize: seq-normalize(n;s) seq-append: seq-append(n;m;s1;s2) uall: [x:A]. B[x] member: t ∈ T implies:  Q all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a less_than: a < b less_than': less_than'(a;b) top: Top true: True squash: T not: ¬A false: False prop: guard: {T} bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb ifthenelse: if then else fi  assert: b iff: ⇐⇒ Q rev_implies:  Q subtract: m subtype_rel: A ⊆B le: A ≤ B has-value: (a)↓
Lemmas referenced :  lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf eq_int_wf assert_of_eq_int less_than_transitivity1 le_weakening less_than_irreflexivity eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base iff_transitivity assert_wf bnot_wf not_wf iff_weakening_uiff assert_of_bnot not-lt-2 condition-implies-le minus-add base_wf minus-one-mul add-swap minus-one-mul-top add-commutes less-iff-le add_functionality_wrt_le add-associates le-add-cancel not-equal-2 zero-add le-add-cancel2 equal-wf-base nat_wf has-value_wf_base is-exception_wf value-type-has-value int-value-type
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut thin lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination hypothesis unionElimination equalityElimination because_Cache productElimination independent_isectElimination equalityTransitivity equalitySymmetry lessCases hypothesisEquality sqequalAxiom isect_memberEquality independent_pairFormation voidElimination voidEquality natural_numberEquality imageMemberEquality baseClosed imageElimination independent_functionElimination addEquality int_eqReduceTrueSq dependent_functionElimination dependent_pairFormation promote_hyp instantiate cumulativity intEquality impliesFunctionality int_eqReduceFalseSq applyEquality lambdaEquality minusEquality sqequalSqle exceptionSqequal axiomSqleEquality divergentSqle sqleReflexivity baseApply closedConclusion exceptionLess callbyvalueLess lessExceptionCases callbyvalueAdd addExceptionCases

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[s,t:Top].    (seq-append(n;1;s;\mlambda{}i.t)  \msim{}  seq-normalize(n  +  1;\mlambda{}m.if  m=n    then  t    else  (s  m)))

Date html generated: 2017_04_14-AM-07_26_55
Last ObjectModification: 2017_02_27-PM-02_56_17

Theory : bar-induction

Home Index