def ur.r9

bend-osdev-u32@0.1.0.0 · PROOF.bend:1236

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 Laws

1236def ur.r9(+x0: Nat, +x1: Nat, +x2: Nat) -> {Nat.add(x0, U.U32Nat.dbl(x1, x2)) == Nat.add(Nat.mul(x2, U.U32Nat.dbl(x1, 1n)), x0) : Nat}:
1237  %Equal.sym(Nat, Nat.add(x0, U.U32Nat.dbl(x1, x2)), Nat.add(U.U32Nat.dbl(x1, x2), x0), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x1, x2), x0), Nat.add(x0, U.U32Nat.dbl(x1, x2)), Laws.nat_add_comm(U.U32Nat.dbl(x1, x2), x0))) : {_ == Nat.add(Nat.mul(x2, U.U32Nat.dbl(x1, 1n)), x0) : Nat}
1238  %Equal.sym(Nat, x2, Nat.mul(1n, x2), Equal.sym(Nat, Nat.mul(1n, x2), x2, Laws.nat_one_mul(x2))) : {Nat.add(U.U32Nat.dbl(x1, _), x0) == Nat.add(Nat.mul(x2, U.U32Nat.dbl(x1, 1n)), x0) : Nat}
1239  %Equal.sym(Nat, Nat.mul(1n, x2), Nat.mul(x2, 1n), Equal.sym(Nat, Nat.mul(x2, 1n), Nat.mul(1n, x2), Laws.nat_mul_comm(x2, 1n))) : {Nat.add(U.U32Nat.dbl(x1, _), x0) == Nat.add(Nat.mul(x2, U.U32Nat.dbl(x1, 1n)), x0) : Nat}
1240  %Equal.sym(Nat, U.U32Nat.dbl(x1, Nat.mul(x2, 1n)), Nat.mul(x2, U.U32Nat.dbl(x1, 1n)), Equal.sym(Nat, Nat.mul(x2, U.U32Nat.dbl(x1, 1n)), U.U32Nat.dbl(x1, Nat.mul(x2, 1n)), Laws.dbl_mul_r(x1, x2, 1n))) : {Nat.add(_, x0) == Nat.add(Nat.mul(x2, U.U32Nat.dbl(x1, 1n)), x0) : Nat}
1241  {==}