proposition: Fact mma_sss_steps_DEC_1_inv k P i x p v u st : (i,DECₐ x p::nil) <sc P -> k <> 0 -> v#>x = S u -> P // (i,v) -[k]-> st -> exists k', k' < k /\ P // (p,v[u/x]) -[k']-> st.
proof: Proof. intros H1 H2 H3 H4. apply sss_steps_inv in H4. destruct H4 as [ (? & ?) | (k' & st2 & ? & H4 & H5) ]; subst; auto. destruct H2; auto. apply sss_step_subcode_inv with (1 := H1) in H4. exists k'; split. + lia. + inversion H4; subst; auto; rewrite H3 in H9. * discriminate. * inversion H9; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)