lawful-fields
Releases (2)
Definitions (234)
proof_cut.bend
- law pbc
- law pbThe ends of split(ys) from s give back its pieces when ys starts xs at s.
- law wc
- law wlThe ends of split(ys) from s lie in s ..
- def FV
- def NX
- def CG
- law nx_eq
- law cg_eq
- law cut_eq
- law cut_pair_t
- law ylenThe slice from s to T has T - s bytes.
- law cgfAfter the last piece (the end reached to): one more end, at to.
- law cgv
- law ce
- law cut_ends_t
- law cut_view_t
- law cut_bounds_t
proof_digits.bend
- def alldEvery element is a digit byte (48 to 57).
- law and_true
- law push_some
- law push_and
- law go_somedec.go keeps a value exactly while every byte is a digit.
- law ne_dec
- law dg_pair
- law dg_view
- law digits_pair_t
- law dtopThe start test of digits against the slice it reads.
- law digits_view_t
- law eta_nn
- def DGThe byte of the last decimal digit of x.
- def lgoNat.show.fin as a list: d is the digit just produced, q what is left.
- law show_fin
- law show_lgo
- def BKA bound on n when put_dec.digits has fuel k: 10^(k+1) - 1, capped at the largest U32 from k = 9 on (all word constants, never a Nat above 2^32).
- law bk_step
- law s48
- law fits64Below 64 is below 2^32 (2^32 only meets itself: pow_lt is symbolic).
- law dgv
- law dg_lt
- law dg_eq_n
- law dg_eqThe digit byte put_dec writes is DG.
- law lt10
- law ge10
- law dg_small_n
- law dg_small
- law lt_add_succ
- law dlt
- law hdm
- law div_mono10
- law hk_stepn <= BK(1 + j) gives n / 10 <= BK(j).
- law ab0
- law lmax
- law hkmaxEvery word is at most the largest one, BK(k) from k = 9 on.
- law RWith n <= BK(k) the fuel k suffices; q = n / 10 and the spec's fuel f >= q.
- law LN
- law ab_cons
- law AL
- law hkb
- law list_show
- law list_len
- law list_bytes
- law pd_eq
- law pd_room
- law put_dec_view_t
- law put_dec_ok_t
proof_list.bend
- law append_nil
- law append_assoc
- law take_zero2
- law sl_fin
- law split_length
- law jg_finjoin.go of the pieces of split is the separator, then their join.
- law jg
- law join_push
- law sj_fin
- law split_join
- law text_codes
- law st_fin
- law split_text
- law text_app
- law jt
- law join_text
- law ja0
- law ja_go
- law jat0
- law join_at
- law ends_arith
- law ej_stepOne step of ej, with the induction hypothesis for the rest (t is not empty).
- law ej
- law ends_join
- law pieces_length
- def decb_if2^32 must never take part in a conversion (the checker would expand it), so the bound stays a variable M and the law instantiates it.
- law decb_fits_m
- law decb_fits