Proof of Nuprl Lemma : sqrt-int-aa-fast

Step * of Lemma sqrt-int-aa-fast

n:

.

r:

. (((r * r)

n)

(n < ((r + 1) * (r + 1))))
BY
{ (InstLemma `natInd4Boot2` [

n.

r:

. (((r * r)

n)

(n < ((r + 1) * (r + 1))))

]

THEN Auto THEN Reduce 0) }

1

r:

. (((r * r)

0)

(0 < ((r + 1) * (r + 1))))

2
1. i :

@i
2. (

n.

r:

. (((r * r)

n)

(n < ((r + 1) * (r + 1))))) (i

4)@i

r:

. (((r * r)

i)

(i < ((r + 1) * (r + 1))))

3
1.

n:

. ((

n.

r:

. (((r * r)

n)

(n < ((r + 1) * (r + 1))))) n)
2. n :

@i

r:

. (((r * r)

n)

(n < ((r + 1) * (r + 1))))

\mforall{}n:\mBbbN{}. \mexists{}r:\mBbbN{}. (((r * r) \mleq{} n) \mwedge{} (n < ((r + 1) * (r + 1)))) By (InstLemma `natInd4Boot2` [\mkleeneopen{}\mlambda{}n.\mexists{}r:\mBbbN{}. (((r * r) \mleq{} n) \mwedge{} (n < ((r + 1) * (r + 1))))\mkleeneclose{}]\mcdot{} THEN Auto THEN Reduce 0) Home Index