law upper_zero

stelliferous@0.0.2.0 · proofs/word_encoding.bend:285

import Base

285law upper_zero:
286  for +n: Nat
287  for +m: Nat
288  for +low: Word(n)
289  for +high: Word(1n+m)
290  for bound: {Cmp.is_lt(Word.cmp(Nat.add(n,1n+m),concat(n,1n+m,low,high),concat(n,1n+m,Word.zero(n),WCon{True{},Word.zero(m)}))) == True{} : Bool}
291  {high == Word.zero(1n+m) : Word(1n+m)}