def gc.elt0.s001
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1439
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
1439def gc.elt0.s001(+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{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, False{}, False{}}) == 0 : U32}:
1440 match b0:
1441 case True{}:
1442 match b1:
1443 case True{}:
1444 match b2:
1445 case True{}:
1446 match b3:
1447 case True{}:
1448 match b4:
1449 case True{}:
1450 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1451 case False{}:
1452 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1453 case False{}:
1454 match b4:
1455 case True{}:
1456 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1457 case False{}:
1458 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1459 case False{}:
1460 match b3:
1461 case True{}:
1462 match b4:
1463 case True{}:
1464 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1465 case False{}:
1466 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1467 case False{}:
1468 match b4:
1469 case True{}:
1470 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1471 case False{}:
1472 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1473 case False{}:
1474 match b2:
1475 case True{}:
1476 match b3:
1477 case True{}:
1478 match b4:
1479 case True{}:
1480 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1481 case False{}:
1482 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1483 case False{}:
1484 match b4:
1485 case True{}:
1486 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1487 case False{}:
1488 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1489 case False{}:
1490 match b3:
1491 case True{}:
1492 match b4:
1493 case True{}:
1494 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1495 case False{}:
1496 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1497 case False{}:
1498 match b4:
1499 case True{}:
1500 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1501 case False{}:
1502 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1503 case False{}:
1504 match b1:
1505 case True{}:
1506 match b2:
1507 case True{}:
1508 match b3:
1509 case True{}:
1510 match b4:
1511 case True{}:
1512 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1513 case False{}:
1514 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1515 case False{}:
1516 match b4:
1517 case True{}:
1518 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1519 case False{}:
1520 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1521 case False{}:
1522 match b3:
1523 case True{}:
1524 match b4:
1525 case True{}:
1526 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1527 case False{}:
1528 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1529 case False{}:
1530 match b4:
1531 case True{}:
1532 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1533 case False{}:
1534 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1535 case False{}:
1536 match b2:
1537 case True{}:
1538 match b3:
1539 case True{}:
1540 match b4:
1541 case True{}:
1542 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1543 case False{}:
1544 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1545 case False{}:
1546 match b4:
1547 case True{}:
1548 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1549 case False{}:
1550 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1551 case False{}:
1552 match b3:
1553 case True{}:
1554 match b4:
1555 case True{}:
1556 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1557 case False{}:
1558 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1559 case False{}:
1560 match b4:
1561 case True{}:
1562 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1563 case False{}:
1564 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, False{}, False{}}) == 0 : U32}, GT.gt.ft(h))