proofs/math/typed/w64dmtop.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmtop.bend as W64dmtop

14 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ./w64div.bend as W64D
import ./w64add.bend as WA
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64dm.bend as DM
import ./w64est.bend as W64E

Definitions

def hd_small source · line 19 · raw

@+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+hz:{U32.is_zero(bh) == True{} : Bool} -> {U32.is_zero(bl) == False{} : Bool}

def vb_small source · line 22 · raw

@+bl:U32 -> @+bh:U32 -> @+hz:{U32.is_zero(bh) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(bl) : Nat}

def vb_pos source · line 26 · raw

@+bl:U32 -> @+bh:U32 -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> {Nat.is_le(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) == True{} : Bool}

def dmq_s source · line 30 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+hz:{U32.is_zero(bh) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.dm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, True{}))) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def dmq_bg source · line 33 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+e:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> @+he:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.X96(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0), Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64dm.v(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.q_start(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, e), 0}) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def dmq_b source · line 43 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+hz:{U32.is_zero(bh) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.dm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, False{}))) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def dmq source · line 46 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}) == False{} : Bool} -> @+z:Bool -> @+hz:{U32.is_zero(bh) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.dm_pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}, z))) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

def divmod_quot source · line 53 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.DivMod.quot(a, b, hb)