10 lines
328 B
Python
10 lines
328 B
Python
# Perform the proofs under the assumption that n is a nonnegative integer input constant
|
|
input: n -> integer.
|
|
assume: n >= 0.
|
|
|
|
# p/1 is an auxiliary predicate
|
|
output: q/1.
|
|
|
|
# Verify that q computes the floor of the square root of n
|
|
spec: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
|