proposition: Fact mma_pop_void_progress v : v#>zero = 0 -> v#>src = stack_enc nil -> (i,mma_pop) // (i,v) -+> (je,v).
proof: Proof. Proof using Hsz. intros H1 H2; unfold mma_pop. apply sss_progress_trans with (st2 := (3+i,v[0/src][(v#>src)/zero])). 1:{ apply subcode_sss_progress with (P := (i,TRANSFERTₐ src zero i)); auto. apply mma_transfert_progress; auto. do 2 f_equal; lia. } apply sss_progress_trans with (st2 := (12+i,v[0/src][0/zero])). 1:{ apply subcode_sss_progress with (P := (3+i,DIV2ₐ zero src (3+i) j0 (12 + i))); auto. simpl in H2. generalize (mma_div2_branch_progress Hzs (3+i) j0 (12+i) (v[0/src][1/zero])); rew vec; intros H3. simpl div2 in H3. rewrite H2; apply H3; f_equal; simpl; rew vec. apply vec_pos_ext; intros p; dest p src. } mma sss DEC zero with src (16+i); rew vec. mma sss INC with src; rew vec. apply subcode_sss_compute with (P := (14+i,JUMPₐ je src)); auto. apply sss_progress_compute, mma_jump_progress. apply vec_pos_ext; intros p; dest p src; 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)