$(**$

The following code implements a function that given a string

it returns a regular expression that only accepts that string.

Fixpoint r$\_$word' l :$=$

match l with

$|$ nil $=>$ r$\_$nil

$|$ x :: l $=>($r$\_$char x$)$ ;; r$\_$word' l

end.

Prove that function $`$r$\_$word'$`$ is correct.

Note that you must copy$/$paste the function to outside of the comment

and in your proof state: exists r$\_$word'.

The proof must proceed by induction.

$*)$

Theorem ex$5$:

forall l$,$ exists $($r$\_$word:list ascii $->$ regex$),$ Accept $($r$\_$word l$)==$ fun w $=>$ w $=$ l$.$

Proof.

Admitted.