1 %

     2 \begin{isabellebody}%

     3 \setisabellecontext{SizeBound}%

     4 %

     5 \isadelimtheory

     6 \isanewline

     7 %

     8 \endisadelimtheory

     9 %

    10 \isatagtheory

    11 \isacommand{theory}\isamarkupfalse%

    12 \ SizeBound\isanewline

    13 \ \ \isakeyword{imports}\ {\isachardoublequoteopen}Lexer{\isachardoublequoteclose}\ \isanewline

    14 \isakeyword{begin}%

    15 \endisatagtheory

    16 {\isafoldtheory}%

    17 %

    18 \isadelimtheory

    19 %

    20 \endisadelimtheory

    21 %

    22 \isadelimdocument

    23 %

    24 \endisadelimdocument

    25 %

    26 \isatagdocument

    27 %

    28 \isamarkupsection{Bit-Encodings%

    29 }

    30 \isamarkuptrue%

    31 %

    32 \endisatagdocument

    33 {\isafolddocument}%

    34 %

    35 \isadelimdocument

    36 %

    37 \endisadelimdocument

    38 \isacommand{datatype}\isamarkupfalse%

    39 \ bit\ {\isacharequal}{\kern0pt}\ Z\ {\isacharbar}{\kern0pt}\ S\isanewline

    40 \isanewline

    41 \isacommand{fun}\isamarkupfalse%

    42 \ code\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}val\ {\isasymRightarrow}\ bit\ list{\isachardoublequoteclose}\isanewline

    43 \isakeyword{where}\isanewline

    44 \ \ {\isachardoublequoteopen}code\ Void\ {\isacharequal}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    45 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}code\ {\isacharparenleft}{\kern0pt}Char\ c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    46 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}code\ {\isacharparenleft}{\kern0pt}Left\ v{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ Z\ {\isacharhash}{\kern0pt}\ {\isacharparenleft}{\kern0pt}code\ v{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    47 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}code\ {\isacharparenleft}{\kern0pt}Right\ v{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ S\ {\isacharhash}{\kern0pt}\ {\isacharparenleft}{\kern0pt}code\ v{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    48 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}code\ {\isacharparenleft}{\kern0pt}Seq\ v{\isadigit{1}}\ v{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}code\ v{\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharat}{\kern0pt}\ {\isacharparenleft}{\kern0pt}code\ v{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    49 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}code\ {\isacharparenleft}{\kern0pt}Stars\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}S{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    50 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}code\ {\isacharparenleft}{\kern0pt}Stars\ {\isacharparenleft}{\kern0pt}v\ {\isacharhash}{\kern0pt}\ vs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ \ {\isacharparenleft}{\kern0pt}Z\ {\isacharhash}{\kern0pt}\ code\ v{\isacharparenright}{\kern0pt}\ {\isacharat}{\kern0pt}\ code\ {\isacharparenleft}{\kern0pt}Stars\ vs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    51 \isanewline

    52 \isanewline

    53 \isacommand{fun}\isamarkupfalse%

    54 \ \isanewline

    55 \ \ Stars{\isacharunderscore}{\kern0pt}add\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}val\ {\isasymRightarrow}\ val\ {\isasymRightarrow}\ val{\isachardoublequoteclose}\isanewline

    56 \isakeyword{where}\isanewline

    57 \ \ {\isachardoublequoteopen}Stars{\isacharunderscore}{\kern0pt}add\ v\ {\isacharparenleft}{\kern0pt}Stars\ vs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ Stars\ {\isacharparenleft}{\kern0pt}v\ {\isacharhash}{\kern0pt}\ vs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    58 \isanewline

    59 \isacommand{function}\isamarkupfalse%

    60 \isanewline

    61 \ \ decode{\isacharprime}{\kern0pt}\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}bit\ list\ {\isasymRightarrow}\ rexp\ {\isasymRightarrow}\ {\isacharparenleft}{\kern0pt}val\ {\isacharasterisk}{\kern0pt}\ bit\ list{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    62 \isakeyword{where}\isanewline

    63 \ \ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ ds\ ZERO\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Void{\isacharcomma}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    64 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ ds\ ONE\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Void{\isacharcomma}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    65 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ ds\ {\isacharparenleft}{\kern0pt}CH\ d{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Char\ d{\isacharcomma}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    66 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}ALT\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Void{\isacharcomma}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    67 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Z\ {\isacharhash}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}ALT\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}let\ {\isacharparenleft}{\kern0pt}v{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ ds\ r{\isadigit{1}}\ in\ {\isacharparenleft}{\kern0pt}Left\ v{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    68 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}S\ {\isacharhash}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}ALT\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}let\ {\isacharparenleft}{\kern0pt}v{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ ds\ r{\isadigit{2}}\ in\ {\isacharparenleft}{\kern0pt}Right\ v{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    69 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ ds\ {\isacharparenleft}{\kern0pt}SEQ\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}let\ {\isacharparenleft}{\kern0pt}v{\isadigit{1}}{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ ds\ r{\isadigit{1}}\ in\isanewline

    70 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ {\isacharparenleft}{\kern0pt}v{\isadigit{2}}{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ ds{\isacharprime}{\kern0pt}\ r{\isadigit{2}}\ in\ {\isacharparenleft}{\kern0pt}Seq\ v{\isadigit{1}}\ v{\isadigit{2}}{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    71 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}STAR\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Void{\isacharcomma}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    72 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}S\ {\isacharhash}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}STAR\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Stars\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharcomma}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    73 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Z\ {\isacharhash}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}STAR\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}let\ {\isacharparenleft}{\kern0pt}v{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ ds\ r\ in\isanewline

    74 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ {\isacharparenleft}{\kern0pt}vs{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ ds{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}STAR\ r{\isacharparenright}{\kern0pt}\ \isanewline

    75 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ {\isacharparenleft}{\kern0pt}Stars{\isacharunderscore}{\kern0pt}add\ v\ vs{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    76 %

    77 \isadelimproof

    78 %

    79 \endisadelimproof

    80 %

    81 \isatagproof

    82 \isacommand{by}\isamarkupfalse%

    83 \ pat{\isacharunderscore}{\kern0pt}completeness\ auto%

    84 \endisatagproof

    85 {\isafoldproof}%

    86 %

    87 \isadelimproof

    88 \isanewline

    89 %

    90 \endisadelimproof

    91 \isanewline

    92 \isacommand{lemma}\isamarkupfalse%

    93 \ decode{\isacharprime}{\kern0pt}{\isacharunderscore}{\kern0pt}smaller{\isacharcolon}{\kern0pt}\isanewline

    94 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}{\isacharunderscore}{\kern0pt}dom\ {\isacharparenleft}{\kern0pt}ds{\isacharcomma}{\kern0pt}\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

    95 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}length\ {\isacharparenleft}{\kern0pt}snd\ {\isacharparenleft}{\kern0pt}decode{\isacharprime}{\kern0pt}\ ds\ r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isasymle}\ length\ ds{\isachardoublequoteclose}\isanewline

    96 %

    97 \isadelimproof

    98 %

    99 \endisadelimproof

   100 %

   101 \isatagproof

   102 \isacommand{using}\isamarkupfalse%

   103 \ assms\isanewline

   104 \isacommand{apply}\isamarkupfalse%

   105 {\isacharparenleft}{\kern0pt}induct\ ds\ r{\isacharparenright}{\kern0pt}\isanewline

   106 \isacommand{apply}\isamarkupfalse%

   107 {\isacharparenleft}{\kern0pt}auto\ simp\ add{\isacharcolon}{\kern0pt}\ decode{\isacharprime}{\kern0pt}{\isachardot}{\kern0pt}psimps\ split{\isacharcolon}{\kern0pt}\ prod{\isachardot}{\kern0pt}split{\isacharparenright}{\kern0pt}\isanewline

   108 \isacommand{using}\isamarkupfalse%

   109 \ dual{\isacharunderscore}{\kern0pt}order{\isachardot}{\kern0pt}trans\ \isacommand{apply}\isamarkupfalse%

   110 \ blast\isanewline

   111 \isacommand{by}\isamarkupfalse%

   112 \ {\isacharparenleft}{\kern0pt}meson\ dual{\isacharunderscore}{\kern0pt}order{\isachardot}{\kern0pt}trans\ le{\isacharunderscore}{\kern0pt}SucI{\isacharparenright}{\kern0pt}%

   113 \endisatagproof

   114 {\isafoldproof}%

   115 %

   116 \isadelimproof

   117 \isanewline

   118 %

   119 \endisadelimproof

   120 \isanewline

   121 \isacommand{termination}\isamarkupfalse%

   122 \ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}{\isachardoublequoteclose}\ \ \isanewline

   123 %

   124 \isadelimproof

   125 %

   126 \endisadelimproof

   127 %

   128 \isatagproof

   129 \isacommand{apply}\isamarkupfalse%

   130 {\isacharparenleft}{\kern0pt}relation\ {\isachardoublequoteopen}inv{\isacharunderscore}{\kern0pt}image\ {\isacharparenleft}{\kern0pt}measure{\isacharparenleft}{\kern0pt}{\isacharpercent}{\kern0pt}cs{\isachardot}{\kern0pt}\ size\ cs{\isacharparenright}{\kern0pt}\ {\isacharless}{\kern0pt}{\isacharasterisk}{\kern0pt}lex{\isacharasterisk}{\kern0pt}{\isachargreater}{\kern0pt}\ measure{\isacharparenleft}{\kern0pt}{\isacharpercent}{\kern0pt}s{\isachardot}{\kern0pt}\ size\ s{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}{\isacharpercent}{\kern0pt}{\isacharparenleft}{\kern0pt}ds{\isacharcomma}{\kern0pt}r{\isacharparenright}{\kern0pt}{\isachardot}{\kern0pt}\ {\isacharparenleft}{\kern0pt}r{\isacharcomma}{\kern0pt}ds{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\ \isanewline

   131 \isacommand{apply}\isamarkupfalse%

   132 {\isacharparenleft}{\kern0pt}auto\ dest{\isacharbang}{\kern0pt}{\isacharcolon}{\kern0pt}\ decode{\isacharprime}{\kern0pt}{\isacharunderscore}{\kern0pt}smaller{\isacharparenright}{\kern0pt}\isanewline

   133 \isacommand{by}\isamarkupfalse%

   134 \ {\isacharparenleft}{\kern0pt}metis\ less{\isacharunderscore}{\kern0pt}Suc{\isacharunderscore}{\kern0pt}eq{\isacharunderscore}{\kern0pt}le\ snd{\isacharunderscore}{\kern0pt}conv{\isacharparenright}{\kern0pt}%

   135 \endisatagproof

   136 {\isafoldproof}%

   137 %

   138 \isadelimproof

   139 \isanewline

   140 %

   141 \endisadelimproof

   142 \isanewline

   143 \isacommand{definition}\isamarkupfalse%

   144 \isanewline

   145 \ \ decode\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}bit\ list\ {\isasymRightarrow}\ rexp\ {\isasymRightarrow}\ val\ option{\isachardoublequoteclose}\isanewline

   146 \isakeyword{where}\isanewline

   147 \ \ {\isachardoublequoteopen}decode\ ds\ r\ {\isasymequiv}\ {\isacharparenleft}{\kern0pt}let\ {\isacharparenleft}{\kern0pt}v{\isacharcomma}{\kern0pt}\ ds{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ ds\ r\ \isanewline

   148 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ {\isacharparenleft}{\kern0pt}if\ ds{\isacharprime}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ then\ Some\ v\ else\ None{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   149 \isanewline

   150 \isacommand{lemma}\isamarkupfalse%

   151 \ decode{\isacharprime}{\kern0pt}{\isacharunderscore}{\kern0pt}code{\isacharunderscore}{\kern0pt}Stars{\isacharcolon}{\kern0pt}\isanewline

   152 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}v{\isasymin}set\ vs{\isachardot}{\kern0pt}\ {\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ r\ {\isasymand}\ {\isacharparenleft}{\kern0pt}{\isasymforall}x{\isachardot}{\kern0pt}\ decode{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}code\ v\ {\isacharat}{\kern0pt}\ x{\isacharparenright}{\kern0pt}\ r\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}v{\isacharcomma}{\kern0pt}\ x{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isasymand}\ flat\ v\ {\isasymnoteq}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\ \isanewline

   153 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}code\ {\isacharparenleft}{\kern0pt}Stars\ vs{\isacharparenright}{\kern0pt}\ {\isacharat}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}STAR\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Stars\ vs{\isacharcomma}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   154 %

   155 \isadelimproof

   156 \ \ %

   157 \endisadelimproof

   158 %

   159 \isatagproof

   160 \isacommand{using}\isamarkupfalse%

   161 \ assms\isanewline

   162 \ \ \isacommand{apply}\isamarkupfalse%

   163 {\isacharparenleft}{\kern0pt}induct\ vs{\isacharparenright}{\kern0pt}\isanewline

   164 \ \ \isacommand{apply}\isamarkupfalse%

   165 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   166 \ \ \isacommand{done}\isamarkupfalse%

   167 %

   168 \endisatagproof

   169 {\isafoldproof}%

   170 %

   171 \isadelimproof

   172 \isanewline

   173 %

   174 \endisadelimproof

   175 \isanewline

   176 \isacommand{lemma}\isamarkupfalse%

   177 \ decode{\isacharprime}{\kern0pt}{\isacharunderscore}{\kern0pt}code{\isacharcolon}{\kern0pt}\isanewline

   178 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

   179 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}decode{\isacharprime}{\kern0pt}\ {\isacharparenleft}{\kern0pt}{\isacharparenleft}{\kern0pt}code\ v{\isacharparenright}{\kern0pt}\ {\isacharat}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}\ r\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}v{\isacharcomma}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   180 %

   181 \isadelimproof

   182 %

   183 \endisadelimproof

   184 %

   185 \isatagproof

   186 \isacommand{using}\isamarkupfalse%

   187 \ assms\isanewline

   188 \ \ \isacommand{apply}\isamarkupfalse%

   189 {\isacharparenleft}{\kern0pt}induct\ v\ r\ arbitrary{\isacharcolon}{\kern0pt}\ ds{\isacharparenright}{\kern0pt}\ \isanewline

   190 \ \ \isacommand{apply}\isamarkupfalse%

   191 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   192 \ \ \isacommand{using}\isamarkupfalse%

   193 \ decode{\isacharprime}{\kern0pt}{\isacharunderscore}{\kern0pt}code{\isacharunderscore}{\kern0pt}Stars\ \isacommand{by}\isamarkupfalse%

   194 \ blast%

   195 \endisatagproof

   196 {\isafoldproof}%

   197 %

   198 \isadelimproof

   199 \isanewline

   200 %

   201 \endisadelimproof

   202 \isanewline

   203 \isacommand{lemma}\isamarkupfalse%

   204 \ decode{\isacharunderscore}{\kern0pt}code{\isacharcolon}{\kern0pt}\isanewline

   205 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

   206 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}decode\ {\isacharparenleft}{\kern0pt}code\ v{\isacharparenright}{\kern0pt}\ r\ {\isacharequal}{\kern0pt}\ Some\ v{\isachardoublequoteclose}\isanewline

   207 %

   208 \isadelimproof

   209 \ \ %

   210 \endisadelimproof

   211 %

   212 \isatagproof

   213 \isacommand{using}\isamarkupfalse%

   214 \ assms\ \isacommand{unfolding}\isamarkupfalse%

   215 \ decode{\isacharunderscore}{\kern0pt}def\isanewline

   216 \ \ \isacommand{by}\isamarkupfalse%

   217 \ {\isacharparenleft}{\kern0pt}smt\ append{\isacharunderscore}{\kern0pt}Nil{\isadigit{2}}\ decode{\isacharprime}{\kern0pt}{\isacharunderscore}{\kern0pt}code\ old{\isachardot}{\kern0pt}prod{\isachardot}{\kern0pt}case{\isacharparenright}{\kern0pt}%

   218 \endisatagproof

   219 {\isafoldproof}%

   220 %

   221 \isadelimproof

   222 %

   223 \endisadelimproof

   224 %

   225 \isadelimdocument

   226 %

   227 \endisadelimdocument

   228 %

   229 \isatagdocument

   230 %

   231 \isamarkupsection{Annotated Regular Expressions%

   232 }

   233 \isamarkuptrue%

   234 %

   235 \endisatagdocument

   236 {\isafolddocument}%

   237 %

   238 \isadelimdocument

   239 %

   240 \endisadelimdocument

   241 \isacommand{datatype}\isamarkupfalse%

   242 \ arexp\ {\isacharequal}{\kern0pt}\ \isanewline

   243 \ \ AZERO\isanewline

   244 {\isacharbar}{\kern0pt}\ AONE\ {\isachardoublequoteopen}bit\ list{\isachardoublequoteclose}\isanewline

   245 {\isacharbar}{\kern0pt}\ ACHAR\ {\isachardoublequoteopen}bit\ list{\isachardoublequoteclose}\ char\isanewline

   246 {\isacharbar}{\kern0pt}\ ASEQ\ {\isachardoublequoteopen}bit\ list{\isachardoublequoteclose}\ arexp\ arexp\isanewline

   247 {\isacharbar}{\kern0pt}\ AALTs\ {\isachardoublequoteopen}bit\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}arexp\ list{\isachardoublequoteclose}\isanewline

   248 {\isacharbar}{\kern0pt}\ ASTAR\ {\isachardoublequoteopen}bit\ list{\isachardoublequoteclose}\ arexp\isanewline

   249 \isanewline

   250 \isacommand{abbreviation}\isamarkupfalse%

   251 \isanewline

   252 \ \ {\isachardoublequoteopen}AALT\ bs\ r{\isadigit{1}}\ r{\isadigit{2}}\ {\isasymequiv}\ AALTs\ bs\ {\isacharbrackleft}{\kern0pt}r{\isadigit{1}}{\isacharcomma}{\kern0pt}\ r{\isadigit{2}}{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   253 \isanewline

   254 \isacommand{fun}\isamarkupfalse%

   255 \ asize\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

   256 \ \ {\isachardoublequoteopen}asize\ AZERO\ {\isacharequal}{\kern0pt}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline

   257 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}asize\ {\isacharparenleft}{\kern0pt}AONE\ cs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isanewline

   258 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}asize\ {\isacharparenleft}{\kern0pt}ACHAR\ cs\ c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline

   259 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}asize\ {\isacharparenleft}{\kern0pt}AALTs\ cs\ rs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ Suc\ {\isacharparenleft}{\kern0pt}sum{\isacharunderscore}{\kern0pt}list\ {\isacharparenleft}{\kern0pt}map\ asize\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   260 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}asize\ {\isacharparenleft}{\kern0pt}ASEQ\ cs\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ Suc\ {\isacharparenleft}{\kern0pt}asize\ r{\isadigit{1}}\ {\isacharplus}{\kern0pt}\ asize\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   261 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}asize\ {\isacharparenleft}{\kern0pt}ASTAR\ cs\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ Suc\ {\isacharparenleft}{\kern0pt}asize\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   262 \isanewline

   263 \isacommand{fun}\isamarkupfalse%

   264 \ \isanewline

   265 \ \ erase\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ rexp{\isachardoublequoteclose}\isanewline

   266 \isakeyword{where}\isanewline

   267 \ \ {\isachardoublequoteopen}erase\ AZERO\ {\isacharequal}{\kern0pt}\ ZERO{\isachardoublequoteclose}\isanewline

   268 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}AONE\ {\isacharunderscore}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ONE{\isachardoublequoteclose}\isanewline

   269 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}ACHAR\ {\isacharunderscore}{\kern0pt}\ c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ CH\ c{\isachardoublequoteclose}\isanewline

   270 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}AALTs\ {\isacharunderscore}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ZERO{\isachardoublequoteclose}\isanewline

   271 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}AALTs\ {\isacharunderscore}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   272 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}r{\isacharhash}{\kern0pt}rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ALT\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}erase\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   273 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}ASEQ\ {\isacharunderscore}{\kern0pt}\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ SEQ\ {\isacharparenleft}{\kern0pt}erase\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}erase\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   274 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}ASTAR\ {\isacharunderscore}{\kern0pt}\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ STAR\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   275 \isanewline

   276 \isanewline

   277 \isanewline

   278 \isanewline

   279 \isacommand{fun}\isamarkupfalse%

   280 \ nonalt\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

   281 \ \ \isakeyword{where}\isanewline

   282 \ \ {\isachardoublequoteopen}nonalt\ {\isacharparenleft}{\kern0pt}AALTs\ bs{\isadigit{2}}\ rs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   283 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}nonalt\ r\ {\isacharequal}{\kern0pt}\ True{\isachardoublequoteclose}\isanewline

   284 \isanewline

   285 \isanewline

   286 \isacommand{fun}\isamarkupfalse%

   287 \ good\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

   288 \ \ {\isachardoublequoteopen}good\ AZERO\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   289 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}AONE\ cs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ True{\isachardoublequoteclose}\ \isanewline

   290 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}ACHAR\ cs\ c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ True{\isachardoublequoteclose}\isanewline

   291 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}AALTs\ cs\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   292 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}AALTs\ cs\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   293 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}AALTs\ cs\ {\isacharparenleft}{\kern0pt}r{\isadigit{1}}{\isacharhash}{\kern0pt}r{\isadigit{2}}{\isacharhash}{\kern0pt}rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}{\isasymforall}r{\isacharprime}{\kern0pt}\ {\isasymin}\ set\ {\isacharparenleft}{\kern0pt}r{\isadigit{1}}{\isacharhash}{\kern0pt}r{\isadigit{2}}{\isacharhash}{\kern0pt}rs{\isacharparenright}{\kern0pt}{\isachardot}{\kern0pt}\ good\ r{\isacharprime}{\kern0pt}\ {\isasymand}\ nonalt\ r{\isacharprime}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   294 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}ASEQ\ {\isacharunderscore}{\kern0pt}\ AZERO\ {\isacharunderscore}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   295 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}ASEQ\ {\isacharunderscore}{\kern0pt}\ {\isacharparenleft}{\kern0pt}AONE\ {\isacharunderscore}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharunderscore}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   296 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}ASEQ\ {\isacharunderscore}{\kern0pt}\ {\isacharunderscore}{\kern0pt}\ AZERO{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   297 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}ASEQ\ cs\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}good\ r{\isadigit{1}}\ {\isasymand}\ good\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   298 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}good\ {\isacharparenleft}{\kern0pt}ASTAR\ cs\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ True{\isachardoublequoteclose}\isanewline

   299 \isanewline

   300 \isanewline

   301 \isanewline

   302 \isanewline

   303 \isacommand{fun}\isamarkupfalse%

   304 \ fuse\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}bit\ list\ {\isasymRightarrow}\ arexp\ {\isasymRightarrow}\ arexp{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

   305 \ \ {\isachardoublequoteopen}fuse\ bs\ AZERO\ {\isacharequal}{\kern0pt}\ AZERO{\isachardoublequoteclose}\isanewline

   306 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}fuse\ bs\ {\isacharparenleft}{\kern0pt}AONE\ cs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ AONE\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ cs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\ \isanewline

   307 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}fuse\ bs\ {\isacharparenleft}{\kern0pt}ACHAR\ cs\ c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ACHAR\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ cs{\isacharparenright}{\kern0pt}\ c{\isachardoublequoteclose}\isanewline

   308 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}fuse\ bs\ {\isacharparenleft}{\kern0pt}AALTs\ cs\ rs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ AALTs\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ cs{\isacharparenright}{\kern0pt}\ rs{\isachardoublequoteclose}\isanewline

   309 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}fuse\ bs\ {\isacharparenleft}{\kern0pt}ASEQ\ cs\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ASEQ\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ cs{\isacharparenright}{\kern0pt}\ r{\isadigit{1}}\ r{\isadigit{2}}{\isachardoublequoteclose}\isanewline

   310 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}fuse\ bs\ {\isacharparenleft}{\kern0pt}ASTAR\ cs\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ASTAR\ {\isacharparenleft}{\kern0pt}bs\ {\isacharat}{\kern0pt}\ cs{\isacharparenright}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

   311 \isanewline

   312 \isacommand{lemma}\isamarkupfalse%

   313 \ fuse{\isacharunderscore}{\kern0pt}append{\isacharcolon}{\kern0pt}\isanewline

   314 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}fuse\ {\isacharparenleft}{\kern0pt}bs{\isadigit{1}}\ {\isacharat}{\kern0pt}\ bs{\isadigit{2}}{\isacharparenright}{\kern0pt}\ r\ {\isacharequal}{\kern0pt}\ fuse\ bs{\isadigit{1}}\ {\isacharparenleft}{\kern0pt}fuse\ bs{\isadigit{2}}\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   315 %

   316 \isadelimproof

   317 \ \ %

   318 \endisadelimproof

   319 %

   320 \isatagproof

   321 \isacommand{apply}\isamarkupfalse%

   322 {\isacharparenleft}{\kern0pt}induct\ r{\isacharparenright}{\kern0pt}\isanewline

   323 \ \ \isacommand{apply}\isamarkupfalse%

   324 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   325 \ \ \isacommand{done}\isamarkupfalse%

   326 %

   327 \endisatagproof

   328 {\isafoldproof}%

   329 %

   330 \isadelimproof

   331 \isanewline

   332 %

   333 \endisadelimproof

   334 \isanewline

   335 \isanewline

   336 \isacommand{fun}\isamarkupfalse%

   337 \ intern\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}rexp\ {\isasymRightarrow}\ arexp{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

   338 \ \ {\isachardoublequoteopen}intern\ ZERO\ {\isacharequal}{\kern0pt}\ AZERO{\isachardoublequoteclose}\isanewline

   339 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}intern\ ONE\ {\isacharequal}{\kern0pt}\ AONE\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   340 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}intern\ {\isacharparenleft}{\kern0pt}CH\ c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ACHAR\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ c{\isachardoublequoteclose}\isanewline

   341 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}intern\ {\isacharparenleft}{\kern0pt}ALT\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ AALT\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}fuse\ {\isacharbrackleft}{\kern0pt}Z{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}intern\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ \isanewline

   342 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\kern0pt}fuse\ {\isacharbrackleft}{\kern0pt}S{\isacharbrackright}{\kern0pt}\ \ {\isacharparenleft}{\kern0pt}intern\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   343 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}intern\ {\isacharparenleft}{\kern0pt}SEQ\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ASEQ\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}intern\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}intern\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   344 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}intern\ {\isacharparenleft}{\kern0pt}STAR\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ASTAR\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   345 \isanewline

   346 \isanewline

   347 \isacommand{fun}\isamarkupfalse%

   348 \ retrieve\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ val\ {\isasymRightarrow}\ bit\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

   349 \ \ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}AONE\ bs{\isacharparenright}{\kern0pt}\ Void\ {\isacharequal}{\kern0pt}\ bs{\isachardoublequoteclose}\isanewline

   350 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}ACHAR\ bs\ c{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Char\ d{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs{\isachardoublequoteclose}\isanewline

   351 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ v\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ retrieve\ r\ v{\isachardoublequoteclose}\ \isanewline

   352 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}r{\isacharhash}{\kern0pt}rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Left\ v{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ retrieve\ r\ v{\isachardoublequoteclose}\isanewline

   353 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}r{\isacharhash}{\kern0pt}rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Right\ v{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ retrieve\ {\isacharparenleft}{\kern0pt}AALTs\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}\ v{\isachardoublequoteclose}\isanewline

   354 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}ASEQ\ bs\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Seq\ v{\isadigit{1}}\ v{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ retrieve\ r{\isadigit{1}}\ v{\isadigit{1}}\ {\isacharat}{\kern0pt}\ retrieve\ r{\isadigit{2}}\ v{\isadigit{2}}{\isachardoublequoteclose}\isanewline

   355 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}ASTAR\ bs\ r{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Stars\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}S{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   356 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}ASTAR\ bs\ r{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Stars\ {\isacharparenleft}{\kern0pt}v{\isacharhash}{\kern0pt}vs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ \isanewline

   357 \ \ \ \ \ bs\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}Z{\isacharbrackright}{\kern0pt}\ {\isacharat}{\kern0pt}\ retrieve\ r\ v\ {\isacharat}{\kern0pt}\ retrieve\ {\isacharparenleft}{\kern0pt}ASTAR\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ r{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Stars\ vs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   358 \isanewline

   359 \isanewline

   360 \isanewline

   361 \isacommand{fun}\isamarkupfalse%

   362 \isanewline

   363 \ bnullable\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline

   364 \isakeyword{where}\isanewline

   365 \ \ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}AZERO{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   366 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}AONE\ bs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ True{\isachardoublequoteclose}\isanewline

   367 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}ACHAR\ bs\ c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ False{\isachardoublequoteclose}\isanewline

   368 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}{\isasymexists}r\ {\isasymin}\ set\ rs{\isachardot}{\kern0pt}\ bnullable\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   369 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}ASEQ\ bs\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bnullable\ r{\isadigit{1}}\ {\isasymand}\ bnullable\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   370 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}ASTAR\ bs\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ True{\isachardoublequoteclose}\isanewline

   371 \isanewline

   372 \isacommand{fun}\isamarkupfalse%

   373 \ \isanewline

   374 \ \ bmkeps\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ bit\ list{\isachardoublequoteclose}\isanewline

   375 \isakeyword{where}\isanewline

   376 \ \ {\isachardoublequoteopen}bmkeps{\isacharparenleft}{\kern0pt}AONE\ bs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs{\isachardoublequoteclose}\isanewline

   377 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bmkeps{\isacharparenleft}{\kern0pt}ASEQ\ bs\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bmkeps\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharat}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bmkeps\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   378 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bmkeps{\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharbrackleft}{\kern0pt}r{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bmkeps\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   379 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bmkeps{\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}r{\isacharhash}{\kern0pt}rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}if\ bnullable{\isacharparenleft}{\kern0pt}r{\isacharparenright}{\kern0pt}\ then\ bs\ {\isacharat}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bmkeps\ r{\isacharparenright}{\kern0pt}\ else\ {\isacharparenleft}{\kern0pt}bmkeps\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   380 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bmkeps{\isacharparenleft}{\kern0pt}ASTAR\ bs\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}S{\isacharbrackright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   381 \isanewline

   382 \isanewline

   383 \isacommand{fun}\isamarkupfalse%

   384 \isanewline

   385 \ bder\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}char\ {\isasymRightarrow}\ arexp\ {\isasymRightarrow}\ arexp{\isachardoublequoteclose}\isanewline

   386 \isakeyword{where}\isanewline

   387 \ \ {\isachardoublequoteopen}bder\ c\ {\isacharparenleft}{\kern0pt}AZERO{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ AZERO{\isachardoublequoteclose}\isanewline

   388 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bder\ c\ {\isacharparenleft}{\kern0pt}AONE\ bs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ AZERO{\isachardoublequoteclose}\isanewline

   389 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bder\ c\ {\isacharparenleft}{\kern0pt}ACHAR\ bs\ d{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}if\ c\ {\isacharequal}{\kern0pt}\ d\ then\ AONE\ bs\ else\ AZERO{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   390 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bder\ c\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ AALTs\ bs\ {\isacharparenleft}{\kern0pt}map\ {\isacharparenleft}{\kern0pt}bder\ c{\isacharparenright}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   391 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bder\ c\ {\isacharparenleft}{\kern0pt}ASEQ\ bs\ r{\isadigit{1}}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ \isanewline

   392 \ \ \ \ \ {\isacharparenleft}{\kern0pt}if\ bnullable\ r{\isadigit{1}}\isanewline

   393 \ \ \ \ \ \ then\ AALT\ bs\ {\isacharparenleft}{\kern0pt}ASEQ\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bder\ c\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}fuse\ {\isacharparenleft}{\kern0pt}bmkeps\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bder\ c\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\isanewline

   394 \ \ \ \ \ \ else\ ASEQ\ bs\ {\isacharparenleft}{\kern0pt}bder\ c\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   395 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bder\ c\ {\isacharparenleft}{\kern0pt}ASTAR\ bs\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ASEQ\ bs\ {\isacharparenleft}{\kern0pt}fuse\ {\isacharbrackleft}{\kern0pt}Z{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bder\ c\ r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}ASTAR\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   396 \isanewline

   397 \isanewline

   398 \isacommand{fun}\isamarkupfalse%

   399 \ \isanewline

   400 \ \ bders\ {\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}arexp\ {\isasymRightarrow}\ string\ {\isasymRightarrow}\ arexp{\isachardoublequoteclose}\isanewline

   401 \isakeyword{where}\isanewline

   402 \ \ {\isachardoublequoteopen}bders\ r\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

   403 {\isacharbar}{\kern0pt}\ {\isachardoublequoteopen}bders\ r\ {\isacharparenleft}{\kern0pt}c{\isacharhash}{\kern0pt}s{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bders\ {\isacharparenleft}{\kern0pt}bder\ c\ r{\isacharparenright}{\kern0pt}\ s{\isachardoublequoteclose}\isanewline

   404 \isanewline

   405 \isacommand{lemma}\isamarkupfalse%

   406 \ bders{\isacharunderscore}{\kern0pt}append{\isacharcolon}{\kern0pt}\isanewline

   407 \ \ {\isachardoublequoteopen}bders\ r\ {\isacharparenleft}{\kern0pt}s{\isadigit{1}}\ {\isacharat}{\kern0pt}\ s{\isadigit{2}}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bders\ {\isacharparenleft}{\kern0pt}bders\ r\ s{\isadigit{1}}{\isacharparenright}{\kern0pt}\ s{\isadigit{2}}{\isachardoublequoteclose}\isanewline

   408 %

   409 \isadelimproof

   410 \ \ %

   411 \endisadelimproof

   412 %

   413 \isatagproof

   414 \isacommand{apply}\isamarkupfalse%

   415 {\isacharparenleft}{\kern0pt}induct\ s{\isadigit{1}}\ arbitrary{\isacharcolon}{\kern0pt}\ r\ s{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

   416 \ \ \isacommand{apply}\isamarkupfalse%

   417 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all{\isacharparenright}{\kern0pt}\isanewline

   418 \ \ \isacommand{done}\isamarkupfalse%

   419 %

   420 \endisatagproof

   421 {\isafoldproof}%

   422 %

   423 \isadelimproof

   424 \isanewline

   425 %

   426 \endisadelimproof

   427 \isanewline

   428 \isacommand{lemma}\isamarkupfalse%

   429 \ bnullable{\isacharunderscore}{\kern0pt}correctness{\isacharcolon}{\kern0pt}\isanewline

   430 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}nullable\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bnullable\ r{\isachardoublequoteclose}\isanewline

   431 %

   432 \isadelimproof

   433 \ \ %

   434 \endisadelimproof

   435 %

   436 \isatagproof

   437 \isacommand{apply}\isamarkupfalse%

   438 {\isacharparenleft}{\kern0pt}induct\ r\ rule{\isacharcolon}{\kern0pt}\ erase{\isachardot}{\kern0pt}induct{\isacharparenright}{\kern0pt}\isanewline

   439 \ \ \isacommand{apply}\isamarkupfalse%

   440 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all{\isacharparenright}{\kern0pt}\isanewline

   441 \ \ \isacommand{done}\isamarkupfalse%

   442 %

   443 \endisatagproof

   444 {\isafoldproof}%

   445 %

   446 \isadelimproof

   447 \isanewline

   448 %

   449 \endisadelimproof

   450 \isanewline

   451 \isacommand{lemma}\isamarkupfalse%

   452 \ erase{\isacharunderscore}{\kern0pt}fuse{\isacharcolon}{\kern0pt}\isanewline

   453 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}fuse\ bs\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ erase\ r{\isachardoublequoteclose}\isanewline

   454 %

   455 \isadelimproof

   456 \ \ %

   457 \endisadelimproof

   458 %

   459 \isatagproof

   460 \isacommand{apply}\isamarkupfalse%

   461 {\isacharparenleft}{\kern0pt}induct\ r\ rule{\isacharcolon}{\kern0pt}\ erase{\isachardot}{\kern0pt}induct{\isacharparenright}{\kern0pt}\isanewline

   462 \ \ \isacommand{apply}\isamarkupfalse%

   463 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all{\isacharparenright}{\kern0pt}\isanewline

   464 \ \ \isacommand{done}\isamarkupfalse%

   465 %

   466 \endisatagproof

   467 {\isafoldproof}%

   468 %

   469 \isadelimproof

   470 \isanewline

   471 %

   472 \endisadelimproof

   473 \isanewline

   474 \isacommand{thm}\isamarkupfalse%

   475 \ Posix{\isachardot}{\kern0pt}induct\isanewline

   476 \isanewline

   477 \isacommand{lemma}\isamarkupfalse%

   478 \ erase{\isacharunderscore}{\kern0pt}intern\ {\isacharbrackleft}{\kern0pt}simp{\isacharbrackright}{\kern0pt}{\isacharcolon}{\kern0pt}\isanewline

   479 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

   480 %

   481 \isadelimproof

   482 \ \ %

   483 \endisadelimproof

   484 %

   485 \isatagproof

   486 \isacommand{apply}\isamarkupfalse%

   487 {\isacharparenleft}{\kern0pt}induct\ r{\isacharparenright}{\kern0pt}\isanewline

   488 \ \ \isacommand{apply}\isamarkupfalse%

   489 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all\ add{\isacharcolon}{\kern0pt}\ erase{\isacharunderscore}{\kern0pt}fuse{\isacharparenright}{\kern0pt}\isanewline

   490 \ \ \isacommand{done}\isamarkupfalse%

   491 %

   492 \endisatagproof

   493 {\isafoldproof}%

   494 %

   495 \isadelimproof

   496 \isanewline

   497 %

   498 \endisadelimproof

   499 \isanewline

   500 \isacommand{lemma}\isamarkupfalse%

   501 \ erase{\isacharunderscore}{\kern0pt}bder\ {\isacharbrackleft}{\kern0pt}simp{\isacharbrackright}{\kern0pt}{\isacharcolon}{\kern0pt}\isanewline

   502 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}bder\ a\ r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ der\ a\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   503 %

   504 \isadelimproof

   505 \ \ %

   506 \endisadelimproof

   507 %

   508 \isatagproof

   509 \isacommand{apply}\isamarkupfalse%

   510 {\isacharparenleft}{\kern0pt}induct\ r\ rule{\isacharcolon}{\kern0pt}\ erase{\isachardot}{\kern0pt}induct{\isacharparenright}{\kern0pt}\isanewline

   511 \ \ \isacommand{apply}\isamarkupfalse%

   512 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all\ add{\isacharcolon}{\kern0pt}\ erase{\isacharunderscore}{\kern0pt}fuse\ bnullable{\isacharunderscore}{\kern0pt}correctness{\isacharparenright}{\kern0pt}\isanewline

   513 \ \ \isacommand{done}\isamarkupfalse%

   514 %

   515 \endisatagproof

   516 {\isafoldproof}%

   517 %

   518 \isadelimproof

   519 \isanewline

   520 %

   521 \endisadelimproof

   522 \isanewline

   523 \isacommand{lemma}\isamarkupfalse%

   524 \ erase{\isacharunderscore}{\kern0pt}bders\ {\isacharbrackleft}{\kern0pt}simp{\isacharbrackright}{\kern0pt}{\isacharcolon}{\kern0pt}\isanewline

   525 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}erase\ {\isacharparenleft}{\kern0pt}bders\ r\ s{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ ders\ s\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   526 %

   527 \isadelimproof

   528 \ \ %

   529 \endisadelimproof

   530 %

   531 \isatagproof

   532 \isacommand{apply}\isamarkupfalse%

   533 {\isacharparenleft}{\kern0pt}induct\ s\ arbitrary{\isacharcolon}{\kern0pt}\ r\ {\isacharparenright}{\kern0pt}\isanewline

   534 \ \ \isacommand{apply}\isamarkupfalse%

   535 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all{\isacharparenright}{\kern0pt}\isanewline

   536 \ \ \isacommand{done}\isamarkupfalse%

   537 %

   538 \endisatagproof

   539 {\isafoldproof}%

   540 %

   541 \isadelimproof

   542 \isanewline

   543 %

   544 \endisadelimproof

   545 \isanewline

   546 \isacommand{lemma}\isamarkupfalse%

   547 \ retrieve{\isacharunderscore}{\kern0pt}encode{\isacharunderscore}{\kern0pt}STARS{\isacharcolon}{\kern0pt}\isanewline

   548 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}v{\isasymin}set\ vs{\isachardot}{\kern0pt}\ {\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ r\ {\isasymand}\ code\ v\ {\isacharequal}{\kern0pt}\ retrieve\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}\ v{\isachardoublequoteclose}\isanewline

   549 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}code\ {\isacharparenleft}{\kern0pt}Stars\ vs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ retrieve\ {\isacharparenleft}{\kern0pt}ASTAR\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Stars\ vs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   550 %

   551 \isadelimproof

   552 \ \ %

   553 \endisadelimproof

   554 %

   555 \isatagproof

   556 \isacommand{using}\isamarkupfalse%

   557 \ assms\isanewline

   558 \ \ \isacommand{apply}\isamarkupfalse%

   559 {\isacharparenleft}{\kern0pt}induct\ vs{\isacharparenright}{\kern0pt}\isanewline

   560 \ \ \isacommand{apply}\isamarkupfalse%

   561 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all{\isacharparenright}{\kern0pt}\isanewline

   562 \ \ \isacommand{done}\isamarkupfalse%

   563 %

   564 \endisatagproof

   565 {\isafoldproof}%

   566 %

   567 \isadelimproof

   568 \isanewline

   569 %

   570 \endisadelimproof

   571 \isanewline

   572 \isanewline

   573 \isacommand{lemma}\isamarkupfalse%

   574 \ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharcolon}{\kern0pt}\isanewline

   575 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   576 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}fuse\ bs\ r{\isacharparenright}{\kern0pt}\ v\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ retrieve\ r\ v{\isachardoublequoteclose}\isanewline

   577 %

   578 \isadelimproof

   579 \ \ %

   580 \endisadelimproof

   581 %

   582 \isatagproof

   583 \isacommand{using}\isamarkupfalse%

   584 \ assms\isanewline

   585 \ \ \isacommand{apply}\isamarkupfalse%

   586 {\isacharparenleft}{\kern0pt}induct\ r\ arbitrary{\isacharcolon}{\kern0pt}\ v\ bs{\isacharparenright}{\kern0pt}\isanewline

   587 \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   588 {\isacharparenleft}{\kern0pt}auto\ elim{\isacharcolon}{\kern0pt}\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{4}}{\isacharbrackright}{\kern0pt}\isanewline

   589 \ \ \ \isacommand{defer}\isamarkupfalse%

   590 \isanewline

   591 \ \ \isacommand{using}\isamarkupfalse%

   592 \ retrieve{\isacharunderscore}{\kern0pt}encode{\isacharunderscore}{\kern0pt}STARS\isanewline

   593 \ \ \ \isacommand{apply}\isamarkupfalse%

   594 {\isacharparenleft}{\kern0pt}auto\ elim{\isacharbang}{\kern0pt}{\isacharcolon}{\kern0pt}\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{1}}{\isacharbrackright}{\kern0pt}\isanewline

   595 \ \ \ \isacommand{apply}\isamarkupfalse%

   596 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ vs{\isacharparenright}{\kern0pt}\isanewline

   597 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   598 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   599 \ \ \ \isacommand{apply}\isamarkupfalse%

   600 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   601 \ \ \isanewline

   602 \ \ \isacommand{apply}\isamarkupfalse%

   603 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   604 \ \ \isacommand{apply}\isamarkupfalse%

   605 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ x{\isadigit{2}}a{\isacharparenright}{\kern0pt}\isanewline

   606 \ \ \ \isacommand{apply}\isamarkupfalse%

   607 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   608 \ \ \ \isacommand{apply}\isamarkupfalse%

   609 {\isacharparenleft}{\kern0pt}auto\ elim{\isacharbang}{\kern0pt}{\isacharcolon}{\kern0pt}\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{1}}{\isacharbrackright}{\kern0pt}\isanewline

   610 \ \ \isacommand{apply}\isamarkupfalse%

   611 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   612 \ \ \ \isacommand{apply}\isamarkupfalse%

   613 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ list{\isacharparenright}{\kern0pt}\isanewline

   614 \ \ \ \isacommand{apply}\isamarkupfalse%

   615 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   616 \ \ \isacommand{apply}\isamarkupfalse%

   617 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   618 \ \ \isacommand{apply}\isamarkupfalse%

   619 {\isacharparenleft}{\kern0pt}auto\ elim{\isacharbang}{\kern0pt}{\isacharcolon}{\kern0pt}\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{1}}{\isacharbrackright}{\kern0pt}\isanewline

   620 \ \ \isacommand{done}\isamarkupfalse%

   621 %

   622 \endisatagproof

   623 {\isafoldproof}%

   624 %

   625 \isadelimproof

   626 \isanewline

   627 %

   628 \endisadelimproof

   629 \isanewline

   630 \isacommand{lemma}\isamarkupfalse%

   631 \ retrieve{\isacharunderscore}{\kern0pt}fuse{\isacharcolon}{\kern0pt}\isanewline

   632 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

   633 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}fuse\ bs\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ v\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ retrieve\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}\ v{\isachardoublequoteclose}\isanewline

   634 %

   635 \isadelimproof

   636 \ \ %

   637 \endisadelimproof

   638 %

   639 \isatagproof

   640 \isacommand{using}\isamarkupfalse%

   641 \ assms\ \isanewline

   642 \ \ \isacommand{by}\isamarkupfalse%

   643 \ {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all\ add{\isacharcolon}{\kern0pt}\ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharparenright}{\kern0pt}%

   644 \endisatagproof

   645 {\isafoldproof}%

   646 %

   647 \isadelimproof

   648 \isanewline

   649 %

   650 \endisadelimproof

   651 \isanewline

   652 \isanewline

   653 \isacommand{lemma}\isamarkupfalse%

   654 \ retrieve{\isacharunderscore}{\kern0pt}code{\isacharcolon}{\kern0pt}\isanewline

   655 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

   656 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}code\ v\ {\isacharequal}{\kern0pt}\ retrieve\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}\ v{\isachardoublequoteclose}\isanewline

   657 %

   658 \isadelimproof

   659 \ \ %

   660 \endisadelimproof

   661 %

   662 \isatagproof

   663 \isacommand{using}\isamarkupfalse%

   664 \ assms\isanewline

   665 \ \ \isacommand{apply}\isamarkupfalse%

   666 {\isacharparenleft}{\kern0pt}induct\ v\ r\ {\isacharparenright}{\kern0pt}\isanewline

   667 \ \ \isacommand{apply}\isamarkupfalse%

   668 {\isacharparenleft}{\kern0pt}simp{\isacharunderscore}{\kern0pt}all\ add{\isacharcolon}{\kern0pt}\ retrieve{\isacharunderscore}{\kern0pt}fuse\ retrieve{\isacharunderscore}{\kern0pt}encode{\isacharunderscore}{\kern0pt}STARS{\isacharparenright}{\kern0pt}\isanewline

   669 \ \ \isacommand{done}\isamarkupfalse%

   670 %

   671 \endisatagproof

   672 {\isafoldproof}%

   673 %

   674 \isadelimproof

   675 \isanewline

   676 %

   677 \endisadelimproof

   678 \isanewline

   679 \isanewline

   680 \isacommand{lemma}\isamarkupfalse%

   681 \ bnullable{\isacharunderscore}{\kern0pt}Hdbmkeps{\isacharunderscore}{\kern0pt}Hd{\isacharcolon}{\kern0pt}\isanewline

   682 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}bnullable\ a{\isachardoublequoteclose}\ \isanewline

   683 \ \ \isakeyword{shows}\ \ {\isachardoublequoteopen}bmkeps\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}a\ {\isacharhash}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bs\ {\isacharat}{\kern0pt}\ {\isacharparenleft}{\kern0pt}bmkeps\ a{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   684 %

   685 \isadelimproof

   686 \ \ %

   687 \endisadelimproof

   688 %

   689 \isatagproof

   690 \isacommand{using}\isamarkupfalse%

   691 \ assms\isanewline

   692 \ \ \isacommand{by}\isamarkupfalse%

   693 \ {\isacharparenleft}{\kern0pt}metis\ bmkeps{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ bmkeps{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ list{\isachardot}{\kern0pt}exhaust{\isacharparenright}{\kern0pt}%

   694 \endisatagproof

   695 {\isafoldproof}%

   696 %

   697 \isadelimproof

   698 \isanewline

   699 %

   700 \endisadelimproof

   701 \isanewline

   702 \isacommand{lemma}\isamarkupfalse%

   703 \ r{\isadigit{1}}{\isacharcolon}{\kern0pt}\isanewline

   704 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymnot}\ bnullable\ a{\isachardoublequoteclose}\ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   705 \ \ \isakeyword{shows}\ \ {\isachardoublequoteopen}bmkeps\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}a\ {\isacharhash}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ bmkeps\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   706 %

   707 \isadelimproof

   708 \ \ %

   709 \endisadelimproof

   710 %

   711 \isatagproof

   712 \isacommand{using}\isamarkupfalse%

   713 \ assms\isanewline

   714 \ \ \isacommand{apply}\isamarkupfalse%

   715 {\isacharparenleft}{\kern0pt}induct\ rs{\isacharparenright}{\kern0pt}\isanewline

   716 \ \ \ \isacommand{apply}\isamarkupfalse%

   717 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   718 \ \ \isacommand{done}\isamarkupfalse%

   719 %

   720 \endisatagproof

   721 {\isafoldproof}%

   722 %

   723 \isadelimproof

   724 \isanewline

   725 %

   726 \endisadelimproof

   727 \isanewline

   728 \isacommand{lemma}\isamarkupfalse%

   729 \ r{\isadigit{2}}{\isacharcolon}{\kern0pt}\isanewline

   730 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ rs{\isachardoublequoteclose}\ {\isachardoublequoteopen}bnullable\ x{\isachardoublequoteclose}\isanewline

   731 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}bnullable\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   732 %

   733 \isadelimproof

   734 \ \ %

   735 \endisadelimproof

   736 %

   737 \isatagproof

   738 \isacommand{using}\isamarkupfalse%

   739 \ assms\isanewline

   740 \ \ \isacommand{apply}\isamarkupfalse%

   741 {\isacharparenleft}{\kern0pt}induct\ rs{\isacharparenright}{\kern0pt}\isanewline

   742 \ \ \ \isacommand{apply}\isamarkupfalse%

   743 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   744 \ \ \isacommand{done}\isamarkupfalse%

   745 %

   746 \endisatagproof

   747 {\isafoldproof}%

   748 %

   749 \isadelimproof

   750 \isanewline

   751 %

   752 \endisadelimproof

   753 \isanewline

   754 \isacommand{lemma}\isamarkupfalse%

   755 \ \ r{\isadigit{3}}{\isacharcolon}{\kern0pt}\isanewline

   756 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymnot}\ bnullable\ r{\isachardoublequoteclose}\ \isanewline

   757 \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}\ {\isasymexists}\ x\ {\isasymin}\ set\ rs{\isachardot}{\kern0pt}\ bnullable\ x{\isachardoublequoteclose}\isanewline

   758 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}mkeps\ {\isacharparenleft}{\kern0pt}erase\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\isanewline

   759 \ \ \ \ \ \ \ \ \ retrieve\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}r\ {\isacharhash}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}mkeps\ {\isacharparenleft}{\kern0pt}erase\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ {\isacharparenleft}{\kern0pt}r\ {\isacharhash}{\kern0pt}\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   760 %

   761 \isadelimproof

   762 \ \ %

   763 \endisadelimproof

   764 %

   765 \isatagproof

   766 \isacommand{using}\isamarkupfalse%

   767 \ assms\isanewline

   768 \ \ \isacommand{apply}\isamarkupfalse%

   769 {\isacharparenleft}{\kern0pt}induct\ rs\ arbitrary{\isacharcolon}{\kern0pt}\ r\ bs{\isacharparenright}{\kern0pt}\isanewline

   770 \ \ \ \isacommand{apply}\isamarkupfalse%

   771 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{1}}{\isacharbrackright}{\kern0pt}\isanewline

   772 \ \ \isacommand{apply}\isamarkupfalse%

   773 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   774 \ \ \isacommand{using}\isamarkupfalse%

   775 \ bnullable{\isacharunderscore}{\kern0pt}correctness\ \isacommand{apply}\isamarkupfalse%

   776 \ blast\isanewline

   777 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   778 {\isacharparenleft}{\kern0pt}auto\ simp\ add{\isacharcolon}{\kern0pt}\ bnullable{\isacharunderscore}{\kern0pt}correctness\ mkeps{\isacharunderscore}{\kern0pt}nullable\ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

   779 \ \ \ \isacommand{apply}\isamarkupfalse%

   780 {\isacharparenleft}{\kern0pt}subst\ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharbrackleft}{\kern0pt}symmetric{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\isanewline

   781 \ \ \isacommand{apply}\isamarkupfalse%

   782 \ {\isacharparenleft}{\kern0pt}smt\ bnullable{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ bnullable{\isacharunderscore}{\kern0pt}correctness\ erase{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{5}}{\isacharparenright}{\kern0pt}\ erase{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{6}}{\isacharparenright}{\kern0pt}\ insert{\isacharunderscore}{\kern0pt}iff\ list{\isachardot}{\kern0pt}exhaust\ list{\isachardot}{\kern0pt}set{\isacharparenleft}{\kern0pt}{\isadigit{2}}{\isacharparenright}{\kern0pt}\ mkeps{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ mkeps{\isacharunderscore}{\kern0pt}nullable{\isacharparenright}{\kern0pt}\isanewline

   783 \ \ \ \isacommand{apply}\isamarkupfalse%

   784 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   785 \ \ \isacommand{apply}\isamarkupfalse%

   786 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}bnullable\ a{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\isanewline

   787 \ \ \isacommand{apply}\isamarkupfalse%

   788 \ {\isacharparenleft}{\kern0pt}smt\ append{\isacharunderscore}{\kern0pt}Nil{\isadigit{2}}\ bnullable{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ bnullable{\isacharunderscore}{\kern0pt}correctness\ erase{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{5}}{\isacharparenright}{\kern0pt}\ erase{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{6}}{\isacharparenright}{\kern0pt}\ fuse{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ insert{\isacharunderscore}{\kern0pt}iff\ list{\isachardot}{\kern0pt}exhaust\ list{\isachardot}{\kern0pt}set{\isacharparenleft}{\kern0pt}{\isadigit{2}}{\isacharparenright}{\kern0pt}\ mkeps{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ mkeps{\isacharunderscore}{\kern0pt}nullable\ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

   789 \ \ \isacommand{apply}\isamarkupfalse%

   790 {\isacharparenleft}{\kern0pt}drule{\isacharunderscore}{\kern0pt}tac\ x{\isacharequal}{\kern0pt}{\isachardoublequoteopen}a{\isachardoublequoteclose}\ \isakeyword{in}\ meta{\isacharunderscore}{\kern0pt}spec{\isacharparenright}{\kern0pt}\isanewline

   791 \ \ \isacommand{apply}\isamarkupfalse%

   792 {\isacharparenleft}{\kern0pt}drule{\isacharunderscore}{\kern0pt}tac\ x{\isacharequal}{\kern0pt}{\isachardoublequoteopen}bs{\isachardoublequoteclose}\ \isakeyword{in}\ meta{\isacharunderscore}{\kern0pt}spec{\isacharparenright}{\kern0pt}\isanewline

   793 \ \ \isacommand{apply}\isamarkupfalse%

   794 {\isacharparenleft}{\kern0pt}drule\ meta{\isacharunderscore}{\kern0pt}mp{\isacharparenright}{\kern0pt}\isanewline

   795 \ \ \ \isacommand{apply}\isamarkupfalse%

   796 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   797 \ \ \isacommand{apply}\isamarkupfalse%

   798 {\isacharparenleft}{\kern0pt}drule\ meta{\isacharunderscore}{\kern0pt}mp{\isacharparenright}{\kern0pt}\isanewline

   799 \ \ \ \isacommand{apply}\isamarkupfalse%

   800 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   801 \ \ \isacommand{apply}\isamarkupfalse%

   802 {\isacharparenleft}{\kern0pt}subst\ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharbrackleft}{\kern0pt}symmetric{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\isanewline

   803 \ \ \isacommand{apply}\isamarkupfalse%

   804 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ rs{\isacharparenright}{\kern0pt}\isanewline

   805 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   806 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   807 \ \ \ \isacommand{apply}\isamarkupfalse%

   808 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{1}}{\isacharbrackright}{\kern0pt}\isanewline

   809 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   810 \ {\isacharparenleft}{\kern0pt}simp\ add{\isacharcolon}{\kern0pt}\ bnullable{\isacharunderscore}{\kern0pt}correctness{\isacharparenright}{\kern0pt}\isanewline

   811 \ \ \isacommand{apply}\isamarkupfalse%

   812 \ {\isacharparenleft}{\kern0pt}metis\ append{\isacharunderscore}{\kern0pt}Nil{\isadigit{2}}\ bnullable{\isacharunderscore}{\kern0pt}correctness\ erase{\isacharunderscore}{\kern0pt}fuse\ fuse{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ list{\isachardot}{\kern0pt}set{\isacharunderscore}{\kern0pt}intros{\isacharparenleft}{\kern0pt}{\isadigit{1}}{\isacharparenright}{\kern0pt}\ mkeps{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ mkeps{\isacharunderscore}{\kern0pt}nullable\ nullable{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

   813 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   814 \ {\isacharparenleft}{\kern0pt}simp\ add{\isacharcolon}{\kern0pt}\ bnullable{\isacharunderscore}{\kern0pt}correctness{\isacharparenright}{\kern0pt}\isanewline

   815 \ \ \isacommand{apply}\isamarkupfalse%

   816 \ {\isacharparenleft}{\kern0pt}metis\ append{\isacharunderscore}{\kern0pt}Nil{\isadigit{2}}\ bnullable{\isacharunderscore}{\kern0pt}correctness\ erase{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{6}}{\isacharparenright}{\kern0pt}\ erase{\isacharunderscore}{\kern0pt}fuse\ fuse{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ list{\isachardot}{\kern0pt}set{\isacharunderscore}{\kern0pt}intros{\isacharparenleft}{\kern0pt}{\isadigit{2}}{\isacharparenright}{\kern0pt}\ mkeps{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ mkeps{\isacharunderscore}{\kern0pt}nullable\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

   817 \ \ \isacommand{apply}\isamarkupfalse%

   818 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   819 \ \ \isacommand{done}\isamarkupfalse%

   820 %

   821 \endisatagproof

   822 {\isafoldproof}%

   823 %

   824 \isadelimproof

   825 \isanewline

   826 %

   827 \endisadelimproof

   828 \isanewline

   829 \isanewline

   830 \isacommand{lemma}\isamarkupfalse%

   831 \ t{\isacharcolon}{\kern0pt}\ \isanewline

   832 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}r\ {\isasymin}\ set\ rs{\isachardot}{\kern0pt}\ nullable\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}\ {\isasymlongrightarrow}\ bmkeps\ r\ {\isacharequal}{\kern0pt}\ retrieve\ r\ {\isacharparenleft}{\kern0pt}mkeps\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\ \isanewline

   833 \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}nullable\ {\isacharparenleft}{\kern0pt}erase\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   834 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}\ bmkeps\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ retrieve\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}mkeps\ {\isacharparenleft}{\kern0pt}erase\ {\isacharparenleft}{\kern0pt}AALTs\ bs\ rs{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   835 %

   836 \isadelimproof

   837 \ \ %

   838 \endisadelimproof

   839 %

   840 \isatagproof

   841 \isacommand{using}\isamarkupfalse%

   842 \ assms\isanewline

   843 \ \ \isacommand{apply}\isamarkupfalse%

   844 {\isacharparenleft}{\kern0pt}induct\ rs\ arbitrary{\isacharcolon}{\kern0pt}\ bs{\isacharparenright}{\kern0pt}\isanewline

   845 \ \ \ \isacommand{apply}\isamarkupfalse%

   846 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   847 \ \ \isacommand{apply}\isamarkupfalse%

   848 {\isacharparenleft}{\kern0pt}auto\ simp\ add{\isacharcolon}{\kern0pt}\ bnullable{\isacharunderscore}{\kern0pt}correctness{\isacharparenright}{\kern0pt}\isanewline

   849 \ \ \ \isacommand{apply}\isamarkupfalse%

   850 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ rs{\isacharparenright}{\kern0pt}\isanewline

   851 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   852 {\isacharparenleft}{\kern0pt}auto\ simp\ add{\isacharcolon}{\kern0pt}\ bnullable{\isacharunderscore}{\kern0pt}correctness{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{2}}{\isacharbrackright}{\kern0pt}\isanewline

   853 \ \ \ \isacommand{apply}\isamarkupfalse%

   854 {\isacharparenleft}{\kern0pt}subst\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\isanewline

   855 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   856 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   857 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   858 {\isacharparenleft}{\kern0pt}rule\ r{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

   859 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   860 {\isacharparenleft}{\kern0pt}assumption{\isacharparenright}{\kern0pt}\isanewline

   861 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   862 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   863 \ \ \ \isacommand{apply}\isamarkupfalse%

   864 {\isacharparenleft}{\kern0pt}drule{\isacharunderscore}{\kern0pt}tac\ x{\isacharequal}{\kern0pt}{\isachardoublequoteopen}bs{\isachardoublequoteclose}\ \isakeyword{in}\ meta{\isacharunderscore}{\kern0pt}spec{\isacharparenright}{\kern0pt}\isanewline

   865 \ \ \ \isacommand{apply}\isamarkupfalse%

   866 {\isacharparenleft}{\kern0pt}drule\ meta{\isacharunderscore}{\kern0pt}mp{\isacharparenright}{\kern0pt}\isanewline

   867 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   868 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{1}}{\isacharbrackright}{\kern0pt}\isanewline

   869 \ \ \ \isacommand{prefer}\isamarkupfalse%

   870 \ {\isadigit{2}}\isanewline

   871 \ \ \isacommand{apply}\isamarkupfalse%

   872 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}bnullable\ a{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\isanewline

   873 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   874 {\isacharparenleft}{\kern0pt}subst\ bnullable{\isacharunderscore}{\kern0pt}Hdbmkeps{\isacharunderscore}{\kern0pt}Hd{\isacharparenright}{\kern0pt}\isanewline

   875 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   876 \ blast\isanewline

   877 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   878 {\isacharparenleft}{\kern0pt}subgoal{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}nullable\ {\isacharparenleft}{\kern0pt}erase\ a{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\isanewline

   879 \ \ \isacommand{prefer}\isamarkupfalse%

   880 \ {\isadigit{2}}\isanewline

   881 \ \ \isacommand{using}\isamarkupfalse%

   882 \ bnullable{\isacharunderscore}{\kern0pt}correctness\ \isacommand{apply}\isamarkupfalse%

   883 \ blast\isanewline

   884 \ \ \isacommand{apply}\isamarkupfalse%

   885 \ {\isacharparenleft}{\kern0pt}metis\ {\isacharparenleft}{\kern0pt}no{\isacharunderscore}{\kern0pt}types{\isacharcomma}{\kern0pt}\ lifting{\isacharparenright}{\kern0pt}\ erase{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{5}}{\isacharparenright}{\kern0pt}\ erase{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{6}}{\isacharparenright}{\kern0pt}\ list{\isachardot}{\kern0pt}exhaust\ mkeps{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ retrieve{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ retrieve{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\isanewline

   886 \ \ \isacommand{apply}\isamarkupfalse%

   887 {\isacharparenleft}{\kern0pt}subst\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}\isanewline

   888 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   889 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   890 \ \ \isacommand{using}\isamarkupfalse%

   891 \ r{\isadigit{2}}\ \isacommand{apply}\isamarkupfalse%

   892 \ blast\isanewline

   893 \ \ \isacommand{apply}\isamarkupfalse%

   894 {\isacharparenleft}{\kern0pt}drule{\isacharunderscore}{\kern0pt}tac\ x{\isacharequal}{\kern0pt}{\isachardoublequoteopen}bs{\isachardoublequoteclose}\ \isakeyword{in}\ meta{\isacharunderscore}{\kern0pt}spec{\isacharparenright}{\kern0pt}\isanewline

   895 \ \ \ \isacommand{apply}\isamarkupfalse%

   896 {\isacharparenleft}{\kern0pt}drule\ meta{\isacharunderscore}{\kern0pt}mp{\isacharparenright}{\kern0pt}\isanewline

   897 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   898 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isadigit{1}}{\isacharbrackright}{\kern0pt}\isanewline

   899 \ \ \ \isacommand{apply}\isamarkupfalse%

   900 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   901 \ \ \isacommand{using}\isamarkupfalse%

   902 \ r{\isadigit{3}}\ \isacommand{apply}\isamarkupfalse%

   903 \ blast\isanewline

   904 \ \ \isacommand{apply}\isamarkupfalse%

   905 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   906 \ \ \isacommand{using}\isamarkupfalse%

   907 \ r{\isadigit{3}}\ \isacommand{by}\isamarkupfalse%

   908 \ blast%

   909 \endisatagproof

   910 {\isafoldproof}%

   911 %

   912 \isadelimproof

   913 \isanewline

   914 %

   915 \endisadelimproof

   916 \isanewline

   917 \isacommand{lemma}\isamarkupfalse%

   918 \ bmkeps{\isacharunderscore}{\kern0pt}retrieve{\isacharcolon}{\kern0pt}\isanewline

   919 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}nullable\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   920 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}bmkeps\ r\ {\isacharequal}{\kern0pt}\ retrieve\ r\ {\isacharparenleft}{\kern0pt}mkeps\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   921 %

   922 \isadelimproof

   923 \ \ %

   924 \endisadelimproof

   925 %

   926 \isatagproof

   927 \isacommand{using}\isamarkupfalse%

   928 \ assms\isanewline

   929 \ \ \isacommand{apply}\isamarkupfalse%

   930 {\isacharparenleft}{\kern0pt}induct\ r{\isacharparenright}{\kern0pt}\isanewline

   931 \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   932 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   933 \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   934 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   935 \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   936 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   937 \ \ \ \ \isacommand{apply}\isamarkupfalse%

   938 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   939 \ \ \ \isacommand{defer}\isamarkupfalse%

   940 \isanewline

   941 \ \ \ \isacommand{apply}\isamarkupfalse%

   942 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   943 \ \ \isacommand{apply}\isamarkupfalse%

   944 {\isacharparenleft}{\kern0pt}rule\ t{\isacharparenright}{\kern0pt}\isanewline

   945 \ \ \ \isacommand{apply}\isamarkupfalse%

   946 {\isacharparenleft}{\kern0pt}auto{\isacharparenright}{\kern0pt}\isanewline

   947 \ \ \isacommand{done}\isamarkupfalse%

   948 %

   949 \endisatagproof

   950 {\isafoldproof}%

   951 %

   952 \isadelimproof

   953 \isanewline

   954 %

   955 \endisadelimproof

   956 \isanewline

   957 \isacommand{lemma}\isamarkupfalse%

   958 \ bder{\isacharunderscore}{\kern0pt}retrieve{\isacharcolon}{\kern0pt}\isanewline

   959 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ der\ c\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   960 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}retrieve\ {\isacharparenleft}{\kern0pt}bder\ c\ r{\isacharparenright}{\kern0pt}\ v\ {\isacharequal}{\kern0pt}\ retrieve\ r\ {\isacharparenleft}{\kern0pt}injval\ {\isacharparenleft}{\kern0pt}erase\ r{\isacharparenright}{\kern0pt}\ c\ v{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}\isanewline

   961 %

   962 \isadelimproof

   963 \ \ %

   964 \endisadelimproof

   965 %

   966 \isatagproof

   967 \isacommand{using}\isamarkupfalse%

   968 \ assms\isanewline

   969 \ \ \isacommand{apply}\isamarkupfalse%

   970 {\isacharparenleft}{\kern0pt}induct\ r\ arbitrary{\isacharcolon}{\kern0pt}\ v\ rule{\isacharcolon}{\kern0pt}\ erase{\isachardot}{\kern0pt}induct{\isacharparenright}{\kern0pt}\isanewline

   971 \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   972 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   973 \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   974 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

   975 \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   976 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   977 \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   978 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\ \isanewline

   979 \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   980 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   981 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   982 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}c\ {\isacharequal}{\kern0pt}\ ca{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\isanewline

   983 \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   984 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   985 \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   986 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

   987 \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   988 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   989 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   990 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   991 \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   992 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

   993 \ \ \isacommand{apply}\isamarkupfalse%

   994 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   995 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   996 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

   997 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

   998 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

   999 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1000 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1001 \ \ \isacommand{apply}\isamarkupfalse%

  1002 {\isacharparenleft}{\kern0pt}rename{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}r\isactrlsub {\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}r\isactrlsub {\isadigit{2}}{\isachardoublequoteclose}\ rs\ v{\isacharparenright}{\kern0pt}\isanewline

  1003 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1004 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

  1005 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1006 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1007 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1008 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1009 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1010 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ rs{\isacharparenright}{\kern0pt}\isanewline

  1011 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1012 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1013 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1014 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1015 \ \ \isacommand{apply}\isamarkupfalse%

  1016 \ {\isacharparenleft}{\kern0pt}smt\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ injval{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{2}}{\isacharparenright}{\kern0pt}\ injval{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{3}}{\isacharparenright}{\kern0pt}\ retrieve{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{4}}{\isacharparenright}{\kern0pt}\ retrieve{\isachardot}{\kern0pt}simps{\isacharparenleft}{\kern0pt}{\isadigit{5}}{\isacharparenright}{\kern0pt}\ same{\isacharunderscore}{\kern0pt}append{\isacharunderscore}{\kern0pt}eq{\isacharparenright}{\kern0pt}\isanewline

  1017 \ \ \ \isacommand{apply}\isamarkupfalse%

  1018 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1019 \ \ \ \isacommand{apply}\isamarkupfalse%

  1020 {\isacharparenleft}{\kern0pt}case{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}nullable\ {\isacharparenleft}{\kern0pt}erase\ r{\isadigit{1}}{\isacharparenright}{\kern0pt}{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\isanewline

  1021 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1022 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1023 \ \ \isacommand{apply}\isamarkupfalse%

  1024 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

  1025 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1026 {\isacharparenleft}{\kern0pt}subgoal{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}bnullable\ r{\isadigit{1}}{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\isanewline

  1027 \ \ \isacommand{prefer}\isamarkupfalse%

  1028 \ {\isadigit{2}}\isanewline

  1029 \ \ \isacommand{using}\isamarkupfalse%

  1030 \ bnullable{\isacharunderscore}{\kern0pt}correctness\ \isacommand{apply}\isamarkupfalse%

  1031 \ blast\isanewline

  1032 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1033 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1034 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1035 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

  1036 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1037 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1038 \ \ \ \isacommand{apply}\isamarkupfalse%

  1039 {\isacharparenleft}{\kern0pt}subgoal{\isacharunderscore}{\kern0pt}tac\ {\isachardoublequoteopen}bnullable\ r{\isadigit{1}}{\isachardoublequoteclose}{\isacharparenright}{\kern0pt}\isanewline

  1040 \ \ \isacommand{prefer}\isamarkupfalse%

  1041 \ {\isadigit{2}}\isanewline

  1042 \ \ \isacommand{using}\isamarkupfalse%

  1043 \ bnullable{\isacharunderscore}{\kern0pt}correctness\ \isacommand{apply}\isamarkupfalse%

  1044 \ blast\isanewline

  1045 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1046 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1047 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1048 {\isacharparenleft}{\kern0pt}simp\ add{\isacharcolon}{\kern0pt}\ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

  1049 \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1050 {\isacharparenleft}{\kern0pt}simp\ add{\isacharcolon}{\kern0pt}\ bmkeps{\isacharunderscore}{\kern0pt}retrieve{\isacharparenright}{\kern0pt}\isanewline

  1051 \ \ \ \isacommand{apply}\isamarkupfalse%

  1052 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1053 \ \ \ \isacommand{apply}\isamarkupfalse%

  1054 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

  1055 \ \ \ \isacommand{apply}\isamarkupfalse%

  1056 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1057 \ \ \isacommand{using}\isamarkupfalse%

  1058 \ bnullable{\isacharunderscore}{\kern0pt}correctness\ \isacommand{apply}\isamarkupfalse%

  1059 \ blast\isanewline

  1060 \ \ \isacommand{apply}\isamarkupfalse%

  1061 {\isacharparenleft}{\kern0pt}rename{\isacharunderscore}{\kern0pt}tac\ bs\ r\ v{\isacharparenright}{\kern0pt}\isanewline

  1062 \ \ \isacommand{apply}\isamarkupfalse%

  1063 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1064 \ \ \isacommand{apply}\isamarkupfalse%

  1065 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

  1066 \ \ \ \ \ \isacommand{apply}\isamarkupfalse%

  1067 {\isacharparenleft}{\kern0pt}clarify{\isacharparenright}{\kern0pt}\isanewline

  1068 \ \ \isacommand{apply}\isamarkupfalse%

  1069 {\isacharparenleft}{\kern0pt}erule\ Prf{\isacharunderscore}{\kern0pt}elims{\isacharparenright}{\kern0pt}\isanewline

  1070 \ \ \isacommand{apply}\isamarkupfalse%

  1071 {\isacharparenleft}{\kern0pt}clarify{\isacharparenright}{\kern0pt}\isanewline

  1072 \ \ \isacommand{apply}\isamarkupfalse%

  1073 {\isacharparenleft}{\kern0pt}subst\ injval{\isachardot}{\kern0pt}simps{\isacharparenright}{\kern0pt}\isanewline

  1074 \ \ \isacommand{apply}\isamarkupfalse%

  1075 {\isacharparenleft}{\kern0pt}simp\ del{\isacharcolon}{\kern0pt}\ retrieve{\isachardot}{\kern0pt}simps{\isacharparenright}{\kern0pt}\isanewline

  1076 \ \ \isacommand{apply}\isamarkupfalse%

  1077 {\isacharparenleft}{\kern0pt}subst\ retrieve{\isachardot}{\kern0pt}simps{\isacharparenright}{\kern0pt}\isanewline

  1078 \ \ \isacommand{apply}\isamarkupfalse%

  1079 {\isacharparenleft}{\kern0pt}subst\ retrieve{\isachardot}{\kern0pt}simps{\isacharparenright}{\kern0pt}\isanewline

  1080 \ \ \isacommand{apply}\isamarkupfalse%

  1081 {\isacharparenleft}{\kern0pt}simp{\isacharparenright}{\kern0pt}\isanewline

  1082 \ \ \isacommand{apply}\isamarkupfalse%

  1083 {\isacharparenleft}{\kern0pt}simp\ add{\isacharcolon}{\kern0pt}\ retrieve{\isacharunderscore}{\kern0pt}fuse{\isadigit{2}}{\isacharparenright}{\kern0pt}\isanewline

  1084 \ \ \isacommand{done}\isamarkupfalse%

  1085 %

  1086 \endisatagproof

  1087 {\isafoldproof}%

  1088 %

  1089 \isadelimproof

  1090 \isanewline

  1091 %

  1092 \endisadelimproof

  1093 \ \ \isanewline

  1094 \isanewline

  1095 \isanewline

  1096 \isacommand{lemma}\isamarkupfalse%

  1097 \ MAIN{\isacharunderscore}{\kern0pt}decode{\isacharcolon}{\kern0pt}\isanewline

  1098 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ ders\ s\ r{\isachardoublequoteclose}\isanewline

  1099 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}Some\ {\isacharparenleft}{\kern0pt}flex\ r\ id\ s\ v{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode\ {\isacharparenleft}{\kern0pt}retrieve\ {\isacharparenleft}{\kern0pt}bders\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}\ s{\isacharparenright}{\kern0pt}\ v{\isacharparenright}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

  1100 %

  1101 \isadelimproof

  1102 \ \ %

  1103 \endisadelimproof

  1104 %

  1105 \isatagproof

  1106 \isacommand{using}\isamarkupfalse%

  1107 \ assms\isanewline

  1108 \isacommand{proof}\isamarkupfalse%

  1109 \ {\isacharparenleft}{\kern0pt}induct\ s\ arbitrary{\isacharcolon}{\kern0pt}\ v\ rule{\isacharcolon}{\kern0pt}\ rev{\isacharunderscore}{\kern0pt}induct{\isacharparenright}{\kern0pt}\isanewline

  1110 \ \ \isacommand{case}\isamarkupfalse%

  1111 \ Nil\isanewline

  1112 \ \ \isacommand{have}\isamarkupfalse%

  1113 \ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ ders\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ r{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1114 \ fact\isanewline

  1115 \ \ \isacommand{then}\isamarkupfalse%

  1116 \ \isacommand{have}\isamarkupfalse%

  1117 \ {\isachardoublequoteopen}{\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ r{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

  1118 \ simp\isanewline

  1119 \ \ \isacommand{then}\isamarkupfalse%

  1120 \ \isacommand{have}\isamarkupfalse%

  1121 \ {\isachardoublequoteopen}Some\ v\ {\isacharequal}{\kern0pt}\ decode\ {\isacharparenleft}{\kern0pt}retrieve\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}\ v{\isacharparenright}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

  1122 \ \ \ \ \isacommand{using}\isamarkupfalse%

  1123 \ decode{\isacharunderscore}{\kern0pt}code\ retrieve{\isacharunderscore}{\kern0pt}code\ \isacommand{by}\isamarkupfalse%

  1124 \ auto\isanewline

  1125 \ \ \isacommand{then}\isamarkupfalse%

  1126 \ \isacommand{show}\isamarkupfalse%

  1127 \ {\isachardoublequoteopen}Some\ {\isacharparenleft}{\kern0pt}flex\ r\ id\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ v{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ decode\ {\isacharparenleft}{\kern0pt}retrieve\ {\isacharparenleft}{\kern0pt}bders\ {\isacharparenleft}{\kern0pt}intern\ r{\isacharparenright}{\kern0pt}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharparenright}{\kern0pt}\ v{\isacharparenright}{\kern0pt}\ r{\isachardoublequoteclose}\isanewline

  1128 \ \ \ \ \isacommand{by}\isamarkupfalse%

  1129 \ simp\isanewline

  1130 \isacommand{next}\isamarkupfalse%

  1131 \isanewline

  1132 \ \ \isacommand{case}\isamarkupfalse%

  1133 \ {\isacharparenleft}{\kern0pt}snoc\ c\ s\ v{\isacharparenright}{\kern0pt}\isanewline

  1134 \ \ \isacommand{have}\isamarkupfalse%

  1135 \ IH{\isacharcolon}{\kern0pt}\ {\isachardoublequoteopen}{\isasymAnd}v{\isachardot}{\kern0pt}\ {\isasymTurnstile}\ v\ {\isacharcolon}{\kern0pt}\ ders\ s\ r\ {\isasymLongrightarrow}\ \isanewline