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