MACHINE
m0
PROPERTIES
/* The structural inductive theorem */
!P.(P<:NATURAL &
!x.(x:NATURAL&!y.(y:NATURAL&yy:P)=>x:P)
=>
NATURAL<:P)
ASSERTIONS
/* it's a technical lemma used in the next one */
!n.(n:NATURAL&
#x.(x:NATURAL&n*n=2*x)
=>
#x.(x:NATURAL&n=2*x));
/* it's the difficult part of the theorem */
!(n,m).(n:NATURAL&
m:NATURAL
=>
(n*n=2*(m*m) => n=0));
/* the theorem */
!(n,m).(n:NATURAL&
m:NATURAL
=>
(n*n=2*(m*m)<=>(n=0&m=0)))
END