proposition: Lemma DoWrite_Terminates (d : option move) (s : sig) : projT1 (DoWrite d s) ↓ DoWrite_T d.
proof: Proof. unfold DoWrite. destruct d as [ [ | | ] | ]. { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir. unfold atCons_current_leftof in HCons. TMSimp. exists (16 + 4 * length (encode_list (@encode_tape sig) tps1)), (20 + 4 * length (encode_list (@encode_tape sig) tps1)). repeat split. { etransitivity. { apply Nat.add_le_mono_l, Nat.add_le_mono_l, Shift_steps_local. } simpl_list; cbn. rewrite removelast_length. lia. } { lia. } intros tmid [] ->. exists (16 + 4 * length (encode_list (@encode_tape sig) tps1)), 3. repeat split. { rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto. rewrite app_comm_cons'. rewrite MoveToSymbol_steps_midtape; cbn; auto. simpl_list. rewrite removelast_length. cbn. lia. } { lia. } intros ? [] ?. exists 1, 1. repeat split. reflexivity. reflexivity. intros _ _ _. reflexivity. } { eapply TerminatesIn_monotone. now auto with nocore TMdb. intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir. unfold atCons_current_rightof in HCons. TMSimp. exists (16 + 4 * length (encode_list (@encode_tape sig) tps2)), (20 + 4 * length (encode_list (@encode_tape sig) tps2)). repeat split. { etransitivity. { apply Nat.add_le_mono_l, Shift_steps_local. } simpl_list; cbn. lia. } { lia. } intros tmid [] ->. exists (16 + 4 * length (encode_list (@encode_tape sig) tps2)), 3. repeat split. { rewrite app_comm_cons. rewrite Shift_fun_correct_midtape; auto. rewrite app_comm_cons'. rewrite MoveToSymbol_L_steps_midtape; cbn; auto. simpl_list. cbn. lia. } { lia. } intros ? [] ?. exists 1, 1. repeat split. reflexivity. reflexivity. intros _ _ _. reflexivity. } { eapply TerminatesIn_monotone. { now auto with nocore TMdb. } intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. assumption. } { eapply TerminatesIn_monotone. { now auto 7 with nocore TMdb. } intros tin k (tps1&tps2&tp&HDir&HCons&Hk). cbn in *. destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; inv HDir. unfold atCons_current_niltape in HCons. TMSimp. rewrite Shift_fun_correct_midtape; auto. cbn. exists (16 + 4 * length (encode_list (@encode_tape sig) tps2)), (56 + 8 * length (encode_list (@encode_tape sig) tps1) + 4 * length (encode_list (@encode_tape sig) tps2)). repeat split; try lia. { etransitivity. { apply Nat.add_le_mono_l, Shift_steps_local. } simpl_list. cbn. lia. } intros tmid [] ->. exists (16 + 4 * length (encode_list (@encode_tape sig) tps2)), (39 + 8 * length (encode_list (@encode_tape sig) tps1)). repeat split; try lia. { rewrite app_comm_cons. rewrite app_comm_cons'. rewrite MoveToSymbol_L_steps_midtape; cbn; auto. simpl_list. cbn. lia. } intros tmid0 [] ->. rewrite app_comm_cons. rewrite app_comm_cons'. rewrite MoveToSymbol_L_correct_midtape; cbn; auto. 2: { intros ? [ (?&<-&?) % in_rev % in_map_iff | [ <- | ] ] % in_app_iff; cbn; auto. } exists (16 + 4 * length (encode_list (@encode_tape sig) tps1)), (22 + 4 * length (encode_list (@encode_tape sig) tps1)). repeat split; try lia. { etransitivity. { apply Nat.add_le_mono_l, Nat.add_le_mono_l, Shift_steps_local. } simpl_list. cbn. rewrite removelast_length. lia. } intros tmid1 [] ->. exists (16 + 4 * length (encode_list (@encode_tape sig) tps1)), (5). repeat split; try lia. { rewrite app_comm_cons. rewrite Shift_L_fun_correct_midtape; auto. rewrite MoveToSymbol_steps_midtape; cbn; auto. simpl_list. rewrite removelast_length. cbn. lia. } intros ? [] ?. exists 1, 3. repeat split. reflexivity. reflexivity. intros ? ? ?. exists 1, 1. repeat split. reflexivity. reflexivity. intros _ _ _. reflexivity. } Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)