proposition: Fact move_tape_spec d t v w : t ~r v -> mv d t ~r w -> (i,move_tape d) // (i,v) -+> (j,w).
proof: Proof. Proof using Hxy. destruct d; simpl move_tape. + apply mv_left_spec. + apply mv_right_spec. Qed.
imports: List Arith Lia Bool Undecidability.Synthetic(ReducibilityFacts) Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.TM(SBTM pctm_defs)