ProofTab.gt.sum_lt: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab
Lines 166-168 of bend-osdev-gf@0.1.1.0/proof_tab.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&start_line=166&end_line=168

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

# two logarithms (each below 255) sum below the exp table's 2^9 slots
def gt.sum_lt(+a: Nat, +b: Nat, +ha: {Nat.is_lt(a, 255n) == True{} : Bool}, +hb: {Nat.is_lt(b, 255n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), A.Arrays.slots(9n)) == True{} : Bool}:
  gt.lt_add_left(2n, Nat.add(a, b), 510n, gt.lt_sum(a, 255n, b, 255n, ha, hb))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.lt_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.lt_sum