def fl_c

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U

127def fl_c(+l: U32, +h: U32, +c: U32, +hc: {c == U32{WD.mask(32n, 16n)} : U32}, +one: Nat, +h1: {one == 1n : Nat}) -> {U32.is_lt(c, l) == Nat.is_lt(65535n, C.low(32n, v(WU.U64{l, h}))) : Bool}:
128  +e = WW.low_u(32n, U32.to_nat(l), U32.to_nat(h), LW.vb(l))
129  Equal.trans(Bool, U32.is_lt(c, l), Nat.is_lt(U32.to_nat(c), U32.to_nat(l)), Nat.is_lt(65535n, C.low(32n, v(WU.U64{l, h}))), U.is_lt_nat(c, l), Equal.trans(Bool, Nat.is_lt(U32.to_nat(c), U32.to_nat(l)), Nat.is_lt(65535n, U32.to_nat(l)), Nat.is_lt(65535n, C.low(32n, v(WU.U64{l, h}))), Equal.cong(Nat, Bool, z => Nat.is_lt(z, U32.to_nat(l)), U32.to_nat(c), 65535n, kv15(one, h1, c, hc)), Equal.cong(Nat, Bool, z => Nat.is_lt(65535n, z), U32.to_nat(l), C.low(32n, v(WU.U64{l, h})), Equal.sym(Nat, C.low(32n, v(WU.U64{l, h})), U32.to_nat(l), e))))