Nuprl Lemma : completeInductionFast

P:

. ((

n:

. ((

m:

n. (P m))

(P n)))

(

n:

. (P n)))

Proof

Definitions occuring in Statement : int_seg: {i..j

}, nat:

, prop:

, all:

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

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

B[x], natural_number: $n
Definitions : so_lambda:

x.t[x], member: t

T, implies: P

Q, prop:

, nat:

, all:

x:A. B[x], so_apply: x[s1;s2], int_seg: {i..j

}, lelt: i

j < k, and: P

Q, le: A

B, not:

A, false: False, so_apply: x[s], uall:

[x:A]. B[x], uimplies: b supposing a, guard: {T}
Lemmas : le_wf, int_seg_wf, all_wf, nat_wf, subtype_rel_dep_function, lelt_wf, subtype_rel_weakening, ext-eq_weakening
\mforall{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. ((\mforall{}n:\mBbbN{}. ((\mforall{}m:\mBbbN{}n. (P m)) {}\mRightarrow{} (P n))) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (P n))) Date html generated: 2013_03_20-AM-09_46_55 Last ObjectModification: 2012_11_27-AM-10_31_58 Home Index