Nuprl Lemma : coded-seq1_wf

[k:ℕ]. ∀[n:ℕ1]. ∀[x:ℕ].  (coded-seq1(k;x;n) ∈ ℕ)


Proof




Definitions occuring in Statement :  coded-seq1: coded-seq1(k;x;n) int_seg: {i..j-} nat: uall: [x:A]. B[x] member: t ∈ T add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A all: x:A. B[x] top: Top and: P ∧ Q prop: coded-seq1: coded-seq1(k;x;n) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff uiff: uiff(P;Q) or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b int_seg: {i..j-} nequal: a ≠ b ∈  lelt: i ≤ j < k decidable: Dec(P) le: A ≤ B less_than: a < b
Lemmas referenced :  nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma 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 less_than_wf nat_wf int_seg_wf eq_int_wf bool_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int coded-pair_wf int_seg_properties intformnot_wf intformeq_wf itermAdd_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_add_lemma decidable__le subtract_wf itermSubtract_wf int_term_value_subtract_lemma subtract-add-cancel decidable__lt lelt_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename sqequalRule intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry addEquality because_Cache unionElimination equalityElimination productElimination promote_hyp instantiate cumulativity productEquality dependent_set_memberEquality

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[n:\mBbbN{}k  +  1].  \mforall{}[x:\mBbbN{}].    (coded-seq1(k;x;n)  \mmember{}  \mBbbN{})



Date html generated: 2019_06_20-PM-02_39_51
Last ObjectModification: 2019_06_12-PM-00_28_00

Theory : num_thy_1


Home Index