proposition: Fact sss_progress_non_termination P st : P // st -+> st -> ~ P // st ↓.
proof: Proof. Proof using sss_fun. intros (a & H1 & H2) (st' & (b & H3) & H4). assert (P // st -[a+b]-> st') as H5. { apply sss_steps_trans with (1 := H2); auto. } destruct sss_steps_stop_fun with (3 := H3) (4 := H5); auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)