proposition: Lemma inverse_simulation q t n i v : (1, P) // (encode_config (q, t)) -[n]-> (i, v) -> out_code i (1, P) -> exists k, steps M k (q, t) = None.
proof: Proof. elim /(Nat.measure_induction _ id) : n q t => - [|n] IH q t. { move=> /sss_steps_0_inv [] /= <- _. rewrite /encode_state P_length (ltac:(done) : c = (S (c-1))). have := svalP (Fin.to_nat q). nia. } case E: (step M (q, t)) => [[q' t']|]; last by (move=> _; exists 1). move: (E) => /simulation_step_Some [m]. move=> Hn Hm Hi. have := (IH (n - m) ltac:(lia) q' t' _ Hi). case. { move: Hn Hm Hi => /subcode_sss_subcode_inv /[apply] /[apply]. case. - by exact: bsm_sss_fun. - by apply: subcode_refl. - move=> n' [?]. by have ->: n' = n - m by lia. } move=> k Hk. exists (1+k). by rewrite (steps_plus 1) /= E. Qed.
imports: Undecidability.StackMachines(BSM BSM.bsm_defs) Undecidability.TM(SBTM Util.SBTM_facts) Undecidability.Shared.Libs.DLW(vec subcode sss) PeanoNat List Lia ssreflect ssrbool ssrfun