### Nuprl Lemma : strictly-increasing-seq-add2-implies

`∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀x,y:ℕ.`
`  (strictly-increasing-seq(n + 2;s.x@n.y@n + 1)`
`  `` {x < y ∧ strictly-increasing-seq(n + 1;s.x@n) ∧ strictly-increasing-seq(n + 1;s.y@n)})`

Proof

Definitions occuring in Statement :  strictly-increasing-seq: `strictly-increasing-seq(n;s)` seq-add: `s.x@n` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` guard: `{T}` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` uimplies: `b supposing a` sq_stable: `SqStable(P)` squash: `↓T` subtract: `n - m` subtype_rel: `A ⊆r B` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` so_lambda: `λ2x.t[x]` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` strictly-increasing-seq: `strictly-increasing-seq(n;s)` seq-add: `s.x@n` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` bfalse: `ff` exists: `∃x:A. B[x]` sq_type: `SQType(T)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` less_than: `a < b` rev_uimplies: `rev_uimplies(P;Q)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality addEquality setElimination rename because_Cache hypothesis natural_numberEquality dependent_functionElimination hypothesisEquality unionElimination voidElimination productElimination independent_functionElimination independent_isectElimination sqequalRule imageMemberEquality baseClosed imageElimination applyEquality lambdaEquality isect_memberEquality voidEquality intEquality minusEquality functionExtensionality setEquality functionEquality multiplyEquality int_eqReduceTrueSq equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp instantiate cumulativity impliesFunctionality int_eqReduceFalseSq inlFormation inrFormation addLevel orFunctionality

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x,y:\mBbbN{}.
(strictly-increasing-seq(n  +  2;s.x@n.y@n  +  1)
{}\mRightarrow{}  \{x  <  y  \mwedge{}  strictly-increasing-seq(n  +  1;s.x@n)  \mwedge{}  strictly-increasing-seq(n  +  1;s.y@n)\})

Date html generated: 2017_04_14-AM-07_26_27
Last ObjectModification: 2017_02_27-PM-02_56_12

Theory : bar-induction

Home Index