proposition: Fact subcode_sss_subcode_inv P Q p k st1 st2 st3 : out_code (fst st3) P -> P <sc Q -> P // st1 -[p]-> st2 -> Q // st1 -[k]-> st3 -> exists q, k = p+q /\ Q // st2 -[q]-> st3.
proof: Proof. Proof using sss_fun. revert P Q st3; intros P (j,cj) (n,d) H1 H2 H3. simpl in H1. revert k. induction H3 as [ st | p st1 st2 st3 H4 H5 IH5 ]; intros k Hk. exists k; auto. apply sss_steps_inv in Hk. destruct Hk as [ (? & Hk) | (m & st4 & ? & Hk & H3) ]. 1: subst st1; apply sss_step_in_code in H4; simpl in H4; lia. apply subcode_sss_step with (1 := H2) in H4. rewrite (sss_step_fun Hk H4) in H3. apply IH5 in H3; auto. destruct H3 as (q & ? & H3). exists q; split; auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)