def wsub_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:151

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/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
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/w64add.bend as WA

151def wsub_g(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32) -> {Nat.add(SG.u32_val(U32.sub(a, b)), SG.u32_val(b)) == Nat.add(SG.u32_val(a), C.shift(32n, SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))) : Nat}:
152  +e1 = Equal.cong(Bool, Nat, t => Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(t, one))), U32.is_lt(a, b), Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), lt_nat(a, b))
153  +e2 = Equal.cong(Nat, Nat, t => Nat.add(SG.u32_val(a), C.shift(32n, t)), WD.bo(Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), one), SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))), bo_bn(one, h1, Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))
154  Equal.trans(Nat, Nat.add(SG.u32_val(U32.sub(a, b)), SG.u32_val(b)), Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(U32.is_lt(a, b), one))), Nat.add(SG.u32_val(a), C.shift(32n, SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))), WA.sub_cons(one, h1, a, b), Equal.trans(Nat, Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(U32.is_lt(a, b), one))), Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), one))), Nat.add(SG.u32_val(a), C.shift(32n, SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))), e1, e2))