def wsub_val

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:345

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/src/math/w64.bend as X
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/lib/nat.bend as N
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/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as LV
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G

345def wsub_val(+m: WU.U64, +one: Nat, +h1: {one == 1n : Nat}, +hmo: {1n+SG.u64_val(m) == C.shift(64n, one) : Nat}, +a: WU.U64, +b: WU.U64) -> {SG.u64_val(X.add(X.add(a, X.sub(m, b)), WU.U64{1, 0})) == C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)) : Nat}:
346  +S = C.shift(64n, one)
347  +hlt = Equal.trans(Bool, Nat.is_lt(SG.u64_val(b), 1n+SG.u64_val(m)), Nat.is_lt(SG.u64_val(b), S), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(SG.u64_val(b), t), 1n+SG.u64_val(m), S, hmo), WW.lt_one(64n, one, h1, SG.u64_val(b), LV.vb(b)))
348  +e2 = Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(t, 1n)), SG.u64_val(X.add(a, X.sub(m, b))), C.low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b)))), WA.add_value(a, X.sub(m, b)))
349  +e3 = G.low_add_low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b))), 1n)
350  +e4 = Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(Nat.add(SG.u64_val(a), t), 1n)), SG.u64_val(X.sub(m, b)), Nat.sub(SG.u64_val(m), SG.u64_val(b)), WA.sub_value(m, b, N.lt_succ_le(SG.u64_val(b), SG.u64_val(m), hlt)))
351  Equal.trans(Nat, SG.u64_val(X.add(X.add(a, X.sub(m, b)), WU.U64{1, 0})), C.low(64n, Nat.add(SG.u64_val(X.add(a, X.sub(m, b))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)), WA.add_value(X.add(a, X.sub(m, b)), WU.U64{1, 0}), Equal.trans(Nat, C.low(64n, Nat.add(SG.u64_val(X.add(a, X.sub(m, b))), 1n)), C.low(64n, Nat.add(C.low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b)))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)), e2, Equal.trans(Nat, C.low(64n, Nat.add(C.low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b)))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)), e3, e4)))