proposition: Fact mma_pop_Zero_progress v s: v#>zero = 0 -> v#>src = stack_enc (Zero::s) -> (i,mma_pop) // (i,v) -+> (j0,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 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)/zero]) st) end. rew vec; intros H3. rewrite div2_2p0 in H3. rewrite (Nat.add_comm _ 0) in H3. rewrite H2. apply H3; f_equal. 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)