proposition: Fact simulator_length : length simulator = 27+lML.
proof: Proof. unfold simulator; rew length; unfold lML; lia. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs bsm_utils)