proposition: Lemma PREPALL_spec i v : (i, PREPALL i) /MM/ (i, Vector.append (Vector.append (0 ## v) (Vector.const 0 n)) (0 ## 0 ## 0 ## vec_nil)) ~~> (i + k * 14 + n + 1, Vector.append (Vector.append (stack_enc nil ## Vector.map (fun n => stack_enc (List.repeat true n)) v) (Vector.const (stack_enc nil) n)) (0 ## 0 ## 0 ## vec_nil)).
proof: Proof. split. 2: cbn; rewrite PREPALL_length; lia. eapply subcode_sss_compute_trans. 2: eapply PREP_spec. 1: unfold PREPALL; auto. eapply subcode_sss_compute_trans. 2: eapply PREPMORE_spec. 1: unfold PREPALL; auto. mm sss INC with pos0. { unfold PREPALL. eexists. eexists nil. cbn. split. 1: now rewrite app_assoc. rewrite app_length, PREP_length; unfold PREPMORE; rewrite PREPMORE'_length. lia. } fold plus. mm sss stop. f_equal. 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)