Nuprl Lemma : natInd4BootFast

P:

. (((P 0)

(

i:

. ((P (i

4))

(P i))))

(

n:

. (P n)))

Proof

Definitions occuring in Statement : nat:

, prop:

, all:

x:A. B[x], implies: P

Q, and: P

Q, apply: f a, function: x:A

B[x], divide: n

m, natural_number: $n
Definitions : nat_plus:

, so_lambda:

x.t[x], false: False, not:

A, le: A

B, member: t

T, and: P

Q, implies: P

Q, prop:

, nat:

, all:

x:A. B[x], int_seg: {i..j

}, lelt: i

j < k, nequal: a

T , int_nzero:

, so_apply: x[s], uall:

[x:A]. B[x], decidable: Dec(P), or: P

Q, sq_type: SQType(T), uimplies: b supposing a, guard: {T}
Lemmas : divide_wf, all_wf, le_wf, nat_wf, completeInductionFast, int_seg_wf, decidable__equal_int, subtype_base_sq, int_subtype_base, lelt_wf, div_rem_sum, nequal_wf, rem_bounds_1, ext-eq_weakening, subtype_rel_weakening
\mforall{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. (((P 0) \mwedge{} (\mforall{}i:\mBbbN{}. ((P (i \mdiv{} 4)) {}\mRightarrow{} (P i)))) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (P n))) Date html generated: 2013_03_20-AM-09_47_12 Last ObjectModification: 2012_11_27-AM-10_31_58 Home Index