bend-osdev-u32

Search uses release 0.1.0.0 · 397 definitions

Releases (1)

0.1.0.0 indexed

Definitions (397)

LAWS.bend

law low_double
law high_double
law high_ltx below 2^(k + j): high(k, x) below 2^j
law nat_mul_lt
law nat_le_dbl
law dbl_le_exp
law divstep_value
law divstep_lt

LAWS_div.bend

LAWS_order.bend

PROOF.bend

def un.bt
def un.ft
def un.tf
def un.cbt
def un.lt_eq
def un.gt_eq
def un.pred
def un.succ_cong
def un.succ_inj
def un.double_cong
def un.add_zero
def un.add_succ
def un.add_comm
def un.double_add
def un.sub_add_l
def un.sub_add
def un.add_cancel_rx + k = y + k: x = y
def un.lt_rw
def un.lt_rw2
def un.le_succ
def un.lt_dbl
def un.lt_dbl1
def un.le_dbl
def un.lt_succ_r
def un.le_lt_trans
def un.le_trans
def un.le_succ_self
def un.le_double
def un.lt_add_lA + X < A + Y exactly when X < Y, on either side
def un.lt_add_r
def un.not_lt_addA + B < A never holds
def un.not_lt_add_l
def un.add_lt_absurdx + k < k never holds
def un.le_not_lt
def un.cmp_refl
def un.bv
def un.vc
def un.nc
def un.fin_eq_tail
def un.bool_eq
def un.fin_eq_head
def un.wcon_eq
def un.word_eq
def un.not_tail2 + (2N + 2T) = 2 * K, from 1 + (N + T) = K
def un.majthe carry out of Word.adc(n, a, b, False, c)
def un.sum
def un.co
def un.dddouble R + double D, from R + D
def un.dd1
def un.sh1 + (2A + (1 + 2B)) = 2 + (2A + 2B)
def un.cellone bit position of the adder
def un.add_vadc(a, b, False, c) + 2^n * carry out = c + a + b
def un.wcon_cong
def un.adc_not
def un.carrys + 2^n * C = A + B with B < 2^n: C is whether s < A
def un.borrows + B = A + 2^n * C with s < 2^n: C is whether A < B
def un.add_nowrap
def un.add_swap(s + b) + k = (s + k) + b
def un.sub_mid(1 + (a + nb)) + b = a + k when 1 + nb + b = k
def un.sub_vs + B = A + 2^n * C, from adc(a, not b, True) + 2^n * carry = 1 + A + not B and 1 + not B + B = 2^n
def un.inc_w
def un.shlput
def un.shl_w
def un.pad
def un.u32_cong