def gc.elt0.s101
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1312
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
1312def gc.elt0.s101(+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{}, False{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, True{}}) == 0 : U32}:
1313 match b0:
1314 case True{}:
1315 match b1:
1316 case True{}:
1317 match b2:
1318 case True{}:
1319 match b3:
1320 case True{}:
1321 match b4:
1322 case True{}:
1323 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1324 case False{}:
1325 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1326 case False{}:
1327 match b4:
1328 case True{}:
1329 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1330 case False{}:
1331 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1332 case False{}:
1333 match b3:
1334 case True{}:
1335 match b4:
1336 case True{}:
1337 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1338 case False{}:
1339 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1340 case False{}:
1341 match b4:
1342 case True{}:
1343 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1344 case False{}:
1345 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1346 case False{}:
1347 match b2:
1348 case True{}:
1349 match b3:
1350 case True{}:
1351 match b4:
1352 case True{}:
1353 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1354 case False{}:
1355 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1356 case False{}:
1357 match b4:
1358 case True{}:
1359 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1360 case False{}:
1361 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1362 case False{}:
1363 match b3:
1364 case True{}:
1365 match b4:
1366 case True{}:
1367 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1368 case False{}:
1369 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1370 case False{}:
1371 match b4:
1372 case True{}:
1373 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1374 case False{}:
1375 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1376 case False{}:
1377 match b1:
1378 case True{}:
1379 match b2:
1380 case True{}:
1381 match b3:
1382 case True{}:
1383 match b4:
1384 case True{}:
1385 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1386 case False{}:
1387 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1388 case False{}:
1389 match b4:
1390 case True{}:
1391 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1392 case False{}:
1393 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1394 case False{}:
1395 match b3:
1396 case True{}:
1397 match b4:
1398 case True{}:
1399 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1400 case False{}:
1401 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1402 case False{}:
1403 match b4:
1404 case True{}:
1405 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1406 case False{}:
1407 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1408 case False{}:
1409 match b2:
1410 case True{}:
1411 match b3:
1412 case True{}:
1413 match b4:
1414 case True{}:
1415 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1416 case False{}:
1417 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1418 case False{}:
1419 match b4:
1420 case True{}:
1421 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1422 case False{}:
1423 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1424 case False{}:
1425 match b3:
1426 case True{}:
1427 match b4:
1428 case True{}:
1429 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1430 case False{}:
1431 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1432 case False{}:
1433 match b4:
1434 case True{}:
1435 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1436 case False{}:
1437 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, False{}, True{}}) == 0 : U32}, GT.gt.ft(h))