proposition: Lemma subcode_sss_steps_inv P Q k st1 st3 : P <sc Q -> in_code (fst st1) P -> out_code (fst st3) P -> Q // st1 -[k]-> st3 -> exists k1 k2 st2, P // st1 -[k1]-> st2 /\ Q // st2 -[k2]-> st3 /\ k = k1+k2 /\ out_code (fst st2) P.
proof: Proof. intros H1 H2 H3 H4; revert H4 H2 H3. induction 1 as [ st1 | k st1 st2 st3 H4 H5 IH5 ]; intros H2 H3. exists 0, 0, st1; repeat split; auto; constructor. apply subcode_sss_step_inv with (1 := H1) in H4; auto. destruct (in_out_code_dec (fst st2) P) as [ H6 | H6 ]. destruct (IH5 H6 H3) as (k1 & k2 & st & ? & ? & ? & ?). exists (S k1), k2, st; repeat split; auto. constructor 2 with (1 := H4); auto. lia. exists 1, k, st2; repeat split; auto. apply sss_steps_1; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)