def uq.nc

bend-osdev-algo@0.1.0.0 · proof_u32.bend:207

import Base

207def uq.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(uq.bv(a, x), uq.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
208  match x y:
209    case 0n 0n:
210      match a b:
211        case False{} False{}:
212          {==}
213        case False{} True{}:
214          {==}
215        case True{} False{}:
216          {==}
217        case True{} True{}:
218          {==}
219    case 0n 1n+q:
220      match a b:
221        case False{} False{}:
222          {==}
223        case False{} True{}:
224          {==}
225        case True{} False{}:
226          {==}
227        case True{} True{}:
228          {==}
229    case 1n+p 0n:
230      match a b:
231        case False{} False{}:
232          {==}
233        case False{} True{}:
234          {==}
235        case True{} False{}:
236          {==}
237        case True{} True{}:
238          {==}
239    case 1n+p 1n+q:
240      match a b:
241        case False{} False{}:
242          uq.nc(p, q, False{}, False{})
243        case False{} True{}:
244          uq.nc(p, q, False{}, True{})
245        case True{} False{}:
246          uq.nc(p, q, True{}, False{})
247        case True{} True{}:
248          uq.nc(p, q, True{}, True{})