def to_nat_from_nat

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32.bend:93

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

93def to_nat_from_nat(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +h: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(i)) == i : Nat}:
94  %Equal.sym(U32, U32.from_nat(i), U32{S.from_nat(32n, i)}, from_nat_word(i, k, hk, h)) : {U32.to_nat(_) == i : Nat}
95  Equal.trans(Nat, U32.to_nat(U32{S.from_nat(32n, i)}), S.unsigned(32n, S.from_nat(32n, i)), i, to_nat_word(S.from_nat(32n, i)), from_nat_value_k(32n, k, i, hk, h))