Recursive Closure Under Reversal

Proof idea: given a decider M for L, first run a finite-state TM0 block routine that rewrites the input tape from w to w.reverse. Then continue with M on that reversed tape. The composed machine halts because both the reversal routine and M halt, and it accepts exactly when M accepts w.reverse, which is the definition of membership in L.reverse.

theorem RecursiveReverse.is_Recursive_reverse {T : Type} [DecidableEq T] [Fintype T] {L : Language T} (hL : is_Recursive L) : is_Recursive L.reverse

Recursive languages over finite alphabets are closed under reversal.

theorem RecursiveReverse.Recursive_closedUnderReverse {T : Type} [DecidableEq T] [Fintype T] : ClosedUnderReverse is_Recursive

Recursive languages over finite alphabets are closed under reversal.