def gc.isz.bits.s101

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

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

270def gc.isz.bits.s101(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool) -> {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}) : Bool}:
271  match b0:
272    case True{}:
273      match b1:
274        case True{}:
275          match b2:
276            case True{}:
277              match b3:
278                case True{}:
279                  match b4:
280                    case True{}:
281                      {==}
282                    case False{}:
283                      {==}
284                case False{}:
285                  match b4:
286                    case True{}:
287                      {==}
288                    case False{}:
289                      {==}
290            case False{}:
291              match b3:
292                case True{}:
293                  match b4:
294                    case True{}:
295                      {==}
296                    case False{}:
297                      {==}
298                case False{}:
299                  match b4:
300                    case True{}:
301                      {==}
302                    case False{}:
303                      {==}
304        case False{}:
305          match b2:
306            case True{}:
307              match b3:
308                case True{}:
309                  match b4:
310                    case True{}:
311                      {==}
312                    case False{}:
313                      {==}
314                case False{}:
315                  match b4:
316                    case True{}:
317                      {==}
318                    case False{}:
319                      {==}
320            case False{}:
321              match b3:
322                case True{}:
323                  match b4:
324                    case True{}:
325                      {==}
326                    case False{}:
327                      {==}
328                case False{}:
329                  match b4:
330                    case True{}:
331                      {==}
332                    case False{}:
333                      {==}
334    case False{}:
335      match b1:
336        case True{}:
337          match b2:
338            case True{}:
339              match b3:
340                case True{}:
341                  match b4:
342                    case True{}:
343                      {==}
344                    case False{}:
345                      {==}
346                case False{}:
347                  match b4:
348                    case True{}:
349                      {==}
350                    case False{}:
351                      {==}
352            case False{}:
353              match b3:
354                case True{}:
355                  match b4:
356                    case True{}:
357                      {==}
358                    case False{}:
359                      {==}
360                case False{}:
361                  match b4:
362                    case True{}:
363                      {==}
364                    case False{}:
365                      {==}
366        case False{}:
367          match b2:
368            case True{}:
369              match b3:
370                case True{}:
371                  match b4:
372                    case True{}:
373                      {==}
374                    case False{}:
375                      {==}
376                case False{}:
377                  match b4:
378                    case True{}:
379                      {==}
380                    case False{}:
381                      {==}
382            case False{}:
383              match b3:
384                case True{}:
385                  match b4:
386                    case True{}:
387                      {==}
388                    case False{}:
389                      {==}
390                case False{}:
391                  match b4:
392                    case True{}:
393                      {==}
394                    case False{}:
395                      {==}