proofs/math/typed/f64divx.bend source

proofs/math/typed/f64divx.bend on the hub · documented module

import Baseimport ../../lib/nat.bend as Nimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../natural/arith.bend as NR# Exponent bookkeeping for Div.value: the spec's quotient exponent plus the# rounding cut is the implementation's biased exponent minus the offset.def 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}:  +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), {==})))))))  +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), {==})))))))  +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))))))))))  NR.add_cancel(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(sy, K), c)def dexp(+E: Nat, +XX: Nat, +XY: Nat, +dp: Nat, +P: Nat, +u: Nat, +K: Nat, +sx: Nat, +sy: Nat, +EA: Nat, +EB: Nat, +e: Nat, +ha: {Nat.add(E, Nat.add(XY, 201n)) == Nat.add(XX, 3000n) : 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}, +hEAx: {Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat}, +hEBy: {Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat}, +hd: {Nat.add(e, EB) == Nat.add(EA, Nat.add(4096n, K)) : Nat}) -> {Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n) == e : Nat}:  +z = dexp_z(dp, P, u, K, sx, sy, hc, hb, hf)  +lz = Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(Nat.add(sy, K), 6267n)), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Nat.add(XX, Nat.add(Nat.add(sy, K), 6267n)), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 7151n))), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 0n), z), Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 7151n)), 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, 7151n), Nat.add(dp, 7151n), Equal.trans(Nat, Nat.add(dp, 7151n), Nat.add(Nat.add(dp, 0n), 7151n), Nat.add(dp, 7151n), Equal.cong(Nat, Nat, z => Nat.add(z, 7151n), 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), 7151n), Nat.add(dp, Nat.add(0n, 7151n)), Nat.add(dp, 7151n), NA.add_assoc(dp, 0n, 7151n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 7151n))), Nat.add(sx, Nat.add(dp, 7151n)), NA.add_assoc(sx, 0n, Nat.add(dp, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 7151n)), Nat.add(dp, 7151n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(0n, 7151n)), Nat.add(dp, 7151n), NA.add_swap(0n, dp, 7151n), {==}))), NA.add_swap(sx, dp, 7151n))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n)))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), NA.add_assoc(XX, 0n, Nat.add(dp, Nat.add(sx, 7151n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(sx, 7151n)), NA.add_swap(0n, dp, Nat.add(sx, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, 7151n)), Nat.add(sx, 7151n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 7151n)), Nat.add(sx, Nat.add(0n, 7151n)), Nat.add(sx, 7151n), NA.add_swap(0n, sx, 7151n), {==})))))), Equal.sym(Nat, Nat.add(XX, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Nat.add(Nat.add(XX, 0n), Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 0n), z), Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), 6267n), Nat.add(dp, Nat.add(sx, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(z, 6267n), 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(dp, Nat.add(sx, 884n)), 6267n), Nat.add(dp, Nat.add(Nat.add(sx, 884n), 6267n)), Nat.add(dp, Nat.add(sx, 7151n)), NA.add_assoc(dp, Nat.add(sx, 884n), 6267n), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(Nat.add(sx, 884n), 6267n), Nat.add(sx, 7151n), Equal.trans(Nat, Nat.add(Nat.add(sx, 884n), 6267n), Nat.add(sx, Nat.add(884n, 6267n)), Nat.add(sx, 7151n), NA.add_assoc(sx, 884n, 6267n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n)))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), NA.add_assoc(XX, 0n, Nat.add(dp, Nat.add(sx, 7151n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(sx, 7151n)), NA.add_swap(0n, dp, Nat.add(sx, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, 7151n)), Nat.add(sx, 7151n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 7151n)), Nat.add(sx, Nat.add(0n, 7151n)), Nat.add(sx, 7151n), NA.add_swap(0n, sx, 7151n), {==})))))))), Equal.cong(Nat, Nat, w => Nat.add(XX, Nat.add(w, 6267n)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(sy, K), z)), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(sy, K), 6267n)), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(sy, K), 6267n)), Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(sy, K), 6267n)), Nat.add(Nat.add(XX, 0n), Nat.add(Nat.add(sy, K), 6267n)), Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(sy, K), 6267n)), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 0n), z), Nat.add(Nat.add(sy, K), 6267n), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), 6267n), Nat.add(Nat.add(K, Nat.add(sy, 0n)), 6267n), Nat.add(K, Nat.add(sy, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(z, 6267n), 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(K, Nat.add(sy, 0n)), 6267n), Nat.add(K, Nat.add(Nat.add(sy, 0n), 6267n)), Nat.add(K, Nat.add(sy, 6267n)), NA.add_assoc(K, Nat.add(sy, 0n), 6267n), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(Nat.add(sy, 0n), 6267n), Nat.add(sy, 6267n), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), 6267n), Nat.add(sy, Nat.add(0n, 6267n)), Nat.add(sy, 6267n), NA.add_assoc(sy, 0n, 6267n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n)))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), NA.add_assoc(XX, 0n, Nat.add(K, Nat.add(sy, 6267n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(0n, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(sy, 6267n)), NA.add_swap(0n, K, Nat.add(sy, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(0n, Nat.add(sy, 6267n)), Nat.add(sy, 6267n), Equal.trans(Nat, Nat.add(0n, Nat.add(sy, 6267n)), Nat.add(sy, Nat.add(0n, 6267n)), Nat.add(sy, 6267n), NA.add_swap(0n, sy, 6267n), {==}))))), NA.add_swap(XX, K, Nat.add(sy, 6267n)))), Equal.sym(Nat, Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(XX, 0n), Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sy, Nat.add(K, 6267n))), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 0n), z), Nat.add(sy, Nat.add(K, 6267n)), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 6267n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 6267n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(K, 6267n)), 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), Nat.add(K, 6267n), Nat.add(K, 6267n), Equal.trans(Nat, Nat.add(K, 6267n), Nat.add(Nat.add(K, 0n), 6267n), Nat.add(K, 6267n), Equal.cong(Nat, Nat, z => Nat.add(z, 6267n), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K))), Equal.trans(Nat, Nat.add(Nat.add(K, 0n), 6267n), Nat.add(K, Nat.add(0n, 6267n)), Nat.add(K, 6267n), NA.add_assoc(K, 0n, 6267n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(sy, Nat.add(K, 6267n)), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 6267n))), Nat.add(sy, Nat.add(K, 6267n)), NA.add_assoc(sy, 0n, Nat.add(K, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 6267n)), Nat.add(K, 6267n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 6267n)), Nat.add(K, Nat.add(0n, 6267n)), Nat.add(K, 6267n), NA.add_swap(0n, K, 6267n), {==}))), NA.add_swap(sy, K, 6267n))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n)))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), NA.add_assoc(XX, 0n, Nat.add(K, Nat.add(sy, 6267n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(0n, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(sy, 6267n)), NA.add_swap(0n, K, Nat.add(sy, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(0n, Nat.add(sy, 6267n)), Nat.add(sy, 6267n), Equal.trans(Nat, Nat.add(0n, Nat.add(sy, 6267n)), Nat.add(sy, Nat.add(0n, 6267n)), Nat.add(sy, 6267n), NA.add_swap(0n, sy, 6267n), {==}))))), NA.add_swap(XX, K, Nat.add(sy, 6267n)))))))  +lh = Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(EB, sy), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Nat.add(Nat.add(EB, sy), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(sy, sx), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sx), 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), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(sx, 0n))), Nat.add(sy, Nat.add(sx, 0n)), NA.add_assoc(sy, 0n, Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(0n, 0n)), Nat.add(sx, 0n), NA.add_swap(0n, sx, 0n), {==}))), NA.add_swap(sy, sx, 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, Nat.add(sy, 0n)), z), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n))), Equal.trans(Nat, Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(Nat.add(EB, 0n), Nat.add(E, Nat.add(dp, 2181n))), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n))), Equal.trans(Nat, Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(Nat.add(EB, 0n), Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(Nat.add(EB, 0n), Nat.add(E, Nat.add(dp, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), EB, Nat.add(EB, 0n), Equal.sym(Nat, Nat.add(EB, 0n), EB, N.add_zero(EB))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EB, 0n), z), Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n), Nat.add(E, Nat.add(dp, 2181n)), Equal.trans(Nat, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n), Nat.add(Nat.add(E, Nat.add(dp, 1n)), 2180n), Nat.add(E, Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(z, 2180n), Nat.add(E, Nat.add(1n, dp)), Nat.add(E, Nat.add(dp, 1n)), Equal.trans(Nat, Nat.add(E, Nat.add(1n, dp)), Nat.add(Nat.add(E, 0n), Nat.add(dp, 1n)), Nat.add(E, Nat.add(dp, 1n)), Equal.trans(Nat, Nat.add(E, Nat.add(1n, dp)), Nat.add(Nat.add(E, 0n), Nat.add(1n, dp)), Nat.add(Nat.add(E, 0n), Nat.add(dp, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, dp)), E, Nat.add(E, 0n), Equal.sym(Nat, Nat.add(E, 0n), E, N.add_zero(E))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(E, 0n), z), Nat.add(1n, dp), Nat.add(dp, 1n), Equal.trans(Nat, Nat.add(1n, dp), Nat.add(1n, Nat.add(dp, 0n)), Nat.add(dp, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), dp, Nat.add(dp, 0n), Equal.sym(Nat, Nat.add(dp, 0n), dp, N.add_zero(dp))), Equal.trans(Nat, Nat.add(1n, Nat.add(dp, 0n)), Nat.add(dp, Nat.add(1n, 0n)), Nat.add(dp, 1n), NA.add_swap(1n, dp, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(E, 0n), Nat.add(dp, 1n)), Nat.add(E, Nat.add(0n, Nat.add(dp, 1n))), Nat.add(E, Nat.add(dp, 1n)), NA.add_assoc(E, 0n, Nat.add(dp, 1n)), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(0n, Nat.add(dp, 1n)), Nat.add(dp, 1n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 1n)), Nat.add(dp, Nat.add(0n, 1n)), Nat.add(dp, 1n), NA.add_swap(0n, dp, 1n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(E, Nat.add(dp, 1n)), 2180n), Nat.add(E, Nat.add(Nat.add(dp, 1n), 2180n)), Nat.add(E, Nat.add(dp, 2181n)), NA.add_assoc(E, Nat.add(dp, 1n), 2180n), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(Nat.add(dp, 1n), 2180n), Nat.add(dp, 2181n), Equal.trans(Nat, Nat.add(Nat.add(dp, 1n), 2180n), Nat.add(dp, Nat.add(1n, 2180n)), Nat.add(dp, 2181n), NA.add_assoc(dp, 1n, 2180n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(EB, 0n), Nat.add(E, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(E, Nat.add(dp, 2181n))), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n))), Equal.trans(Nat, Nat.add(Nat.add(EB, 0n), Nat.add(E, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(0n, Nat.add(E, Nat.add(dp, 2181n)))), Nat.add(EB, Nat.add(E, Nat.add(dp, 2181n))), NA.add_assoc(EB, 0n, Nat.add(E, Nat.add(dp, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(0n, Nat.add(E, Nat.add(dp, 2181n))), Nat.add(E, Nat.add(dp, 2181n)), Equal.trans(Nat, Nat.add(0n, Nat.add(E, Nat.add(dp, 2181n))), Nat.add(E, Nat.add(0n, Nat.add(dp, 2181n))), Nat.add(E, Nat.add(dp, 2181n)), NA.add_swap(0n, E, Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, 2181n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(0n, 2181n)), Nat.add(dp, 2181n), NA.add_swap(0n, dp, 2181n), {==}))))), NA.add_swap(EB, E, Nat.add(dp, 2181n)))))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(sx, Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n))))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(sx, Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n))))), Nat.add(sx, Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n))))), NA.add_assoc(sx, Nat.add(sy, 0n), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(sy, Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(sy, Nat.add(0n, Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n))))), Nat.add(sy, Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), NA.add_assoc(sy, 0n, Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n))), Equal.trans(Nat, Nat.add(0n, Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(0n, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n))), NA.add_swap(0n, E, Nat.add(EB, Nat.add(dp, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(0n, Nat.add(EB, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(dp, 2181n)), Equal.trans(Nat, Nat.add(0n, Nat.add(EB, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(0n, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(dp, 2181n)), NA.add_swap(0n, EB, Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, 2181n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(0n, 2181n)), Nat.add(dp, 2181n), NA.add_swap(0n, dp, 2181n), {==}))))))), Equal.trans(Nat, Nat.add(sy, Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(sy, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n)))), NA.add_swap(sy, E, Nat.add(EB, Nat.add(dp, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(sy, Nat.add(EB, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n))), Equal.trans(Nat, Nat.add(sy, Nat.add(EB, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(sy, Nat.add(dp, 2181n))), Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n))), NA.add_swap(sy, EB, Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(sy, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(sy, 2181n)), NA.add_swap(sy, dp, 2181n)))))))), Equal.trans(Nat, Nat.add(sx, Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n))))), Nat.add(E, Nat.add(sx, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n))))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), NA.add_swap(sx, E, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(sx, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n)))), Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n)))), Equal.trans(Nat, Nat.add(sx, Nat.add(EB, Nat.add(dp, Nat.add(sy, 2181n)))), Nat.add(EB, Nat.add(sx, Nat.add(dp, Nat.add(sy, 2181n)))), Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n)))), NA.add_swap(sx, EB, Nat.add(dp, Nat.add(sy, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(sx, Nat.add(dp, Nat.add(sy, 2181n))), Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))), NA.add_swap(sx, dp, Nat.add(sy, 2181n)))))))), Equal.sym(Nat, Nat.add(Nat.add(EB, sy), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(EB, sy), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(EB, Nat.add(sy, 0n)), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(EB, sy), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(EB, Nat.add(sy, 0n)), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(EB, Nat.add(sy, 0n)), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(EB, sy), Nat.add(EB, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(EB, sy), Nat.add(Nat.add(EB, 0n), Nat.add(sy, 0n)), Nat.add(EB, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(EB, sy), Nat.add(Nat.add(EB, 0n), sy), Nat.add(Nat.add(EB, 0n), Nat.add(sy, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sy), EB, Nat.add(EB, 0n), Equal.sym(Nat, Nat.add(EB, 0n), EB, N.add_zero(EB))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EB, 0n), z), sy, Nat.add(sy, 0n), Equal.sym(Nat, Nat.add(sy, 0n), sy, N.add_zero(sy)))), Equal.trans(Nat, Nat.add(Nat.add(EB, 0n), Nat.add(sy, 0n)), Nat.add(EB, Nat.add(0n, Nat.add(sy, 0n))), Nat.add(EB, Nat.add(sy, 0n)), NA.add_assoc(EB, 0n, Nat.add(sy, 0n)), Equal.cong(Nat, Nat, z => Nat.add(EB, 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.cong(Nat, Nat, z => Nat.add(Nat.add(EB, Nat.add(sy, 0n)), z), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.trans(Nat, Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(Nat.add(E, 0n), Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.trans(Nat, Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(Nat.add(E, 0n), Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(Nat.add(E, 0n), Nat.add(dp, Nat.add(sx, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 2181n))), E, Nat.add(E, 0n), Equal.sym(Nat, Nat.add(E, 0n), E, N.add_zero(E))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(E, 0n), z), Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 2181n)), 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, 2181n), Nat.add(dp, 2181n), Equal.trans(Nat, Nat.add(dp, 2181n), Nat.add(Nat.add(dp, 0n), 2181n), Nat.add(dp, 2181n), Equal.cong(Nat, Nat, z => Nat.add(z, 2181n), 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), 2181n), Nat.add(dp, Nat.add(0n, 2181n)), Nat.add(dp, 2181n), NA.add_assoc(dp, 0n, 2181n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 2181n))), Nat.add(sx, Nat.add(dp, 2181n)), NA.add_assoc(sx, 0n, Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, 2181n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(0n, 2181n)), Nat.add(dp, 2181n), NA.add_swap(0n, dp, 2181n), {==}))), NA.add_swap(sx, dp, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(E, 0n), Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(E, Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), NA.add_assoc(E, 0n, Nat.add(dp, Nat.add(sx, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 2181n)), NA.add_swap(0n, dp, Nat.add(sx, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, 2181n)), Nat.add(sx, 2181n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 2181n)), Nat.add(sx, Nat.add(0n, 2181n)), Nat.add(sx, 2181n), NA.add_swap(0n, sx, 2181n), {==})))))))), Equal.trans(Nat, Nat.add(Nat.add(EB, Nat.add(sy, 0n)), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(EB, Nat.add(E, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(EB, Nat.add(sy, 0n)), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(EB, Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))))), Nat.add(EB, Nat.add(E, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), NA.add_assoc(EB, Nat.add(sy, 0n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(sy, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(sy, Nat.add(0n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))))), Nat.add(sy, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), NA.add_assoc(sy, 0n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.trans(Nat, Nat.add(0n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), NA.add_swap(0n, E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 2181n)), NA.add_swap(0n, dp, Nat.add(sx, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, 2181n)), Nat.add(sx, 2181n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 2181n)), Nat.add(sx, Nat.add(0n, 2181n)), Nat.add(sx, 2181n), NA.add_swap(0n, sx, 2181n), {==}))))))), Equal.trans(Nat, Nat.add(sy, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(sy, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n)))), NA.add_swap(sy, E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(sy, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))), Equal.trans(Nat, Nat.add(sy, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sy, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))), NA.add_swap(sy, dp, Nat.add(sx, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(sy, Nat.add(sx, 2181n)), Nat.add(sx, Nat.add(sy, 2181n)), NA.add_swap(sy, sx, 2181n)))))))), NA.add_swap(EB, E, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n)))))))), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(EB, sy), Nat.add(XY, 2171n), hEBy)), Equal.trans(Nat, Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n)))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Equal.trans(Nat, Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n)))), Equal.trans(Nat, Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(XY, 2171n), Nat.add(XY, 2171n), Equal.trans(Nat, Nat.add(XY, 2171n), Nat.add(Nat.add(XY, 0n), 2171n), Nat.add(XY, 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 2171n), Nat.add(XY, Nat.add(0n, 2171n)), Nat.add(XY, 2171n), NA.add_assoc(XY, 0n, 2171n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XY, 2171n), z), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.trans(Nat, Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(Nat.add(E, 0n), Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.trans(Nat, Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(Nat.add(E, 0n), Nat.add(sx, Nat.add(dp, 2181n))), Nat.add(Nat.add(E, 0n), Nat.add(dp, Nat.add(sx, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 2181n))), E, Nat.add(E, 0n), Equal.sym(Nat, Nat.add(E, 0n), E, N.add_zero(E))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(E, 0n), z), Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 2181n)), 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, 2181n), Nat.add(dp, 2181n), Equal.trans(Nat, Nat.add(dp, 2181n), Nat.add(Nat.add(dp, 0n), 2181n), Nat.add(dp, 2181n), Equal.cong(Nat, Nat, z => Nat.add(z, 2181n), 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), 2181n), Nat.add(dp, Nat.add(0n, 2181n)), Nat.add(dp, 2181n), NA.add_assoc(dp, 0n, 2181n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(sx, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 2181n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 2181n))), Nat.add(sx, Nat.add(dp, 2181n)), NA.add_assoc(sx, 0n, Nat.add(dp, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, 2181n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 2181n)), Nat.add(dp, Nat.add(0n, 2181n)), Nat.add(dp, 2181n), NA.add_swap(0n, dp, 2181n), {==}))), NA.add_swap(sx, dp, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(E, 0n), Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(E, Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))), NA.add_assoc(E, 0n, Nat.add(dp, Nat.add(sx, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 2181n)), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 2181n)), NA.add_swap(0n, dp, Nat.add(sx, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, 2181n)), Nat.add(sx, 2181n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 2181n)), Nat.add(sx, Nat.add(0n, 2181n)), Nat.add(sx, 2181n), NA.add_swap(0n, sx, 2181n), {==})))))))), Equal.trans(Nat, Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(XY, Nat.add(E, Nat.add(dp, Nat.add(sx, 4352n)))), Nat.add(E, Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n)))), Equal.trans(Nat, Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(XY, Nat.add(2171n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n))))), Nat.add(XY, Nat.add(E, Nat.add(dp, Nat.add(sx, 4352n)))), NA.add_assoc(XY, 2171n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(XY, z), Nat.add(2171n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, 4352n))), Equal.trans(Nat, Nat.add(2171n, Nat.add(E, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(2171n, Nat.add(dp, Nat.add(sx, 2181n)))), Nat.add(E, Nat.add(dp, Nat.add(sx, 4352n))), NA.add_swap(2171n, E, Nat.add(dp, Nat.add(sx, 2181n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(2171n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 4352n)), Equal.trans(Nat, Nat.add(2171n, Nat.add(dp, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(2171n, Nat.add(sx, 2181n))), Nat.add(dp, Nat.add(sx, 4352n)), NA.add_swap(2171n, dp, Nat.add(sx, 2181n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(2171n, Nat.add(sx, 2181n)), Nat.add(sx, 4352n), Equal.trans(Nat, Nat.add(2171n, Nat.add(sx, 2181n)), Nat.add(sx, Nat.add(2171n, 2181n)), Nat.add(sx, 4352n), NA.add_swap(2171n, sx, 2181n), {==}))))))), NA.add_swap(XY, E, Nat.add(dp, Nat.add(sx, 4352n))))), Equal.sym(Nat, Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(E, Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n)))), Equal.trans(Nat, Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(E, Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n)))), Equal.trans(Nat, Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(dp, Nat.add(sx, 4151n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(E, Nat.add(XY, 201n)), Nat.add(E, Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(E, Nat.add(XY, 201n)), Nat.add(Nat.add(E, 0n), Nat.add(XY, 201n)), Nat.add(E, Nat.add(XY, 201n)), Equal.trans(Nat, Nat.add(E, Nat.add(XY, 201n)), Nat.add(Nat.add(E, 0n), Nat.add(XY, 201n)), Nat.add(Nat.add(E, 0n), Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(XY, 201n)), E, Nat.add(E, 0n), Equal.sym(Nat, Nat.add(E, 0n), E, N.add_zero(E))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(E, 0n), z), Nat.add(XY, 201n), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(XY, 201n), Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, 201n), Equal.cong(Nat, Nat, z => Nat.add(z, 201n), XY, Nat.add(XY, 0n), Equal.sym(Nat, Nat.add(XY, 0n), XY, N.add_zero(XY))), Equal.trans(Nat, Nat.add(Nat.add(XY, 0n), 201n), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_assoc(XY, 0n, 201n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(E, 0n), Nat.add(XY, 201n)), Nat.add(E, Nat.add(0n, Nat.add(XY, 201n))), Nat.add(E, Nat.add(XY, 201n)), NA.add_assoc(E, 0n, Nat.add(XY, 201n)), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, 201n), Equal.trans(Nat, Nat.add(0n, Nat.add(XY, 201n)), Nat.add(XY, Nat.add(0n, 201n)), Nat.add(XY, 201n), NA.add_swap(0n, XY, 201n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(E, Nat.add(XY, 201n)), z), Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(sx, 4151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(sx, 4151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 4151n)), 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, 4151n), Nat.add(dp, 4151n), Equal.trans(Nat, Nat.add(dp, 4151n), Nat.add(Nat.add(dp, 0n), 4151n), Nat.add(dp, 4151n), Equal.cong(Nat, Nat, z => Nat.add(z, 4151n), 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), 4151n), Nat.add(dp, Nat.add(0n, 4151n)), Nat.add(dp, 4151n), NA.add_assoc(dp, 0n, 4151n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(sx, 4151n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 4151n))), Nat.add(sx, Nat.add(dp, 4151n)), NA.add_assoc(sx, 0n, Nat.add(dp, 4151n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 4151n)), Nat.add(dp, 4151n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(0n, 4151n)), Nat.add(dp, 4151n), NA.add_swap(0n, dp, 4151n), {==}))), NA.add_swap(sx, dp, 4151n))))), Equal.trans(Nat, Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(E, Nat.add(Nat.add(XY, 201n), Nat.add(dp, Nat.add(sx, 4151n)))), Nat.add(E, Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n)))), NA.add_assoc(E, Nat.add(XY, 201n), Nat.add(dp, Nat.add(sx, 4151n))), Equal.cong(Nat, Nat, z => Nat.add(E, z), Nat.add(Nat.add(XY, 201n), Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n))), Equal.trans(Nat, Nat.add(Nat.add(XY, 201n), Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(XY, Nat.add(201n, Nat.add(dp, Nat.add(sx, 4151n)))), Nat.add(XY, Nat.add(dp, Nat.add(sx, 4352n))), NA.add_assoc(XY, 201n, Nat.add(dp, Nat.add(sx, 4151n))), Equal.cong(Nat, Nat, z => Nat.add(XY, z), Nat.add(201n, Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(dp, Nat.add(sx, 4352n)), Equal.trans(Nat, Nat.add(201n, Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(dp, Nat.add(201n, Nat.add(sx, 4151n))), Nat.add(dp, Nat.add(sx, 4352n)), NA.add_swap(201n, dp, Nat.add(sx, 4151n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(201n, Nat.add(sx, 4151n)), Nat.add(sx, 4352n), Equal.trans(Nat, Nat.add(201n, Nat.add(sx, 4151n)), Nat.add(sx, Nat.add(201n, 4151n)), Nat.add(sx, 4352n), NA.add_swap(201n, sx, 4151n), {==}))))))))))), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(E, Nat.add(XY, 201n)), Nat.add(XX, 3000n), ha)), Equal.trans(Nat, Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(XX, 3000n), Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(XX, 3000n), Nat.add(dp, Nat.add(sx, 4151n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(XX, 3000n), Nat.add(XX, 3000n), Equal.trans(Nat, Nat.add(XX, 3000n), Nat.add(Nat.add(XX, 0n), 3000n), Nat.add(XX, 3000n), Equal.cong(Nat, Nat, z => Nat.add(z, 3000n), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), 3000n), Nat.add(XX, Nat.add(0n, 3000n)), Nat.add(XX, 3000n), NA.add_assoc(XX, 0n, 3000n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 3000n), z), Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(sx, 4151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(sx, 4151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 4151n)), 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, 4151n), Nat.add(dp, 4151n), Equal.trans(Nat, Nat.add(dp, 4151n), Nat.add(Nat.add(dp, 0n), 4151n), Nat.add(dp, 4151n), Equal.cong(Nat, Nat, z => Nat.add(z, 4151n), 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), 4151n), Nat.add(dp, Nat.add(0n, 4151n)), Nat.add(dp, 4151n), NA.add_assoc(dp, 0n, 4151n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(sx, Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(sx, 4151n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 4151n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 4151n))), Nat.add(sx, Nat.add(dp, 4151n)), NA.add_assoc(sx, 0n, Nat.add(dp, 4151n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 4151n)), Nat.add(dp, 4151n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 4151n)), Nat.add(dp, Nat.add(0n, 4151n)), Nat.add(dp, 4151n), NA.add_swap(0n, dp, 4151n), {==}))), NA.add_swap(sx, dp, 4151n))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 3000n), Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(XX, Nat.add(3000n, Nat.add(dp, Nat.add(sx, 4151n)))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), NA.add_assoc(XX, 3000n, Nat.add(dp, Nat.add(sx, 4151n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(3000n, Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(3000n, Nat.add(dp, Nat.add(sx, 4151n))), Nat.add(dp, Nat.add(3000n, Nat.add(sx, 4151n))), Nat.add(dp, Nat.add(sx, 7151n)), NA.add_swap(3000n, dp, Nat.add(sx, 4151n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(3000n, Nat.add(sx, 4151n)), Nat.add(sx, 7151n), Equal.trans(Nat, Nat.add(3000n, Nat.add(sx, 4151n)), Nat.add(sx, Nat.add(3000n, 4151n)), Nat.add(sx, 7151n), NA.add_swap(3000n, sx, 4151n), {==})))))), Equal.sym(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 7151n))), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 0n), z), Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 7151n)), 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, 7151n), Nat.add(dp, 7151n), Equal.trans(Nat, Nat.add(dp, 7151n), Nat.add(Nat.add(dp, 0n), 7151n), Nat.add(dp, 7151n), Equal.cong(Nat, Nat, z => Nat.add(z, 7151n), 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), 7151n), Nat.add(dp, Nat.add(0n, 7151n)), Nat.add(dp, 7151n), NA.add_assoc(dp, 0n, 7151n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(sx, Nat.add(0n, Nat.add(dp, 7151n))), Nat.add(sx, Nat.add(dp, 7151n)), NA.add_assoc(sx, 0n, Nat.add(dp, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(dp, 7151n)), Nat.add(dp, 7151n), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(0n, 7151n)), Nat.add(dp, 7151n), NA.add_swap(0n, dp, 7151n), {==}))), NA.add_swap(sx, dp, 7151n))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n)))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), NA.add_assoc(XX, 0n, Nat.add(dp, Nat.add(sx, 7151n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(0n, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(0n, Nat.add(sx, 7151n))), Nat.add(dp, Nat.add(sx, 7151n)), NA.add_swap(0n, dp, Nat.add(sx, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(dp, z), Nat.add(0n, Nat.add(sx, 7151n)), Nat.add(sx, 7151n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 7151n)), Nat.add(sx, Nat.add(0n, 7151n)), Nat.add(sx, 7151n), NA.add_swap(0n, sx, 7151n), {==})))))))))  +rh = Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(EA, Nat.add(4096n, K)), Nat.add(sy, sx)), Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(e, EB), Nat.add(sy, sx)), Nat.add(Nat.add(EA, Nat.add(4096n, K)), Nat.add(sy, sx)), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), Nat.add(Nat.add(e, EB), Nat.add(sy, sx)), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, e)), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(e, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(EB, e)), Nat.add(sy, sx), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sx), 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), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(sx, 0n))), Nat.add(sy, Nat.add(sx, 0n)), NA.add_assoc(sy, 0n, Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(0n, 0n)), Nat.add(sx, 0n), NA.add_swap(0n, sx, 0n), {==}))), NA.add_swap(sy, sx, 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, Nat.add(sy, 0n)), z), Nat.add(EB, e), Nat.add(EB, Nat.add(e, 0n)), Equal.trans(Nat, Nat.add(EB, e), Nat.add(Nat.add(EB, 0n), Nat.add(e, 0n)), Nat.add(EB, Nat.add(e, 0n)), Equal.trans(Nat, Nat.add(EB, e), Nat.add(Nat.add(EB, 0n), e), Nat.add(Nat.add(EB, 0n), Nat.add(e, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, e), EB, Nat.add(EB, 0n), Equal.sym(Nat, Nat.add(EB, 0n), EB, N.add_zero(EB))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EB, 0n), z), e, Nat.add(e, 0n), Equal.sym(Nat, Nat.add(e, 0n), e, N.add_zero(e)))), Equal.trans(Nat, Nat.add(Nat.add(EB, 0n), Nat.add(e, 0n)), Nat.add(EB, Nat.add(0n, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, 0n)), NA.add_assoc(EB, 0n, Nat.add(e, 0n)), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(0n, Nat.add(e, 0n)), Nat.add(e, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(e, 0n)), Nat.add(e, Nat.add(0n, 0n)), Nat.add(e, 0n), NA.add_swap(0n, e, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(e, 0n))), Nat.add(sx, Nat.add(EB, Nat.add(e, Nat.add(sy, 0n)))), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(e, 0n))), Nat.add(sx, Nat.add(Nat.add(sy, 0n), Nat.add(EB, Nat.add(e, 0n)))), Nat.add(sx, Nat.add(EB, Nat.add(e, Nat.add(sy, 0n)))), NA.add_assoc(sx, Nat.add(sy, 0n), Nat.add(EB, Nat.add(e, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(Nat.add(sy, 0n), Nat.add(EB, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, Nat.add(sy, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(EB, Nat.add(e, 0n))), Nat.add(sy, Nat.add(EB, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, Nat.add(sy, 0n))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(EB, Nat.add(e, 0n))), Nat.add(sy, Nat.add(0n, Nat.add(EB, Nat.add(e, 0n)))), Nat.add(sy, Nat.add(EB, Nat.add(e, 0n))), NA.add_assoc(sy, 0n, Nat.add(EB, Nat.add(e, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(EB, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(EB, Nat.add(e, 0n))), Nat.add(EB, Nat.add(0n, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, 0n)), NA.add_swap(0n, EB, Nat.add(e, 0n)), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(0n, Nat.add(e, 0n)), Nat.add(e, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(e, 0n)), Nat.add(e, Nat.add(0n, 0n)), Nat.add(e, 0n), NA.add_swap(0n, e, 0n), {==}))))), Equal.trans(Nat, Nat.add(sy, Nat.add(EB, Nat.add(e, 0n))), Nat.add(EB, Nat.add(sy, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, Nat.add(sy, 0n))), NA.add_swap(sy, EB, Nat.add(e, 0n)), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(sy, Nat.add(e, 0n)), Nat.add(e, Nat.add(sy, 0n)), NA.add_swap(sy, e, 0n)))))), Equal.trans(Nat, Nat.add(sx, Nat.add(EB, Nat.add(e, Nat.add(sy, 0n)))), Nat.add(EB, Nat.add(sx, Nat.add(e, Nat.add(sy, 0n)))), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), NA.add_swap(sx, EB, Nat.add(e, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(sx, Nat.add(e, Nat.add(sy, 0n))), Nat.add(e, Nat.add(sx, Nat.add(sy, 0n))), NA.add_swap(sx, e, Nat.add(sy, 0n)))))), Equal.sym(Nat, Nat.add(Nat.add(e, EB), Nat.add(sy, sx)), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(e, EB), Nat.add(sy, sx)), Nat.add(Nat.add(EB, Nat.add(e, 0n)), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(e, EB), Nat.add(sy, sx)), Nat.add(Nat.add(EB, Nat.add(e, 0n)), Nat.add(sy, sx)), Nat.add(Nat.add(EB, Nat.add(e, 0n)), Nat.add(sx, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sy, sx)), Nat.add(e, EB), Nat.add(EB, Nat.add(e, 0n)), Equal.trans(Nat, Nat.add(e, EB), Nat.add(Nat.add(e, 0n), Nat.add(EB, 0n)), Nat.add(EB, Nat.add(e, 0n)), Equal.trans(Nat, Nat.add(e, EB), Nat.add(Nat.add(e, 0n), EB), Nat.add(Nat.add(e, 0n), Nat.add(EB, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, EB), e, Nat.add(e, 0n), Equal.sym(Nat, Nat.add(e, 0n), e, N.add_zero(e))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(e, 0n), z), EB, Nat.add(EB, 0n), Equal.sym(Nat, Nat.add(EB, 0n), EB, N.add_zero(EB)))), Equal.trans(Nat, Nat.add(Nat.add(e, 0n), Nat.add(EB, 0n)), Nat.add(e, Nat.add(EB, 0n)), Nat.add(EB, Nat.add(e, 0n)), Equal.trans(Nat, Nat.add(Nat.add(e, 0n), Nat.add(EB, 0n)), Nat.add(e, Nat.add(0n, Nat.add(EB, 0n))), Nat.add(e, Nat.add(EB, 0n)), NA.add_assoc(e, 0n, Nat.add(EB, 0n)), Equal.cong(Nat, Nat, z => Nat.add(e, z), Nat.add(0n, Nat.add(EB, 0n)), Nat.add(EB, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(EB, 0n)), Nat.add(EB, Nat.add(0n, 0n)), Nat.add(EB, 0n), NA.add_swap(0n, EB, 0n), {==}))), NA.add_swap(e, EB, 0n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EB, Nat.add(e, 0n)), z), Nat.add(sy, sx), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sx), 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), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(sx, 0n))), Nat.add(sy, Nat.add(sx, 0n)), NA.add_assoc(sy, 0n, Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(0n, 0n)), Nat.add(sx, 0n), NA.add_swap(0n, sx, 0n), {==}))), NA.add_swap(sy, sx, 0n))))), Equal.trans(Nat, Nat.add(Nat.add(EB, Nat.add(e, 0n)), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(EB, Nat.add(Nat.add(e, 0n), Nat.add(sx, Nat.add(sy, 0n)))), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), NA.add_assoc(EB, Nat.add(e, 0n), Nat.add(sx, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(EB, z), Nat.add(Nat.add(e, 0n), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(e, Nat.add(sx, Nat.add(sy, 0n))), Equal.trans(Nat, Nat.add(Nat.add(e, 0n), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(e, Nat.add(0n, Nat.add(sx, Nat.add(sy, 0n)))), Nat.add(e, Nat.add(sx, Nat.add(sy, 0n))), NA.add_assoc(e, 0n, Nat.add(sx, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(e, z), Nat.add(0n, Nat.add(sx, Nat.add(sy, 0n))), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, Nat.add(sy, 0n))), Nat.add(sx, Nat.add(0n, Nat.add(sy, 0n))), Nat.add(sx, Nat.add(sy, 0n)), NA.add_swap(0n, sx, Nat.add(sy, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sx, 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.cong(Nat, Nat, w => Nat.add(w, Nat.add(sy, sx)), Nat.add(e, EB), Nat.add(EA, Nat.add(4096n, K)), hd)), Equal.trans(Nat, Nat.add(Nat.add(EA, Nat.add(4096n, K)), Nat.add(sy, sx)), Nat.add(EA, Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n)))), Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(EA, Nat.add(4096n, K)), Nat.add(sy, sx)), Nat.add(Nat.add(EA, Nat.add(K, 4096n)), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(EA, Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n)))), Equal.trans(Nat, Nat.add(Nat.add(EA, Nat.add(4096n, K)), Nat.add(sy, sx)), Nat.add(Nat.add(EA, Nat.add(K, 4096n)), Nat.add(sy, sx)), Nat.add(Nat.add(EA, Nat.add(K, 4096n)), Nat.add(sx, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sy, sx)), Nat.add(EA, Nat.add(4096n, K)), Nat.add(EA, Nat.add(K, 4096n)), Equal.trans(Nat, Nat.add(EA, Nat.add(4096n, K)), Nat.add(Nat.add(EA, 0n), Nat.add(K, 4096n)), Nat.add(EA, Nat.add(K, 4096n)), Equal.trans(Nat, Nat.add(EA, Nat.add(4096n, K)), Nat.add(Nat.add(EA, 0n), Nat.add(4096n, K)), Nat.add(Nat.add(EA, 0n), Nat.add(K, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(4096n, K)), EA, Nat.add(EA, 0n), Equal.sym(Nat, Nat.add(EA, 0n), EA, N.add_zero(EA))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EA, 0n), z), Nat.add(4096n, K), Nat.add(K, 4096n), Equal.trans(Nat, Nat.add(4096n, K), Nat.add(4096n, Nat.add(K, 0n)), Nat.add(K, 4096n), Equal.cong(Nat, Nat, z => Nat.add(4096n, z), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K))), Equal.trans(Nat, Nat.add(4096n, Nat.add(K, 0n)), Nat.add(K, Nat.add(4096n, 0n)), Nat.add(K, 4096n), NA.add_swap(4096n, K, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(EA, 0n), Nat.add(K, 4096n)), Nat.add(EA, Nat.add(0n, Nat.add(K, 4096n))), Nat.add(EA, Nat.add(K, 4096n)), NA.add_assoc(EA, 0n, Nat.add(K, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(EA, z), Nat.add(0n, Nat.add(K, 4096n)), Nat.add(K, 4096n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 4096n)), Nat.add(K, Nat.add(0n, 4096n)), Nat.add(K, 4096n), NA.add_swap(0n, K, 4096n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EA, Nat.add(K, 4096n)), z), Nat.add(sy, sx), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sx), 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), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(sx, 0n))), Nat.add(sy, Nat.add(sx, 0n)), NA.add_assoc(sy, 0n, Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(0n, 0n)), Nat.add(sx, 0n), NA.add_swap(0n, sx, 0n), {==}))), NA.add_swap(sy, sx, 0n))))), Equal.trans(Nat, Nat.add(Nat.add(EA, Nat.add(K, 4096n)), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(EA, Nat.add(Nat.add(K, 4096n), Nat.add(sx, Nat.add(sy, 0n)))), Nat.add(EA, Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n)))), NA.add_assoc(EA, Nat.add(K, 4096n), Nat.add(sx, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(EA, z), Nat.add(Nat.add(K, 4096n), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(K, 4096n), Nat.add(sx, Nat.add(sy, 0n))), Nat.add(K, Nat.add(4096n, Nat.add(sx, Nat.add(sy, 0n)))), Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n))), NA.add_assoc(K, 4096n, Nat.add(sx, Nat.add(sy, 0n))), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(4096n, Nat.add(sx, Nat.add(sy, 0n))), Nat.add(sx, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(4096n, Nat.add(sx, Nat.add(sy, 0n))), Nat.add(sx, Nat.add(4096n, Nat.add(sy, 0n))), Nat.add(sx, Nat.add(sy, 4096n)), NA.add_swap(4096n, sx, Nat.add(sy, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(4096n, Nat.add(sy, 0n)), Nat.add(sy, 4096n), Equal.trans(Nat, Nat.add(4096n, Nat.add(sy, 0n)), Nat.add(sy, Nat.add(4096n, 0n)), Nat.add(sy, 4096n), NA.add_swap(4096n, sy, 0n), {==})))))))), Equal.sym(Nat, Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(EA, Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n)))), Equal.trans(Nat, Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(EA, Nat.add(sx, 0n)), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(EA, Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n)))), Equal.trans(Nat, Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(EA, Nat.add(sx, 0n)), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(EA, Nat.add(sx, 0n)), Nat.add(K, Nat.add(sy, 4096n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sy, Nat.add(K, 4096n))), Nat.add(EA, sx), Nat.add(EA, Nat.add(sx, 0n)), Equal.trans(Nat, Nat.add(EA, sx), Nat.add(Nat.add(EA, 0n), Nat.add(sx, 0n)), Nat.add(EA, Nat.add(sx, 0n)), Equal.trans(Nat, Nat.add(EA, sx), Nat.add(Nat.add(EA, 0n), sx), Nat.add(Nat.add(EA, 0n), Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sx), EA, Nat.add(EA, 0n), Equal.sym(Nat, Nat.add(EA, 0n), EA, N.add_zero(EA))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EA, 0n), z), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx)))), Equal.trans(Nat, Nat.add(Nat.add(EA, 0n), Nat.add(sx, 0n)), Nat.add(EA, Nat.add(0n, Nat.add(sx, 0n))), Nat.add(EA, Nat.add(sx, 0n)), NA.add_assoc(EA, 0n, Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(EA, z), Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(0n, 0n)), Nat.add(sx, 0n), NA.add_swap(0n, sx, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(EA, Nat.add(sx, 0n)), z), Nat.add(sy, Nat.add(K, 4096n)), Nat.add(K, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 4096n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(K, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 4096n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(K, 4096n)), 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), Nat.add(K, 4096n), Nat.add(K, 4096n), Equal.trans(Nat, Nat.add(K, 4096n), Nat.add(Nat.add(K, 0n), 4096n), Nat.add(K, 4096n), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K))), Equal.trans(Nat, Nat.add(Nat.add(K, 0n), 4096n), Nat.add(K, Nat.add(0n, 4096n)), Nat.add(K, 4096n), NA.add_assoc(K, 0n, 4096n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(sy, Nat.add(K, 4096n)), Nat.add(K, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 4096n))), Nat.add(sy, Nat.add(K, 4096n)), NA.add_assoc(sy, 0n, Nat.add(K, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 4096n)), Nat.add(K, 4096n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 4096n)), Nat.add(K, Nat.add(0n, 4096n)), Nat.add(K, 4096n), NA.add_swap(0n, K, 4096n), {==}))), NA.add_swap(sy, K, 4096n))))), Equal.trans(Nat, Nat.add(Nat.add(EA, Nat.add(sx, 0n)), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(EA, Nat.add(Nat.add(sx, 0n), Nat.add(K, Nat.add(sy, 4096n)))), Nat.add(EA, Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n)))), NA.add_assoc(EA, Nat.add(sx, 0n), Nat.add(K, Nat.add(sy, 4096n))), Equal.cong(Nat, Nat, z => Nat.add(EA, z), Nat.add(Nat.add(sx, 0n), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(sx, Nat.add(K, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(sx, Nat.add(sy, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(sx, Nat.add(0n, Nat.add(K, Nat.add(sy, 4096n)))), Nat.add(sx, Nat.add(K, Nat.add(sy, 4096n))), NA.add_assoc(sx, 0n, Nat.add(K, Nat.add(sy, 4096n))), Equal.cong(Nat, Nat, z => Nat.add(sx, z), Nat.add(0n, Nat.add(K, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(0n, Nat.add(K, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(0n, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(sy, 4096n)), NA.add_swap(0n, K, Nat.add(sy, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(0n, Nat.add(sy, 4096n)), Nat.add(sy, 4096n), Equal.trans(Nat, Nat.add(0n, Nat.add(sy, 4096n)), Nat.add(sy, Nat.add(0n, 4096n)), Nat.add(sy, 4096n), NA.add_swap(0n, sy, 4096n), {==}))))), NA.add_swap(sx, K, Nat.add(sy, 4096n))))))))), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.add(sy, Nat.add(K, 4096n))), Nat.add(EA, sx), Nat.add(XX, 2171n), hEAx)), Equal.trans(Nat, Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(XX, 2171n), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(XX, 2171n), Nat.add(K, Nat.add(sy, 4096n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sy, Nat.add(K, 4096n))), Nat.add(XX, 2171n), Nat.add(XX, 2171n), Equal.trans(Nat, Nat.add(XX, 2171n), Nat.add(Nat.add(XX, 0n), 2171n), Nat.add(XX, 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), 2171n), Nat.add(XX, Nat.add(0n, 2171n)), Nat.add(XX, 2171n), NA.add_assoc(XX, 0n, 2171n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 2171n), z), Nat.add(sy, Nat.add(K, 4096n)), Nat.add(K, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 4096n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(K, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 4096n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(K, 4096n)), 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), Nat.add(K, 4096n), Nat.add(K, 4096n), Equal.trans(Nat, Nat.add(K, 4096n), Nat.add(Nat.add(K, 0n), 4096n), Nat.add(K, 4096n), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K))), Equal.trans(Nat, Nat.add(Nat.add(K, 0n), 4096n), Nat.add(K, Nat.add(0n, 4096n)), Nat.add(K, 4096n), NA.add_assoc(K, 0n, 4096n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(sy, Nat.add(K, 4096n)), Nat.add(K, Nat.add(sy, 4096n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 4096n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 4096n))), Nat.add(sy, Nat.add(K, 4096n)), NA.add_assoc(sy, 0n, Nat.add(K, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 4096n)), Nat.add(K, 4096n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 4096n)), Nat.add(K, Nat.add(0n, 4096n)), Nat.add(K, 4096n), NA.add_swap(0n, K, 4096n), {==}))), NA.add_swap(sy, K, 4096n))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 2171n), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 2171n), Nat.add(K, Nat.add(sy, 4096n))), Nat.add(XX, Nat.add(2171n, Nat.add(K, Nat.add(sy, 4096n)))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), NA.add_assoc(XX, 2171n, Nat.add(K, Nat.add(sy, 4096n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(2171n, Nat.add(K, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(2171n, Nat.add(K, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(2171n, Nat.add(sy, 4096n))), Nat.add(K, Nat.add(sy, 6267n)), NA.add_swap(2171n, K, Nat.add(sy, 4096n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(2171n, Nat.add(sy, 4096n)), Nat.add(sy, 6267n), Equal.trans(Nat, Nat.add(2171n, Nat.add(sy, 4096n)), Nat.add(sy, Nat.add(2171n, 4096n)), Nat.add(sy, 6267n), NA.add_swap(2171n, sy, 4096n), {==}))))), NA.add_swap(XX, K, Nat.add(sy, 6267n)))), Equal.sym(Nat, Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(XX, 0n), Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sy, Nat.add(K, 6267n))), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 0n), z), Nat.add(sy, Nat.add(K, 6267n)), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 6267n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(sy, Nat.add(K, 6267n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(K, 6267n)), 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), Nat.add(K, 6267n), Nat.add(K, 6267n), Equal.trans(Nat, Nat.add(K, 6267n), Nat.add(Nat.add(K, 0n), 6267n), Nat.add(K, 6267n), Equal.cong(Nat, Nat, z => Nat.add(z, 6267n), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K))), Equal.trans(Nat, Nat.add(Nat.add(K, 0n), 6267n), Nat.add(K, Nat.add(0n, 6267n)), Nat.add(K, 6267n), NA.add_assoc(K, 0n, 6267n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(sy, Nat.add(K, 6267n)), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 6267n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 6267n))), Nat.add(sy, Nat.add(K, 6267n)), NA.add_assoc(sy, 0n, Nat.add(K, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 6267n)), Nat.add(K, 6267n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 6267n)), Nat.add(K, Nat.add(0n, 6267n)), Nat.add(K, 6267n), NA.add_swap(0n, K, 6267n), {==}))), NA.add_swap(sy, K, 6267n))))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(XX, Nat.add(sy, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(K, Nat.add(sy, 6267n))), Nat.add(XX, Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n)))), Nat.add(XX, Nat.add(K, Nat.add(sy, 6267n))), NA.add_assoc(XX, 0n, Nat.add(K, Nat.add(sy, 6267n))), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(sy, 6267n)), Equal.trans(Nat, Nat.add(0n, Nat.add(K, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(0n, Nat.add(sy, 6267n))), Nat.add(K, Nat.add(sy, 6267n)), NA.add_swap(0n, K, Nat.add(sy, 6267n)), Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(0n, Nat.add(sy, 6267n)), Nat.add(sy, 6267n), Equal.trans(Nat, Nat.add(0n, Nat.add(sy, 6267n)), Nat.add(sy, Nat.add(0n, 6267n)), Nat.add(sy, 6267n), NA.add_swap(0n, sy, 6267n), {==}))))), NA.add_swap(XX, K, Nat.add(sy, 6267n)))))))  +all = Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), lh, Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), lz, Equal.sym(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), rh)))  +c1 = NR.add_cancel(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(EB, e), all)  +c2 = Equal.trans(Nat, Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(EB, e), Nat.add(EB, e), c1, {==})  NR.add_cancel(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n), e, c1)