proposition: Fact mma_push_One_progress s v : v#>zero = 0 -> v#>src = stack_enc s -> (i,mma_push_One) // (i,v) -+> (11+i,v[(stack_enc (One::s))/src]).
proof: Proof. Proof using Hsz. intros H1 H2. unfold mma_push_One. apply sss_progress_trans with (10+i,v[(stack_enc (Zero::s))/src]). + apply subcode_sss_progress with (P := (i,mma_push_Zero)); auto. apply mma_push_Zero_progress; auto. + mma sss INC with src. mma sss stop; f_equal; rew vec. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)