Generate constraints ensuring that p is an algebraic relation.

Generate constraints describing the relationship between entries of B and the closed forms.

Generate constraints defining the initial values.

Generate constraints ensuring that sequence is not constant, i.e. BBx0 != B*x0.

Generate constraints ensuring that the root symbols are roots of the characteristic polynomial of B.

Return true if the invariant is a relation among a single loop iteration.