def swap3

minebender-game@1.0.0.0 · proof_gen.bend:864

import Base
import minebender-game@1.0.0.0/proof_base.bend as P

864# ((a+b)+c) + ((a'+b')+c') regrouped as ((a+a')+(b+b')) + (c+c').
865def swap3(+a: Nat, +b: Nat, +c: Nat, +a2: Nat, +b2: Nat, +c2: Nat) ->
866  {Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a2, b2), c2))
867    == Nat.add(Nat.add(Nat.add(a, a2), Nat.add(b, b2)), Nat.add(c, c2)) : Nat}:
868  %P.add_swap(a, b, a2, b2) : {Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a2, b2), c2))
869    == Nat.add(_, Nat.add(c, c2)) : Nat}
870  P.add_swap(Nat.add(a, b), c, Nat.add(a2, b2), c2)