proposition: Lemma PREPMORE_spec i x (w : Vector.t nat k) : (i, PREPMORE) /MM/ (i, Vector.append (Vector.append (x ## w) (Vector.const 0 n)) (0 ## 0 ## 0 ## vec_nil)) ~~> (i + n, Vector.append (Vector.append (x ## w) (Vector.const 1 n)) (0 ## 0 ## 0 ## vec_nil)).
proof: Proof. pose proof (PREPMORE'_spec i x w n 0). cbn in H. cbn. match goal with [ |- sss_output _ _ _ (_, ?st) ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end. 1: eapply H. repeat f_equal. eapply vec_list_inj. rewrite vec_list_cast, vec_list_const, <- vec_app_spec, vec_list_vec_app, vec_list_const. now simpl_list. Unshelve. 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)