\* Tape optimizer specification
\* Default bounds: MaxTapeLen=5, NumInputs=2 (~20s on 14 cores)
\* For thorough runs: MaxTapeLen=6+ (minutes to hours)

CONSTANTS
    MaxTapeLen = 5
    NumInputs = 2

SPECIFICATION Spec

\* Terminal state "done" has no successor -- not a deadlock.
CHECK_DEADLOCK FALSE

INVARIANT
    InputPrefixInvariant
    DAGOrderInvariant
    ValidRefsInvariant
    OutputValidInvariant
    InputsPreserved
    CSERemapMonotone
    CSERemapIdempotent
    DCEInputsReachable
    DCEOutputReachable
    DCECompactProgress
    PostOptValid

PROPERTY
    Termination
