proposition: Fact bsm_progress_POP_0 P i x p q ll v st : (i,POP x p q::nil) <sc P -> v#>x = Zero::ll -> P // (p,v[ll/x]) ->> st -> P // (i,v) -+> st.
proof: Proof. intros H1 H2. apply sss_progress_compute_trans. apply subcode_sss_progress with (1 := H1). exists 1; split; auto; apply sss_steps_1. apply in_sss_step with (l := nil). + simpl; lia. + constructor; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)