proposition: Fact subcode_sss_terminates_instr P i st1 st2 : i // st1 -1> st2 -> (fst st1,i::nil) <sc P -> P // st2 ↓ -> P // st1 ↓.
proof: Proof. intros H1 H2 (st3 & H3 & H4). exists st3; split; auto. revert H1 H2 H3; apply subcode_sss_compute_instr. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)