proposition: Fact mm_pop_One_progress v s: v#>tmp1 = 0 -> v#>tmp2 = 0 -> v#>src = stack_enc (One::s) -> (i,mm_pop) // (i,v) -+> (k,v[(stack_enc s)/src]).
proof: Proof. Proof using Hs1 Hs2 H12. unfold mm_pop. intros H1 H2 H4; unfold stack_enc in H4; fold stack_enc in H4. apply sss_progress_trans with (3+i,v[0/src][(2*stack_enc s+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; f_equal; lia. apply sss_progress_trans with (9+i,v[0/tmp1][(stack_enc s)/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 := stack_enc s); auto; rew vec. rewrite div2_2p1; auto. f_equal. apply vec_pos_ext; intros p. dest p tmp2; dest p src; dest p tmp1. destruct (stack_enc_S s) as (q & Hq). mm sss DEC S with src (13+i) q; rew vec. mm sss INC with src; rew vec. mm sss DEC S with tmp2 j 0; rew vec. mm sss DEC zero with tmp1 k; rew vec. mm sss stop; f_equal. apply vec_pos_ext; intros p. dest p src; dest p tmp2; dest p tmp1. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)