proposition: Lemma mma_step {P : list mm_instr} {offset} i {v st} : match nth_error P i with | Some (INC X) => (offset, P) // (1 + i + offset, vec_change v X (S (vec_pos v X))) ->> st | Some (DEC X p) => match vec_pos v X with | 0 => (offset, P) // (1 + i + offset, v) ->> st | S n => (offset, P) // (p, vec_change v X n) ->> st end | None => False end -> (offset, P) // (i + offset, v) ->> st.
proof: Proof. case EPi: (nth_error P i) => [instr|]; last done. move: EPi => /(@nth_error_split mm_instr) => - [l] [r] [-> <-]. case: instr. - move=> ?. apply: sss_compute_trans. exists 1. apply: in_sss_steps_S; [|by apply: in_sss_steps_0]. do 5 eexists. split; [done|]. rewrite (Nat.add_comm offset). split; [done|]. by apply: in_mma_sss_inc. - move=> X ?. case E: (vec_pos v X) => [|?]. + apply: sss_compute_trans. exists 1. apply: in_sss_steps_S; [|by apply: in_sss_steps_0]. do 5 eexists. split; [done|]. rewrite (Nat.add_comm offset). split; [done|]. by apply: in_mma_sss_dec_0. + apply: sss_compute_trans. exists 1. apply: in_sss_steps_S; [|by apply: in_sss_steps_0]. do 5 eexists. split; [done|]. rewrite (Nat.add_comm offset). split; [done|]. by apply: in_mma_sss_dec_1. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun