Nuprl Lemma : seq-max-lower_wf

[k,n:ℕ]. ∀[f:ℕ+ ⟶ ℤ].  (seq-max-lower(k;n;f) ∈ ℕ+)


Proof




Definitions occuring in Statement :  seq-max-lower: seq-max-lower(k;n;f) nat_plus: + nat: uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T seq-max-lower: seq-max-lower(k;n;f) nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True and: P ∧ Q prop: int_seg: {i..j-} nat: le: A ≤ B all: x:A. B[x] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q implies:  Q false: False uiff: uiff(P;Q) uimplies: supposing a lelt: i ≤ j < k subtract: m subtype_rel: A ⊆B top: Top bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff
Lemmas referenced :  primrec_wf nat_plus_wf less_than_wf le_int_wf subtract_wf decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel bool_wf eqtt_to_assert assert_of_le_int equal_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation imageMemberEquality baseClosed lambdaEquality multiplyEquality addEquality setElimination rename because_Cache applyEquality functionExtensionality productElimination dependent_functionElimination unionElimination lambdaFormation voidElimination independent_functionElimination independent_isectElimination isect_memberEquality voidEquality intEquality minusEquality equalityElimination equalityTransitivity equalitySymmetry axiomEquality functionEquality

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].    (seq-max-lower(k;n;f)  \mmember{}  \mBbbN{}\msupplus{})



Date html generated: 2017_10_03-AM-08_43_58
Last ObjectModification: 2017_09_12-PM-00_25_50

Theory : reals


Home Index