def wr.m10

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:289

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

289def wr.m10(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat, +x4: Nat, +x5: Nat, +x6: Nat, +x7: Nat, +x8: Nat) -> {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(Nat.add(x3, x4), Nat.add(Nat.add(x5, x6), Nat.mul(x7, x8)))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}:
290  %Equal.sym(Nat, Nat.add(Nat.add(x5, x6), Nat.mul(x7, x8)), Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8))), UL.nat_add_assoc(x5, x6, Nat.mul(x7, x8))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(Nat.add(x3, x4), _)))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
291  %Equal.sym(Nat, Nat.add(Nat.add(x3, x4), Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8)))), Nat.add(x3, Nat.add(x4, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8))))), UL.nat_add_assoc(x3, x4, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, _))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
292  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x3, Nat.add(x4, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8)))))), Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, Nat.add(x4, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8)))))), UL.dbl_add(x1, x3, Nat.add(x4, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8)))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), U.U32Nat.dbl(x1, _)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
293  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x4, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8))))), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8))))), UL.dbl_add(x1, x4, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), _))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
294  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x5, Nat.add(x6, Nat.mul(x7, x8)))), Nat.add(U.U32Nat.dbl(x1, x5), U.U32Nat.dbl(x1, Nat.add(x6, Nat.mul(x7, x8)))), UL.dbl_add(x1, x5, Nat.add(x6, Nat.mul(x7, x8)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, x4), _)))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
295  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x6, Nat.mul(x7, x8))), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8))), UL.dbl_add(x1, x6, Nat.mul(x7, x8))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, x5), _))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
296  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), UL.dbl_add(x1, U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
297  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), UL.dbl_add(x1, U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), _)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
298  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8))))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8))))), UL.dbl_add(x1, U.U32Nat.dbl(x1, x5), Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), _))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
299  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))), UL.dbl_add(x1, U.U32Nat.dbl(x1, x6), U.U32Nat.dbl(x1, Nat.mul(x7, x8)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), _)))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
300  %Equal.sym(Nat, Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))))), Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))))), UL.nat_add_assoc(x0, U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
301  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), Nat.add(Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), UL.nat_add_assoc(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))))) : {Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), _)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
302  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), Nat.add(Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), UL.nat_add_assoc(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))))) : {Nat.add(x0, _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
303  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))), Nat.add(x0, Nat.add(Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))))), UL.nat_add_assoc(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))))) : {_ == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
304  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))), Nat.add(Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))), UL.nat_add_assoc(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8)))))) : {Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))))), _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
305  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x5), U.U32Nat.dbl(x1, x6))), Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x5), U.U32Nat.dbl(x1, x6))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))), UL.dbl_add(x1, U.U32Nat.dbl(x1, x5), U.U32Nat.dbl(x1, x6)))) : {Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))))), Nat.add(_, U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
306  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x5), U.U32Nat.dbl(x1, x6)), U.U32Nat.dbl(x1, Nat.add(x5, x6)), Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x5, x6)), Nat.add(U.U32Nat.dbl(x1, x5), U.U32Nat.dbl(x1, x6)), UL.dbl_add(x1, x5, x6))) : {Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))))), Nat.add(U.U32Nat.dbl(x1, _), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
307  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4))), Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x3)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x4))), UL.dbl_add(x1, U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)))) : {Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), _)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
308  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x2), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)))), U.U32Nat.dbl(x1, Nat.add(x2, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)))), Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x2, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)))), Nat.add(U.U32Nat.dbl(x1, x2), U.U32Nat.dbl(x1, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)))), UL.dbl_add(x1, x2, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4))))) : {Nat.add(Nat.add(x0, _), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
309  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, x3)), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, x3)), Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)), UL.nat_add_comm(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, x3)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(x2, _))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
310  %Equal.sym(Nat, Nat.add(x2, Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, x3))), Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)), Equal.sym(Nat, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)), Nat.add(x2, Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, x3))), UL.nat_add_assoc(x2, U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, x3)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, _)), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, Nat.add(Nat.add(x2, U.U32Nat.dbl(x1, x4)), U.U32Nat.dbl(x1, x3)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.add(x5, x6))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
311  {==}