def succ_t

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:68

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/fixed.bend as SF
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/lib/word.bend as WD
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/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64

68def succ_t(+one: Nat, +h1: {one == 1n : Nat}, +m: U32) -> {Nat.add(v(U32.add(m, 1)), C.shift(32n, WD.bo(U32.is_zero(U32.add(m, 1)), one))) == 1n+v(m) : Nat}:
69  +m1 = U32.add(m, 1)
70  +c = P64.carry32(m, 1)
71  +e0 = WA.acons_o(one, h1, m, 1)
72  +z = zc(one, h1, v(m1), v(m), c, e0, LW.vb(m))
73  +ez = bn_bo(U32.is_zero(m1), c, one, h1, Equal.trans(Nat, SF.bn(U32.is_zero(m1)), SF.bn(Nat.is_eq(v(m1), 0n)), WD.bo(c, one), Equal.cong(Bool, Nat, t => SF.bn(t), U32.is_zero(m1), Nat.is_eq(v(m1), 0n), LW.zero_nat(m1)), z))
74  Equal.trans(Nat, Nat.add(v(m1), C.shift(32n, WD.bo(U32.is_zero(m1), one))), Nat.add(v(m1), C.shift(32n, WD.bo(c, one))), 1n+v(m), Equal.cong(Nat, Nat, t => Nat.add(v(m1), C.shift(32n, t)), WD.bo(U32.is_zero(m1), one), WD.bo(c, one), ez), Equal.trans(Nat, Nat.add(v(m1), C.shift(32n, WD.bo(c, one))), Nat.add(v(m), 1n), 1n+v(m), e0, N.add_comm(v(m), 1n)))