proposition: Lemma GoToCurrent_Terminates : projT1 GoToCurrent ↓ GoToCurrent_T.
proof: Proof. eapply TerminatesIn_monotone. { unfold GoToCurrent. now auto with nocore TMdb. } { intros tin k (tps1&tps2&tp&HCons&Hk). unfold GoToCurrent_steps in Hk. exists (GoToCurrent_steps' tp), 2. cbn. repeat split. 2: lia. { destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp. - do 2 ( rewrite MoveToSymbol_steps_equation; cbn in * ). reflexivity. - do 2 ( rewrite MoveToSymbol_steps_equation; cbn in * ). reflexivity. - replace (inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l; RightBlank true])) ++ map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l]))) ++ inr (sigList_X (RightBlank true)) :: (map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])) by (now simpl_list; cbn; rewrite <- !app_assoc). rewrite MoveToSymbol_steps_midtape; cbn; auto. simpl_list. cbn. rewrite Nat.mul_succ_r. cbn. lia. - replace (inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ MarkedSymbol m :: map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls)))) ++ inr (sigList_X (MarkedSymbol m)) :: (map inr (map sigList_X (map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (@encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])). rewrite MoveToSymbol_steps_midtape; cbn; auto. + simpl_list. cbn. lia. + simpl_list. cbn. f_equal. f_equal. f_equal. rewrite !map_app, <- !app_assoc. cbn. f_equal. } { intros ? [] ?. exists 1, 0. repeat split. lia. lia. intros ? ? (->&->). destruct *; 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)