proposition: Theorem sss_compute_max_ind st1 st3 : P // st1 -]] st3 -> R st1 st3.
proof: Proof. Proof using sss_fun HQ0 HQ1. intros ((k & H1) & H2); revert st1 H1. induction k as [ k IH ] using (well_founded_induction_type lt_wf). intros st1 H1. destruct k as [ | k ]. apply sss_steps_0_inv in H1. subst; apply HQ0; auto. apply HQ1. intros Q st2' HQ H5 ((q & H6) & _). apply subcode_sss_progress with (1 := HQ) in H5. destruct H5 as (l & Hl & H5). generalize (sss_steps_trans H5 H6); intro H7. generalize (sss_steps_stall_fun H2 H1 H7); intros H8. apply IH with q; auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)