### Nuprl Lemma : seq-append_wf

`∀[T:Type]. ∀[n,m:ℕ]. ∀[s1:ℕn ⟶ T]. ∀[s2:ℕm ⟶ T].  (seq-append(n;m;s1;s2) ∈ ℕn + m ⟶ T)`

Proof

Definitions occuring in Statement :  seq-append: `seq-append(n;m;s1;s2)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` seq-append: `seq-append(n;m;s1;s2)` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` and: `P ∧ Q` less_than': `less_than'(a;b)` true: `True` squash: `↓T` top: `Top` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` lelt: `i ≤ j < k` sq_stable: `SqStable(P)` uimplies: `b supposing a` subtract: `n - m` le: `A ≤ B` all: `∀x:A. B[x]` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` nat_plus: `ℕ+` decidable: `Dec(P)` or: `P ∨ Q`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality sqequalHypSubstitution setElimination thin rename because_Cache hypothesis lessCases independent_pairFormation isectElimination baseClosed natural_numberEquality equalityTransitivity equalitySymmetry imageMemberEquality hypothesisEquality axiomSqEquality isect_memberEquality voidElimination voidEquality lambdaFormation imageElimination productElimination extract_by_obid independent_functionElimination applyEquality functionExtensionality dependent_set_memberEquality addEquality axiomEquality functionEquality universeEquality dependent_functionElimination independent_isectElimination multiplyEquality minusEquality intEquality unionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[s1:\mBbbN{}n  {}\mrightarrow{}  T].  \mforall{}[s2:\mBbbN{}m  {}\mrightarrow{}  T].    (seq-append(n;m;s1;s2)  \mmember{}  \mBbbN{}n  +  m  {}\mrightarrow{}  T)

Date html generated: 2019_06_20-AM-11_28_33
Last ObjectModification: 2018_08_20-PM-09_29_12

Theory : bar-induction

Home Index