def internal_cmp_bits

bend-mathlib@0.8.1.0 · u32.bend:85

import Base

85def internal_cmp_bits(x: Nat, y: Nat, ab: Bool, bb: Bool) -> {Word.cmp.fin(ab, bb, Nat.cmp(x, y)) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(x)), Nat.add(internal_bv(bb), Nat.double(y))) : Cmp}:
86  match x y:
87    case 0n 0n:
88      match ab bb:
89        case False{} False{}:
90          {==}
91        case False{} True{}:
92          {==}
93        case True{} False{}:
94          {==}
95        case True{} True{}:
96          {==}
97    case 0n 1n+q:
98      match ab bb:
99        case False{} False{}:
100          {==}
101        case False{} True{}:
102          {==}
103        case True{} False{}:
104          {==}
105        case True{} True{}:
106          {==}
107    case 1n+p 0n:
108      match ab bb:
109        case False{} False{}:
110          {==}
111        case False{} True{}:
112          {==}
113        case True{} False{}:
114          {==}
115        case True{} True{}:
116          {==}
117    case 1n+p 1n+q:
118      match ab bb:
119        case False{} False{}:
120          internal_cmp_bits(p, q, False{}, False{})
121        case False{} True{}:
122          internal_cmp_bits(p, q, False{}, True{})
123        case True{} False{}:
124          internal_cmp_bits(p, q, True{}, False{})
125        case True{} True{}:
126          internal_cmp_bits(p, q, True{}, True{})