def gt.sum_lt

bend-osdev-gf@0.1.1.0 · proof_tab.bend:166

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

166# two logarithms (each below 255) sum below the exp table's 2^9 slots
167def 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}:
168  gt.lt_add_left(2n, Nat.add(a, b), 510n, gt.lt_sum(a, 255n, b, 255n, ha, hb))