def ur.r19
bend-osdev-u32@0.1.0.0 · PROOF.bend:1418
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws
1418def ur.r19(+x0: Nat, +x1: Nat, +x2: Nat) -> {Nat.add(Nat.add(x0, x1), Nat.mul(x2, Nat.double(x1))) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}:
1419 %Equal.sym(Nat, Nat.double(x1), Nat.add(x1, x1), Laws.nat_double(x1)) : {Nat.add(Nat.add(x0, x1), Nat.mul(x2, _)) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1420 %Equal.sym(Nat, Nat.mul(x2, Nat.add(x1, x1)), Nat.add(Nat.mul(x2, x1), Nat.mul(x2, x1)), Laws.nat_mul_add(x2, x1, x1)) : {Nat.add(Nat.add(x0, x1), _) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1421 %Equal.sym(Nat, Nat.mul(x2, x1), Nat.mul(x1, x2), Laws.nat_mul_comm(x2, x1)) : {Nat.add(Nat.add(x0, x1), Nat.add(_, Nat.mul(x2, x1))) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1422 %Equal.sym(Nat, Nat.mul(x2, x1), Nat.mul(x1, x2), Laws.nat_mul_comm(x2, x1)) : {Nat.add(Nat.add(x0, x1), Nat.add(Nat.mul(x1, x2), _)) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1423 %Equal.sym(Nat, Nat.add(Nat.add(x0, x1), Nat.add(Nat.mul(x1, x2), Nat.mul(x1, x2))), Nat.add(x0, Nat.add(x1, Nat.add(Nat.mul(x1, x2), Nat.mul(x1, x2)))), Laws.nat_add_assoc(x0, x1, Nat.add(Nat.mul(x1, x2), Nat.mul(x1, x2)))) : {_ == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1424 %Equal.sym(Nat, Nat.mul(x1, x2), Nat.mul(x2, x1), Equal.sym(Nat, Nat.mul(x2, x1), Nat.mul(x1, x2), Laws.nat_mul_comm(x2, x1))) : {Nat.add(x0, Nat.add(x1, Nat.add(Nat.mul(x1, x2), _))) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1425 %Equal.sym(Nat, Nat.mul(x1, x2), Nat.mul(x2, x1), Equal.sym(Nat, Nat.mul(x2, x1), Nat.mul(x1, x2), Laws.nat_mul_comm(x2, x1))) : {Nat.add(x0, Nat.add(x1, Nat.add(_, Nat.mul(x2, x1)))) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1426 %Equal.sym(Nat, x1, Nat.mul(1n, x1), Equal.sym(Nat, Nat.mul(1n, x1), x1, Laws.nat_one_mul(x1))) : {Nat.add(x0, Nat.add(_, Nat.add(Nat.mul(x2, x1), Nat.mul(x2, x1)))) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1427 %Equal.sym(Nat, Nat.add(Nat.mul(x2, x1), Nat.mul(x2, x1)), Nat.mul(Nat.add(x2, x2), x1), Equal.sym(Nat, Nat.mul(Nat.add(x2, x2), x1), Nat.add(Nat.mul(x2, x1), Nat.mul(x2, x1)), Laws.nat_add_mul(x2, x2, x1))) : {Nat.add(x0, Nat.add(Nat.mul(1n, x1), _)) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1428 %Equal.sym(Nat, Nat.add(Nat.mul(1n, x1), Nat.mul(Nat.add(x2, x2), x1)), Nat.mul(Nat.add(1n, Nat.add(x2, x2)), x1), Equal.sym(Nat, Nat.mul(Nat.add(1n, Nat.add(x2, x2)), x1), Nat.add(Nat.mul(1n, x1), Nat.mul(Nat.add(x2, x2), x1)), Laws.nat_add_mul(1n, Nat.add(x2, x2), x1))) : {Nat.add(x0, _) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1429 %Equal.sym(Nat, Nat.add(x2, x2), Nat.double(x2), Equal.sym(Nat, Nat.double(x2), Nat.add(x2, x2), Laws.nat_double(x2))) : {Nat.add(x0, Nat.mul(Nat.add(1n, _), x1)) == Nat.add(x0, Nat.mul(1n+Nat.double(x2), x1)) : Nat}
1430 {==}