proposition: Lemma concat_sss_compute_trans {Ps : list (list mm_instr)} {offset} (i : nat) {v st st'} : let j := length (concat (firstn i Ps)) in (j + offset, nth i Ps []) // (j + offset, v) ->> st' -> (offset, concat Ps) // st' ->> st -> (offset, concat Ps) // (j + offset, v) ->> st.
proof: Proof. move=> j H. apply: sss_compute_trans. have : ({(j + offset, v) = st'} + {(j + offset, v) <> st'}). { do ? decide equality. apply: vec_eq_dec. by apply: Nat.eq_dec. } move=> [<-|H']. { by apply: sss_compute_refl. } apply: (subcode_sss_compute (P := (_, nth i Ps []))). - exists (concat (firstn i Ps)), (concat (skipn (S i) Ps)). split; last done. have -> : nth i Ps [] = concat [nth i Ps []]. { by rewrite /concat app_nil_r. } rewrite -?concat_app. congr concat. rewrite [LHS](esym (firstn_skipn i Ps)). congr List.app. have : nth i Ps [] <> []. { move=> H''. move: H. rewrite H''. move=> [[|k]]. - by move=> /sss_steps_0_inv. - move=> /sss_steps_S_inv' [?] [+ _]. by move=> [?] [[|??]] [?] [?] [?] [[]]. } elim: (i) (Ps); first by case. move=> i' IH [|? ?]; first done. rewrite !skipn_cons. by apply: IH. - by rewrite (Nat.add_comm offset). 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