def gc.isz.bits.s011

bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:143

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

143def gc.isz.bits.s011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}) : Bool}:
144  match b0:
145    case True{}:
146      match b1:
147        case True{}:
148          match b2:
149            case True{}:
150              match b3:
151                case True{}:
152                  match b4:
153                    case True{}:
154                      {==}
155                    case False{}:
156                      {==}
157                case False{}:
158                  match b4:
159                    case True{}:
160                      {==}
161                    case False{}:
162                      {==}
163            case False{}:
164              match b3:
165                case True{}:
166                  match b4:
167                    case True{}:
168                      {==}
169                    case False{}:
170                      {==}
171                case False{}:
172                  match b4:
173                    case True{}:
174                      {==}
175                    case False{}:
176                      {==}
177        case False{}:
178          match b2:
179            case True{}:
180              match b3:
181                case True{}:
182                  match b4:
183                    case True{}:
184                      {==}
185                    case False{}:
186                      {==}
187                case False{}:
188                  match b4:
189                    case True{}:
190                      {==}
191                    case False{}:
192                      {==}
193            case False{}:
194              match b3:
195                case True{}:
196                  match b4:
197                    case True{}:
198                      {==}
199                    case False{}:
200                      {==}
201                case False{}:
202                  match b4:
203                    case True{}:
204                      {==}
205                    case False{}:
206                      {==}
207    case False{}:
208      match b1:
209        case True{}:
210          match b2:
211            case True{}:
212              match b3:
213                case True{}:
214                  match b4:
215                    case True{}:
216                      {==}
217                    case False{}:
218                      {==}
219                case False{}:
220                  match b4:
221                    case True{}:
222                      {==}
223                    case False{}:
224                      {==}
225            case False{}:
226              match b3:
227                case True{}:
228                  match b4:
229                    case True{}:
230                      {==}
231                    case False{}:
232                      {==}
233                case False{}:
234                  match b4:
235                    case True{}:
236                      {==}
237                    case False{}:
238                      {==}
239        case False{}:
240          match b2:
241            case True{}:
242              match b3:
243                case True{}:
244                  match b4:
245                    case True{}:
246                      {==}
247                    case False{}:
248                      {==}
249                case False{}:
250                  match b4:
251                    case True{}:
252                      {==}
253                    case False{}:
254                      {==}
255            case False{}:
256              match b3:
257                case True{}:
258                  match b4:
259                    case True{}:
260                      {==}
261                    case False{}:
262                      {==}
263                case False{}:
264                  match b4:
265                    case True{}:
266                      {==}
267                    case False{}:
268                      {==}