def dexp_z

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divx.bend:9

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR

9def dexp_z(+dp: Nat, +P: Nat, +u: Nat, +K: Nat, +sx: Nat, +sy: Nat, +hc: {Nat.add(dp, P) == 200n : Nat}, +hb: {Nat.add(62n, u) == Nat.add(sy, P) : Nat}, +hf: {Nat.add(u, K) == Nat.add(sx, 1022n) : Nat}) -> {Nat.add(sx, Nat.add(dp, 884n)) == Nat.add(sy, K) : Nat}:
10  +a = Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, P), Nat.add(sx, Nat.add(u, 884n))), Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Nat.add(Nat.add(dp, P), Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(P, u)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 884n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(dp, 884n), Nat.add(dp, 884n), Equal.trans(Nat, Nat.add(dp, 884n), Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, 884n), Equal.cong(Nat, Nat, z => Nat.add(z, 884n), dp, Nat.add(dp, 0n), Equal.sym(Nat, Nat.add(dp, 0n), dp, N.add_zero(dp))), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, Nat.add(0n, 884n)), Nat.add(dp, 884n), NA.add_assoc(dp, 0n, 884n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 884n))), Nat.add(sx, Nat.add(dp, 884n)), NA.add_assoc(sx, 0n, Nat.add(dp, 884n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 884n)), Nat.add(dp, 884n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(0n, 884n)), Nat.add(dp, 884n), NA.add_swap(0n, dp, 884n), {==}))), NA.add_swap(sx, dp, 884n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(dp, Nat.add(sx, 884n)), z), Nat.add(P, u), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, u), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, 0n), z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)))), Equal.trans(Nat, Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_assoc(P, 0n, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(dp, Nat.add(P, Nat.add(sx, Nat.add(u, 884n)))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(dp, Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n)))), Nat.add(dp, Nat.add(P, Nat.add(sx, Nat.add(u, 884n)))), NA.add_assoc(dp, Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sx, Nat.add(P, Nat.add(u, 884n))), Nat.add(P, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sx, Nat.add(884n, Nat.add(P, Nat.add(u, 0n)))), Nat.add(sx, Nat.add(P, Nat.add(u, 884n))), NA.add_assoc(sx, 884n, Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(884n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 884n)), Equal.trans(Nat, Nat.add(884n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(884n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 884n)), NA.add_swap(884n, P, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(884n, Nat.add(u, 0n)), Nat.add(u, 884n), Equal.trans(Nat, Nat.add(884n, Nat.add(u, 0n)), Nat.add(u, Nat.add(884n, 0n)), Nat.add(u, 884n), NA.add_swap(884n, u, 0n), {==}))))), NA.add_swap(sx, P, Nat.add(u, 884n))))), NA.add_swap(dp, P, Nat.add(sx, Nat.add(u, 884n))))), Equal.sym(Nat, Nat.add(Nat.add(dp, P), Nat.add(sx, Nat.add(u, 884n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(dp, P), Nat.add(sx, Nat.add(u, 884n))), Nat.add(Nat.add(P, Nat.add(dp, 0n)), Nat.add(sx, Nat.add(u, 884n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(dp, P), Nat.add(sx, Nat.add(u, 884n))), Nat.add(Nat.add(P, Nat.add(dp, 0n)), Nat.add(sx, Nat.add(u, 884n))), Nat.add(Nat.add(P, Nat.add(dp, 0n)), Nat.add(sx, Nat.add(u, 884n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(u, 884n))), Nat.add(dp, P), Nat.add(P, Nat.add(dp, 0n)), Equal.trans(Nat, Nat.add(dp, P), Nat.add(Nat.add(dp, 0n), Nat.add(P, 0n)), Nat.add(P, Nat.add(dp, 0n)), Equal.trans(Nat, Nat.add(dp, P), Nat.add(Nat.add(dp, 0n), P), Nat.add(Nat.add(dp, 0n), Nat.add(P, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, P), dp, Nat.add(dp, 0n), Equal.sym(Nat, Nat.add(dp, 0n), dp, N.add_zero(dp))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(dp, 0n), z), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P)))), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), Nat.add(P, 0n)), Nat.add(dp, Nat.add(P, 0n)), Nat.add(P, Nat.add(dp, 0n)), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), Nat.add(P, 0n)), Nat.add(dp, Nat.add(0n, Nat.add(P, 0n))), Nat.add(dp, Nat.add(P, 0n)), NA.add_assoc(dp, 0n, Nat.add(P, 0n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(P, 0n)), Nat.add(P, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(P, 0n)), Nat.add(P, Nat.add(0n, 0n)), Nat.add(P, 0n), NA.add_swap(0n, P, 0n), {==}))), NA.add_swap(dp, P, 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, Nat.add(dp, 0n)), z), Nat.add(sx, Nat.add(u, 884n)), Nat.add(sx, Nat.add(u, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Nat.add(sx, Nat.add(u, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(u, 884n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(u, 884n), Nat.add(u, 884n), Equal.trans(Nat, Nat.add(u, 884n), Nat.add(Nat.add(u, 0n), 884n), Nat.add(u, 884n), Equal.cong(Nat, Nat, z => Nat.add(z, 884n), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), 884n), Nat.add(u, Nat.add(0n, 884n)), Nat.add(u, 884n), NA.add_assoc(u, 0n, 884n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Nat.add(sx, Nat.add(0n, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 884n)), NA.add_assoc(sx, 0n, Nat.add(u, 884n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(u, 884n)), Nat.add(u, 884n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 884n)), Nat.add(u, Nat.add(0n, 884n)), Nat.add(u, 884n), NA.add_swap(0n, u, 884n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(dp, 0n)), Nat.add(sx, Nat.add(u, 884n))), Nat.add(P, Nat.add(Nat.add(dp, 0n), Nat.add(sx, Nat.add(u, 884n)))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), NA.add_assoc(P, Nat.add(dp, 0n), Nat.add(sx, Nat.add(u, 884n))), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(Nat.add(dp, 0n), Nat.add(sx, Nat.add(u, 884n))), Nat.add(dp, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), Nat.add(sx, Nat.add(u, 884n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, Nat.add(u, 884n)))), Nat.add(dp, Nat.add(sx, Nat.add(u, 884n))), NA.add_assoc(dp, 0n, Nat.add(sx, Nat.add(u, 884n))), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 884n)), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(sx, Nat.add(0n, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 884n)), NA.add_swap(0n, sx, Nat.add(u, 884n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(u, 884n)), Nat.add(u, 884n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 884n)), Nat.add(u, Nat.add(0n, 884n)), Nat.add(u, 884n), NA.add_swap(0n, u, 884n), {==})))))))))), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.add(sx, Nat.add(u, 884n))), Nat.add(dp, P), 200n, hc)), Equal.trans(Nat, Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 1084n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 1084n)), Equal.cong(Nat, Nat, z => Nat.add(200n, z), Nat.add(sx, Nat.add(u, 884n)), Nat.add(sx, Nat.add(u, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Nat.add(sx, Nat.add(u, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(u, 884n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(u, 884n), Nat.add(u, 884n), Equal.trans(Nat, Nat.add(u, 884n), Nat.add(Nat.add(u, 0n), 884n), Nat.add(u, 884n), Equal.cong(Nat, Nat, z => Nat.add(z, 884n), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), 884n), Nat.add(u, Nat.add(0n, 884n)), Nat.add(u, 884n), NA.add_assoc(u, 0n, 884n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(u, 884n)), Nat.add(sx, Nat.add(0n, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 884n)), NA.add_assoc(sx, 0n, Nat.add(u, 884n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(u, 884n)), Nat.add(u, 884n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 884n)), Nat.add(u, Nat.add(0n, 884n)), Nat.add(u, 884n), NA.add_swap(0n, u, 884n), {==}))))), Equal.trans(Nat, Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(sx, Nat.add(200n, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 1084n)), NA.add_swap(200n, sx, Nat.add(u, 884n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(200n, Nat.add(u, 884n)), Nat.add(u, 1084n), Equal.trans(Nat, Nat.add(200n, Nat.add(u, 884n)), Nat.add(u, Nat.add(200n, 884n)), Nat.add(u, 1084n), NA.add_swap(200n, u, 884n), {==})))), Equal.sym(Nat, Nat.add(sx, Nat.add(u, 1084n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 1084n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 1084n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(u, 1084n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(u, 1084n), Nat.add(u, 1084n), Equal.trans(Nat, Nat.add(u, 1084n), Nat.add(Nat.add(u, 0n), 1084n), Nat.add(u, 1084n), Equal.cong(Nat, Nat, z => Nat.add(z, 1084n), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), 1084n), Nat.add(u, Nat.add(0n, 1084n)), Nat.add(u, 1084n), NA.add_assoc(u, 0n, 1084n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Nat.add(sx, Nat.add(0n, Nat.add(u, 1084n))), Nat.add(sx, Nat.add(u, 1084n)), NA.add_assoc(sx, 0n, Nat.add(u, 1084n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(u, 1084n)), Nat.add(u, 1084n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 1084n)), Nat.add(u, Nat.add(0n, 1084n)), Nat.add(u, 1084n), NA.add_swap(0n, u, 1084n), {==})))))))
11  +b = Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(62n, u), Nat.add(sx, 1022n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(62n, u), Nat.add(u, K)), Nat.add(Nat.add(62n, u), Nat.add(sx, 1022n)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(sy, P), Nat.add(u, K)), Nat.add(Nat.add(62n, u), Nat.add(u, K)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Nat.add(Nat.add(sy, P), Nat.add(u, K)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(P, u)), Nat.add(sy, K), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, K), sy, Nat.add(sy, 0n), Equal.sym(Nat, Nat.add(sy, 0n), sy, N.add_zero(sy))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sy, 0n), z), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 0n))), Nat.add(sy, Nat.add(K, 0n)), NA.add_assoc(sy, 0n, Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, Nat.add(0n, 0n)), Nat.add(K, 0n), NA.add_swap(0n, K, 0n), {==}))), NA.add_swap(sy, K, 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(K, Nat.add(sy, 0n)), z), Nat.add(P, u), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, u), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, 0n), z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)))), Equal.trans(Nat, Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_assoc(P, 0n, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(K, Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n)))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), NA.add_assoc(K, Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sy, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sy, Nat.add(0n, Nat.add(P, Nat.add(u, 0n)))), Nat.add(sy, Nat.add(P, Nat.add(u, 0n))), NA.add_assoc(sy, 0n, Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_swap(0n, P, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==}))))), NA.add_swap(sy, P, Nat.add(u, 0n)))))), Equal.sym(Nat, Nat.add(Nat.add(sy, P), Nat.add(u, K)), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, P), Nat.add(u, K)), Nat.add(Nat.add(P, Nat.add(sy, 0n)), Nat.add(K, Nat.add(u, 0n))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, P), Nat.add(u, K)), Nat.add(Nat.add(P, Nat.add(sy, 0n)), Nat.add(u, K)), Nat.add(Nat.add(P, Nat.add(sy, 0n)), Nat.add(K, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(u, K)), Nat.add(sy, P), Nat.add(P, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, P), Nat.add(Nat.add(sy, 0n), Nat.add(P, 0n)), Nat.add(P, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, P), Nat.add(Nat.add(sy, 0n), P), Nat.add(Nat.add(sy, 0n), Nat.add(P, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, P), sy, Nat.add(sy, 0n), Equal.sym(Nat, Nat.add(sy, 0n), sy, N.add_zero(sy))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sy, 0n), z), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(P, 0n)), Nat.add(sy, Nat.add(P, 0n)), Nat.add(P, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(P, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(P, 0n))), Nat.add(sy, Nat.add(P, 0n)), NA.add_assoc(sy, 0n, Nat.add(P, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(P, 0n)), Nat.add(P, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(P, 0n)), Nat.add(P, Nat.add(0n, 0n)), Nat.add(P, 0n), NA.add_swap(0n, P, 0n), {==}))), NA.add_swap(sy, P, 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, Nat.add(sy, 0n)), z), Nat.add(u, K), Nat.add(K, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(u, K), Nat.add(Nat.add(u, 0n), Nat.add(K, 0n)), Nat.add(K, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(u, K), Nat.add(Nat.add(u, 0n), K), Nat.add(Nat.add(u, 0n), Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, K), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(u, 0n), z), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K)))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), Nat.add(K, 0n)), Nat.add(u, Nat.add(K, 0n)), Nat.add(K, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), Nat.add(K, 0n)), Nat.add(u, Nat.add(0n, Nat.add(K, 0n))), Nat.add(u, Nat.add(K, 0n)), NA.add_assoc(u, 0n, Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(u, z), Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, Nat.add(0n, 0n)), Nat.add(K, 0n), NA.add_swap(0n, K, 0n), {==}))), NA.add_swap(u, K, 0n))))), Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(sy, 0n)), Nat.add(K, Nat.add(u, 0n))), Nat.add(P, Nat.add(K, Nat.add(sy, Nat.add(u, 0n)))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(sy, 0n)), Nat.add(K, Nat.add(u, 0n))), Nat.add(P, Nat.add(Nat.add(sy, 0n), Nat.add(K, Nat.add(u, 0n)))), Nat.add(P, Nat.add(K, Nat.add(sy, Nat.add(u, 0n)))), NA.add_assoc(P, Nat.add(sy, 0n), Nat.add(K, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(Nat.add(sy, 0n), Nat.add(K, Nat.add(u, 0n))), Nat.add(K, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, Nat.add(u, 0n))), Nat.add(sy, Nat.add(K, Nat.add(u, 0n))), Nat.add(K, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, Nat.add(u, 0n))), Nat.add(sy, Nat.add(0n, Nat.add(K, Nat.add(u, 0n)))), Nat.add(sy, Nat.add(K, Nat.add(u, 0n))), NA.add_assoc(sy, 0n, Nat.add(K, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, Nat.add(u, 0n))), Nat.add(K, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(K, Nat.add(u, 0n))), Nat.add(K, Nat.add(0n, Nat.add(u, 0n))), Nat.add(K, Nat.add(u, 0n)), NA.add_swap(0n, K, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==}))))), NA.add_swap(sy, K, Nat.add(u, 0n))))), NA.add_swap(P, K, Nat.add(sy, Nat.add(u, 0n))))))), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.add(u, K)), Nat.add(sy, P), Nat.add(62n, u), Equal.sym(Nat, Nat.add(62n, u), Nat.add(sy, P), hb))), Equal.cong(Nat, Nat, w => Nat.add(Nat.add(62n, u), w), Nat.add(u, K), Nat.add(sx, 1022n), hf)), Equal.trans(Nat, Nat.add(Nat.add(62n, u), Nat.add(sx, 1022n)), Nat.add(sx, Nat.add(u, 1084n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(Nat.add(62n, u), Nat.add(sx, 1022n)), Nat.add(Nat.add(u, 62n), Nat.add(sx, 1022n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(Nat.add(62n, u), Nat.add(sx, 1022n)), Nat.add(Nat.add(u, 62n), Nat.add(sx, 1022n)), Nat.add(Nat.add(u, 62n), Nat.add(sx, 1022n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, 1022n)), Nat.add(62n, u), Nat.add(u, 62n), Equal.trans(Nat, Nat.add(62n, u), Nat.add(62n, Nat.add(u, 0n)), Nat.add(u, 62n), Equal.cong(Nat, Nat, z => Nat.add(62n, z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u))), Equal.trans(Nat, Nat.add(62n, Nat.add(u, 0n)), Nat.add(u, Nat.add(62n, 0n)), Nat.add(u, 62n), NA.add_swap(62n, u, 0n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(u, 62n), z), Nat.add(sx, 1022n), Nat.add(sx, 1022n), Equal.trans(Nat, Nat.add(sx, 1022n), Nat.add(Nat.add(sx, 0n), 1022n), Nat.add(sx, 1022n), Equal.cong(Nat, Nat, z => Nat.add(z, 1022n), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), 1022n), Nat.add(sx, Nat.add(0n, 1022n)), Nat.add(sx, 1022n), NA.add_assoc(sx, 0n, 1022n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(u, 62n), Nat.add(sx, 1022n)), Nat.add(u, Nat.add(sx, 1084n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(Nat.add(u, 62n), Nat.add(sx, 1022n)), Nat.add(u, Nat.add(62n, Nat.add(sx, 1022n))), Nat.add(u, Nat.add(sx, 1084n)), NA.add_assoc(u, 62n, Nat.add(sx, 1022n)), Equal.cong(Nat, Nat, z => Nat.add(u, z), Nat.add(62n, Nat.add(sx, 1022n)), Nat.add(sx, 1084n), Equal.trans(Nat, Nat.add(62n, Nat.add(sx, 1022n)), Nat.add(sx, Nat.add(62n, 1022n)), Nat.add(sx, 1084n), NA.add_swap(62n, sx, 1022n), {==}))), NA.add_swap(u, sx, 1084n))), Equal.sym(Nat, Nat.add(sx, Nat.add(u, 1084n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 1084n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(sx, Nat.add(u, 1084n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(u, 1084n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(u, 1084n), Nat.add(u, 1084n), Equal.trans(Nat, Nat.add(u, 1084n), Nat.add(Nat.add(u, 0n), 1084n), Nat.add(u, 1084n), Equal.cong(Nat, Nat, z => Nat.add(z, 1084n), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), 1084n), Nat.add(u, Nat.add(0n, 1084n)), Nat.add(u, 1084n), NA.add_assoc(u, 0n, 1084n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(u, 1084n)), Nat.add(sx, Nat.add(0n, Nat.add(u, 1084n))), Nat.add(sx, Nat.add(u, 1084n)), NA.add_assoc(sx, 0n, Nat.add(u, 1084n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(u, 1084n)), Nat.add(u, 1084n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 1084n)), Nat.add(u, Nat.add(0n, 1084n)), Nat.add(u, 1084n), NA.add_swap(0n, u, 1084n), {==})))))))
12  +c = Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(P, u), Nat.add(sy, K)), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(dp, Nat.add(sx, 884n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(dp, Nat.add(sx, 884n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 884n))), Nat.add(P, u), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, u), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, 0n), z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)))), Equal.trans(Nat, Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_assoc(P, 0n, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, Nat.add(u, 0n)), z), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 884n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(dp, 884n), Nat.add(dp, 884n), Equal.trans(Nat, Nat.add(dp, 884n), Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, 884n), Equal.cong(Nat, Nat, z => Nat.add(z, 884n), dp, Nat.add(dp, 0n), Equal.sym(Nat, Nat.add(dp, 0n), dp, N.add_zero(dp))), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, Nat.add(0n, 884n)), Nat.add(dp, 884n), NA.add_assoc(dp, 0n, 884n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 884n))), Nat.add(sx, Nat.add(dp, 884n)), NA.add_assoc(sx, 0n, Nat.add(dp, 884n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 884n)), Nat.add(dp, 884n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(0n, 884n)), Nat.add(dp, 884n), NA.add_swap(0n, dp, 884n), {==}))), NA.add_swap(sx, dp, 884n))))), Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(dp, Nat.add(sx, 884n))), Nat.add(P, Nat.add(Nat.add(u, 0n), Nat.add(dp, Nat.add(sx, 884n)))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), NA.add_assoc(P, Nat.add(u, 0n), Nat.add(dp, Nat.add(sx, 884n))), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(Nat.add(u, 0n), Nat.add(dp, Nat.add(sx, 884n))), Nat.add(dp, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), Nat.add(dp, Nat.add(sx, 884n))), Nat.add(u, Nat.add(dp, Nat.add(sx, 884n))), Nat.add(dp, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), Nat.add(dp, Nat.add(sx, 884n))), Nat.add(u, Nat.add(0n, Nat.add(dp, Nat.add(sx, 884n)))), Nat.add(u, Nat.add(dp, Nat.add(sx, 884n))), NA.add_assoc(u, 0n, Nat.add(dp, Nat.add(sx, 884n))), Equal.cong(Nat, Nat, z => Nat.add(u, z), Nat.add(0n, Nat.add(dp, Nat.add(sx, 884n))), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, Nat.add(sx, 884n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, 884n))), Nat.add(dp, Nat.add(sx, 884n)), NA.add_swap(0n, dp, Nat.add(sx, 884n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, 884n)), Nat.add(sx, 884n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 884n)), Nat.add(sx, Nat.add(0n, 884n)), Nat.add(sx, 884n), NA.add_swap(0n, sx, 884n), {==}))))), Equal.trans(Nat, Nat.add(u, Nat.add(dp, Nat.add(sx, 884n))), Nat.add(dp, Nat.add(u, Nat.add(sx, 884n))), Nat.add(dp, Nat.add(sx, Nat.add(u, 884n))), NA.add_swap(u, dp, Nat.add(sx, 884n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(u, Nat.add(sx, 884n)), Nat.add(sx, Nat.add(u, 884n)), NA.add_swap(u, sx, 884n))))))), Equal.sym(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(P, u)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 884n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(dp, 884n), Nat.add(dp, 884n), Equal.trans(Nat, Nat.add(dp, 884n), Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, 884n), Equal.cong(Nat, Nat, z => Nat.add(z, 884n), dp, Nat.add(dp, 0n), Equal.sym(Nat, Nat.add(dp, 0n), dp, N.add_zero(dp))), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, Nat.add(0n, 884n)), Nat.add(dp, 884n), NA.add_assoc(dp, 0n, 884n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 884n))), Nat.add(sx, Nat.add(dp, 884n)), NA.add_assoc(sx, 0n, Nat.add(dp, 884n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 884n)), Nat.add(dp, 884n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(0n, 884n)), Nat.add(dp, 884n), NA.add_swap(0n, dp, 884n), {==}))), NA.add_swap(sx, dp, 884n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(dp, Nat.add(sx, 884n)), z), Nat.add(P, u), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, u), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, 0n), z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)))), Equal.trans(Nat, Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_assoc(P, 0n, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(dp, Nat.add(P, Nat.add(sx, Nat.add(u, 884n)))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(dp, Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n)))), Nat.add(dp, Nat.add(P, Nat.add(sx, Nat.add(u, 884n)))), NA.add_assoc(dp, Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sx, Nat.add(P, Nat.add(u, 884n))), Nat.add(P, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, 884n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sx, Nat.add(884n, Nat.add(P, Nat.add(u, 0n)))), Nat.add(sx, Nat.add(P, Nat.add(u, 884n))), NA.add_assoc(sx, 884n, Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(884n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 884n)), Equal.trans(Nat, Nat.add(884n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(884n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 884n)), NA.add_swap(884n, P, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(884n, Nat.add(u, 0n)), Nat.add(u, 884n), Equal.trans(Nat, Nat.add(884n, Nat.add(u, 0n)), Nat.add(u, Nat.add(884n, 0n)), Nat.add(u, 884n), NA.add_swap(884n, u, 0n), {==}))))), NA.add_swap(sx, P, Nat.add(u, 884n))))), NA.add_swap(dp, P, Nat.add(sx, Nat.add(u, 884n))))))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(sx, Nat.add(u, 1084n)), Nat.add(Nat.add(P, u), Nat.add(sy, K)), a, Equal.trans(Nat, Nat.add(sx, Nat.add(u, 1084n)), Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(P, u), Nat.add(sy, K)), Equal.sym(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(sx, Nat.add(u, 1084n)), b), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Nat.add(Nat.add(P, u), Nat.add(sy, K)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(P, u)), Nat.add(sy, K), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, K), sy, Nat.add(sy, 0n), Equal.sym(Nat, Nat.add(sy, 0n), sy, N.add_zero(sy))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sy, 0n), z), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 0n))), Nat.add(sy, Nat.add(K, 0n)), NA.add_assoc(sy, 0n, Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, Nat.add(0n, 0n)), Nat.add(K, 0n), NA.add_swap(0n, K, 0n), {==}))), NA.add_swap(sy, K, 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(K, Nat.add(sy, 0n)), z), Nat.add(P, u), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, u), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, 0n), z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)))), Equal.trans(Nat, Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_assoc(P, 0n, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(K, Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n)))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), NA.add_assoc(K, Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sy, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(P, Nat.add(u, 0n))), Nat.add(sy, Nat.add(0n, Nat.add(P, Nat.add(u, 0n)))), Nat.add(sy, Nat.add(P, Nat.add(u, 0n))), NA.add_assoc(sy, 0n, Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_swap(0n, P, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==}))))), NA.add_swap(sy, P, Nat.add(u, 0n)))))), Equal.sym(Nat, Nat.add(Nat.add(P, u), Nat.add(sy, K)), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sy, K)), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(K, Nat.add(sy, 0n))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sy, K)), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(sy, K)), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(K, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sy, K)), Nat.add(P, u), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, u), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, 0n), z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)))), Equal.trans(Nat, Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_assoc(P, 0n, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, Nat.add(u, 0n)), z), Nat.add(sy, K), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, K), sy, Nat.add(sy, 0n), Equal.sym(Nat, Nat.add(sy, 0n), sy, N.add_zero(sy))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sy, 0n), z), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 0n))), Nat.add(sy, Nat.add(K, 0n)), NA.add_assoc(sy, 0n, Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, Nat.add(0n, 0n)), Nat.add(K, 0n), NA.add_swap(0n, K, 0n), {==}))), NA.add_swap(sy, K, 0n))))), Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(K, Nat.add(sy, 0n))), Nat.add(P, Nat.add(K, Nat.add(sy, Nat.add(u, 0n)))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(K, Nat.add(sy, 0n))), Nat.add(P, Nat.add(Nat.add(u, 0n), Nat.add(K, Nat.add(sy, 0n)))), Nat.add(P, Nat.add(K, Nat.add(sy, Nat.add(u, 0n)))), NA.add_assoc(P, Nat.add(u, 0n), Nat.add(K, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(Nat.add(u, 0n), Nat.add(K, Nat.add(sy, 0n))), Nat.add(K, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), Nat.add(K, Nat.add(sy, 0n))), Nat.add(u, Nat.add(K, Nat.add(sy, 0n))), Nat.add(K, Nat.add(sy, Nat.add(u, 0n))), Equal.trans(Nat, Nat.add(Nat.add(u, 0n), Nat.add(K, Nat.add(sy, 0n))), Nat.add(u, Nat.add(0n, Nat.add(K, Nat.add(sy, 0n)))), Nat.add(u, Nat.add(K, Nat.add(sy, 0n))), NA.add_assoc(u, 0n, Nat.add(K, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(u, z), Nat.add(0n, Nat.add(K, Nat.add(sy, 0n))), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(K, Nat.add(sy, 0n))), Nat.add(K, Nat.add(0n, Nat.add(sy, 0n))), Nat.add(K, Nat.add(sy, 0n)), NA.add_swap(0n, K, Nat.add(sy, 0n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(0n, Nat.add(sy, 0n)), Nat.add(sy, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sy, 0n)), Nat.add(sy, Nat.add(0n, 0n)), Nat.add(sy, 0n), NA.add_swap(0n, sy, 0n), {==}))))), Equal.trans(Nat, Nat.add(u, Nat.add(K, Nat.add(sy, 0n))), Nat.add(K, Nat.add(u, Nat.add(sy, 0n))), Nat.add(K, Nat.add(sy, Nat.add(u, 0n))), NA.add_swap(u, K, Nat.add(sy, 0n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(u, Nat.add(sy, 0n)), Nat.add(sy, Nat.add(u, 0n)), NA.add_swap(u, sy, 0n)))))), NA.add_swap(P, K, Nat.add(sy, Nat.add(u, 0n))))))))))
13  NR.add_cancel(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(sy, K), c)