def xtop

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:91

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/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

91def xtop(+p: Nat, +w: Word(1n+p)) -> {S.unsigned(1n+p, Word.xor(1n+p, w, WD.pw(1n+p, p))) == Nat.add(C.low(p, S.unsigned(1n+p, w)), C.shift(p, Nat.sub(1n, C.high(p, S.unsigned(1n+p, w))))) : Nat}:
92  match p:
93    case 0n:
94      match w:
95        case WCon{+b, +t}:
96          match b:
97            case True{}:
98              {==}
99            case False{}:
100              {==}
101    case 1n+ +q:
102      match w:
103        case WCon{+b, +t}:
104          xstep(q, b, t, xtop(q, t))