proposition: Lemma PREPALL_length i : length (PREPALL i) = k * 14 + n + 1.
proof: Proof. unfold PREPALL, PREPMORE; rewrite !app_length, PREP_length, PREPMORE'_length; cbn; lia. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)