Arith.sub_word: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
Lines 188-255 of bendtorch-core@0.1.0.0/src/storage/arith.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&start_line=188&end_line=255

import Base

# Word.sub(a, b) is Word.adc(a, b, True, True): it adds the complement of b
# with an incoming carry, so a cleared carry is a borrow of one.
def sub_word(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool,
  h: {Nat.is_le(Nat.add(borrow(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) ->
  {Nat.add(borrow(c), Nat.add(Word.to_nat(n, b), Word.to_nat(n, Word.adc(n, a, b, True{}, c)))) == Word.to_nat(n, a) : Nat}:
  match n:
    case 0n:
      match c:
        case False{}:
          Empty.absurd({1n == 0n : Nat}, clash(h))
        case True{}:
          {==}
    case 1n+p:
      match a:
        case WCon{+x, +xs}:
          match x:
            case False{}:
              match b:
                case WCon{+y, +ys}:
                  match y:
                    case False{}:
                      match c:
                        case False{}:
                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
                          {==}
                        case True{}:
                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
                          {==}
                    case True{}:
                      match c:
                        case False{}:
                          %sub_word(p, xs, ys, False{}, le_dd(1n+Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
                          {==}
                        case True{}:
                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
                          {==}
            case True{}:
              match b:
                case WCon{+y, +ys}:
                  match y:
                    case False{}:
                      match c:
                        case False{}:
                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
                          {==}
                        case True{}:
                          %sub_word(p, xs, ys, True{}, le_ds(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
                          {==}
                    case True{}:
                      match c:
                        case False{}:
                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 3n+_ : Nat}
                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
                          {==}
                        case True{}:
                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
                          {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.adc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=borrow
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=double_add
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=le_dd
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=le_ds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=le_sd