fact: Fixpoint decoder s i lt := match lt with | nil => decoder_error | (th,tl) :: lt => POP c (3+length (tile h l th tl)+i) q :: tile h l th tl ++ PUSH c Zero :: POP c s s :: decoder s (3+length (tile h l th tl)+i) lt end.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)