### 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