def wv.ncmp

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

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

324def wv.ncmp(+n: Nat, ah: Nat, bh: Nat, +al: Nat, +bl: Nat, hal: {Nat.is_lt(al, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, hbl: {Nat.is_lt(bl, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {wv.lex(Nat.cmp(ah, bh), Nat.cmp(al, bl)) == Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))) : Cmp}:
325  match ah bh:
326    case 0n 0n:
327      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 0n))), Nat.cmp(al, bl), wv.ncmp0(n, al, bl))
328    case 0n 1n+ +q:
329      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))), LT{}, wn.lt_of(Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))), wv.nlt(n, al, bl, q, hal)))
330    case 1n+ +p 0n:
331      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(bl, U.U32Nat.dbl(n, 0n))), GT{}, wn.cmp_gt(Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(bl, U.U32Nat.dbl(n, 0n)), wv.nlt(n, bl, al, p, hbl)))
332    case 1n+ +p 1n+ +q:
333      +ea = Equal.trans(Nat, Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(al, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), Equal.cong(Nat, Nat, v => Nat.add(al, v), U.U32Nat.dbl(n, 1n+p), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), UL.dbl_add(n, 1n, p)), UL.nat_add_left_comm(al, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)))
334      +eb = Equal.trans(Nat, Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), Nat.add(bl, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(bl, v), U.U32Nat.dbl(n, 1n+q), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)), UL.dbl_add(n, 1n, q)), UL.nat_add_left_comm(bl, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)))
335      %Equal.sym(Nat, Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), ea) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == Nat.cmp(_, Nat.add(bl, U.U32Nat.dbl(n, 1n+q))) : Cmp}
336      %Equal.sym(Nat, Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q))), eb) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == Nat.cmp(Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), _) : Cmp}
337      %Equal.sym(Cmp, Nat.cmp(Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q)))), Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, p)), Nat.add(bl, U.U32Nat.dbl(n, q))), wn.cmp_add_l(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p)), Nat.add(bl, U.U32Nat.dbl(n, q)))) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == _ : Cmp}
338      wv.ncmp(n, p, q, al, bl, hal, hbl)