import Base
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR

# Exponent bookkeeping for Sqrt.value: with the spec exponent made even
# (XX = 2q + cs) and the implementation's made odd (EN = Ep + ci,
# 2p + 1075 = Ep + 4096), the root's rounding cut j (2j + 72 + sa + ci =
# 200 + cs) lines the spec's ulp up with roundPackToF64's.

def sqexp(+q: Nat, +p: Nat, +j: Nat, +x: Nat, +XX: Nat, +EN: Nat, +Ep: Nat, +sa: Nat, +ci: Nat, +cs: Nat, +hq: {Nat.add(Nat.add(q, q), cs) == XX : Nat}, +hp: {Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat}, +hE: {Nat.add(Ep, ci) == EN : Nat}, +hEN: {Nat.add(EN, sa) == Nat.add(XX, 2171n) : Nat}, +hj: {Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))) == Nat.add(200n, cs) : Nat}, +hx: {Nat.add(x, 2180n) == Nat.add(p, 1048n) : Nat}) -> {Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)) == x : Nat}:
  +A = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(XX, Nat.add(Nat.add(200n, cs), 2800n)), Nat.add(cs, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(XX, Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(XX, Nat.add(Nat.add(200n, cs), 2800n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(XX, Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(q, 1400n)), z), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n)))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), NA.add_assoc(j, Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n)))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), NA.add_assoc(q, 1400n, Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), Equal.trans(Nat, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(1400n, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), NA.add_swap(1400n, j, Nat.add(q, 1400n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, 2800n), Equal.trans(Nat, Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, Nat.add(1400n, 1400n)), Nat.add(q, 2800n), NA.add_swap(1400n, q, 1400n), {==}))))), NA.add_swap(q, j, Nat.add(q, 2800n))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), z), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(cs, 0n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), cs), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, cs), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, Nat.add(sa, 72n)), z), cs, Nat.add(cs, 0n), Equal.sym(Nat, Nat.add(cs, 0n), cs, N.add_zero(cs)))), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(cs, 0n)), Nat.add(ci, Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))), NA.add_assoc(ci, Nat.add(sa, 72n), Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n)), Nat.add(cs, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n)), Nat.add(sa, Nat.add(cs, 72n)), Nat.add(cs, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n)), Nat.add(sa, Nat.add(72n, Nat.add(cs, 0n))), Nat.add(sa, Nat.add(cs, 72n)), NA.add_assoc(sa, 72n, Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(72n, Nat.add(cs, 0n)), Nat.add(cs, 72n), Equal.trans(Nat, Nat.add(72n, Nat.add(cs, 0n)), Nat.add(cs, Nat.add(72n, 0n)), Nat.add(cs, 72n), NA.add_swap(72n, cs, 0n), {==}))), NA.add_swap(sa, cs, 72n))))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_assoc(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_assoc(j, Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_assoc(q, Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n)))), NA.add_assoc(q, 2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(2800n, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n))), NA.add_swap(2800n, ci, Nat.add(cs, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(2800n, Nat.add(cs, Nat.add(sa, 72n))), Nat.add(cs, Nat.add(sa, 2872n)), Equal.trans(Nat, Nat.add(2800n, Nat.add(cs, Nat.add(sa, 72n))), Nat.add(cs, Nat.add(2800n, Nat.add(sa, 72n))), Nat.add(cs, Nat.add(sa, 2872n)), NA.add_swap(2800n, cs, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(cs, z), Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, 2872n), Equal.trans(Nat, Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(2800n, 72n)), Nat.add(sa, 2872n), NA.add_swap(2800n, sa, 72n), {==}))))))), Equal.trans(Nat, Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(q, Nat.add(cs, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(q, ci, Nat.add(cs, Nat.add(sa, 2872n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(q, Nat.add(cs, Nat.add(sa, 2872n))), Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))), NA.add_swap(q, cs, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(q, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(q, ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(q, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(q, cs, Nat.add(q, Nat.add(sa, 2872n)))))))), Equal.trans(Nat, Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(j, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(j, ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(j, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(j, cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))))), Equal.trans(Nat, Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(j, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_swap(j, ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(j, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(j, cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(Nat.add(q, q), cs), Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Equal.trans(Nat, Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(cs, 0n)), Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Equal.trans(Nat, Nat.add(Nat.add(q, q), cs), Nat.add(Nat.add(q, Nat.add(q, 0n)), cs), Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, cs), Nat.add(q, q), Nat.add(q, Nat.add(q, 0n)), Equal.trans(Nat, Nat.add(q, q), Nat.add(Nat.add(q, 0n), Nat.add(q, 0n)), Nat.add(q, Nat.add(q, 0n)), Equal.trans(Nat, Nat.add(q, q), Nat.add(Nat.add(q, 0n), q), Nat.add(Nat.add(q, 0n), Nat.add(q, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, q), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 0n), z), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q)))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), Nat.add(q, 0n)), Nat.add(q, Nat.add(0n, Nat.add(q, 0n))), Nat.add(q, Nat.add(q, 0n)), NA.add_assoc(q, 0n, Nat.add(q, 0n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(0n, Nat.add(q, 0n)), Nat.add(q, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(q, 0n)), Nat.add(q, Nat.add(0n, 0n)), Nat.add(q, 0n), NA.add_swap(0n, q, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, Nat.add(q, 0n)), z), cs, Nat.add(cs, 0n), Equal.sym(Nat, Nat.add(cs, 0n), cs, N.add_zero(cs)))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(cs, 0n)), Nat.add(q, Nat.add(cs, Nat.add(q, 0n))), Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(cs, 0n)), Nat.add(q, Nat.add(Nat.add(q, 0n), Nat.add(cs, 0n))), Nat.add(q, Nat.add(cs, Nat.add(q, 0n))), NA.add_assoc(q, Nat.add(q, 0n), Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(Nat.add(q, 0n), Nat.add(cs, 0n)), Nat.add(cs, Nat.add(q, 0n)), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), Nat.add(cs, 0n)), Nat.add(q, Nat.add(cs, 0n)), Nat.add(cs, Nat.add(q, 0n)), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), Nat.add(cs, 0n)), Nat.add(q, Nat.add(0n, Nat.add(cs, 0n))), Nat.add(q, Nat.add(cs, 0n)), NA.add_assoc(q, 0n, Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(0n, Nat.add(cs, 0n)), Nat.add(cs, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(cs, 0n)), Nat.add(cs, Nat.add(0n, 0n)), Nat.add(cs, 0n), NA.add_swap(0n, cs, 0n), {==}))), NA.add_swap(q, cs, 0n)))), NA.add_swap(q, cs, Nat.add(q, 0n))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), z), Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n), Nat.add(Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 72n)))), 2800n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(z, 2800n), Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(72n, Nat.add(sa, ci))), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(72n, Nat.add(sa, ci))), Nat.add(j, j), Nat.add(j, Nat.add(j, 0n)), Equal.trans(Nat, Nat.add(j, j), Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Nat.add(j, Nat.add(j, 0n)), Equal.trans(Nat, Nat.add(j, j), Nat.add(Nat.add(j, 0n), j), Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, j), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, 0n), z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Nat.add(j, Nat.add(0n, Nat.add(j, 0n))), Nat.add(j, Nat.add(j, 0n)), NA.add_assoc(j, 0n, Nat.add(j, 0n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(j, 0n)), Nat.add(j, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(j, 0n)), Nat.add(j, Nat.add(0n, 0n)), Nat.add(j, 0n), NA.add_swap(0n, j, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(j, 0n)), z), Nat.add(72n, Nat.add(sa, ci)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(72n, Nat.add(sa, ci)), Nat.add(72n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(72n, z), Nat.add(sa, ci), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(sa, ci), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 0n)), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(sa, ci), Nat.add(Nat.add(sa, 0n), ci), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, ci), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci)))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 0n)), Nat.add(sa, Nat.add(ci, 0n)), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 0n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 0n))), Nat.add(sa, Nat.add(ci, 0n)), NA.add_assoc(sa, 0n, Nat.add(ci, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 0n)), Nat.add(ci, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 0n)), Nat.add(ci, Nat.add(0n, 0n)), Nat.add(ci, 0n), NA.add_swap(0n, ci, 0n), {==}))), NA.add_swap(sa, ci, 0n)))), Equal.trans(Nat, Nat.add(72n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(72n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 72n)), NA.add_swap(72n, ci, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(72n, Nat.add(sa, 0n)), Nat.add(sa, 72n), Equal.trans(Nat, Nat.add(72n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(72n, 0n)), Nat.add(sa, 72n), NA.add_swap(72n, sa, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(ci, Nat.add(j, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(Nat.add(j, 0n), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(j, Nat.add(sa, 72n)))), NA.add_assoc(j, Nat.add(j, 0n), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(j, Nat.add(sa, 72n))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(j, Nat.add(sa, 72n))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(sa, 72n))), NA.add_assoc(j, 0n, Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(0n, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 72n)), NA.add_swap(0n, ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 72n)), Nat.add(sa, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(0n, 72n)), Nat.add(sa, 72n), NA.add_swap(0n, sa, 72n), {==}))))), NA.add_swap(j, ci, Nat.add(sa, 72n))))), NA.add_swap(j, ci, Nat.add(j, Nat.add(sa, 72n)))))), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 72n)))), 2800n), Nat.add(ci, Nat.add(Nat.add(j, Nat.add(j, Nat.add(sa, 72n))), 2800n)), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), NA.add_assoc(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 72n))), 2800n), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(j, Nat.add(j, Nat.add(sa, 72n))), 2800n), Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(sa, 72n))), 2800n), Nat.add(j, Nat.add(Nat.add(j, Nat.add(sa, 72n)), 2800n)), Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))), NA.add_assoc(j, Nat.add(j, Nat.add(sa, 72n)), 2800n), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, Nat.add(sa, 72n)), 2800n), Nat.add(j, Nat.add(sa, 2872n)), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(sa, 72n)), 2800n), Nat.add(j, Nat.add(Nat.add(sa, 72n), 2800n)), Nat.add(j, Nat.add(sa, 2872n)), NA.add_assoc(j, Nat.add(sa, 72n), 2800n), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(sa, 72n), 2800n), Nat.add(sa, 2872n), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), 2800n), Nat.add(sa, Nat.add(72n, 2800n)), Nat.add(sa, 2872n), NA.add_assoc(sa, 72n, 2800n), {==})))))))))), Equal.trans(Nat, Nat.add(Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(cs, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(cs, Nat.add(q, Nat.add(q, 0n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(cs, Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))))), Nat.add(cs, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_assoc(cs, Nat.add(q, Nat.add(q, 0n)), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(cs, z), Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(q, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 0n)), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(q, Nat.add(Nat.add(q, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))))), Nat.add(q, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_assoc(q, Nat.add(q, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(Nat.add(q, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(q, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(q, Nat.add(0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))))), Nat.add(q, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), NA.add_assoc(q, 0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(0n, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), NA.add_swap(0n, ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(0n, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Nat.add(j, Nat.add(0n, Nat.add(j, Nat.add(sa, 2872n)))), Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))), NA.add_swap(0n, j, Nat.add(j, Nat.add(sa, 2872n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(j, Nat.add(sa, 2872n))), Nat.add(j, Nat.add(sa, 2872n)), Equal.trans(Nat, Nat.add(0n, Nat.add(j, Nat.add(sa, 2872n))), Nat.add(j, Nat.add(0n, Nat.add(sa, 2872n))), Nat.add(j, Nat.add(sa, 2872n)), NA.add_swap(0n, j, Nat.add(sa, 2872n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(sa, 2872n)), Nat.add(sa, 2872n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 2872n)), Nat.add(sa, Nat.add(0n, 2872n)), Nat.add(sa, 2872n), NA.add_swap(0n, sa, 2872n), {==}))))))))), Equal.trans(Nat, Nat.add(q, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(q, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(q, ci, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(q, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(q, Nat.add(j, Nat.add(j, Nat.add(sa, 2872n)))), Nat.add(j, Nat.add(q, Nat.add(j, Nat.add(sa, 2872n)))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(q, j, Nat.add(j, Nat.add(sa, 2872n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(q, Nat.add(j, Nat.add(sa, 2872n))), Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))), NA.add_swap(q, j, Nat.add(sa, 2872n))))))))), Equal.trans(Nat, Nat.add(q, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(q, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(q, ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(q, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(q, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(j, Nat.add(q, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(q, j, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(q, Nat.add(j, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(q, j, Nat.add(q, Nat.add(sa, 2872n)))))))))), NA.add_swap(cs, ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))))))), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.add(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), 2800n)), Nat.add(Nat.add(q, q), cs), XX, hq)), Equal.cong(Nat, Nat, w => Nat.add(XX, Nat.add(w, 2800n)), Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), Nat.add(200n, cs), hj)), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(200n, cs), 2800n)), Nat.add(XX, Nat.add(cs, 3000n)), Nat.add(cs, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(200n, cs), 2800n)), Nat.add(Nat.add(XX, 0n), Nat.add(cs, 3000n)), Nat.add(XX, Nat.add(cs, 3000n)), Equal.trans(Nat, Nat.add(XX, Nat.add(Nat.add(200n, cs), 2800n)), Nat.add(Nat.add(XX, 0n), Nat.add(Nat.add(200n, cs), 2800n)), Nat.add(Nat.add(XX, 0n), Nat.add(cs, 3000n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(200n, cs), 2800n)), 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(200n, cs), 2800n), Nat.add(cs, 3000n), Equal.trans(Nat, Nat.add(Nat.add(200n, cs), 2800n), Nat.add(Nat.add(cs, 200n), 2800n), Nat.add(cs, 3000n), Equal.cong(Nat, Nat, z => Nat.add(z, 2800n), Nat.add(200n, cs), Nat.add(cs, 200n), Equal.trans(Nat, Nat.add(200n, cs), Nat.add(200n, Nat.add(cs, 0n)), Nat.add(cs, 200n), Equal.cong(Nat, Nat, z => Nat.add(200n, z), cs, Nat.add(cs, 0n), Equal.sym(Nat, Nat.add(cs, 0n), cs, N.add_zero(cs))), Equal.trans(Nat, Nat.add(200n, Nat.add(cs, 0n)), Nat.add(cs, Nat.add(200n, 0n)), Nat.add(cs, 200n), NA.add_swap(200n, cs, 0n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(cs, 200n), 2800n), Nat.add(cs, Nat.add(200n, 2800n)), Nat.add(cs, 3000n), NA.add_assoc(cs, 200n, 2800n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(XX, 0n), Nat.add(cs, 3000n)), Nat.add(XX, Nat.add(0n, Nat.add(cs, 3000n))), Nat.add(XX, Nat.add(cs, 3000n)), NA.add_assoc(XX, 0n, Nat.add(cs, 3000n)), Equal.cong(Nat, Nat, z => Nat.add(XX, z), Nat.add(0n, Nat.add(cs, 3000n)), Nat.add(cs, 3000n), Equal.trans(Nat, Nat.add(0n, Nat.add(cs, 3000n)), Nat.add(cs, Nat.add(0n, 3000n)), Nat.add(cs, 3000n), NA.add_swap(0n, cs, 3000n), {==})))), Equal.sym(Nat, Nat.add(cs, Nat.add(XX, 3000n)), Nat.add(XX, Nat.add(cs, 3000n)), Equal.trans(Nat, Nat.add(cs, Nat.add(XX, 3000n)), Nat.add(Nat.add(cs, 0n), Nat.add(XX, 3000n)), Nat.add(XX, Nat.add(cs, 3000n)), Equal.trans(Nat, Nat.add(cs, Nat.add(XX, 3000n)), Nat.add(Nat.add(cs, 0n), Nat.add(XX, 3000n)), Nat.add(Nat.add(cs, 0n), Nat.add(XX, 3000n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(XX, 3000n)), cs, Nat.add(cs, 0n), Equal.sym(Nat, Nat.add(cs, 0n), cs, N.add_zero(cs))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(cs, 0n), z), 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.trans(Nat, Nat.add(Nat.add(cs, 0n), Nat.add(XX, 3000n)), Nat.add(cs, Nat.add(XX, 3000n)), Nat.add(XX, Nat.add(cs, 3000n)), Equal.trans(Nat, Nat.add(Nat.add(cs, 0n), Nat.add(XX, 3000n)), Nat.add(cs, Nat.add(0n, Nat.add(XX, 3000n))), Nat.add(cs, Nat.add(XX, 3000n)), NA.add_assoc(cs, 0n, Nat.add(XX, 3000n)), Equal.cong(Nat, Nat, z => Nat.add(cs, z), Nat.add(0n, Nat.add(XX, 3000n)), Nat.add(XX, 3000n), Equal.trans(Nat, Nat.add(0n, Nat.add(XX, 3000n)), Nat.add(XX, Nat.add(0n, 3000n)), Nat.add(XX, 3000n), NA.add_swap(0n, XX, 3000n), {==}))), NA.add_swap(cs, XX, 3000n))))))
  +A2 = NR.add_cancel(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(XX, 3000n), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(cs, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(cs, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(cs, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(cs, 0n), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(cs, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n)))), cs, Nat.add(cs, 0n), Equal.sym(Nat, Nat.add(cs, 0n), cs, N.add_zero(cs))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(cs, 0n), z), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(q, 1400n)), z), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n)))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), NA.add_assoc(j, Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n)))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), NA.add_assoc(q, 1400n, Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), Equal.trans(Nat, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(1400n, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), NA.add_swap(1400n, j, Nat.add(q, 1400n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, 2800n), Equal.trans(Nat, Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, Nat.add(1400n, 1400n)), Nat.add(q, 2800n), NA.add_swap(1400n, q, 1400n), {==}))))), NA.add_swap(q, j, Nat.add(q, 2800n))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), z), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_assoc(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_assoc(j, Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_assoc(q, Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(ci, Nat.add(sa, 2872n))), Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(2800n, Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(sa, 2872n))), NA.add_assoc(q, 2800n, Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(2800n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 2872n)), Equal.trans(Nat, Nat.add(2800n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(2800n, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 2872n)), NA.add_swap(2800n, ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, 2872n), Equal.trans(Nat, Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(2800n, 72n)), Nat.add(sa, 2872n), NA.add_swap(2800n, sa, 72n), {==}))))), NA.add_swap(q, ci, Nat.add(sa, 2872n))))), NA.add_swap(q, ci, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(j, ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_swap(j, ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))))), Equal.trans(Nat, Nat.add(Nat.add(cs, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(cs, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(cs, 0n), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(cs, Nat.add(0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))))), Nat.add(cs, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_assoc(cs, 0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.cong(Nat, Nat, z => Nat.add(cs, z), Nat.add(0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(0n, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(0n, ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(0n, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(j, Nat.add(0n, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(0n, j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(0n, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(j, Nat.add(0n, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(0n, j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(0n, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(q, Nat.add(0n, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))), NA.add_swap(0n, q, Nat.add(q, Nat.add(sa, 2872n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(0n, Nat.add(q, Nat.add(sa, 2872n))), Nat.add(q, Nat.add(sa, 2872n)), Equal.trans(Nat, Nat.add(0n, Nat.add(q, Nat.add(sa, 2872n))), Nat.add(q, Nat.add(0n, Nat.add(sa, 2872n))), Nat.add(q, Nat.add(sa, 2872n)), NA.add_swap(0n, q, Nat.add(sa, 2872n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(0n, Nat.add(sa, 2872n)), Nat.add(sa, 2872n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 2872n)), Nat.add(sa, Nat.add(0n, 2872n)), Nat.add(sa, 2872n), NA.add_swap(0n, sa, 2872n), {==}))))))))))))), NA.add_swap(cs, ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(q, 1400n)), z), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n)))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), NA.add_assoc(j, Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n)))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), NA.add_assoc(q, 1400n, Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), Equal.trans(Nat, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(1400n, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), NA.add_swap(1400n, j, Nat.add(q, 1400n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, 2800n), Equal.trans(Nat, Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, Nat.add(1400n, 1400n)), Nat.add(q, 2800n), NA.add_swap(1400n, q, 1400n), {==}))))), NA.add_swap(q, j, Nat.add(q, 2800n))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), z), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(cs, 0n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), cs), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), cs), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, cs), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, Nat.add(sa, 72n)), z), cs, Nat.add(cs, 0n), Equal.sym(Nat, Nat.add(cs, 0n), cs, N.add_zero(cs)))), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(cs, 0n)), Nat.add(ci, Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))), NA.add_assoc(ci, Nat.add(sa, 72n), Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n)), Nat.add(cs, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n)), Nat.add(sa, Nat.add(cs, 72n)), Nat.add(cs, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), Nat.add(cs, 0n)), Nat.add(sa, Nat.add(72n, Nat.add(cs, 0n))), Nat.add(sa, Nat.add(cs, 72n)), NA.add_assoc(sa, 72n, Nat.add(cs, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(72n, Nat.add(cs, 0n)), Nat.add(cs, 72n), Equal.trans(Nat, Nat.add(72n, Nat.add(cs, 0n)), Nat.add(cs, Nat.add(72n, 0n)), Nat.add(cs, 72n), NA.add_swap(72n, cs, 0n), {==}))), NA.add_swap(sa, cs, 72n))))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_assoc(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_assoc(j, Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_assoc(q, Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n))))), Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n)))), NA.add_assoc(q, 2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(2800n, Nat.add(ci, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(2800n, Nat.add(cs, Nat.add(sa, 72n)))), Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n))), NA.add_swap(2800n, ci, Nat.add(cs, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(2800n, Nat.add(cs, Nat.add(sa, 72n))), Nat.add(cs, Nat.add(sa, 2872n)), Equal.trans(Nat, Nat.add(2800n, Nat.add(cs, Nat.add(sa, 72n))), Nat.add(cs, Nat.add(2800n, Nat.add(sa, 72n))), Nat.add(cs, Nat.add(sa, 2872n)), NA.add_swap(2800n, cs, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(cs, z), Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, 2872n), Equal.trans(Nat, Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(2800n, 72n)), Nat.add(sa, 2872n), NA.add_swap(2800n, sa, 72n), {==}))))))), Equal.trans(Nat, Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(q, Nat.add(cs, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(q, ci, Nat.add(cs, Nat.add(sa, 2872n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(q, Nat.add(cs, Nat.add(sa, 2872n))), Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))), NA.add_swap(q, cs, Nat.add(sa, 2872n))))))), Equal.trans(Nat, Nat.add(q, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(q, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(q, ci, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(q, Nat.add(cs, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(q, cs, Nat.add(q, Nat.add(sa, 2872n)))))))), Equal.trans(Nat, Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(j, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(j, ci, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(j, Nat.add(cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(j, cs, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))))), Equal.trans(Nat, Nat.add(j, Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(j, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), Nat.add(ci, Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_swap(j, ci, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(j, Nat.add(cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(cs, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(j, cs, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))))))), A))
  +B = Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(XX, 2171n), 6192n), Nat.add(5363n, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(EN, sa), 6192n), Nat.add(Nat.add(XX, 2171n), 6192n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Ep, ci), sa), 6192n), Nat.add(Nat.add(EN, sa), 6192n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), 2096n), Nat.add(Nat.add(Nat.add(Ep, ci), sa), 6192n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), 2096n), Nat.add(Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), 2096n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), 2096n), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(1075n, Nat.add(ci, sa))), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), Nat.add(Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(1075n, Nat.add(ci, sa))), Equal.trans(Nat, Nat.add(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n)))), Nat.add(5363n, Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n))))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), Equal.cong(Nat, Nat, z => Nat.add(5363n, z), Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sa, Nat.add(ci, 72n))), Nat.add(x, x), Nat.add(x, Nat.add(x, 0n)), Equal.trans(Nat, Nat.add(x, x), Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Nat.add(x, Nat.add(x, 0n)), Equal.trans(Nat, Nat.add(x, x), Nat.add(Nat.add(x, 0n), x), Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, x), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, 0n), z), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x)))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Nat.add(x, Nat.add(0n, Nat.add(x, 0n))), Nat.add(x, Nat.add(x, 0n)), NA.add_assoc(x, 0n, Nat.add(x, 0n)), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(0n, Nat.add(x, 0n)), Nat.add(x, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(x, 0n)), Nat.add(x, Nat.add(0n, 0n)), Nat.add(x, 0n), NA.add_swap(0n, x, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, Nat.add(x, 0n)), z), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n))))), Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 72n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 72n)))), NA.add_assoc(x, Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 72n))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 72n))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(x, Nat.add(ci, Nat.add(sa, 72n))), NA.add_assoc(x, 0n, Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(0n, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 72n)), NA.add_swap(0n, ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 72n)), Nat.add(sa, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(0n, 72n)), Nat.add(sa, 72n), NA.add_swap(0n, sa, 72n), {==}))))), Equal.trans(Nat, Nat.add(x, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(x, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 72n))), NA.add_swap(x, ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(x, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(x, 72n)), NA.add_swap(x, sa, 72n)))))), Equal.trans(Nat, Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 72n)))), Nat.add(ci, Nat.add(x, Nat.add(sa, Nat.add(x, 72n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), NA.add_swap(x, ci, Nat.add(sa, Nat.add(x, 72n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(x, Nat.add(sa, Nat.add(x, 72n))), Nat.add(sa, Nat.add(x, Nat.add(x, 72n))), NA.add_swap(x, sa, Nat.add(x, 72n))))))), Equal.trans(Nat, Nat.add(5363n, Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n))))), Nat.add(ci, Nat.add(5363n, Nat.add(sa, Nat.add(x, Nat.add(x, 72n))))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), NA.add_swap(5363n, ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(5363n, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Nat.add(sa, Nat.add(x, Nat.add(x, 5435n))), Equal.trans(Nat, Nat.add(5363n, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Nat.add(sa, Nat.add(5363n, Nat.add(x, Nat.add(x, 72n)))), Nat.add(sa, Nat.add(x, Nat.add(x, 5435n))), NA.add_swap(5363n, sa, Nat.add(x, Nat.add(x, 72n))), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(5363n, Nat.add(x, Nat.add(x, 72n))), Nat.add(x, Nat.add(x, 5435n)), Equal.trans(Nat, Nat.add(5363n, Nat.add(x, Nat.add(x, 72n))), Nat.add(x, Nat.add(5363n, Nat.add(x, 72n))), Nat.add(x, Nat.add(x, 5435n)), NA.add_swap(5363n, x, Nat.add(x, 72n)), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(5363n, Nat.add(x, 72n)), Nat.add(x, 5435n), Equal.trans(Nat, Nat.add(5363n, Nat.add(x, 72n)), Nat.add(x, Nat.add(5363n, 72n)), Nat.add(x, 5435n), NA.add_swap(5363n, x, 72n), {==})))))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(x, Nat.add(x, 4360n)), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(x, Nat.add(x, 4360n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(x, Nat.add(x, 4360n)), Nat.add(ci, Nat.add(sa, 1075n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(x, Nat.add(x, 4360n)), Equal.trans(Nat, Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(x, Nat.add(x, 4360n)), Equal.trans(Nat, Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(x, 2180n)), Nat.add(x, 2180n), Nat.add(x, 2180n), Equal.trans(Nat, Nat.add(x, 2180n), Nat.add(Nat.add(x, 0n), 2180n), Nat.add(x, 2180n), Equal.cong(Nat, Nat, z => Nat.add(z, 2180n), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), 2180n), Nat.add(x, Nat.add(0n, 2180n)), Nat.add(x, 2180n), NA.add_assoc(x, 0n, 2180n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, 2180n), z), Nat.add(x, 2180n), Nat.add(x, 2180n), Equal.trans(Nat, Nat.add(x, 2180n), Nat.add(Nat.add(x, 0n), 2180n), Nat.add(x, 2180n), Equal.cong(Nat, Nat, z => Nat.add(z, 2180n), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), 2180n), Nat.add(x, Nat.add(0n, 2180n)), Nat.add(x, 2180n), NA.add_assoc(x, 0n, 2180n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(x, 2180n), Nat.add(x, 2180n)), Nat.add(x, Nat.add(2180n, Nat.add(x, 2180n))), Nat.add(x, Nat.add(x, 4360n)), NA.add_assoc(x, 2180n, Nat.add(x, 2180n)), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(2180n, Nat.add(x, 2180n)), Nat.add(x, 4360n), Equal.trans(Nat, Nat.add(2180n, Nat.add(x, 2180n)), Nat.add(x, Nat.add(2180n, 2180n)), Nat.add(x, 4360n), NA.add_swap(2180n, x, 2180n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, Nat.add(x, 4360n)), z), Nat.add(1075n, Nat.add(ci, sa)), Nat.add(ci, Nat.add(sa, 1075n)), Equal.trans(Nat, Nat.add(1075n, Nat.add(ci, sa)), Nat.add(1075n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 1075n)), Equal.cong(Nat, Nat, z => Nat.add(1075n, z), Nat.add(ci, sa), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sa), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, 0n), z), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa)))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(0n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 0n)), NA.add_assoc(ci, 0n, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(0n, 0n)), Nat.add(sa, 0n), NA.add_swap(0n, sa, 0n), {==}))))), Equal.trans(Nat, Nat.add(1075n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(1075n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 1075n)), NA.add_swap(1075n, ci, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(1075n, Nat.add(sa, 0n)), Nat.add(sa, 1075n), Equal.trans(Nat, Nat.add(1075n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(1075n, 0n)), Nat.add(sa, 1075n), NA.add_swap(1075n, sa, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(x, 4360n)), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 5435n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(x, 4360n)), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(x, Nat.add(Nat.add(x, 4360n), Nat.add(ci, Nat.add(sa, 1075n)))), Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 5435n)))), NA.add_assoc(x, Nat.add(x, 4360n), Nat.add(ci, Nat.add(sa, 1075n))), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(Nat.add(x, 4360n), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 5435n))), Equal.trans(Nat, Nat.add(Nat.add(x, 4360n), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(x, Nat.add(ci, Nat.add(sa, 5435n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 5435n))), Equal.trans(Nat, Nat.add(Nat.add(x, 4360n), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(x, Nat.add(4360n, Nat.add(ci, Nat.add(sa, 1075n)))), Nat.add(x, Nat.add(ci, Nat.add(sa, 5435n))), NA.add_assoc(x, 4360n, Nat.add(ci, Nat.add(sa, 1075n))), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(4360n, Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(sa, 5435n)), Equal.trans(Nat, Nat.add(4360n, Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(4360n, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(sa, 5435n)), NA.add_swap(4360n, ci, Nat.add(sa, 1075n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(4360n, Nat.add(sa, 1075n)), Nat.add(sa, 5435n), Equal.trans(Nat, Nat.add(4360n, Nat.add(sa, 1075n)), Nat.add(sa, Nat.add(4360n, 1075n)), Nat.add(sa, 5435n), NA.add_swap(4360n, sa, 1075n), {==}))))), Equal.trans(Nat, Nat.add(x, Nat.add(ci, Nat.add(sa, 5435n))), Nat.add(ci, Nat.add(x, Nat.add(sa, 5435n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 5435n))), NA.add_swap(x, ci, Nat.add(sa, 5435n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(x, Nat.add(sa, 5435n)), Nat.add(sa, Nat.add(x, 5435n)), NA.add_swap(x, sa, 5435n)))))), Equal.trans(Nat, Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 5435n)))), Nat.add(ci, Nat.add(x, Nat.add(sa, Nat.add(x, 5435n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 5435n)))), NA.add_swap(x, ci, Nat.add(sa, Nat.add(x, 5435n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(x, Nat.add(sa, Nat.add(x, 5435n))), Nat.add(sa, Nat.add(x, Nat.add(x, 5435n))), NA.add_swap(x, sa, Nat.add(x, 5435n)))))))), Equal.cong(Nat, Nat, w => Nat.add(Nat.add(w, w), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(x, 2180n), Nat.add(p, 1048n), hx)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 3171n)))), Nat.add(Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), 2096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(p, Nat.add(p, 2096n)), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 3171n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(p, Nat.add(p, 2096n)), Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(p, Nat.add(p, 2096n)), Nat.add(ci, Nat.add(sa, 1075n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1075n, Nat.add(ci, sa))), Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(p, Nat.add(p, 2096n)), Equal.trans(Nat, Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(p, Nat.add(p, 2096n)), Equal.trans(Nat, Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(p, 1048n)), Nat.add(p, 1048n), Nat.add(p, 1048n), Equal.trans(Nat, Nat.add(p, 1048n), Nat.add(Nat.add(p, 0n), 1048n), Nat.add(p, 1048n), Equal.cong(Nat, Nat, z => Nat.add(z, 1048n), p, Nat.add(p, 0n), Equal.sym(Nat, Nat.add(p, 0n), p, N.add_zero(p))), Equal.trans(Nat, Nat.add(Nat.add(p, 0n), 1048n), Nat.add(p, Nat.add(0n, 1048n)), Nat.add(p, 1048n), NA.add_assoc(p, 0n, 1048n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(p, 1048n), z), Nat.add(p, 1048n), Nat.add(p, 1048n), Equal.trans(Nat, Nat.add(p, 1048n), Nat.add(Nat.add(p, 0n), 1048n), Nat.add(p, 1048n), Equal.cong(Nat, Nat, z => Nat.add(z, 1048n), p, Nat.add(p, 0n), Equal.sym(Nat, Nat.add(p, 0n), p, N.add_zero(p))), Equal.trans(Nat, Nat.add(Nat.add(p, 0n), 1048n), Nat.add(p, Nat.add(0n, 1048n)), Nat.add(p, 1048n), NA.add_assoc(p, 0n, 1048n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(p, 1048n), Nat.add(p, 1048n)), Nat.add(p, Nat.add(1048n, Nat.add(p, 1048n))), Nat.add(p, Nat.add(p, 2096n)), NA.add_assoc(p, 1048n, Nat.add(p, 1048n)), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(1048n, Nat.add(p, 1048n)), Nat.add(p, 2096n), Equal.trans(Nat, Nat.add(1048n, Nat.add(p, 1048n)), Nat.add(p, Nat.add(1048n, 1048n)), Nat.add(p, 2096n), NA.add_swap(1048n, p, 1048n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(p, Nat.add(p, 2096n)), z), Nat.add(1075n, Nat.add(ci, sa)), Nat.add(ci, Nat.add(sa, 1075n)), Equal.trans(Nat, Nat.add(1075n, Nat.add(ci, sa)), Nat.add(1075n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 1075n)), Equal.cong(Nat, Nat, z => Nat.add(1075n, z), Nat.add(ci, sa), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sa), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, 0n), z), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa)))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(0n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 0n)), NA.add_assoc(ci, 0n, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(0n, 0n)), Nat.add(sa, 0n), NA.add_swap(0n, sa, 0n), {==}))))), Equal.trans(Nat, Nat.add(1075n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(1075n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 1075n)), NA.add_swap(1075n, ci, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(1075n, Nat.add(sa, 0n)), Nat.add(sa, 1075n), Equal.trans(Nat, Nat.add(1075n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(1075n, 0n)), Nat.add(sa, 1075n), NA.add_swap(1075n, sa, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(p, Nat.add(p, 2096n)), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(p, Nat.add(ci, Nat.add(p, Nat.add(sa, 3171n)))), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 3171n)))), Equal.trans(Nat, Nat.add(Nat.add(p, Nat.add(p, 2096n)), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(p, Nat.add(Nat.add(p, 2096n), Nat.add(ci, Nat.add(sa, 1075n)))), Nat.add(p, Nat.add(ci, Nat.add(p, Nat.add(sa, 3171n)))), NA.add_assoc(p, Nat.add(p, 2096n), Nat.add(ci, Nat.add(sa, 1075n))), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(Nat.add(p, 2096n), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(p, Nat.add(sa, 3171n))), Equal.trans(Nat, Nat.add(Nat.add(p, 2096n), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(p, Nat.add(ci, Nat.add(sa, 3171n))), Nat.add(ci, Nat.add(p, Nat.add(sa, 3171n))), Equal.trans(Nat, Nat.add(Nat.add(p, 2096n), Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(p, Nat.add(2096n, Nat.add(ci, Nat.add(sa, 1075n)))), Nat.add(p, Nat.add(ci, Nat.add(sa, 3171n))), NA.add_assoc(p, 2096n, Nat.add(ci, Nat.add(sa, 1075n))), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(2096n, Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(sa, 3171n)), Equal.trans(Nat, Nat.add(2096n, Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(2096n, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(sa, 3171n)), NA.add_swap(2096n, ci, Nat.add(sa, 1075n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(2096n, Nat.add(sa, 1075n)), Nat.add(sa, 3171n), Equal.trans(Nat, Nat.add(2096n, Nat.add(sa, 1075n)), Nat.add(sa, Nat.add(2096n, 1075n)), Nat.add(sa, 3171n), NA.add_swap(2096n, sa, 1075n), {==}))))), NA.add_swap(p, ci, Nat.add(sa, 3171n))))), NA.add_swap(p, ci, Nat.add(p, Nat.add(sa, 3171n))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), 2096n), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 3171n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), 2096n), Nat.add(Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 1075n)))), 2096n), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 3171n)))), Equal.cong(Nat, Nat, z => Nat.add(z, 2096n), Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 1075n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), Nat.add(Nat.add(p, Nat.add(p, 1075n)), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 1075n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(p, p), 1075n), Nat.add(ci, sa)), Nat.add(Nat.add(p, Nat.add(p, 1075n)), Nat.add(ci, sa)), Nat.add(Nat.add(p, Nat.add(p, 1075n)), Nat.add(ci, Nat.add(sa, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, sa)), Nat.add(Nat.add(p, p), 1075n), Nat.add(p, Nat.add(p, 1075n)), Equal.trans(Nat, Nat.add(Nat.add(p, p), 1075n), Nat.add(Nat.add(p, Nat.add(p, 0n)), 1075n), Nat.add(p, Nat.add(p, 1075n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1075n), Nat.add(p, p), Nat.add(p, Nat.add(p, 0n)), Equal.trans(Nat, Nat.add(p, p), Nat.add(Nat.add(p, 0n), Nat.add(p, 0n)), Nat.add(p, Nat.add(p, 0n)), Equal.trans(Nat, Nat.add(p, p), Nat.add(Nat.add(p, 0n), p), Nat.add(Nat.add(p, 0n), Nat.add(p, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, p), 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), p, Nat.add(p, 0n), Equal.sym(Nat, Nat.add(p, 0n), p, N.add_zero(p)))), Equal.trans(Nat, Nat.add(Nat.add(p, 0n), Nat.add(p, 0n)), Nat.add(p, Nat.add(0n, Nat.add(p, 0n))), Nat.add(p, Nat.add(p, 0n)), NA.add_assoc(p, 0n, Nat.add(p, 0n)), Equal.cong(Nat, Nat, z => Nat.add(p, 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), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(p, Nat.add(p, 0n)), 1075n), Nat.add(p, Nat.add(Nat.add(p, 0n), 1075n)), Nat.add(p, Nat.add(p, 1075n)), NA.add_assoc(p, Nat.add(p, 0n), 1075n), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(Nat.add(p, 0n), 1075n), Nat.add(p, 1075n), Equal.trans(Nat, Nat.add(Nat.add(p, 0n), 1075n), Nat.add(p, Nat.add(0n, 1075n)), Nat.add(p, 1075n), NA.add_assoc(p, 0n, 1075n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(p, Nat.add(p, 1075n)), z), Nat.add(ci, sa), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sa), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, 0n), z), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa)))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(0n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 0n)), NA.add_assoc(ci, 0n, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(0n, 0n)), Nat.add(sa, 0n), NA.add_swap(0n, sa, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(p, Nat.add(p, 1075n)), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(p, Nat.add(ci, Nat.add(p, Nat.add(sa, 1075n)))), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 1075n)))), Equal.trans(Nat, Nat.add(Nat.add(p, Nat.add(p, 1075n)), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(p, Nat.add(Nat.add(p, 1075n), Nat.add(ci, Nat.add(sa, 0n)))), Nat.add(p, Nat.add(ci, Nat.add(p, Nat.add(sa, 1075n)))), NA.add_assoc(p, Nat.add(p, 1075n), Nat.add(ci, Nat.add(sa, 0n))), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(Nat.add(p, 1075n), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(p, Nat.add(sa, 1075n))), Equal.trans(Nat, Nat.add(Nat.add(p, 1075n), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(p, Nat.add(ci, Nat.add(sa, 1075n))), Nat.add(ci, Nat.add(p, Nat.add(sa, 1075n))), Equal.trans(Nat, Nat.add(Nat.add(p, 1075n), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(p, Nat.add(1075n, Nat.add(ci, Nat.add(sa, 0n)))), Nat.add(p, Nat.add(ci, Nat.add(sa, 1075n))), NA.add_assoc(p, 1075n, Nat.add(ci, Nat.add(sa, 0n))), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(1075n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 1075n)), Equal.trans(Nat, Nat.add(1075n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(1075n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 1075n)), NA.add_swap(1075n, ci, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(1075n, Nat.add(sa, 0n)), Nat.add(sa, 1075n), Equal.trans(Nat, Nat.add(1075n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(1075n, 0n)), Nat.add(sa, 1075n), NA.add_swap(1075n, sa, 0n), {==}))))), NA.add_swap(p, ci, Nat.add(sa, 1075n))))), NA.add_swap(p, ci, Nat.add(p, Nat.add(sa, 1075n)))))), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 1075n)))), 2096n), Nat.add(ci, Nat.add(Nat.add(p, Nat.add(p, Nat.add(sa, 1075n))), 2096n)), Nat.add(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 3171n)))), NA.add_assoc(ci, Nat.add(p, Nat.add(p, Nat.add(sa, 1075n))), 2096n), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(p, Nat.add(p, Nat.add(sa, 1075n))), 2096n), Nat.add(p, Nat.add(p, Nat.add(sa, 3171n))), Equal.trans(Nat, Nat.add(Nat.add(p, Nat.add(p, Nat.add(sa, 1075n))), 2096n), Nat.add(p, Nat.add(Nat.add(p, Nat.add(sa, 1075n)), 2096n)), Nat.add(p, Nat.add(p, Nat.add(sa, 3171n))), NA.add_assoc(p, Nat.add(p, Nat.add(sa, 1075n)), 2096n), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(Nat.add(p, Nat.add(sa, 1075n)), 2096n), Nat.add(p, Nat.add(sa, 3171n)), Equal.trans(Nat, Nat.add(Nat.add(p, Nat.add(sa, 1075n)), 2096n), Nat.add(p, Nat.add(Nat.add(sa, 1075n), 2096n)), Nat.add(p, Nat.add(sa, 3171n)), NA.add_assoc(p, Nat.add(sa, 1075n), 2096n), Equal.cong(Nat, Nat, z => Nat.add(p, z), Nat.add(Nat.add(sa, 1075n), 2096n), Nat.add(sa, 3171n), Equal.trans(Nat, Nat.add(Nat.add(sa, 1075n), 2096n), Nat.add(sa, Nat.add(1075n, 2096n)), Nat.add(sa, 3171n), NA.add_assoc(sa, 1075n, 2096n), {==}))))))))))), Equal.cong(Nat, Nat, w => Nat.add(Nat.add(w, Nat.add(ci, sa)), 2096n), Nat.add(Nat.add(p, p), 1075n), Nat.add(Ep, 4096n), hp)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), 2096n), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 6192n))), Nat.add(Nat.add(Nat.add(Ep, ci), sa), 6192n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), 2096n), Nat.add(Nat.add(Ep, Nat.add(ci, Nat.add(sa, 4096n))), 2096n), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 6192n))), Equal.cong(Nat, Nat, z => Nat.add(z, 2096n), Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, sa)), Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, Nat.add(sa, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, sa)), Nat.add(Ep, 4096n), Nat.add(Ep, 4096n), Equal.trans(Nat, Nat.add(Ep, 4096n), Nat.add(Nat.add(Ep, 0n), 4096n), Nat.add(Ep, 4096n), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), Ep, Nat.add(Ep, 0n), Equal.sym(Nat, Nat.add(Ep, 0n), Ep, N.add_zero(Ep))), Equal.trans(Nat, Nat.add(Nat.add(Ep, 0n), 4096n), Nat.add(Ep, Nat.add(0n, 4096n)), Nat.add(Ep, 4096n), NA.add_assoc(Ep, 0n, 4096n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Ep, 4096n), z), Nat.add(ci, sa), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(ci, sa), Nat.add(Nat.add(ci, 0n), sa), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sa), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, 0n), z), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa)))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(0n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 0n)), NA.add_assoc(ci, 0n, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(0n, 0n)), Nat.add(sa, 0n), NA.add_swap(0n, sa, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(Ep, 4096n), Nat.add(ci, Nat.add(sa, 0n))), Nat.add(Ep, Nat.add(4096n, Nat.add(ci, Nat.add(sa, 0n)))), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 4096n))), NA.add_assoc(Ep, 4096n, Nat.add(ci, Nat.add(sa, 0n))), Equal.cong(Nat, Nat, z => Nat.add(Ep, z), Nat.add(4096n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 4096n)), Equal.trans(Nat, Nat.add(4096n, Nat.add(ci, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(4096n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 4096n)), NA.add_swap(4096n, ci, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(4096n, Nat.add(sa, 0n)), Nat.add(sa, 4096n), Equal.trans(Nat, Nat.add(4096n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(4096n, 0n)), Nat.add(sa, 4096n), NA.add_swap(4096n, sa, 0n), {==}))))))), Equal.trans(Nat, Nat.add(Nat.add(Ep, Nat.add(ci, Nat.add(sa, 4096n))), 2096n), Nat.add(Ep, Nat.add(Nat.add(ci, Nat.add(sa, 4096n)), 2096n)), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 6192n))), NA.add_assoc(Ep, Nat.add(ci, Nat.add(sa, 4096n)), 2096n), Equal.cong(Nat, Nat, z => Nat.add(Ep, z), Nat.add(Nat.add(ci, Nat.add(sa, 4096n)), 2096n), Nat.add(ci, Nat.add(sa, 6192n)), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(sa, 4096n)), 2096n), Nat.add(ci, Nat.add(Nat.add(sa, 4096n), 2096n)), Nat.add(ci, Nat.add(sa, 6192n)), NA.add_assoc(ci, Nat.add(sa, 4096n), 2096n), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(sa, 4096n), 2096n), Nat.add(sa, 6192n), Equal.trans(Nat, Nat.add(Nat.add(sa, 4096n), 2096n), Nat.add(sa, Nat.add(4096n, 2096n)), Nat.add(sa, 6192n), NA.add_assoc(sa, 4096n, 2096n), {==})))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Ep, ci), sa), 6192n), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 6192n))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Ep, ci), sa), 6192n), Nat.add(Nat.add(Ep, Nat.add(ci, Nat.add(sa, 0n))), 6192n), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 6192n))), Equal.cong(Nat, Nat, z => Nat.add(z, 6192n), Nat.add(Nat.add(Ep, ci), sa), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 0n))), Equal.trans(Nat, Nat.add(Nat.add(Ep, ci), sa), Nat.add(Nat.add(Ep, Nat.add(ci, 0n)), Nat.add(sa, 0n)), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 0n))), Equal.trans(Nat, Nat.add(Nat.add(Ep, ci), sa), Nat.add(Nat.add(Ep, Nat.add(ci, 0n)), sa), Nat.add(Nat.add(Ep, Nat.add(ci, 0n)), Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sa), Nat.add(Ep, ci), Nat.add(Ep, Nat.add(ci, 0n)), Equal.trans(Nat, Nat.add(Ep, ci), Nat.add(Nat.add(Ep, 0n), Nat.add(ci, 0n)), Nat.add(Ep, Nat.add(ci, 0n)), Equal.trans(Nat, Nat.add(Ep, ci), Nat.add(Nat.add(Ep, 0n), ci), Nat.add(Nat.add(Ep, 0n), Nat.add(ci, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, ci), Ep, Nat.add(Ep, 0n), Equal.sym(Nat, Nat.add(Ep, 0n), Ep, N.add_zero(Ep))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Ep, 0n), z), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci)))), Equal.trans(Nat, Nat.add(Nat.add(Ep, 0n), Nat.add(ci, 0n)), Nat.add(Ep, Nat.add(0n, Nat.add(ci, 0n))), Nat.add(Ep, Nat.add(ci, 0n)), NA.add_assoc(Ep, 0n, Nat.add(ci, 0n)), Equal.cong(Nat, Nat, z => Nat.add(Ep, z), Nat.add(0n, Nat.add(ci, 0n)), Nat.add(ci, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 0n)), Nat.add(ci, Nat.add(0n, 0n)), Nat.add(ci, 0n), NA.add_swap(0n, ci, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Ep, Nat.add(ci, 0n)), z), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa)))), Equal.trans(Nat, Nat.add(Nat.add(Ep, Nat.add(ci, 0n)), Nat.add(sa, 0n)), Nat.add(Ep, Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n))), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 0n))), NA.add_assoc(Ep, Nat.add(ci, 0n), Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(Ep, z), Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(sa, 0n)), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), Nat.add(sa, 0n)), Nat.add(ci, Nat.add(0n, Nat.add(sa, 0n))), Nat.add(ci, Nat.add(sa, 0n)), NA.add_assoc(ci, 0n, Nat.add(sa, 0n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 0n)), Nat.add(sa, Nat.add(0n, 0n)), Nat.add(sa, 0n), NA.add_swap(0n, sa, 0n), {==}))))))), Equal.trans(Nat, Nat.add(Nat.add(Ep, Nat.add(ci, Nat.add(sa, 0n))), 6192n), Nat.add(Ep, Nat.add(Nat.add(ci, Nat.add(sa, 0n)), 6192n)), Nat.add(Ep, Nat.add(ci, Nat.add(sa, 6192n))), NA.add_assoc(Ep, Nat.add(ci, Nat.add(sa, 0n)), 6192n), Equal.cong(Nat, Nat, z => Nat.add(Ep, z), Nat.add(Nat.add(ci, Nat.add(sa, 0n)), 6192n), Nat.add(ci, Nat.add(sa, 6192n)), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(sa, 0n)), 6192n), Nat.add(ci, Nat.add(Nat.add(sa, 0n), 6192n)), Nat.add(ci, Nat.add(sa, 6192n)), NA.add_assoc(ci, Nat.add(sa, 0n), 6192n), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(sa, 0n), 6192n), Nat.add(sa, 6192n), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), 6192n), Nat.add(sa, Nat.add(0n, 6192n)), Nat.add(sa, 6192n), NA.add_assoc(sa, 0n, 6192n), {==}))))))))), Equal.cong(Nat, Nat, w => Nat.add(Nat.add(w, sa), 6192n), Nat.add(Ep, ci), EN, hE)), Equal.cong(Nat, Nat, w => Nat.add(w, 6192n), Nat.add(EN, sa), Nat.add(XX, 2171n), hEN)), Equal.trans(Nat, Nat.add(Nat.add(XX, 2171n), 6192n), Nat.add(XX, 8363n), Nat.add(5363n, Nat.add(XX, 3000n)), Equal.trans(Nat, Nat.add(Nat.add(XX, 2171n), 6192n), Nat.add(Nat.add(XX, 2171n), 6192n), Nat.add(XX, 8363n), Equal.cong(Nat, Nat, z => Nat.add(z, 6192n), 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.trans(Nat, Nat.add(Nat.add(XX, 2171n), 6192n), Nat.add(XX, Nat.add(2171n, 6192n)), Nat.add(XX, 8363n), NA.add_assoc(XX, 2171n, 6192n), {==})), Equal.sym(Nat, Nat.add(5363n, Nat.add(XX, 3000n)), Nat.add(XX, 8363n), Equal.trans(Nat, Nat.add(5363n, Nat.add(XX, 3000n)), Nat.add(5363n, Nat.add(XX, 3000n)), Nat.add(XX, 8363n), Equal.cong(Nat, Nat, z => Nat.add(5363n, z), 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.trans(Nat, Nat.add(5363n, Nat.add(XX, 3000n)), Nat.add(XX, Nat.add(5363n, 3000n)), Nat.add(XX, 8363n), NA.add_swap(5363n, XX, 3000n), {==})))))
  +B2 = NR.add_cancel(5363n, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(XX, 3000n), B)
  +C1 = NR.add_cancel(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(x, x), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)))), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, Nat.add(sa, 72n)), z), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(q, 1400n)), z), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n)))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), NA.add_assoc(j, Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n)))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), NA.add_assoc(q, 1400n, Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), Equal.trans(Nat, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(1400n, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), NA.add_swap(1400n, j, Nat.add(q, 1400n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, 2800n), Equal.trans(Nat, Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, Nat.add(1400n, 1400n)), Nat.add(q, 2800n), NA.add_swap(1400n, q, 1400n), {==}))))), NA.add_swap(q, j, Nat.add(q, 2800n)))))))), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(ci, Nat.add(Nat.add(sa, 72n), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_assoc(ci, Nat.add(sa, 72n), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(sa, 72n), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(sa, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2872n))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(sa, Nat.add(72n, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))))), Nat.add(sa, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2872n))))), NA.add_assoc(sa, 72n, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(72n, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2872n)))), Equal.trans(Nat, Nat.add(72n, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(j, Nat.add(72n, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2872n)))), NA.add_swap(72n, j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(72n, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(j, Nat.add(q, Nat.add(q, 2872n))), Equal.trans(Nat, Nat.add(72n, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(j, Nat.add(72n, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(j, Nat.add(q, Nat.add(q, 2872n))), NA.add_swap(72n, j, Nat.add(q, Nat.add(q, 2800n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(72n, Nat.add(q, Nat.add(q, 2800n))), Nat.add(q, Nat.add(q, 2872n)), Equal.trans(Nat, Nat.add(72n, Nat.add(q, Nat.add(q, 2800n))), Nat.add(q, Nat.add(72n, Nat.add(q, 2800n))), Nat.add(q, Nat.add(q, 2872n)), NA.add_swap(72n, q, Nat.add(q, 2800n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(72n, Nat.add(q, 2800n)), Nat.add(q, 2872n), Equal.trans(Nat, Nat.add(72n, Nat.add(q, 2800n)), Nat.add(q, Nat.add(72n, 2800n)), Nat.add(q, 2872n), NA.add_swap(72n, q, 2800n), {==}))))))))), Equal.trans(Nat, Nat.add(sa, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2872n))))), Nat.add(j, Nat.add(sa, Nat.add(j, Nat.add(q, Nat.add(q, 2872n))))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_swap(sa, j, Nat.add(j, Nat.add(q, Nat.add(q, 2872n)))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(sa, Nat.add(j, Nat.add(q, Nat.add(q, 2872n)))), Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(sa, Nat.add(j, Nat.add(q, Nat.add(q, 2872n)))), Nat.add(j, Nat.add(sa, Nat.add(q, Nat.add(q, 2872n)))), Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_swap(sa, j, Nat.add(q, Nat.add(q, 2872n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(sa, Nat.add(q, Nat.add(q, 2872n))), Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(sa, Nat.add(q, Nat.add(q, 2872n))), Nat.add(q, Nat.add(sa, Nat.add(q, 2872n))), Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))), NA.add_swap(sa, q, Nat.add(q, 2872n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(sa, Nat.add(q, 2872n)), Nat.add(q, Nat.add(sa, 2872n)), NA.add_swap(sa, q, 2872n))))))))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(q, 1400n)), z), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(1n, j)), Nat.add(q, 1399n), Nat.add(q, 1399n), Equal.trans(Nat, Nat.add(q, 1399n), Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.add(z, 1399n), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), Equal.trans(Nat, Nat.add(Nat.add(q, 0n), 1399n), Nat.add(q, Nat.add(0n, 1399n)), Nat.add(q, 1399n), NA.add_assoc(q, 0n, 1399n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(q, 1399n), z), Nat.add(1n, j), Nat.add(j, 1n), Equal.trans(Nat, Nat.add(1n, j), Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, 1n), Equal.cong(Nat, Nat, z => Nat.add(1n, z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.trans(Nat, Nat.add(1n, Nat.add(j, 0n)), Nat.add(j, Nat.add(1n, 0n)), Nat.add(j, 1n), NA.add_swap(1n, j, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(j, 1400n)), Nat.add(j, Nat.add(q, 1400n)), Equal.trans(Nat, Nat.add(Nat.add(q, 1399n), Nat.add(j, 1n)), Nat.add(q, Nat.add(1399n, Nat.add(j, 1n))), Nat.add(q, Nat.add(j, 1400n)), NA.add_assoc(q, 1399n, Nat.add(j, 1n)), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, 1400n), Equal.trans(Nat, Nat.add(1399n, Nat.add(j, 1n)), Nat.add(j, Nat.add(1399n, 1n)), Nat.add(j, 1400n), NA.add_swap(1399n, j, 1n), {==}))), NA.add_swap(q, j, 1400n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, 1400n)), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n)))), Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), NA.add_assoc(j, Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Equal.trans(Nat, Nat.add(Nat.add(q, 1400n), Nat.add(j, Nat.add(q, 1400n))), Nat.add(q, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n)))), Nat.add(q, Nat.add(j, Nat.add(q, 2800n))), NA.add_assoc(q, 1400n, Nat.add(j, Nat.add(q, 1400n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), Equal.trans(Nat, Nat.add(1400n, Nat.add(j, Nat.add(q, 1400n))), Nat.add(j, Nat.add(1400n, Nat.add(q, 1400n))), Nat.add(j, Nat.add(q, 2800n)), NA.add_swap(1400n, j, Nat.add(q, 1400n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, 2800n), Equal.trans(Nat, Nat.add(1400n, Nat.add(q, 1400n)), Nat.add(q, Nat.add(1400n, 1400n)), Nat.add(q, 2800n), NA.add_swap(1400n, q, 1400n), {==}))))), NA.add_swap(q, j, Nat.add(q, 2800n))))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), z), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Nat.add(ci, Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n)))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_assoc(j, Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Nat.add(ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(q, Nat.add(q, 2800n))), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(j, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(j, Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))), NA.add_assoc(j, Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n)))), Nat.add(ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n)))), Equal.trans(Nat, Nat.add(Nat.add(q, Nat.add(q, 2800n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n)))), NA.add_assoc(q, Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(ci, Nat.add(sa, 2872n))), Nat.add(ci, Nat.add(q, Nat.add(sa, 2872n))), Equal.trans(Nat, Nat.add(Nat.add(q, 2800n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(q, Nat.add(2800n, Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(q, Nat.add(ci, Nat.add(sa, 2872n))), NA.add_assoc(q, 2800n, Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(q, z), Nat.add(2800n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 2872n)), Equal.trans(Nat, Nat.add(2800n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(2800n, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 2872n)), NA.add_swap(2800n, ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, 2872n), Equal.trans(Nat, Nat.add(2800n, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(2800n, 72n)), Nat.add(sa, 2872n), NA.add_swap(2800n, sa, 72n), {==}))))), NA.add_swap(q, ci, Nat.add(sa, 2872n))))), NA.add_swap(q, ci, Nat.add(q, Nat.add(sa, 2872n)))))), NA.add_swap(j, ci, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))), NA.add_swap(j, ci, Nat.add(j, Nat.add(q, Nat.add(q, Nat.add(sa, 2872n))))))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(XX, 3000n), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), A2, Equal.trans(Nat, Nat.add(XX, 3000n), Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), Equal.sym(Nat, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(XX, 3000n), B2), Equal.trans(Nat, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), Equal.trans(Nat, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(x, x), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(sa, Nat.add(ci, 72n))), Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sa, Nat.add(ci, 72n))), Nat.add(x, x), Nat.add(x, Nat.add(x, 0n)), Equal.trans(Nat, Nat.add(x, x), Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Nat.add(x, Nat.add(x, 0n)), Equal.trans(Nat, Nat.add(x, x), Nat.add(Nat.add(x, 0n), x), Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, x), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, 0n), z), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x)))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Nat.add(x, Nat.add(0n, Nat.add(x, 0n))), Nat.add(x, Nat.add(x, 0n)), NA.add_assoc(x, 0n, Nat.add(x, 0n)), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(0n, Nat.add(x, 0n)), Nat.add(x, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(x, 0n)), Nat.add(x, Nat.add(0n, 0n)), Nat.add(x, 0n), NA.add_swap(0n, x, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, Nat.add(x, 0n)), z), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n))))), Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 72n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(x, 0n)), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 72n)))), NA.add_assoc(x, Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 72n))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 72n))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), Nat.add(ci, Nat.add(sa, 72n))), Nat.add(x, Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n)))), Nat.add(x, Nat.add(ci, Nat.add(sa, 72n))), NA.add_assoc(x, 0n, Nat.add(ci, Nat.add(sa, 72n))), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(0n, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, 72n)), NA.add_swap(0n, ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(0n, Nat.add(sa, 72n)), Nat.add(sa, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(0n, 72n)), Nat.add(sa, 72n), NA.add_swap(0n, sa, 72n), {==}))))), Equal.trans(Nat, Nat.add(x, Nat.add(ci, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(x, Nat.add(sa, 72n))), Nat.add(ci, Nat.add(sa, Nat.add(x, 72n))), NA.add_swap(x, ci, Nat.add(sa, 72n)), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(x, Nat.add(sa, 72n)), Nat.add(sa, Nat.add(x, 72n)), NA.add_swap(x, sa, 72n)))))), Equal.trans(Nat, Nat.add(x, Nat.add(ci, Nat.add(sa, Nat.add(x, 72n)))), Nat.add(ci, Nat.add(x, Nat.add(sa, Nat.add(x, 72n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), NA.add_swap(x, ci, Nat.add(sa, Nat.add(x, 72n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(x, Nat.add(sa, Nat.add(x, 72n))), Nat.add(sa, Nat.add(x, Nat.add(x, 72n))), NA.add_swap(x, sa, Nat.add(x, 72n)))))), Equal.sym(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(x, Nat.add(x, 0n))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), Equal.trans(Nat, Nat.add(Nat.add(sa, Nat.add(ci, 72n)), Nat.add(x, x)), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(x, x)), Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(x, Nat.add(x, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(x, x)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(sa, Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(ci, 72n)), sa, Nat.add(sa, 0n), Equal.sym(Nat, Nat.add(sa, 0n), sa, N.add_zero(sa))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sa, 0n), z), Nat.add(ci, 72n), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(ci, 72n), Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, 72n), Equal.cong(Nat, Nat, z => Nat.add(z, 72n), ci, Nat.add(ci, 0n), Equal.sym(Nat, Nat.add(ci, 0n), ci, N.add_zero(ci))), Equal.trans(Nat, Nat.add(Nat.add(ci, 0n), 72n), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_assoc(ci, 0n, 72n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(sa, 72n)), Equal.trans(Nat, Nat.add(Nat.add(sa, 0n), Nat.add(ci, 72n)), Nat.add(sa, Nat.add(0n, Nat.add(ci, 72n))), Nat.add(sa, Nat.add(ci, 72n)), NA.add_assoc(sa, 0n, Nat.add(ci, 72n)), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(ci, 72n)), Nat.add(ci, Nat.add(0n, 72n)), Nat.add(ci, 72n), NA.add_swap(0n, ci, 72n), {==}))), NA.add_swap(sa, ci, 72n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(ci, Nat.add(sa, 72n)), z), Nat.add(x, x), Nat.add(x, Nat.add(x, 0n)), Equal.trans(Nat, Nat.add(x, x), Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Nat.add(x, Nat.add(x, 0n)), Equal.trans(Nat, Nat.add(x, x), Nat.add(Nat.add(x, 0n), x), Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, x), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, 0n), z), x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x)))), Equal.trans(Nat, Nat.add(Nat.add(x, 0n), Nat.add(x, 0n)), Nat.add(x, Nat.add(0n, Nat.add(x, 0n))), Nat.add(x, Nat.add(x, 0n)), NA.add_assoc(x, 0n, Nat.add(x, 0n)), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(0n, Nat.add(x, 0n)), Nat.add(x, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(x, 0n)), Nat.add(x, Nat.add(0n, 0n)), Nat.add(x, 0n), NA.add_swap(0n, x, 0n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(ci, Nat.add(sa, 72n)), Nat.add(x, Nat.add(x, 0n))), Nat.add(ci, Nat.add(Nat.add(sa, 72n), Nat.add(x, Nat.add(x, 0n)))), Nat.add(ci, Nat.add(sa, Nat.add(x, Nat.add(x, 72n)))), NA.add_assoc(ci, Nat.add(sa, 72n), Nat.add(x, Nat.add(x, 0n))), Equal.cong(Nat, Nat, z => Nat.add(ci, z), Nat.add(Nat.add(sa, 72n), Nat.add(x, Nat.add(x, 0n))), Nat.add(sa, Nat.add(x, Nat.add(x, 72n))), Equal.trans(Nat, Nat.add(Nat.add(sa, 72n), Nat.add(x, Nat.add(x, 0n))), Nat.add(sa, Nat.add(72n, Nat.add(x, Nat.add(x, 0n)))), Nat.add(sa, Nat.add(x, Nat.add(x, 72n))), NA.add_assoc(sa, 72n, Nat.add(x, Nat.add(x, 0n))), Equal.cong(Nat, Nat, z => Nat.add(sa, z), Nat.add(72n, Nat.add(x, Nat.add(x, 0n))), Nat.add(x, Nat.add(x, 72n)), Equal.trans(Nat, Nat.add(72n, Nat.add(x, Nat.add(x, 0n))), Nat.add(x, Nat.add(72n, Nat.add(x, 0n))), Nat.add(x, Nat.add(x, 72n)), NA.add_swap(72n, x, Nat.add(x, 0n)), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(72n, Nat.add(x, 0n)), Nat.add(x, 72n), Equal.trans(Nat, Nat.add(72n, Nat.add(x, 0n)), Nat.add(x, Nat.add(72n, 0n)), Nat.add(x, 72n), NA.add_swap(72n, x, 0n), {==}))))))))))))))
  N.double_inj(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), x, Equal.trans(Nat, Nat.double(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.double(x), NA.double_self(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)), Nat.add(Nat.add(q, 1399n), Nat.add(1n, j))), Nat.add(x, x), Nat.double(x), C1, Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x)))))