ProofGen.swap3: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 864-870 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=864&end_line=870

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

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

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=add_swap