proposition: Lemma lemma_5_3 i v : P // (i,v) ->> (k,vec_zero) -> Σ; vec_map_list v rx ⊦ q i.
proof: Proof. Proof using Hk. intros (r & Hr); revert i v Hr. induction r as [ | r IHr ]; intros i v Hr. + apply sss_steps_0_inv in Hr. inversion Hr; subst i v; clear Hr. rewrite vec_map_list_zero. apply in_geill_inc with (q k) (q k). left; auto. apply in_geill_ax. + apply sss_steps_S_inv' in Hr. destruct Hr as ((j,w) & H1 & H2). apply IHr in H2. generalize (sss_step_in_code H1); simpl fst; intros H3. apply in_code_subcode in H3. destruct H3 as (ii & Hii). apply sss_step_subcode_inv with (1 := Hii) in H1. destruct ii as [ p | p l ]. * apply mm_sss_INC_inv in H1. destruct H1; subst. apply in_geill_inc with (rx p) (q (1+i)). - apply in_or_app; right. unfold ΣI; destruct P as (ip,lP). apply subcode_mm_linstr_enc; auto. - revert H2; apply in_geill_perm. rewrite vec_change_succ, vec_map_list_plus, vec_map_list_one; auto. * case_eq (vec_pos v p). - intros Hv. apply mm_sss_DEC0_inv in H1; auto. destruct H1; subst l w. apply in_geill_fork with (ry p) (q j); auto. ++ apply in_or_app; right. unfold ΣI; destruct P as (ip,lP). apply subcode_mm_linstr_dec with (1 := Hii); auto. left; auto. ++ apply prop_5_2; auto. - intros u Hu. apply mm_sss_DEC1_inv with (u := u) in H1; auto. destruct H1; subst j w. rewrite vec_change_pred with (1 := Hu). apply in_geill_perm with (1 := Permutation_sym (vec_map_list_plus _ _ _)). rewrite vec_map_list_one. apply in_geill_dec with (rx p) (q (1+i)); auto. ++ apply in_or_app; right. unfold ΣI; destruct P as (ip,lP). apply subcode_mm_linstr_dec with (1 := Hii); auto. right; left; auto. ++ apply in_geill_ax. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs mm_utils) Undecidability.ILL(ILL EILL ill eill)