def gc.elt0.s010
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1693
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
1693def gc.elt0.s010(+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{}, False{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, False{}, True{}, False{}}) == 0 : U32}:
1694 match b0:
1695 case True{}:
1696 match b1:
1697 case True{}:
1698 match b2:
1699 case True{}:
1700 match b3:
1701 case True{}:
1702 match b4:
1703 case True{}:
1704 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1705 case False{}:
1706 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1707 case False{}:
1708 match b4:
1709 case True{}:
1710 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1711 case False{}:
1712 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1713 case False{}:
1714 match b3:
1715 case True{}:
1716 match b4:
1717 case True{}:
1718 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1719 case False{}:
1720 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1721 case False{}:
1722 match b4:
1723 case True{}:
1724 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1725 case False{}:
1726 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1727 case False{}:
1728 match b2:
1729 case True{}:
1730 match b3:
1731 case True{}:
1732 match b4:
1733 case True{}:
1734 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1735 case False{}:
1736 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1737 case False{}:
1738 match b4:
1739 case True{}:
1740 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1741 case False{}:
1742 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1743 case False{}:
1744 match b3:
1745 case True{}:
1746 match b4:
1747 case True{}:
1748 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1749 case False{}:
1750 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1751 case False{}:
1752 match b4:
1753 case True{}:
1754 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1755 case False{}:
1756 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1757 case False{}:
1758 match b1:
1759 case True{}:
1760 match b2:
1761 case True{}:
1762 match b3:
1763 case True{}:
1764 match b4:
1765 case True{}:
1766 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1767 case False{}:
1768 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1769 case False{}:
1770 match b4:
1771 case True{}:
1772 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1773 case False{}:
1774 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1775 case False{}:
1776 match b3:
1777 case True{}:
1778 match b4:
1779 case True{}:
1780 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1781 case False{}:
1782 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1783 case False{}:
1784 match b4:
1785 case True{}:
1786 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1787 case False{}:
1788 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1789 case False{}:
1790 match b2:
1791 case True{}:
1792 match b3:
1793 case True{}:
1794 match b4:
1795 case True{}:
1796 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1797 case False{}:
1798 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1799 case False{}:
1800 match b4:
1801 case True{}:
1802 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1803 case False{}:
1804 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1805 case False{}:
1806 match b3:
1807 case True{}:
1808 match b4:
1809 case True{}:
1810 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1811 case False{}:
1812 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1813 case False{}:
1814 match b4:
1815 case True{}:
1816 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))
1817 case False{}:
1818 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, False{}, True{}, False{}}) == 0 : U32}, GT.gt.ft(h))