\* Idempotency verification for the tape optimizer.
\* Checks optimize(optimize(tape)) = optimize(tape) for all valid tapes.
\* Default bounds: MaxTapeLen=5, NumInputs=2 (~2s on 14 cores)

CONSTANTS
    MaxTapeLen = 5
    NumInputs = 2

SPECIFICATION Spec

\* Terminal state "done" has no successor.
CHECK_DEADLOCK FALSE

INVARIANT
    IdempotencyProperty

PROPERTY
    Termination
