def succ_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:172

import Base
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/lib/arith.bend as AR
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD

172# r + 1 below 2^16 when r < m == 2^16 - 1: its value and its exact square
173def succ_v(+one: Nat, +h1: {one == 1n : Nat}, +r: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}, +lt: {Nat.is_lt(v(r), v(m)) == True{} : Bool}) -> {v(U32.add(r, 1)) == 1n+v(r) : Nat}:
174  +em = m16(one, h1, m, pm)
175  +bs = N.le_lt_trans(1n+v(r), v(m), WD.sc(16n, one), lt_to_le(v(r), v(m), lt), L.subst(Nat, z => {Nat.is_lt(v(m), z) == True{} : Bool}, 1n+v(m), WD.sc(16n, one), em, N.lt_succ(v(m))))
176  +a1 = Equal.trans(Nat, Nat.add(v(r), 1n), 1n+Nat.add(v(r), 0n), 1n+v(r), NA.add_succ(v(r), 0n), N.succ_cong(Nat.add(v(r), 0n), v(r), N.add_zero(v(r))))
177  +lt32 = N.lt_le_trans(Nat.add(v(r), 1n), WD.sc(16n, one), WD.sc(32n, one), L.subst(Nat, z => {Nat.is_lt(z, WD.sc(16n, one)) == True{} : Bool}, 1n+v(r), Nat.add(v(r), 1n), Equal.sym(Nat, Nat.add(v(r), 1n), 1n+v(r), a1), bs), AR.le_sc(16n, WD.sc(16n, one)))
178  Equal.trans(Nat, v(U32.add(r, 1)), Nat.add(v(r), 1n), 1n+v(r), PD.add32(one, h1, r, 1, lt32), a1)