def fV

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/impl.bend:45

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

45# adding the carry
46def fV(+a: WU.U64, +cb: Bool) -> {SW.value(X.add(a, WU.U64{X.b32(cb), 0})) == C.low(64n, Nat.add(SW.value(a), S.bit_value(cb))) : Nat}:
47  Equal.trans(Nat, SW.value(X.add(a, WU.U64{X.b32(cb), 0})), C.low(64n, Nat.add(SW.value(a), SW.value(WU.U64{X.b32(cb), 0}))), C.low(64n, Nat.add(SW.value(a), S.bit_value(cb))),
48    WA.add_value(a, WU.U64{X.b32(cb), 0}),
49    Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(SW.value(a), z)), SW.value(WU.U64{X.b32(cb), 0}), S.bit_value(cb), carry_value(cb)))