def RES
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrtimport Base
254def RES(+fu: Nat, +x: U32, +r: U32, +m: U32) -> Nat:
255 v(up32g(fu, x, r, up_okg(x, r, m), m))
Uses (5)
Used by (0)
No other definition uses this definition.