169 | "intern (CHAR c) = ACHAR [] c"

   169 | "intern (CHAR c) = ACHAR [] c"

   170 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 

   170 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 

   171                                 (fuse [S]  (intern r2))"

   171                                 (fuse [S]  (intern r2))"

   172 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"

   172 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"

   173 | "intern (STAR r) = ASTAR [S] (intern r)"

   173 | "intern (STAR r) = ASTAR [S] (intern r)"

   174 

   176 

   175 

   177 

   176 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where

   178 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where

   177   "retrieve (AONE bs) Void = bs"

   179   "retrieve (AONE bs) Void = bs"

   178 | "retrieve (ACHAR bs c) (Char d) = bs"

   180 | "retrieve (ACHAR bs c) (Char d) = bs"