def wv.ncmp0

bend-osdev-word64@0.1.1.0 · proof_value.bend:309

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

309def wv.ncmp0(+n: Nat, +al: Nat, +bl: Nat) -> {Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 0n))) == Nat.cmp(al, bl) : Cmp}:
310  %Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, UL.dbl_zero(n)) : {Nat.cmp(Nat.add(al, _), Nat.add(bl, _)) == Nat.cmp(al, bl) : Cmp}
311  %Equal.sym(Nat, Nat.add(al, 0n), al, UL.nat_add_zero(al)) : {Nat.cmp(_, Nat.add(bl, 0n)) == Nat.cmp(al, bl) : Cmp}
312  %Equal.sym(Nat, Nat.add(bl, 0n), bl, UL.nat_add_zero(bl)) : {Nat.cmp(al, _) == Nat.cmp(al, bl) : Cmp}
313  {==}