proposition: Fact sss_compute_step_out_inv P k st1 st2 st3 : st1 <> st2 -> out_code (fst st3) P -> P // st1 ->> st2 -> P // st1 -[k]-> st3 -> exists q, q < k /\ P // st2 -[q]-> st3.
proof: Proof. Proof using sss_fun. intros H1 H2 (p & H3) H4. apply subcode_sss_subcode_inv with (3 := H3) in H4; auto. destruct H4 as (q & H4 & H5). exists q; split; auto. destruct p; try lia. apply sss_steps_0_inv in H3. destruct H1; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)