proposition: Fact subcode_sss_compute_linstr k li P st1 st2 st : (fst st1,li) // st1 -[k]-> st2 -> (fst st1,li) <sc P -> P // st2 ->> st -> P // st1 ->> st.
proof: Proof. intros H1 H2. apply subcode_sss_compute_trans with (1 := H2). exists k; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)