### Nuprl Lemma : firstn-append

`∀[L1,L2:Top List]. ∀[n:ℕ].  (firstn(n;L1 @ L2) ~ if n ≤z ||L1|| then firstn(n;L1) else L1 @ firstn(n - ||L1||;L2) fi )`

Proof

Definitions occuring in Statement :  firstn: `firstn(n;as)` length: `||as||` append: `as @ bs` list: `T List` nat: `ℕ` le_int: `i ≤z j` ifthenelse: `if b then t else f fi ` uall: `∀[x:A]. B[x]` top: `Top` subtract: `n - m` 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` and: `P ∧ Q` ge: `i ≥ j ` le: `A ≤ B` cand: `A c∧ B` less_than: `a < b` squash: `↓T` guard: `{T}` uimplies: `b supposing a` prop: `ℙ` or: `P ∨ Q` firstn: `firstn(n;as)` append: `as @ bs` so_lambda: so_lambda3 so_apply: `x[s1;s2;s3]` cons: `[a / b]` less_than': `less_than'(a;b)` not: `¬A` colength: `colength(L)` nil: `[]` it: `⋅` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` sq_stable: `SqStable(P)` decidable: `Dec(P)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` true: `True` subtype_rel: `A ⊆r B` bool: `𝔹` unit: `Unit` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` bnot: `¬bb` assert: `↑b` nat_plus: `ℕ+`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin lambdaFormation_alt extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination independent_pairFormation productElimination imageElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination universeIsType sqequalRule lambdaEquality_alt dependent_functionElimination isect_memberEquality_alt axiomSqEquality isectIsTypeImplies inhabitedIsType functionIsTypeImplies unionElimination Error :memTop,  promote_hyp hypothesis_subsumption equalityIstype dependent_set_memberEquality_alt because_Cache instantiate cumulativity intEquality equalityTransitivity equalitySymmetry imageMemberEquality baseClosed applyLambdaEquality addEquality minusEquality baseApply closedConclusion applyEquality sqequalBase equalityElimination dependent_pairFormation_alt multiplyEquality

Latex:
\mforall{}[L1,L2:Top  List].  \mforall{}[n:\mBbbN{}].
(firstn(n;L1  @  L2)  \msim{}  if  n  \mleq{}z  ||L1||  then  firstn(n;L1)  else  L1  @  firstn(n  -  ||L1||;L2)  fi  )

Date html generated: 2020_05_19-PM-09_37_57
Last ObjectModification: 2020_03_09-PM-01_32_32

Theory : list_0

Home Index