def shr_split

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

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

143def shr_split(+x: U32) -> {U32.to_nat(x) == Nat.add(S.bit_value(low_bit(x)), Nat.double(U32.to_nat(U32.shr(x)))) : Nat}:
144  match x:
145    case U32{w}:
146      match w:
147        case WCon{+b, +t}:
148          %Equal.sym(Nat, U32.to_nat(U32{WCon{b, t}}), S.unsigned(32n, WCon{b, t}), to_nat_word(WCon{b, t})) : {_ == Nat.add(S.bit_value(b), Nat.double(U32.to_nat(U32{Word.shr.pad(31n, t)}))) : Nat}
149          %Equal.sym(Nat, U32.to_nat(U32{Word.shr.pad(31n, t)}), S.unsigned(32n, Word.shr.pad(31n, t)), to_nat_word(Word.shr.pad(31n, t))) : {S.unsigned(32n, WCon{b, t}) == Nat.add(S.bit_value(b), Nat.double(_)) : Nat}
150          %Equal.sym(Nat, S.unsigned(32n, Word.shr.pad(31n, t)), S.unsigned(31n, t), pad_value(31n, t)) : {S.unsigned(32n, WCon{b, t}) == Nat.add(S.bit_value(b), Nat.double(_)) : Nat}
151          {==}