def gc.elt0.s111
bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:1057
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
1057
1058def gc.elt0.s111(+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{}, True{}}), 0) == True{} : Bool}) -> {G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, True{}, True{}, True{}}) == 0 : U32}:
1059 match b0:
1060 case True{}:
1061 match b1:
1062 case True{}:
1063 match b2:
1064 case True{}:
1065 match b3:
1066 case True{}:
1067 match b4:
1068 case True{}:
1069 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1070 case False{}:
1071 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1072 case False{}:
1073 match b4:
1074 case True{}:
1075 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1076 case False{}:
1077 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1078 case False{}:
1079 match b3:
1080 case True{}:
1081 match b4:
1082 case True{}:
1083 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1084 case False{}:
1085 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1086 case False{}:
1087 match b4:
1088 case True{}:
1089 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1090 case False{}:
1091 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, True{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1092 case False{}:
1093 match b2:
1094 case True{}:
1095 match b3:
1096 case True{}:
1097 match b4:
1098 case True{}:
1099 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1100 case False{}:
1101 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1102 case False{}:
1103 match b4:
1104 case True{}:
1105 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1106 case False{}:
1107 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1108 case False{}:
1109 match b3:
1110 case True{}:
1111 match b4:
1112 case True{}:
1113 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1114 case False{}:
1115 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1116 case False{}:
1117 match b4:
1118 case True{}:
1119 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1120 case False{}:
1121 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{True{}, False{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1122 case False{}:
1123 match b1:
1124 case True{}:
1125 match b2:
1126 case True{}:
1127 match b3:
1128 case True{}:
1129 match b4:
1130 case True{}:
1131 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1132 case False{}:
1133 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1134 case False{}:
1135 match b4:
1136 case True{}:
1137 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1138 case False{}:
1139 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1140 case False{}:
1141 match b3:
1142 case True{}:
1143 match b4:
1144 case True{}:
1145 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1146 case False{}:
1147 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1148 case False{}:
1149 match b4:
1150 case True{}:
1151 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1152 case False{}:
1153 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, True{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1154 case False{}:
1155 match b2:
1156 case True{}:
1157 match b3:
1158 case True{}:
1159 match b4:
1160 case True{}:
1161 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1162 case False{}:
1163 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1164 case False{}:
1165 match b4:
1166 case True{}:
1167 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1168 case False{}:
1169 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, True{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1170 case False{}:
1171 match b3:
1172 case True{}:
1173 match b4:
1174 case True{}:
1175 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1176 case False{}:
1177 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, True{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1178 case False{}:
1179 match b4:
1180 case True{}:
1181 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, True{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))
1182 case False{}:
1183 Empty.absurd({G.Gf8Bits.to(G.Gf8Bits{False{}, False{}, False{}, False{}, False{}, True{}, True{}, True{}}) == 0 : U32}, GT.gt.ft(h))