Common pitfall

What is an infinite loop of the prover?

For instance, consider applying the rule:

a * a == a * a * a / a

on the following goal

cc(v) = vv * vv

We will obtain successively the following goals:

cc(v) = vv * vv * vv / vv
cc(v) = (vv * vv * vv / vv) * vv / vv
...

The kernel of the prover then produces the following messageskrt: sequence memory short

krt: asking for 1500000 int, waiting for system reply...
krt: OK, memory obtained, we continue.
krt: sequence memory short
krt: asking for 2249997 int, waiting for system reply...
krt: OK, memory obtained, we continue.
krt: sequence memory short
 krt: asking for 3374992 int, waiting for system reply...
krt: OK, memory obtained, we continue.
...

The messages krt: sequence memory short are generated by the kernel when it dynamically claims additional memory.

This example is simple. Infinite loops may be caused by combination of rule applications and be more difficult to detect a priori.