proposition: Lemma subcode_sss_compute_inv P Q st1 st3 : P <sc Q -> out_code (fst st3) P -> Q // st1 ->> st3 -> exists st2, P // st1 ->> st2 /\ Q // st2 ->> st3 /\ out_code (fst st2) P.
proof: Proof. intros H1 H3 (k & Hk). destruct (in_out_code_dec (fst st1) P) as [ H2 | H2 ]. + apply subcode_sss_steps_inv with (1 := H1) in Hk; auto. destruct Hk as (k1 & k2 & st2 & H4 & H5 & H6 & H7). exists st2; repeat split; auto; red; firstorder. + exists st1; repeat split; auto. * exists 0; constructor. * red; firstorder. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)