proposition: Fact bsm_steps_PUSH_inv k P i x b v st : (i,PUSH x b::nil) <sc P -> st <> (i,v) -> P // (i,v) -[k]-> st -> { a | a < k /\ P // (1+i,v[(b::v#>x)/x]) -[a]-> st }.
proof: Proof. intros H1 H2 H4. apply sss_steps_inv in H4. destruct H4 as [ (? & ?) | (a & H4) ]; subst; auto. 1: destruct H2; auto. exists a. destruct H4 as (st2 & ? & H4 & H5); subst. split; try lia. apply sss_step_subcode_inv with (1 := H1) in H4. inversion H4; subst; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss)