def dsplit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbytes.bend:242

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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH

242def dsplit(+a: Nat, +b: Nat, +lo: Nat, +hi: Nat, +hlo: {C.fits(w8(a), lo) == True{} : Bool}) -> {SF.le_digits(Nat.add(a, b), Nat.add(lo, C.shift(w8(a), hi))) == C.append(Nat, SF.le_digits(a, lo), SF.le_digits(b, hi)) : List<&2, Nat>}:
243  match a:
244    case 0n:
245      %Equal.sym(Nat, lo, 0n, fits0(lo, hlo)) : {SF.le_digits(b, Nat.add(_, hi)) == SF.le_digits(b, hi) : List<&2, Nat>}
246      {==}
247    case 1n+ +p:
248      +Q = C.shift(w8(p), hi)
249      +ets = Equal.trans(List<&2, Nat>, SF.le_digits(Nat.add(p, b), C.high(8n, Nat.add(lo, C.shift(8n, Q)))), SF.le_digits(Nat.add(p, b), Nat.add(C.high(8n, lo), Q)), C.append(Nat, SF.le_digits(p, C.high(8n, lo)), SF.le_digits(b, hi)), Equal.cong(Nat, List<&2, Nat>, t => SF.le_digits(Nat.add(p, b), t), C.high(8n, Nat.add(lo, C.shift(8n, Q))), Nat.add(C.high(8n, lo), Q), WW.high_add_shift(8n, lo, Q)), dsplit(p, b, C.high(8n, lo), hi, SH.fits_high(8n, w8(p), lo, hlo)))
250      %Equal.sym(Nat, C.shift(Nat.add(8n, w8(p)), hi), C.shift(8n, Q), WW.shift_comp(8n, w8(p), hi)) : {SF.le_digits(Nat.add(1n+p, b), Nat.add(lo, _)) == C.append(Nat, SF.le_digits(1n+p, lo), SF.le_digits(b, hi)) : List<&2, Nat>}
251      con_eq(C.low(8n, Nat.add(lo, C.shift(8n, Q))), C.low(8n, lo), SF.le_digits(Nat.add(p, b), C.high(8n, Nat.add(lo, C.shift(8n, Q)))), C.append(Nat, SF.le_digits(p, C.high(8n, lo)), SF.le_digits(b, hi)), WW.low_add_shift(8n, lo, Q), ets)