Help$-(*$

#####################################################

### PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY ###

#####################################################

$*)$

Set Default Goal Selector $"!".$

Require Import Coq.Strings.Ascii.

Require Import Coq.Lists.List.

From Turing Require Import Lang.

From Turing Require Import Util.

Import LangNotations.

Import ListNotations.

Import Lang.Examples.

Open Scope lang$\_$scope.

Open Scope char$\_$scope.

$(*---------------------------------------------------------------------------*)$

$(**$

Show that any word that is in L$4$ is either empty or starts with $"$a$".$

$*)$

Theorem ex$1$:

forall w$,$ L$4$ w $->$ w $=[]\backslash /$ exists w$\text{'},$ w $="$a$"$ :: w$\text{'}.$

Proof.

intros w H$.$

destruct H as $[$H$1|$ H$2].$

left. reflexivity.

right. exists $($tl w$).$

reflexivity.

Qed.

$(**$

Show that the following word is accepted by the given language.

$*)$

Theorem ex$2$:

In $["$a$"$; $"$b$"$; $"$b$"$; $"$a$"]("$a$">>"$b$"*>>"$a$").$

Proof.

Admitted.

$(**$

Show that the following word is rejected by the given language.

$*)$

Theorem ex$3$:

~ In $["$b$"$; $"$b$"]("$a$">>"$b$"*>>"$a$").$

Proof.

Admitted.

$(**$

Show that the following language is empty.

$*)$

Theorem ex$4$:

$"0"*>>\{\}==\{\}.$

Proof.

Admitted.

$(**$

Rearrange the following terms. Hint use the distribution and absorption laws.

$*)$

Theorem ex$5$:

$("0"$ U Nil$)>>("1"*)==("0">>"1"*)$ U $("1"*).$

Proof.

Admitted.

$(**$

Show that the following langue only accepts two words.

$*)$

Theorem ex$6$:

$("0">>"1"$ U $"1">>"0")==$ fun w $=>($w $=["0"$; $"1"]\backslash /$ w $=["1"$; $"0"]).$

Proof.

Admitted.

Theorem ex$7$:

$"$b$">>("$a$"$ U $"$b$"$ U Nil$)*>>$ Nil $=="$b$">>("$b$"$ U $"$a$")*.$

Proof.

Admitted.

Theorem ex$8$:

$(("$b$">>("$a$"$ U $\{\}))$ U $($Nil $>>\{\}>>"$c$")*)*==("$b$">>"$a$")*.$

Proof.

Admitted.