### Nuprl Lemma : seq-append1-assoc

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

Proof

Definitions occuring in Statement :  seq-append: seq-append(n;m;s1;s2) nat: uall: [x:A]. B[x] top: Top int_eq: if a=b then else d apply: a lambda: λx.A[x] add: m natural_number: \$n sqequal: t
Definitions unfolded in proof :  seq-append: seq-append(n;m;s1;s2) has-value: (a)↓ member: t ∈ T subtype_rel: A ⊆B nat: uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a and: P ∧ Q all: x:A. B[x] decidable: Dec(P) or: P ∨ Q less_than: a < b less_than': less_than'(a;b) top: Top true: True squash: T not: ¬A implies:  Q false: False prop: bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb ifthenelse: if then else fi  assert: b iff: ⇐⇒ Q rev_implies:  Q subtract: m le: A ≤ B ge: i ≥  nat_plus: +
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut thin sqequalSqle divergentSqle callbyvalueIntEq sqequalHypSubstitution hypothesis baseApply closedConclusion baseClosed hypothesisEquality applyEquality introduction extract_by_obid isectElimination intEquality Error :lambdaEquality_alt,  natural_numberEquality independent_isectElimination productElimination dependent_functionElimination equalityTransitivity equalitySymmetry setElimination rename unionElimination because_Cache lessCases Error :isect_memberFormation_alt,  axiomSqEquality Error :inhabitedIsType,  Error :isect_memberEquality_alt,  Error :universeIsType,  independent_pairFormation voidElimination imageMemberEquality Error :lambdaFormation_alt,  imageElimination independent_functionElimination int_eqReduceTrueSq int_eqReduceFalseSq sqleReflexivity addEquality equalityElimination Error :dependent_pairFormation_alt,  Error :equalityIsType1,  promote_hyp instantiate cumulativity Error :equalityIsType2,  minusEquality int_eqExceptionCases axiomSqleEquality exceptionSqequal callbyvalueLess lessExceptionCases multiplyEquality Error :dependent_set_memberEquality_alt

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

Date html generated: 2019_06_20-AM-11_28_46
Last ObjectModification: 2018_09_28-PM-10_41_38

Theory : bar-induction

Home Index