def sc_sc

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:117

import Base
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

117# 2^j (2^k x) == 2^(j+k) x
118def sc_sc(+j: Nat, +k: Nat, +x: Nat) -> {WD.sc(j, WD.sc(k, x)) == WD.sc(Nat.add(j, k), x) : Nat}:
119  Equal.sym(Nat, WD.sc(Nat.add(j, k), x), WD.sc(j, WD.sc(k, x)), AR.sc_idx(j, k, x))