`∀[n:ℕ]. ∀[s:ℕn ⟶ ℤ].`
`  ∀x,y:ℕ.  (x < y `` strictly-increasing-seq(n + 1;s.x@n) `` strictly-increasing-seq(n + 2;s.x@n.y@n + 1))`

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` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` strictly-increasing-seq: `strictly-increasing-seq(n;s)` member: `t ∈ T` int_seg: `{i..j-}` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` rev_implies: `P `` Q` false: `False` prop: `ℙ` 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` sq_type: `SQType(T)` guard: `{T}` seq-add: `s.x@n` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` lelt: `i ≤ j < k` bfalse: `ff` exists: `∃x:A. B[x]` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` less_than: `a < b`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution cut introduction extract_by_obid dependent_functionElimination thin setElimination rename because_Cache hypothesis addEquality natural_numberEquality unionElimination isectElimination hypothesisEquality dependent_set_memberEquality independent_pairFormation voidElimination productElimination independent_functionElimination independent_isectElimination sqequalRule imageMemberEquality baseClosed imageElimination applyEquality lambdaEquality isect_memberEquality voidEquality intEquality minusEquality functionExtensionality functionEquality instantiate cumulativity equalityTransitivity equalitySymmetry int_eqReduceTrueSq equalityElimination dependent_pairFormation promote_hyp impliesFunctionality int_eqReduceFalseSq multiplyEquality hyp_replacement int_eqEquality

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

Date html generated: 2017_04_14-AM-07_26_21
Last ObjectModification: 2017_02_27-PM-02_56_34

Theory : bar-induction

Home Index