Nuprl Lemma : coded-code-seq

k:ℕ. ∀s:ℕk ⟶ ℕ.  (coded-seq(code-seq(k;s)) = <k, s> ∈ (k:ℕ × (ℕk ⟶ ℕ)))


Proof




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

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}.    (coded-seq(code-seq(k;s))  =  <k,  s>)



Date html generated: 2019_06_20-PM-02_40_43
Last ObjectModification: 2019_06_12-PM-00_28_38

Theory : num_thy_1


Home Index