def wr.m12

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

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

319def wr.m12(+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, Nat.add(Nat.add(x2, x3), x4))), 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}:
320  %Equal.sym(Nat, Nat.add(Nat.add(x2, x3), x4), Nat.add(x2, Nat.add(x3, x4)), UL.nat_add_assoc(x2, x3, x4)) : {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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
321  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x2, Nat.add(x3, x4))), Nat.add(U.U32Nat.dbl(x1, x2), U.U32Nat.dbl(x1, Nat.add(x3, x4))), UL.dbl_add(x1, x2, Nat.add(x3, 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
322  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x3, x4)), Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, x4)), UL.dbl_add(x1, x3, 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
323  %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, x3), 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
324  %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, x3), 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
325  %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, x3), U.U32Nat.dbl(x1, x4)))), _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
326  %Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, x3), 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, x3), 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, x3), 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
327  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, x3), 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, x3), 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, x3), 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
328  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x1, x3), 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, x3), Nat.add(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, x3), 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
329  %Equal.sym(Nat, Nat.add(x0, Nat.add(U.U32Nat.dbl(x1, x2), Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(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, x2)), Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(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, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(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, x3), Nat.add(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, x3), Nat.add(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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
330  %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, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, x4), _))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
331  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x4), 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(Nat.add(U.U32Nat.dbl(x1, x4), 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, x4), 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, x4), 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))))), UL.nat_add_assoc(U.U32Nat.dbl(x1, x4), 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(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, x3), _)) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
332  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(Nat.add(U.U32Nat.dbl(x1, x4), 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(Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, x4), 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, x3), Nat.add(U.U32Nat.dbl(x1, x4), 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, x3), Nat.add(Nat.add(U.U32Nat.dbl(x1, x4), 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))))), UL.nat_add_assoc(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, x4), 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(Nat.add(x0, U.U32Nat.dbl(x1, x2)), _) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
333  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)))), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)))), Nat.add(U.U32Nat.dbl(x1, x4), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)))), UL.nat_add_left_comm(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, x3), _), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
334  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))))), Nat.add(Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5))), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5))), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)))), Nat.add(U.U32Nat.dbl(x1, x3), Nat.add(U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))))), UL.nat_add_assoc(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5)), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6)))))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(_, U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
335  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6))), Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6))), Nat.add(U.U32Nat.dbl(x1, x4), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x6))), UL.dbl_add(x1, x4, U.U32Nat.dbl(x1, x6)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5))), _), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) == Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
336  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), Nat.add(U.U32Nat.dbl(x1, x3), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, x5))), UL.dbl_add(x1, x3, U.U32Nat.dbl(x1, x5)))) : {Nat.add(Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(Nat.add(_, U.U32Nat.dbl(x1, Nat.add(x4, 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, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x1, Nat.add(x3, U.U32Nat.dbl(x1, x5))), U.U32Nat.dbl(x1, Nat.add(x4, U.U32Nat.dbl(x1, x6)))), U.U32Nat.dbl(x1, U.U32Nat.dbl(x1, Nat.mul(x7, x8))))) : Nat}
337  {==}