def succ_m

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64isq.bend:89

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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
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/width.bend as WW

89def succ_m(+one: Nat, +h1: {one == 1n : Nat}, +q: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}, +lt: {Nat.is_lt(v(q), v(m)) == True{} : Bool}) -> {v(U32.add(q, 1)) == 1n+v(q) : Nat}:
90  +em = m32(one, h1, m, pm)
91  +h = N.le_lt_trans(Nat.add(v(q), 1n), v(m), C.shift(32n, one), L.subst(Nat, z => {Nat.is_le(z, v(m)) == True{} : Bool}, 1n+v(q), Nat.add(v(q), 1n), Equal.sym(Nat, Nat.add(v(q), 1n), 1n+v(q), WA.plus1(v(q))), N.lt_succ_le_succ(v(q), v(m), lt)), L.subst(Nat, z => {Nat.is_lt(v(m), z) == True{} : Bool}, 1n+v(m), C.shift(32n, one), em, N.lt_succ(v(m))))
92  Equal.trans(Nat, v(U32.add(q, 1)), Nat.add(v(q), 1n), 1n+v(q), WA.add_exact(one, h1, q, 1, WW.fits_one(32n, one, h1, Nat.add(v(q), 1n), h)), WA.plus1(v(q)))