law lt_w

lawful-words@0.1.0.0 · proof_word.bend:978

import Base

978law lt_w:
979  for +p: Nat
980  for +y: Bool
981  for +t: Word(p)
982  for +j: Nat
983  for +h: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, t}), Nat.pow(2n, 1n+j)) == True{} : Bool}
984  {Nat.is_lt(Word.to_nat(p, t), Nat.pow(2n, j)) == True{} : Bool}