law x3_lt_e

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1142

import Base

1142# x + y < 2^e for x <= 4 * 2^d and y <= 3, when d + 2 < e (e a variable:
1143# the callers put 32n only in the final type).
1144law x3_lt_e:
1145  for +x: Nat
1146  for +y: Nat
1147  for +d: Nat
1148  for +e: Nat
1149  for +hy: {Nat.is_le(y, 3n) == True{} : Bool}
1150  for +hx: {Nat.is_le(x, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
1151  for +he: {Nat.is_lt(Nat.add(2n, d), e) == True{} : Bool}
1152  {Nat.is_lt(Nat.add(x, y), Nat.pow(2n, e)) == True{} : Bool}