Nuprl Lemma : coded-code-seq1

[k:ℕ+]. ∀s:ℕk ⟶ ℕ. ∀[n:ℕk]. (coded-seq1(k 1;code-seq1(k;s);n) (s n) ∈ ℤ)


Proof




Definitions occuring in Statement :  coded-seq1: coded-seq1(k;x;n) code-seq1: code-seq1(k;s) int_seg: {i..j-} nat_plus: + nat: uall: [x:A]. B[x] all: x:A. B[x] apply: a function: x:A ⟶ B[x] subtract: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] coded-seq1: coded-seq1(k;x;n) subtract: m eq_int: (i =z j) ifthenelse: if then else fi  btrue: tt nat_plus: + implies:  Q prop: so_lambda: λ2x.t[x] nat: guard: {T} int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top subtype_rel: A ⊆B so_apply: x[s] code-seq1: code-seq1(k;s) sq_type: SQType(T) le: A ≤ B less_than': less_than'(a;b) less_than: a < b squash: T true: True bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) bfalse: ff bnot: ¬bb assert: b coded-pair: coded-pair(m) tsqrt: tsqrt(n) isqrt: isqrt(x) integer-sqrt-ext genrec-ap: genrec-ap le_int: i ≤j lt_int: i <j triangular-num: t(n) nequal: a ≠ b ∈  iff: ⇐⇒ Q rev_implies:  Q ge: i ≥  label: ...$L... t
Lemmas referenced :  int_seg_wf nat_wf nat_plus_properties all_wf uall_wf equal_wf coded-seq1_wf subtract_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf subtract-add-cancel decidable__lt lelt_wf code-seq1_wf nat_plus_wf primrec-wf-nat-plus nat_plus_subtype_nat primrec1_lemma decidable__equal_int subtype_base_sq int_subtype_base intformeq_wf int_formula_prop_eq_lemma int_seg_subtype false_wf int_seg_cases eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int add-subtract-cancel eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_int primrec-unroll lt_int_wf assert_of_lt_int itermAdd_wf int_term_value_add_lemma less_than_wf squash_wf true_wf coded-code-pair subtype_rel_function not-le-2 not-equal-2 condition-implies-le minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-associates add-commutes le-add-cancel subtype_rel_self nat_properties iff_weakening_equal integer-sqrt-ext
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesis functionEquality rename hypothesisEquality setElimination addEquality lambdaEquality because_Cache intEquality dependent_set_memberEquality productElimination dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation functionExtensionality applyEquality axiomEquality instantiate cumulativity equalityTransitivity equalitySymmetry imageMemberEquality baseClosed hypothesis_subsumption equalityElimination promote_hyp imageElimination universeEquality spreadEquality minusEquality multiplyEquality

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}.  \mforall{}[n:\mBbbN{}k].  (coded-seq1(k  -  1;code-seq1(k;s);n)  =  (s  n))



Date html generated: 2019_06_20-PM-02_39_58
Last ObjectModification: 2019_06_12-PM-00_28_05

Theory : num_thy_1


Home Index