def c3_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:333

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

333def c3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.c3(x)), 4n) == True{} : Bool}:
334  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {Nat.is_lt(_, 4n) == True{} : Bool}
335  t3_lt(x, h)