def gc.elt0.s011
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1185
import bend-osdev-gf@0.1.1.0/proof_tab_cases.bend as ProofTabCases
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-osdev-gf@0.1.1.0/proof_tab.bend as GT
1185def gc.elt0.s011(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, False{}}) == 0 : U32}:
1186 match b0:
1187 case True{}:
1188 match b1:
1189 case True{}:
1190 match b2:
1191 case True{}:
1192 match b3:
1193 case True{}:
1194 match b4:
1195 case True{}:
1196 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1197 case False{}:
1198 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1199 case False{}:
1200 match b4:
1201 case True{}:
1202 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1203 case False{}:
1204 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1205 case False{}:
1206 match b3:
1207 case True{}:
1208 match b4:
1209 case True{}:
1210 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1211 case False{}:
1212 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1213 case False{}:
1214 match b4:
1215 case True{}:
1216 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1217 case False{}:
1218 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1219 case False{}:
1220 match b2:
1221 case True{}:
1222 match b3:
1223 case True{}:
1224 match b4:
1225 case True{}:
1226 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1227 case False{}:
1228 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1229 case False{}:
1230 match b4:
1231 case True{}:
1232 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1233 case False{}:
1234 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1235 case False{}:
1236 match b3:
1237 case True{}:
1238 match b4:
1239 case True{}:
1240 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1241 case False{}:
1242 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1243 case False{}:
1244 match b4:
1245 case True{}:
1246 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1247 case False{}:
1248 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1249 case False{}:
1250 match b1:
1251 case True{}:
1252 match b2:
1253 case True{}:
1254 match b3:
1255 case True{}:
1256 match b4:
1257 case True{}:
1258 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1259 case False{}:
1260 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1261 case False{}:
1262 match b4:
1263 case True{}:
1264 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1265 case False{}:
1266 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1267 case False{}:
1268 match b3:
1269 case True{}:
1270 match b4:
1271 case True{}:
1272 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1273 case False{}:
1274 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1275 case False{}:
1276 match b4:
1277 case True{}:
1278 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1279 case False{}:
1280 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1281 case False{}:
1282 match b2:
1283 case True{}:
1284 match b3:
1285 case True{}:
1286 match b4:
1287 case True{}:
1288 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1289 case False{}:
1290 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1291 case False{}:
1292 match b4:
1293 case True{}:
1294 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1295 case False{}:
1296 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1297 case False{}:
1298 match b3:
1299 case True{}:
1300 match b4:
1301 case True{}:
1302 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1303 case False{}:
1304 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1305 case False{}:
1306 match b4:
1307 case True{}:
1308 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1309 case False{}:
1310 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))