proposition: Fact mma_mult_cst_with_zero_progress v st : v#>z = 0 -> st = (8+k+i,v[(k*(v#>x))/x]) -> (i,mma_mult_cst_with_zero) // (i,v) -+> st.
proof: Proof. Proof using Hxz. unfold mma_mult_cst_with_zero. intros H1 H2. apply sss_progress_trans with (st2 := (5+k+i, v[0/x][(k*(v#>x))/z])). + apply subcode_sss_progress with (P := (i,MULT_CSTₐ x z k i)); auto. apply mma_mult_cst_progress; auto. do 2 f_equal; lia. + apply subcode_sss_progress with (P := (5+k+i,TRANSFERTₐ z x (5+k+i))); auto. apply mma_transfert_progress; auto. rewrite H2; f_equal; rew vec. apply vec_pos_ext; intros p. dest p x; dest p z. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)