def un.nc

bend-osdev-u32@0.1.0.0 · PROOF.bend:367

import Base

367def un.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(un.bv(a, x), un.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
368  match x y:
369    case 0n 0n:
370      match a b:
371        case False{} False{}:
372          {==}
373        case False{} True{}:
374          {==}
375        case True{} False{}:
376          {==}
377        case True{} True{}:
378          {==}
379    case 0n 1n+q:
380      match a b:
381        case False{} False{}:
382          {==}
383        case False{} True{}:
384          {==}
385        case True{} False{}:
386          {==}
387        case True{} True{}:
388          {==}
389    case 1n+p 0n:
390      match a b:
391        case False{} False{}:
392          {==}
393        case False{} True{}:
394          {==}
395        case True{} False{}:
396          {==}
397        case True{} True{}:
398          {==}
399    case 1n+p 1n+q:
400      match a b:
401        case False{} False{}:
402          un.nc(p, q, False{}, False{})
403        case False{} True{}:
404          un.nc(p, q, False{}, True{})
405        case True{} False{}:
406          un.nc(p, q, True{}, False{})
407        case True{} True{}:
408          un.nc(p, q, True{}, True{})