def even "Ek m=2*k":
eval davisthm "Am,n ($even(m) & $even(n)) => $even(m+n)":

eval test "Ei,n (n>=1) & Aj (j<=n) => T[i+j] = T[i+j+n]";

eval thuesquare "n>=1 & Ei Aj (j<n) => T[i+j]=T[i+j+n]":