faster guessing of size based termination proofs

[ordinarymath]

With the termination checker slowness, it could be made much faster if isabelle style compute a matrix is done. Reduces the number of solver calls required. https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf