proposition: Fact mm_push_One_progress s v : v#>tmp = 0 -> v#>zero = 0 -> v#>src = stack_enc s -> (i,mm_push_One) // (i,v) -+> (8+i,v[(stack_enc (One::s))/src]).
proof: Proof. Proof using Htz Hsz Hst. intros H1 H2 H3. unfold mm_push_One. apply sss_progress_trans with (7+i,v[(stack_enc (Zero::s))/src]). apply subcode_sss_progress with (P := (i,mm_push_Zero)); auto. apply mm_push_Zero_progress; auto. mm sss INC with src. mm sss stop; f_equal; auto. apply vec_pos_ext; intros p. dest p src. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)