def exp_log_rs.bits
bend-osdev-gf@0.1.1.0 · PROOF.bend:6276
import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
6276def exp_log_rs.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.rs(), G.Gf8.log(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})) : U32}:
6277 match b0:
6278 case True{}:
6279 match b1:
6280 case True{}:
6281 match b2:
6282 case True{}:
6283 match b3:
6284 case True{}:
6285 match b4:
6286 case True{}:
6287 exp_log_rs.s11111(b5, b6, b7)
6288 case False{}:
6289 exp_log_rs.s11110(b5, b6, b7)
6290 case False{}:
6291 match b4:
6292 case True{}:
6293 exp_log_rs.s11101(b5, b6, b7)
6294 case False{}:
6295 exp_log_rs.s11100(b5, b6, b7)
6296 case False{}:
6297 match b3:
6298 case True{}:
6299 match b4:
6300 case True{}:
6301 exp_log_rs.s11011(b5, b6, b7)
6302 case False{}:
6303 exp_log_rs.s11010(b5, b6, b7)
6304 case False{}:
6305 match b4:
6306 case True{}:
6307 exp_log_rs.s11001(b5, b6, b7)
6308 case False{}:
6309 exp_log_rs.s11000(b5, b6, b7)
6310 case False{}:
6311 match b2:
6312 case True{}:
6313 match b3:
6314 case True{}:
6315 match b4:
6316 case True{}:
6317 exp_log_rs.s10111(b5, b6, b7)
6318 case False{}:
6319 exp_log_rs.s10110(b5, b6, b7)
6320 case False{}:
6321 match b4:
6322 case True{}:
6323 exp_log_rs.s10101(b5, b6, b7)
6324 case False{}:
6325 exp_log_rs.s10100(b5, b6, b7)
6326 case False{}:
6327 match b3:
6328 case True{}:
6329 match b4:
6330 case True{}:
6331 exp_log_rs.s10011(b5, b6, b7)
6332 case False{}:
6333 exp_log_rs.s10010(b5, b6, b7)
6334 case False{}:
6335 match b4:
6336 case True{}:
6337 exp_log_rs.s10001(b5, b6, b7)
6338 case False{}:
6339 exp_log_rs.s10000(b5, b6, b7)
6340 case False{}:
6341 match b1:
6342 case True{}:
6343 match b2:
6344 case True{}:
6345 match b3:
6346 case True{}:
6347 match b4:
6348 case True{}:
6349 exp_log_rs.s01111(b5, b6, b7)
6350 case False{}:
6351 exp_log_rs.s01110(b5, b6, b7)
6352 case False{}:
6353 match b4:
6354 case True{}:
6355 exp_log_rs.s01101(b5, b6, b7)
6356 case False{}:
6357 exp_log_rs.s01100(b5, b6, b7)
6358 case False{}:
6359 match b3:
6360 case True{}:
6361 match b4:
6362 case True{}:
6363 exp_log_rs.s01011(b5, b6, b7)
6364 case False{}:
6365 exp_log_rs.s01010(b5, b6, b7)
6366 case False{}:
6367 match b4:
6368 case True{}:
6369 exp_log_rs.s01001(b5, b6, b7)
6370 case False{}:
6371 exp_log_rs.s01000(b5, b6, b7)
6372 case False{}:
6373 match b2:
6374 case True{}:
6375 match b3:
6376 case True{}:
6377 match b4:
6378 case True{}:
6379 exp_log_rs.s00111(b5, b6, b7)
6380 case False{}:
6381 exp_log_rs.s00110(b5, b6, b7)
6382 case False{}:
6383 match b4:
6384 case True{}:
6385 exp_log_rs.s00101(b5, b6, b7)
6386 case False{}:
6387 exp_log_rs.s00100(b5, b6, b7)
6388 case False{}:
6389 match b3:
6390 case True{}:
6391 match b4:
6392 case True{}:
6393 exp_log_rs.s00011(b5, b6, b7)
6394 case False{}:
6395 exp_log_rs.s00010(b5, b6, b7)
6396 case False{}:
6397 match b4:
6398 case True{}:
6399 exp_log_rs.s00001(b5, b6, b7)
6400 case False{}:
6401 exp_log_rs.s00000(b5, b6, b7)