proposition: Fact mma_pop_One_progress v s: v#>zero = 0 -> v#>src = stack_enc (One::s) -> (i,mma_pop) // (i,v) -+> (j1,v[(stack_enc s)/src]).
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[(stack_enc s)/src][0/zero])). 1:{ apply subcode_sss_progress with (P := (3+i,DIV2ₐ zero src (3+i) j0 (12 + i))); auto. match goal with |- _ // _ -+> ?st => generalize (mma_div2_branch_progress Hzs (3+i) j0 (12+i) (v[0/src][(2*stack_enc s+1)/zero]) st) end. rew vec; intros H3. rewrite div2_2p1 in H3. rewrite (Nat.add_comm _ 1) in H3. rewrite H2. apply H3; f_equal; simpl; rew vec. apply vec_pos_ext; intros p; dest p src; dest p zero. } destruct (stack_enc_S s) as (k & Hk). mma sss DEC S with src (16+i) k; rew vec. mma sss INC with src'; rew vec. apply subcode_sss_compute with (P := (17+i,JUMPₐ j1 src)); auto. apply sss_progress_compute, mma_jump_progress. unfold src'; 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)