def gc.elt0.s110
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1566
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
1566def gc.elt0.s110(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, h: {U32.is_eq(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, True{}}) == 0 : U32}:
1567 match b0:
1568 case True{}:
1569 match b1:
1570 case True{}:
1571 match b2:
1572 case True{}:
1573 match b3:
1574 case True{}:
1575 match b4:
1576 case True{}:
1577 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1578 case False{}:
1579 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1580 case False{}:
1581 match b4:
1582 case True{}:
1583 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1584 case False{}:
1585 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1586 case False{}:
1587 match b3:
1588 case True{}:
1589 match b4:
1590 case True{}:
1591 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1592 case False{}:
1593 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1594 case False{}:
1595 match b4:
1596 case True{}:
1597 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1598 case False{}:
1599 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1600 case False{}:
1601 match b2:
1602 case True{}:
1603 match b3:
1604 case True{}:
1605 match b4:
1606 case True{}:
1607 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1608 case False{}:
1609 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1610 case False{}:
1611 match b4:
1612 case True{}:
1613 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1614 case False{}:
1615 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1616 case False{}:
1617 match b3:
1618 case True{}:
1619 match b4:
1620 case True{}:
1621 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1622 case False{}:
1623 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1624 case False{}:
1625 match b4:
1626 case True{}:
1627 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1628 case False{}:
1629 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1630 case False{}:
1631 match b1:
1632 case True{}:
1633 match b2:
1634 case True{}:
1635 match b3:
1636 case True{}:
1637 match b4:
1638 case True{}:
1639 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1640 case False{}:
1641 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1642 case False{}:
1643 match b4:
1644 case True{}:
1645 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1646 case False{}:
1647 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1648 case False{}:
1649 match b3:
1650 case True{}:
1651 match b4:
1652 case True{}:
1653 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1654 case False{}:
1655 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1656 case False{}:
1657 match b4:
1658 case True{}:
1659 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1660 case False{}:
1661 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1662 case False{}:
1663 match b2:
1664 case True{}:
1665 match b3:
1666 case True{}:
1667 match b4:
1668 case True{}:
1669 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1670 case False{}:
1671 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1672 case False{}:
1673 match b4:
1674 case True{}:
1675 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1676 case False{}:
1677 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1678 case False{}:
1679 match b3:
1680 case True{}:
1681 match b4:
1682 case True{}:
1683 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1684 case False{}:
1685 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1686 case False{}:
1687 match b4:
1688 case True{}:
1689 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1690 case False{}:
1691 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))