proposition: Theorem lemma_5_5 v i : Σ; vec_map_list v rx ⊦ q i -> P // (i,v) ->> (k,vec_zero).
proof: Proof. Proof using Hk. intros H. apply G_eill_S_ill_wc in H. apply ill_tps_sound with (s := s) in H. red in H. specialize (H v). rewrite vec_add_comm, vec_zero_plus in H. apply H_s_q; auto. apply H. rewrite ill_tps_app. exists vec_zero, v; repeat split. + rew vec. + apply ill_tps_Σ_zero. + apply ill_tps_vec_map_list; auto. 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)