law compare_high_only

stelliferous@0.0.2.0 · proofs/word_encoding.bend:67

import Base

67law compare_high_only:
68  for +n: Nat
69  for +m: Nat
70  for +w: Word(n)
71  for +top: Word(m)
72  for +other: Word(m)
73  {Cmp.is_lt(Word.cmp(Nat.add(n,m),concat(n,m,w,top),concat(n,m,Word.zero(n),other))) == Cmp.is_lt(Word.cmp(m,top,other)) : Bool}