Nuprl Lemma : test-nat-bootstrap

P:

.

b:P 0.

c:n:

P n

(P (n + 1)).

n:

. ((

n.primrec(n;b;c)) n

P n)

Proof

Definitions occuring in Statement : nat:

, prop:

, all:

x:A. B[x], member: t

T, apply: f a, lambda:

x.A[x], function: x:A

B[x], add: n + m, natural_number: $n, primrec: primrec(n;b;c)
Definitions : all:

x:A. B[x], nat:

, prop:

, member: t

T, le: A

B, not:

A, implies: P

Q, false: False, primrec: primrec(n;b;c), and: P

Q, iff: P

Q, rev_implies: P

Q, has-value: (a)

, so_lambda:

x.t[x], uall:

[x:A]. B[x], bool:

, unit: Unit, uimplies: b supposing a, uiff: uiff(P;Q), guard: {T}, sq_type: SQType(T), so_apply: x[s], it:

, btrue: tt, bfalse: ff
Lemmas : nat_wf, le_wf, eq_int_wf, bool_wf, uiff_transitivity, equal_wf, subtype_rel_weakening, ext-eq_weakening, assert_wf, eqtt_to_assert, assert_of_eq_int, subtype_base_sq, int_subtype_base, subtype_rel_self, iff_transitivity, bnot_wf, not_wf, iff_weakening_uiff, eqff_to_assert, assert_of_bnot, set-value-type, int-value-type
\mforall{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. \mforall{}b:P 0. \mforall{}c:n:\mBbbN{} {}\mrightarrow{} P n {}\mrightarrow{} (P (n + 1)). \mforall{}n:\mBbbN{}. ((\mlambda{}n.primrec(n;b;c)) n \mmember{} P n) Date html generated: 2013_03_20-AM-09_46_07 Last ObjectModification: 2012_11_27-AM-10_31_56 Home Index