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: f a,  lambda: λx.A[x],  add: n + m,  natural_number: $n,  sqequal: s ~ 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: P ⇒ Q,  all: ∀x:A. B[x],  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  and: P ∧ Q,  uimplies: b 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 b then t else f fi ,  assert: ↑b,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  subtract: n - m,  subtype_rel: A ⊆r 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