proposition: Fact main_loop_size : length_main_loop = 59+3*length lt+size_cards lt.
proof: Proof. unfold length_main_loop, lFD, length_full_decoder. rewrite length_decoder_size; 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)