### Nuprl Lemma : seq-add_wf

`∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[x:T].  (s.x@n ∈ ℕn + 1 ⟶ T)`

Proof

Definitions occuring in Statement :  seq-add: `s.x@n` 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-add: `s.x@n` int_seg: `{i..j-}` nat: `ℕ` false: `False` implies: `P `` Q` not: `¬A` lelt: `i ≤ j < k` and: `P ∧ Q` le: `A ≤ B` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` prop: `ℙ` uiff: `uiff(P;Q)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` top: `Top` less_than': `less_than'(a;b)` true: `True` subtract: `n - m` less_than: `a < b`
Lemmas referenced :  decidable__lt false_wf not-lt-2 not-equal-2 add_functionality_wrt_le add-swap add-commutes le-add-cancel less-iff-le condition-implies-le add-associates nat_wf minus-add minus-one-mul minus-one-mul-top zero-add le-add-cancel2 and_wf le_wf less_than_wf int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality int_eqEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality hypothesis applyEquality dependent_set_memberEquality productElimination independent_pairFormation lemma_by_obid dependent_functionElimination unionElimination lambdaFormation voidElimination independent_functionElimination independent_isectElimination isectElimination addEquality natural_numberEquality isect_memberEquality voidEquality intEquality because_Cache minusEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  T].  \mforall{}[x:T].    (s.x@n  \mmember{}  \mBbbN{}n  +  1  {}\mrightarrow{}  T)

Date html generated: 2016_05_13-PM-03_48_28
Last ObjectModification: 2015_12_26-AM-10_18_16

Theory : bar-induction

Home Index