### Nuprl Lemma : assert-equal-upto-finite-nat-seq

[n:ℕ]. ∀[f,g:ℕn ⟶ ℕ].  (↑equal-upto-finite-nat-seq(n;f;g) ⇐⇒ g ∈ (ℕn ⟶ ℕ))

Proof

Definitions occuring in Statement :  equal-upto-finite-nat-seq: equal-upto-finite-nat-seq(n;f;g) int_seg: {i..j-} nat: assert: b uall: [x:A]. B[x] iff: ⇐⇒ Q function: x:A ⟶ B[x] natural_number: \$n equal: t ∈ T
Definitions unfolded in proof :  equal-upto-finite-nat-seq: equal-upto-finite-nat-seq(n;f;g) uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] all: x:A. B[x] top: Top and: P ∧ Q prop: iff: ⇐⇒ Q rev_implies:  Q assert: b ifthenelse: if then else fi  btrue: tt int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q sq_type: SQType(T) guard: {T} uiff: uiff(P;Q) subtype_rel: A ⊆B bfalse: ff band: p ∧b q true: True so_lambda: λ2x.t[x] so_apply: x[s] le: A ≤ B less_than': less_than'(a;b) subtract: m cand: c∧ B squash: T
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than assert_witness primrec0_lemma int_seg_wf int_seg_properties primrec_wf bool_wf decidable__le intformnot_wf int_formula_prop_not_lemma istype-le btrue_wf bool_cases subtype_base_sq bool_subtype_base eqtt_to_assert band_wf eq_int_wf bfalse_wf subtract-1-ge-0 istype-nat equal-upto-finite-nat-seq_wf true_wf primrec-unroll-1 assert_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma decidable__lt equal-wf-base set_subtype_base le_wf int_subtype_base istype-assert iff_transitivity iff_weakening_uiff assert_of_band assert_of_eq_int subtype_rel_function nat_wf int_seg_subtype istype-false not-le-2 condition-implies-le add-associates minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-commutes le-add-cancel2 subtype_rel_self equal_functionality_wrt_subtype_rel2 equal_wf iff_weakening_equal decidable__equal_int intformeq_wf int_formula_prop_eq_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination Error :lambdaFormation_alt,  natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality dependent_functionElimination Error :isect_memberEquality_alt,  voidElimination sqequalRule independent_pairFormation Error :universeIsType,  productElimination independent_pairEquality axiomEquality Error :functionIsTypeImplies,  Error :inhabitedIsType,  Error :functionIsType,  Error :dependent_set_memberEquality_alt,  unionElimination instantiate equalityTransitivity equalitySymmetry applyEquality because_Cache cumulativity Error :isect_memberFormation_alt,  Error :isectIsTypeImplies,  Error :equalityIstype,  Error :functionExtensionality_alt,  Error :productIsType,  productEquality intEquality sqequalBase promote_hyp addEquality minusEquality multiplyEquality functionEquality imageElimination imageMemberEquality baseClosed applyLambdaEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}].    (\muparrow{}equal-upto-finite-nat-seq(n;f;g)  \mLeftarrow{}{}\mRightarrow{}  f  =  g)

Date html generated: 2019_06_20-PM-03_03_18
Last ObjectModification: 2019_01_02-PM-00_36_10

Theory : continuity

Home Index