Affine Programs Invariant Builder And Reachability Checker

Input Format Explanation

On the first line write the start point, target and optionally whether you expect it to be reachable. If the start point is negative, the problem will be inverted so it is positive. Supported targets are single numbers, or Z-linear sets, with {b+pZ} specified as b+p.
On subsequent lines, write the functions by writing the multiplier and the adder, i.e. a b means f(x) = ax+b. Do not include redundant functions.
On the line after the last function, optionally, write ENDS. Everything after ENDS will be ignored.


start target[+period] [True|False]
a b
a b

Input area


Output area