def ckw.fnv

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:48

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

48def ckw.fnv(+n: Nat, +z: U32, +h: {Nat.is_le(n, U32.to_nat(z)) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(n)) == n : Nat}:
49  match n:
50    case 0n:
51      {==}
52    case 1n+p:
53      %Equal.sym(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), UL.u32_inc_value(U32.from_nat(p), z, ckw.fnh(p, z, h, ckw.fnv(p, z, UO.nat_le_trans(p, 1n+p, U32.to_nat(z), UL.nat_le_add(p, 1n), h))))) : {_ == 1n+p : Nat}
54      %Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ckw.fnv(p, z, UO.nat_le_trans(p, 1n+p, U32.to_nat(z), UL.nat_le_add(p, 1n), h))) : {1n+_ == 1n+p : Nat}
55      {==}