proposition: Fact mma_push_Zero_progress s v : v#>zero = 0 -> v#>src = stack_enc s -> (i,mma_push_Zero) // (i,v) -+> (10+i,v[(stack_enc (Zero::s))/src]).
proof: Proof. Proof using Hsz. intros H1 H2. unfold mma_push_Zero. apply sss_progress_trans with (st2 := (3+i,v[0/src][(v#>src)/zero])). + apply subcode_sss_progress with (P := (i,TRANSFERTₐ src zero i)); auto. apply mma_transfert_progress; auto. do 2 f_equal; lia. + apply subcode_sss_progress with (P := (3+i,MULT_CSTₐ zero src 2 (3+i))); auto. apply mma_mult_cst_progress; auto. f_equal; rew vec. apply vec_pos_ext; intros p. dest p src; simpl; try lia. dest p zero. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)