Nuprl Lemma : member-nat-to-str

∀n:ℕ. ∀s:Atom. ((s ∈ nat-to-str(n)) ⇒ (s ∈ ``0 1 2 3 4 5 6 7 8 9``))

Proof

Definitions occuring in Statement : nat-to-str: nat-to-str(n), l_member: (x ∈ l), cons: [a / b], nil: [], nat: ℕ, all: ∀x:A. B[x], implies: P ⇒ Q, token: "$token", atom: Atom
Definitions unfolded in proof : all: ∀x:A. B[x], uall: ∀[x:A]. B[x], member: t ∈ T, int_seg: {i..j^-}, lelt: i ≤ j < k, and: P ∧ Q, le: A ≤ B, uimplies: b supposing a, not: ¬A, implies: P ⇒ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, top: Top, prop: ℙ, decidable: Dec(P), or: P ∨ Q, subtype_rel: A ⊆r B, so_lambda: λ₂x.t[x], so_apply: x[s], guard: {T}, sq_type: SQType(T), nat: ℕ, nat-to-str: nat-to-str(n), less_than: a < b, squash: ↓T, ge: i ≥ j , iff: P ⇐⇒ Q, l_member: (x ∈ l), select: L[n], cons: [a / b], cand: A c∧ B, less_than': less_than'(a;b), true: True, nequal: a ≠ b ∈ T , int_upper: {i...}, subtract: n - m, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , btrue: tt, rev_implies: P ⇐ Q, bfalse: ff, nat_plus: ℕ⁺, int_nzero: ℤ^-^o
Lemmas referenced : int_seg_properties, full-omega-unsat, intformand_wf, intformless_wf, itermVar_wf, itermConstant_wf, intformle_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_less_lemma, int_term_value_var_lemma, int_term_value_constant_lemma, int_formula_prop_le_lemma, int_formula_prop_wf, int_seg_wf, decidable__equal_int, subtract_wf, subtype_base_sq, set_subtype_base, int_subtype_base, intformnot_wf, intformeq_wf, itermSubtract_wf, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_subtract_lemma, decidable__le, decidable__lt, istype-le, istype-less_than, subtype_rel_self, l_member_wf, nat-to-str_wf, istype-atom, cons_wf, nil_wf, primrec-wf2, nat_properties, itermAdd_wf, int_term_value_add_lemma, istype-nat, eq_int_wf, member_singleton, atom_subtype_base, length_of_cons_lemma, length_of_nil_lemma, length_wf, list_subtype_base, le_wf, assert_wf, bnot_wf, not_wf, equal-wf-base, istype-assert, upper_subtype_nat, istype-false, nequal-le-implies, zero-add, int_upper_properties, upper_subtype_upper, add-commutes, bool_cases, bool_wf, bool_subtype_base, eqtt_to_assert, assert_of_eq_int, eqff_to_assert, iff_transitivity, iff_weakening_uiff, assert_of_bnot, member_append, divide_wf, remainder_wf, rem_bounds_1, div_rem_sum, nequal_wf, divide_wfa, add-is-int-iff, multiply-is-int-iff, itermMultiply_wf, int_term_value_mul_lemma, false_wf, remainder_wfa
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :lambdaFormation_alt, cut, thin, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, setElimination, rename, productElimination, hypothesis, hypothesisEquality, 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, unionElimination, applyEquality, instantiate, because_Cache, equalityTransitivity, equalitySymmetry, applyLambdaEquality, Error :dependent_set_memberEquality_alt, Error :productIsType, hypothesis_subsumption, atomEquality, Error :functionIsType, functionEquality, imageElimination, tokenEquality, Error :setIsType, Error :inhabitedIsType, addEquality, cumulativity, imageMemberEquality, baseClosed, Error :equalityIstype, baseApply, closedConclusion, intEquality, sqequalBase, promote_hyp, pointwiseFunctionality

Latex:
\mforall{}n:\mBbbN{}. \mforall{}s:Atom. ((s \mmember{} nat-to-str(n)) {}\mRightarrow{} (s \mmember{} ``0 1 2 3 4 5 6 7 8 9``)) Date html generated: 2019_06_20-PM-01_58_21 Last ObjectModification: 2019_03_06-AM-10_52_18 Theory : decidable!equality Home Index