def ur.r26

bend-osdev-u32@0.1.0.0 · PROOF.bend:1545
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

1545def ur.r26(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat, +x4: Nat, +x5: Nat) -> {Nat.add(Nat.add(Nat.add(x0, x1), Nat.add(Nat.double(x2), 1n+x3)), 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}:
1546  %Equal.sym(Nat, Nat.double(x2), Nat.add(x2, x2), Laws.nat_double(x2)) : {Nat.add(Nat.add(Nat.add(x0, x1), Nat.add(_, 1n+x3)), 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1547  %Equal.sym(Nat, Nat.add(Nat.add(x2, x2), Nat.add(1n, x3)), Nat.add(x2, Nat.add(x2, Nat.add(1n, x3))), Laws.nat_add_assoc(x2, x2, Nat.add(1n, x3))) : {Nat.add(Nat.add(Nat.add(x0, x1), _), 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1548  %Equal.sym(Nat, Nat.add(x2, Nat.add(1n, x3)), Nat.add(1n, Nat.add(x2, x3)), Laws.nat_add_left_comm(x2, 1n, x3)) : {Nat.add(Nat.add(Nat.add(x0, x1), Nat.add(x2, _)), 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1549  %Equal.sym(Nat, Nat.add(x2, Nat.add(1n, Nat.add(x2, x3))), Nat.add(1n, Nat.add(x2, Nat.add(x2, x3))), Laws.nat_add_left_comm(x2, 1n, Nat.add(x2, x3))) : {Nat.add(Nat.add(Nat.add(x0, x1), _), 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1550  %Equal.sym(Nat, Nat.add(Nat.add(x0, x1), Nat.add(1n, Nat.add(x2, Nat.add(x2, x3)))), Nat.add(x0, Nat.add(x1, Nat.add(1n, Nat.add(x2, Nat.add(x2, x3))))), Laws.nat_add_assoc(x0, x1, Nat.add(1n, Nat.add(x2, Nat.add(x2, x3))))) : {Nat.add(_, 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1551  %Equal.sym(Nat, Nat.add(x1, Nat.add(1n, Nat.add(x2, Nat.add(x2, x3)))), Nat.add(1n, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3)))), Laws.nat_add_left_comm(x1, 1n, Nat.add(x2, Nat.add(x2, x3)))) : {Nat.add(Nat.add(x0, _), 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1552  %Equal.sym(Nat, Nat.add(x0, Nat.add(1n, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))))), Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))))), Laws.nat_add_left_comm(x0, 1n, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))))) : {Nat.add(_, 1n+Nat.add(x4, Nat.double(x5))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1553  %Equal.sym(Nat, Nat.double(x5), Nat.add(x5, x5), Laws.nat_double(x5)) : {Nat.add(Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))))), Nat.add(1n, Nat.add(x4, _))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1554  %Equal.sym(Nat, Nat.add(Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))))), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5)))), Nat.add(1n, Nat.add(Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3)))), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))), Laws.nat_add_assoc(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3)))), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))) : {_ == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1555  %Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3)))), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5)))), Nat.add(x0, Nat.add(Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))), Laws.nat_add_assoc(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))) : {Nat.add(1n, _) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1556  %Equal.sym(Nat, Nat.add(Nat.add(x1, Nat.add(x2, Nat.add(x2, x3))), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5)))), Nat.add(x1, Nat.add(Nat.add(x2, Nat.add(x2, x3)), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))), Laws.nat_add_assoc(x1, Nat.add(x2, Nat.add(x2, x3)), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))) : {Nat.add(1n, Nat.add(x0, _)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1557  %Equal.sym(Nat, Nat.add(Nat.add(x2, Nat.add(x2, x3)), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5)))), Nat.add(x2, Nat.add(Nat.add(x2, x3), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))), Laws.nat_add_assoc(x2, Nat.add(x2, x3), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))) : {Nat.add(1n, Nat.add(x0, Nat.add(x1, _))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1558  %Equal.sym(Nat, Nat.add(Nat.add(x2, x3), Nat.add(1n, Nat.add(x4, Nat.add(x5, x5)))), Nat.add(x2, Nat.add(x3, Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))), Laws.nat_add_assoc(x2, x3, Nat.add(1n, Nat.add(x4, Nat.add(x5, x5))))) : {Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, _)))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1559  %Equal.sym(Nat, Nat.add(x3, Nat.add(1n, Nat.add(x4, Nat.add(x5, x5)))), Nat.add(1n, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))), Laws.nat_add_left_comm(x3, 1n, Nat.add(x4, Nat.add(x5, x5)))) : {Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, _))))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1560  %Equal.sym(Nat, Nat.add(x2, Nat.add(1n, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))), Nat.add(1n, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))), Laws.nat_add_left_comm(x2, 1n, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))) : {Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, _)))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1561  %Equal.sym(Nat, Nat.add(x2, Nat.add(1n, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))), Nat.add(1n, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))), Laws.nat_add_left_comm(x2, 1n, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))) : {Nat.add(1n, Nat.add(x0, Nat.add(x1, _))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1562  %Equal.sym(Nat, Nat.add(x1, Nat.add(1n, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))))), Nat.add(1n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))))), Laws.nat_add_left_comm(x1, 1n, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))))) : {Nat.add(1n, Nat.add(x0, _)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1563  %Equal.sym(Nat, Nat.add(x0, Nat.add(1n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))))), Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))))), Laws.nat_add_left_comm(x0, 1n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))))) : {Nat.add(1n, _) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1564  %Equal.sym(Nat, Nat.add(1n, Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))))))), Nat.add(Nat.add(1n, 1n), Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))))), Equal.sym(Nat, Nat.add(Nat.add(1n, 1n), Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))))), Nat.add(1n, Nat.add(1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5))))))))), Laws.nat_add_assoc(1n, 1n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, Nat.add(x4, Nat.add(x5, x5)))))))))) : {_ == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1565  %Equal.sym(Nat, Nat.add(x4, Nat.add(x5, x5)), Nat.add(x5, Nat.add(x4, x5)), Equal.sym(Nat, Nat.add(x5, Nat.add(x4, x5)), Nat.add(x4, Nat.add(x5, x5)), Laws.nat_add_left_comm(x5, x4, x5))) : {Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x3, _)))))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1566  %Equal.sym(Nat, Nat.add(x3, Nat.add(x5, Nat.add(x4, x5))), Nat.add(x5, Nat.add(x3, Nat.add(x4, x5))), Equal.sym(Nat, Nat.add(x5, Nat.add(x3, Nat.add(x4, x5))), Nat.add(x3, Nat.add(x5, Nat.add(x4, x5))), Laws.nat_add_left_comm(x5, x3, Nat.add(x4, x5)))) : {Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, _))))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1567  %Equal.sym(Nat, Nat.add(x4, x5), Nat.add(x5, x4), Equal.sym(Nat, Nat.add(x5, x4), Nat.add(x4, x5), Laws.nat_add_comm(x5, x4))) : {Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, Nat.add(x3, _))))))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1568  %Equal.sym(Nat, Nat.add(x3, Nat.add(x5, x4)), Nat.add(x5, Nat.add(x3, x4)), Equal.sym(Nat, Nat.add(x5, Nat.add(x3, x4)), Nat.add(x3, Nat.add(x5, x4)), Laws.nat_add_left_comm(x5, x3, x4))) : {Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, _)))))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1569  %Equal.sym(Nat, Nat.add(x5, Nat.add(x5, Nat.add(x3, x4))), Nat.add(Nat.add(x5, x5), Nat.add(x3, x4)), Equal.sym(Nat, Nat.add(Nat.add(x5, x5), Nat.add(x3, x4)), Nat.add(x5, Nat.add(x5, Nat.add(x3, x4))), Laws.nat_add_assoc(x5, x5, Nat.add(x3, x4)))) : {Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, _))))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1570  %Equal.sym(Nat, Nat.add(x2, Nat.add(Nat.add(x5, x5), Nat.add(x3, x4))), Nat.add(Nat.add(x2, Nat.add(x5, x5)), Nat.add(x3, x4)), Equal.sym(Nat, Nat.add(Nat.add(x2, Nat.add(x5, x5)), Nat.add(x3, x4)), Nat.add(x2, Nat.add(Nat.add(x5, x5), Nat.add(x3, x4))), Laws.nat_add_assoc(x2, Nat.add(x5, x5), Nat.add(x3, x4)))) : {Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, _)))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1571  %Equal.sym(Nat, Nat.add(x2, Nat.add(Nat.add(x2, Nat.add(x5, x5)), Nat.add(x3, x4))), Nat.add(Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))), Nat.add(x3, x4)), Equal.sym(Nat, Nat.add(Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))), Nat.add(x3, x4)), Nat.add(x2, Nat.add(Nat.add(x2, Nat.add(x5, x5)), Nat.add(x3, x4))), Laws.nat_add_assoc(x2, Nat.add(x2, Nat.add(x5, x5)), Nat.add(x3, x4)))) : {Nat.add(2n, Nat.add(x0, Nat.add(x1, _))) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1572  %Equal.sym(Nat, Nat.add(x1, Nat.add(Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))), Nat.add(x3, x4))), Nat.add(Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Nat.add(x3, x4)), Equal.sym(Nat, Nat.add(Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Nat.add(x3, x4)), Nat.add(x1, Nat.add(Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))), Nat.add(x3, x4))), Laws.nat_add_assoc(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))), Nat.add(x3, x4)))) : {Nat.add(2n, Nat.add(x0, _)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1573  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Nat.add(x3, x4))), Nat.add(Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(x3, x4)), Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(x3, x4)), Nat.add(x0, Nat.add(Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Nat.add(x3, x4))), Laws.nat_add_assoc(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Nat.add(x3, x4)))) : {Nat.add(2n, _) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1574  %Equal.sym(Nat, Nat.add(2n, Nat.add(Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(x3, x4))), Nat.add(Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Nat.add(x3, x4)), Equal.sym(Nat, Nat.add(Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Nat.add(x3, x4)), Nat.add(2n, Nat.add(Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(x3, x4))), Laws.nat_add_assoc(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(x3, x4)))) : {_ == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1575  %Equal.sym(Nat, Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Nat.add(x0, Nat.add(2n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Equal.sym(Nat, Nat.add(x0, Nat.add(2n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Nat.add(2n, Nat.add(x0, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Laws.nat_add_left_comm(x0, 2n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))))) : {Nat.add(_, Nat.add(x3, x4)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1576  %Equal.sym(Nat, Nat.add(2n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(x1, Nat.add(2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Equal.sym(Nat, Nat.add(x1, Nat.add(2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(2n, Nat.add(x1, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Laws.nat_add_left_comm(x1, 2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))) : {Nat.add(Nat.add(x0, _), Nat.add(x3, x4)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1577  %Equal.sym(Nat, Nat.add(x0, Nat.add(x1, Nat.add(2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Nat.add(Nat.add(x0, x1), Nat.add(2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Equal.sym(Nat, Nat.add(Nat.add(x0, x1), Nat.add(2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(x0, Nat.add(x1, Nat.add(2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))))), Laws.nat_add_assoc(x0, x1, Nat.add(2n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))))) : {Nat.add(_, Nat.add(x3, x4)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1578  %Equal.sym(Nat, Nat.add(Nat.add(1n, 1n), Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Nat.add(1n, Nat.add(1n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Equal.sym(Nat, Nat.add(1n, Nat.add(1n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Nat.add(Nat.add(1n, 1n), Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Equal.sym(Nat, Nat.add(Nat.add(1n, 1n), Nat.add(x2, Nat.add(x2, Nat.add(x5, x5)))), Nat.add(1n, Nat.add(1n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))), Laws.nat_add_assoc(1n, 1n, Nat.add(x2, Nat.add(x2, Nat.add(x5, x5))))))) : {Nat.add(Nat.add(Nat.add(x0, x1), _), Nat.add(x3, x4)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1579  %Equal.sym(Nat, Nat.add(x2, Nat.add(x5, x5)), Nat.add(x5, Nat.add(x2, x5)), Equal.sym(Nat, Nat.add(x5, Nat.add(x2, x5)), Nat.add(x2, Nat.add(x5, x5)), Laws.nat_add_left_comm(x5, x2, x5))) : {Nat.add(Nat.add(Nat.add(x0, x1), Nat.add(1n, Nat.add(1n, Nat.add(x2, _)))), Nat.add(x3, x4)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1580  %Equal.sym(Nat, Nat.add(x2, Nat.add(x5, Nat.add(x2, x5))), Nat.add(Nat.add(x2, x5), Nat.add(x2, x5)), Equal.sym(Nat, Nat.add(Nat.add(x2, x5), Nat.add(x2, x5)), Nat.add(x2, Nat.add(x5, Nat.add(x2, x5))), Laws.nat_add_assoc(x2, x5, Nat.add(x2, x5)))) : {Nat.add(Nat.add(Nat.add(x0, x1), Nat.add(1n, Nat.add(1n, _))), Nat.add(x3, x4)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1581  %Equal.sym(Nat, Nat.add(Nat.add(x2, x5), Nat.add(x2, x5)), Nat.double(Nat.add(x2, x5)), Equal.sym(Nat, Nat.double(Nat.add(x2, x5)), Nat.add(Nat.add(x2, x5), Nat.add(x2, x5)), Laws.nat_double(Nat.add(x2, x5)))) : {Nat.add(Nat.add(Nat.add(x0, x1), Nat.add(1n, Nat.add(1n, _))), Nat.add(x3, x4)) == Nat.add(Nat.add(Nat.add(x0, x1), 2n+Nat.double(Nat.add(x2, x5))), Nat.add(x3, x4)) : Nat}
1582  {==}
Uses (8)

Used by (1)

bend-osdev-u32@0.1.0.0/PROOF:ud.k