proposition: Lemma POSTP_spec i v out : v #> pos0 = 0 -> v #> tmp pos0 = 0 -> v #> tmp pos1 = 0 -> v #> tmp pos2 = stack_enc (List.repeat true out) -> (i, POSTP i) /MM/ (i, v) ~~> (i + 18, v [ out / pos0] [ (stack_enc nil) / tmp pos2 ]).
proof: Proof. intros Htgt Htmp0 Htmp1 Htmp2. pose proof (POSTP_spec_strong i v out 0 Htgt Htmp0 Htmp1 Htmp2). rewrite NPeano.Nat.add_0_r in H. eapply H. 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)