PROOF.AP.nc: def of bend-osdev-array@0.1.0.1
Import: import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
Lines 123-164 of bend-osdev-array@0.1.0.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&start_line=123&end_line=164

import Base

def AP.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(AP.bv(a, x), AP.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
  match x y:
    case 0n 0n:
      match a b:
        case False{} False{}:
          {==}
        case False{} True{}:
          {==}
        case True{} False{}:
          {==}
        case True{} True{}:
          {==}
    case 0n 1n+q:
      match a b:
        case False{} False{}:
          {==}
        case False{} True{}:
          {==}
        case True{} False{}:
          {==}
        case True{} True{}:
          {==}
    case 1n+p 0n:
      match a b:
        case False{} False{}:
          {==}
        case False{} True{}:
          {==}
        case True{} False{}:
          {==}
        case True{} True{}:
          {==}
    case 1n+p 1n+q:
      match a b:
        case False{} False{}:
          AP.nc(p, q, False{}, False{})
        case False{} True{}:
          AP.nc(p, q, False{}, True{})
        case True{} False{}:
          AP.nc(p, q, True{}, False{})
        case True{} True{}:
          AP.nc(p, q, True{}, True{})

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.bv