def nbc

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:232

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as BN

232# nbloop with its arguments rewritten
233def nbc(+g: Nat, +x: Nat, +y: Nat, +y2: Nat, +z: Bool, +z2: Bool, +w: Bool, +w2: Bool, +ey: {y == y2 : Nat}, +ez: {z == z2 : Bool}, +ew: {w == w2 : Bool}) -> {BN.nbloop(g, x, y, z, w) == BN.nbloop(g, x, y2, z2, w2) : Nat}:
234  Equal.trans(Nat, BN.nbloop(g, x, y, z, w), BN.nbloop(g, x, y2, z, w), BN.nbloop(g, x, y2, z2, w2), Equal.cong(Nat, Nat, t => BN.nbloop(g, x, t, z, w), y, y2, ey), Equal.trans(Nat, BN.nbloop(g, x, y2, z, w), BN.nbloop(g, x, y2, z2, w), BN.nbloop(g, x, y2, z2, w2), Equal.cong(Bool, Nat, t => BN.nbloop(g, x, y2, t, w), z, z2, ez), Equal.cong(Bool, Nat, t => BN.nbloop(g, x, y2, z2, t), w, w2, ew)))