676 

   676 

   677 subsection {* EXERCISE 5 *}

   677 subsection {* EXERCISE 5 *}

   678 

   678 

   679 text {* Complete the proof and remove the sorries. *}

   679 text {* Complete the proof and remove the sorries. *}

   680 

   680 

   682   shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"

   682   shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"

   683 proof (induct E1)

   683 proof (induct E1)

   684   case Hole

   684   case Hole

   685   show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by simp

   685   show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by simp

   686 next

   686 next