proposition: Fact subcode_sss_steps_stop P i k st1 st2 : (forall st, ~ i // st1 -1> st) -> (fst st1,i::nil) <sc P -> P // st1 -[k]-> st2 -> k = 0 /\ st1 = st2.
proof: Proof. intros H1 H2 H3. apply sss_steps_inv in H3. destruct H3 as [ | (k' & st & ? & H3 & H4) ]; auto; exfalso. apply (H1 st), subcode_sss_step_inv_1 with (1 := H2); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)