def gc.isz.bits.s111

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

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

15# the table's zero test on a byte is Gf8.is_zero
16def gc.isz.bits.s111(+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{}, True{}}), 0) == G.Gf8Bits.is_zero(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}) : Bool}:
17  match b0:
18    case True{}:
19      match b1:
20        case True{}:
21          match b2:
22            case True{}:
23              match b3:
24                case True{}:
25                  match b4:
26                    case True{}:
27                      {==}
28                    case False{}:
29                      {==}
30                case False{}:
31                  match b4:
32                    case True{}:
33                      {==}
34                    case False{}:
35                      {==}
36            case False{}:
37              match b3:
38                case True{}:
39                  match b4:
40                    case True{}:
41                      {==}
42                    case False{}:
43                      {==}
44                case False{}:
45                  match b4:
46                    case True{}:
47                      {==}
48                    case False{}:
49                      {==}
50        case False{}:
51          match b2:
52            case True{}:
53              match b3:
54                case True{}:
55                  match b4:
56                    case True{}:
57                      {==}
58                    case False{}:
59                      {==}
60                case False{}:
61                  match b4:
62                    case True{}:
63                      {==}
64                    case False{}:
65                      {==}
66            case False{}:
67              match b3:
68                case True{}:
69                  match b4:
70                    case True{}:
71                      {==}
72                    case False{}:
73                      {==}
74                case False{}:
75                  match b4:
76                    case True{}:
77                      {==}
78                    case False{}:
79                      {==}
80    case False{}:
81      match b1:
82        case True{}:
83          match b2:
84            case True{}:
85              match b3:
86                case True{}:
87                  match b4:
88                    case True{}:
89                      {==}
90                    case False{}:
91                      {==}
92                case False{}:
93                  match b4:
94                    case True{}:
95                      {==}
96                    case False{}:
97                      {==}
98            case False{}:
99              match b3:
100                case True{}:
101                  match b4:
102                    case True{}:
103                      {==}
104                    case False{}:
105                      {==}
106                case False{}:
107                  match b4:
108                    case True{}:
109                      {==}
110                    case False{}:
111                      {==}
112        case False{}:
113          match b2:
114            case True{}:
115              match b3:
116                case True{}:
117                  match b4:
118                    case True{}:
119                      {==}
120                    case False{}:
121                      {==}
122                case False{}:
123                  match b4:
124                    case True{}:
125                      {==}
126                    case False{}:
127                      {==}
128            case False{}:
129              match b3:
130                case True{}:
131                  match b4:
132                    case True{}:
133                      {==}
134                    case False{}:
135                      {==}
136                case False{}:
137                  match b4:
138                    case True{}:
139                      {==}
140                    case False{}:
141                      {==}