def word.cmp_nat.h

bend-osdev-algo@0.1.0.0 · PROOF.bend:906

import Base

906def word.cmp_nat.h(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), ih: {Word.cmp(p, at, bt) == Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)) : Cmp}) -> {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == Nat.cmp(nat.dbit(x, Word.to_nat(p, at)), nat.dbit(y, Word.to_nat(p, bt))) : Cmp}:
907  %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), ih) : {Word.cmp.fin(x, y, _) == Nat.cmp(nat.dbit(x, Word.to_nat(p, at)), nat.dbit(y, Word.to_nat(p, bt))) : Cmp}
908  word.cmp_nat.d(Word.to_nat(p, at), Word.to_nat(p, bt), x, y)