def low_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:454

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/logic.bend as L

454# low(s + t, shift(s, y)) == shift(s, low(t, y))
455def low_shift(+s: Nat, +t: Nat, +y: Nat) -> {C.low(Nat.add(s, t), C.shift(s, y)) == C.shift(s, C.low(t, y)) : Nat}:
456  +l = C.low(t, y)
457  +h = C.high(t, y)
458  +e = Equal.trans(Nat, C.shift(s, y), C.shift(s, Nat.add(l, C.shift(t, h))), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h)), Equal.cong(Nat, Nat, z => C.shift(s, z), y, Nat.add(l, C.shift(t, h)), low_high(t, y)), Equal.trans(Nat, C.shift(s, Nat.add(l, C.shift(t, h))), Nat.add(C.shift(s, l), C.shift(s, C.shift(t, h))), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h)), shift_add(s, l, C.shift(t, h)), Equal.cong(Nat, Nat, z => Nat.add(C.shift(s, l), z), C.shift(s, C.shift(t, h)), C.shift(Nat.add(s, t), h), Equal.sym(Nat, C.shift(Nat.add(s, t), h), C.shift(s, C.shift(t, h)), shift_comp(s, t, h)))))
459  +hf = fits_of_lt(Nat.add(s, t), C.shift(s, l), L.subst(Nat, z => {Nat.is_lt(C.shift(s, l), z) == True{} : Bool}, C.shift(s, C.pow2(t)), C.pow2(Nat.add(s, t)), shift_pow2(s, t), shift_lt(s, l, C.pow2(t), low_lt(t, y))))
460  Equal.trans(Nat, C.low(Nat.add(s, t), C.shift(s, y)), C.low(Nat.add(s, t), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h))), C.shift(s, l), Equal.cong(Nat, Nat, z => C.low(Nat.add(s, t), z), C.shift(s, y), Nat.add(C.shift(s, l), C.shift(Nat.add(s, t), h)), e), low_u(Nat.add(s, t), C.shift(s, l), h, hf))