iterateb unwinds a loop once by rephrasing [a*]P to the equivalent P∧[a][a*]P, which says that the system is safe initially and after at least one repetition. Unwinding will not itself prove properties of loops but can be useful to disprove them or to identify required conditions for the safety.

See also