## Now one-step transitions are encoded within a time step by FSM flight graph

## To ensure multi-step consistency, need to enforce equality between cells on a diagonal

- Implemented using round-trip priceable-units that enforce same-flight-number restrictions on outbound flight and return flight
- Key issue is ensuring that right cells are paired; implemented using minimum and maximum stay restrictions: min stay = max stay = TAPE-LENGTH * 2 - 1
- EXP-SPACE limit comes from encoding of min/max stay: n bits encodes 2^n length

This flight equality restriction can be enforced using round-trip priceable units. The fare database is constructed so that each white cell (in a non-final row) can only be priced using a fare with rules that ensure it is paired in a round-trip priceable unit with another same-flight fare. The rules also have 2T-1 day minimum and maximum stay restrictions, ensuring that exactly the right white and gray cell are paired. Without this restriction the tape could become scrambled from one time step to the next.

These minimum and maximum stay restrictions are the limiting factor in the simulation. It takes n bits to encode a minimum stay of length 2^n, so this construction can “only” simulate a TM with a tape of length exponential in the length of the encoding of the TM. On the other hand, there is no limit to the number of steps the TM can run.