def inc_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:777

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/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
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/math/typed/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

777# inc(i) for i < n is i + 1
778def inc_v(+K: Nat, +hK: {K == 64n : Nat}, +i: WU.U64, +n: WU.U64, +ni: Nat, +nn: Nat, +hi: {v(i) == ni : Nat}, +hn: {v(n) == nn : Nat}, +hlt: {Nat.is_lt(ni, nn) == True{} : Bool}) -> {v(G.inc(~WU.U64, ~I.u64_op, i)) == 1n+ni : Nat}:
779  +one = I.u64_op(NM.One{})
780  +hnK = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(n), nn, hn, LW.val_lt(K, hK, n))
781  +hfit = fits32(K, hK, 1n+ni, N.le_lt_trans(1n+ni, nn, C.pow2(K), succ_le(ni, nn, hlt), hnK))
782  +hn1 = Equal.trans(Nat, Nat.add(v(i), v(one)), Nat.add(ni, 1n), 1n+ni, nadd(v(i), v(one), ni, 1n, hi, one_v()), plus1(ni))
783  Equal.trans(Nat, v(I.u64_op(NM.Add{i, one})), Nat.add(v(i), v(one)), 1n+ni, LW.ops_add(i, one, ao_of(i, one, 1n+ni, hn1, True{}, hfit)), hn1)