Nuprl Lemma : first-25-rationals

map(λn.nth-rational(n);upto(25))
= [0;
   -1;
   1;
   (-1/2);
   -2;
   (1/2);
   (-1/3);
   2;
   (1/3);
   (-1/4);
   -3;
   (-2/3);
   (1/4);
   (-1/5);
   3;
   (-3/2);
   (2/3);
   (1/5);
   (-1/6);
   -4;
   (3/2);
   (-2/5);
   (1/6);
   (-1/7);
   4]
∈ (ℚ List)

Proof

Definitions occuring in Statement : nth-rational: nth-rational(n), qdiv: (r/s), rationals: ℚ, upto: upto(n), map: map(f;as), cons: [a / b], nil: [], list: T List, lambda: λx.A[x], minus: -n, natural_number: $n, equal: s = t ∈ T
Definitions unfolded in proof : upto: upto(n), from-upto: [n, m), lt_int: i <z j, ifthenelse: if b then t else f fi , btrue: tt, all: ∀x:A. B[x], member: t ∈ T, top: Top, bfalse: ff, squash: ↓T, uall: ∀[x:A]. B[x], prop: ℙ, subtype_rel: A ⊆r B, nat: ℕ, le: A ≤ B, and: P ∧ Q, less_than': less_than'(a;b), false: False, not: ¬A, implies: P ⇒ Q, uiff: uiff(P;Q), rev_uimplies: rev_uimplies(P;Q), uimplies: b supposing a, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], true: True
Lemmas referenced : map_cons_lemma, map_nil_lemma, cons_wf, squash_wf, true_wf, list_wf, rationals_wf, assert-qeq, int-subtype-rationals, nth-rational_wf, false_wf, le_wf, eqtt_to_assert, qeq_wf2, btrue_wf, qdiv_wf, satisfiable-full-omega-tt, intformeq_wf, itermConstant_wf, int_formula_prop_eq_lemma, int_term_value_constant_lemma, int_formula_prop_wf, equal-wf-base, int-equal-in-rationals, not_wf, nil_wf
Rules used in proof : equalitySymmetry, sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, sqequalRule, callbyvalueReduce, sqleReflexivity, cut, introduction, extract_by_obid, sqequalHypSubstitution, dependent_functionElimination, thin, isect_memberEquality, voidElimination, voidEquality, hypothesis, applyEquality, lambdaEquality, imageElimination, isectElimination, hypothesisEquality, equalityTransitivity, universeEquality, natural_numberEquality, dependent_set_memberEquality, independent_pairFormation, lambdaFormation, productElimination, independent_isectElimination, because_Cache, computeAll, minusEquality, intEquality, dependent_pairFormation, baseClosed, addLevel, impliesFunctionality, imageMemberEquality

Latex:
map(\mlambda{}n.nth-rational(n);upto(25)) = [0; -1; 1; (-1/2); -2; (1/2); (-1/3); 2; (1/3); (-1/4); -3; (-2/3); (1/4); (-1/5); 3; (-3/2); (2/3); (1/5); (-1/6); -4; (3/2); (-2/5); (1/6); (-1/7); 4] Date html generated: 2018_05_21-PM-11_49_21 Last ObjectModification: 2017_07_26-PM-06_43_18 Theory : rationals Home Index