def kv16

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:109

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64D
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

109# 2^16 and 2^16 - 1 as words c: their values are the Nat literals, reached
110# over an open unit (a closed U32.to_nat(65536) unfolds in unary)
111def kv16(+one: Nat, +h1: {one == 1n : Nat}, +c: U32, +hc: {c == U32{WD.pw(32n, 16n)} : U32}) -> {U32.to_nat(c) == 65536n : Nat}:
112  Equal.trans(Nat, U32.to_nat(c), WD.sc(16n, one), 65536n, PD.pow32(16n, {==}, one, h1, c, hc), Equal.sym(Nat, 65536n, WD.sc(16n, one), W64D.k65536(one, h1)))