proposition: Lemma simulation_step q t : TM.halt M q = false -> exists k, (omap (fun '(q', t') => (q', truncate_tape t')) (steps (S k) (encode_state q, encode_tape t))) = Some (encode_config (TM_step (TM_facts.mk_mconfig q (| t |)))).
proof: Proof. move=> Hq. case: t. - rewrite /TM_facts.step. move E: (TM.trans _) => [q' a']. move: E. rewrite (Vector.eta a') /TM_facts.current_chars /=. move: (Vector.hd a') => [ob m] /=. case: m ob. + move=> [b|] /= E. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. + move=> [b|] /= E. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. + move=> [b|] /= E. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. - move=> a rs. rewrite /TM_facts.step. move E: (TM.trans _) => [q' a']. move: E. rewrite (Vector.eta a') /TM_facts.current_chars /=. move: (Vector.hd a') => [ob m] /=. case: m ob. + move=> [b|] /= E. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. + move=> [b|] /= E. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 3. do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. by case: a. + move=> [b|] /= E. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. - move=> a ls. rewrite /TM_facts.step. move E: (TM.trans _) => [q' a']. move: E. rewrite (Vector.eta a') /TM_facts.current_chars /=. move: (Vector.hd a') => [ob m] /=. case: m ob. + move=> [b|] /= E. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. + move=> [b|] /= E. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 3. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. + move=> [b|] /= E. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. - move=> ls a rs. rewrite /TM_facts.step. move E: (TM.trans _) => [q' a']. move: E. rewrite (Vector.eta a') /TM_facts.current_chars /=. move: (Vector.hd a') => [ob m] /=. case: m ob. + move=> [b|] /= E. * exists 1. do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. move: ls => [|l ls]; by do ? rewrite construct_trans_spec decode_encode_space. * exists 1. do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. move: ls => [|l ls]; by do ? rewrite /= construct_trans_spec decode_encode_space. + move=> [b|] /= E. * exists 3. do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. move: rs => [|r rs]; by do ? rewrite /= construct_trans_spec decode_encode_space. * exists 3. do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. move: rs => [|r rs]; by do ? rewrite /= construct_trans_spec decode_encode_space. + move=> [b|] /= E. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. * exists 1. by do ? rewrite /= /step /= construct_trans_spec decode_encode_space ?E ?Hq. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun