proposition: Theorem sss_terminates_ind st : P // st ↓ -> R st.
proof: Proof. Proof using sss_fun HR0 HR1. intros (st2 & (k & H1) & H2); revert st st2 H1 H2. induction k as [ k IH ] using (well_founded_induction_type lt_wf). intros st1 st2 H1 H2. destruct k as [ | k ]. + apply sss_steps_0_inv in H1. subst; apply HR0; auto. + apply HR1. intros Q st2' HQ H5. assert (P // st2' ↓) as (st3 & H6 & H7). { assert (P // st1 ↓) as (st3' & H'6 & H'7). { exists st2. split; [exists (S k)|]; assumption. } apply (subcode_sss_progress _ HQ) in H5. apply (sss_progress_compute) in H5. assert (H8 := sss_compute_inv H'7 H5 H'6). exists st3'. split; assumption. } apply subcode_sss_progress_inv with (3 := H5) in H1; auto. destruct H1 as (q & G1 & G2). apply IH with (2 := G2); auto. revert H2; apply subcode_out_code; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)