proposition: Fact mm_push_Zero_progress s v : v#>tmp = 0 -> v#>zero = 0 -> v#>src = stack_enc s -> (i,mm_push_Zero) // (i,v) -+> (7+i,v[(stack_enc (Zero::s))/src]).
proof: Proof. Proof using Htz Hsz Hst. intros H1 H2 H3. unfold mm_push_Zero. apply sss_progress_trans with (st2 := (3+i,v[0/src][(v#>src)/tmp])). apply subcode_sss_progress with (P := (i,mm_transfert src tmp zero i)); auto. apply mm_transfert_progress; auto. apply subcode_sss_progress with (P := (3+i,mm_mul2 tmp src zero (3 + i))); auto. apply mm_mul2_progress; auto; rew vec. f_equal. apply vec_pos_ext; intros p. dest p src. rewrite H3; auto. dest p tmp. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)