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