def swap5

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/adc.bend:42

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

42# (a + A') + (b + B') + c == (a + b + c) + (A' + B') rearranged
43def swap5(+a: Nat, +b: Nat, +c: Nat, +X: Nat, +Y: Nat) -> {Nat.add(Nat.add(Nat.add(a, X), Nat.add(b, Y)), c) == Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)) : Nat}:
44  +e1 = M.cong_l(Nat.add(Nat.add(a, X), Nat.add(b, Y)), Nat.add(Nat.add(a, b), Nat.add(X, Y)), c, M.add4(a, X, b, Y))
45  +e2 = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, b), Nat.add(X, Y)), c), Nat.add(Nat.add(a, b), Nat.add(Nat.add(X, Y), c)), Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), NA.add_assoc(Nat.add(a, b), Nat.add(X, Y), c), Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(Nat.add(X, Y), c)), Nat.add(Nat.add(a, b), Nat.add(c, Nat.add(X, Y))), Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), M.cong_r(Nat.add(a, b), Nat.add(Nat.add(X, Y), c), Nat.add(c, Nat.add(X, Y)), NA.add_comm(Nat.add(X, Y), c)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), Nat.add(Nat.add(a, b), Nat.add(c, Nat.add(X, Y))), NA.add_assoc(Nat.add(a, b), c, Nat.add(X, Y)))))
46  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, X), Nat.add(b, Y)), c), Nat.add(Nat.add(Nat.add(a, b), Nat.add(X, Y)), c), Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), e1, e2)