fact: Fixpoint length_decoder lt := match lt with | nil => 2 | (th,tl) :: lt => 3+length th+length tl+length_decoder 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)