proposition: Fact mm_pop_void_progress v : v#>tmp1 = 0 -> v#>tmp2 = 0 -> v#>src = stack_enc nil -> (i,mm_pop) // (i,v) -+> (e,v).
proof: Proof. Proof using Hs1 Hs2 H12. unfold mm_pop. intros H1 H2 H4; simpl in H4. apply sss_progress_trans with (3+i,v[0/src][1/tmp1]). apply subcode_sss_progress with (P := (i,mm_transfert src tmp1 tmp2 i)); auto. apply mm_transfert_progress; auto; f_equal. rewrite H4; auto. apply sss_progress_trans with (9+i,v[0/tmp1][0/src][1/tmp2]). apply subcode_sss_progress with (P := (3+i,mm_div2 tmp1 src tmp2 (3 + i))); auto. apply mm_div2_progress_1 with (k := 0); auto; rew vec. f_equal. apply vec_pos_ext; intros p. dest p tmp2; dest p src; dest p tmp1. mm sss DEC zero with src (13+i); rew vec. mm sss DEC S with tmp2 k 0; rew vec. mm sss INC with src'; unfold src'; rew vec. mm sss DEC zero with tmp2 e; rew vec. mm sss stop; f_equal. apply vec_pos_ext; intros p. dest p tmp2; dest p src; dest p tmp1. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)