bend-collections-laws-containers@1.0.0.0 fails

0x5c489f5d9646d7cc9aa3dd8137e9dc07

no description

bend-collections-laws-containers@1.0.0.0 by Giulio2002

Published

2026-09-30

Size

10,725,953 bytes, 583 files

License

MIT (LICENSE)

Declarations

922 laws (922 proved), 11191 defs, 180 types

Import

import bend-collections-laws-containers@1.0.0.0/laws_containers.bend as Laws_containers
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/laws_containers.bend as Laws_containers
import bend-collections-laws-containers@1.0.0.0/proofs/END_TO_END.bend as END_TO_END
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/END_TO_END.bend as END_TO_END
import bend-collections-laws-containers@1.0.0.0/proofs/PROOF.bend as PROOF
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/PROOF.bend as PROOF
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/agree.bend as Agree
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/agree.bend as Agree
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/alloc.bend as Alloc
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/alloc.bend as Alloc
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/alls.bend as Alls
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/alls.bend as Alls
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/api.bend as Api
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/api.bend as Api
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/arr.bend as Arr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/arr.bend as Arr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/attach.bend as Attach
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/attach.bend as Attach
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/bk.bend as Bk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bend as Bk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/capi.bend as Capi
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/capi.bend as Capi
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ccv.bend as Ccv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ccv.bend as Ccv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cnx.bend as Cnx
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cnx.bend as Cnx
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/components.bend as Components
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/components.bend as Components
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/crk.bend as Crk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/crk.bend as Crk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/crm.bend as Crm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/crm.bend as Crm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/csv.bend as Csv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/csv.bend as Csv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cur.bend as Cur
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.bend as Cur
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/da.bend as Da
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/da.bend as Da
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dfix.bend as Dfix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/dfix.bend as Dfix
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dj.bend as Dj
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/dj.bend as Dj
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dord.bend as Dord
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/dord.bend as Dord
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as Ends
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ends.bend as Ends
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/find.bend as Find
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/find.bend as Find
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/fix.bend as Fix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/fix.bend as Fix
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/frame.bend as Frame
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/frame.bend as Frame
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/hdr.bend as Hdr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/hdr.bend as Hdr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/idmv.bend as Idmv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/idmv.bend as Idmv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ins.bend as Ins
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ins.bend as Ins
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/insf.bend as Insf
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/insf.bend as Insf
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/life.bend as Life
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/life.bend as Life
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as Mirror
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.bend as Mirror
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mk.bend as Mk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mk.bend as Mk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mokx.bend as Mokx
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mokx.bend as Mokx
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nav.bend as Nav
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nav.bend as Nav
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/navl.bend as Navl
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/navl.bend as Navl
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/navm.bend as Navm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/navm.bend as Navm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/navs.bend as Navs
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/navs.bend as Navs
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nbr.bend as Nbr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nbr.bend as Nbr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsf.bend as Nsf
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsf.bend as Nsf
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsl.bend as Nsl
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsl.bend as Nsl
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsr.bend as Nsr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.bend as Nsr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as Ok
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.bend as Ok
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as Ord
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.bend as Ord
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as Path
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.bend as Path
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/plug.bend as Plug
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.bend as Plug
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as Prim
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/prim.bend as Prim
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/putf.bend as Putf
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/putf.bend as Putf
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/putm.bend as Putm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/putm.bend as Putm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/range.bend as Range
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/range.bend as Range
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/reads.bend as Reads
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/reads.bend as Reads
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmd.bend as Rmd
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rmd.bend as Rmd
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmf.bend as Rmf
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rmf.bend as Rmf
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmi.bend as Rmi
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rmi.bend as Rmi
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmp.bend as Rmp
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rmp.bend as Rmp
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rms.bend as Rms
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rms.bend as Rms
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmv.bend as Rmv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rmv.bend as Rmv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rot.bend as Rot
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rot.bend as Rot
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rotm.bend as Rotm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rotm.bend as Rotm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rotn.bend as Rotn
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rotn.bend as Rotn
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rotp.bend as Rotp
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/rotp.bend as Rotp
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/setters.bend as Setters
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/setters.bend as Setters
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/sim.bend as Sim
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/sim.bend as Sim
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/slot.bend as Slot
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/slot.bend as Slot
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/spath.bend as Spath
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/spath.bend as Spath
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/succ.bend as Succ
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/succ.bend as Succ
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/tree.bend as Tree
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.bend as Tree
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/unl.bend as Unl
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/unl.bend as Unl
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vapi.bend as Vapi
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vapi.bend as Vapi
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vclr.bend as Vclr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vclr.bend as Vclr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vdef.bend as Vdef
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.bend as Vdef
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vit.bend as Vit
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vit.bend as Vit
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vnav.bend as Vnav
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vnav.bend as Vnav
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsp.bend as Vsp
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vsp.bend as Vsp
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsz.bend as Vsz
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vsz.bend as Vsz
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vw.bend as Vw
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vw.bend as Vw
import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/xtr.bend as Xtr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/xtr.bend as Xtr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/bag.bend as Bag
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/bag.bend as Bag
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/budget.bend as Budget
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/budget.bend as Budget
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/down.bend as Down
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/down.bend as Down
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/grow.bend as Grow
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/grow.bend as Grow
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as Idx
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.bend as Idx
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/multiset.bend as Multiset
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/multiset.bend as Multiset
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/pop.bend as Pop
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/pop.bend as Pop
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/push.bend as Push
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/push.bend as Push
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/root.bend as Root
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/root.bend as Root
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/slots.bend as Slots
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.bend as Slots
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/sorted.bend as Sorted
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/sorted.bend as Sorted
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/steps.bend as Steps
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.bend as Steps
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/u32idx.bend as U32idx
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/u32idx.bend as U32idx
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/up.bend as Up
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/up.bend as Up
import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as Vals
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.bend as Vals
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/bits.bend as Bits
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/bits.bend as Bits
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/da.bend as Da
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.bend as Da
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/loops.bend as Loops
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/loops.bend as Loops
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/steps.bend as Steps
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/steps.bend as Steps
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/arr.bend as Arr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.bend as Arr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/depth.bend as Depth
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/depth.bend as Depth
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/fastcount.bend as Fastcount
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/fastcount.bend as Fastcount
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/index.bend as Index
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/index.bend as Index
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/lists.bend as Lists
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.bend as Lists
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/listx.bend as Listx
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/listx.bend as Listx
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/loops.bend as Loops
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/loops.bend as Loops
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as Model
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.bend as Model
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/steps.bend as Steps
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.bend as Steps
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/walk.bend as Walk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/walk.bend as Walk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/word.bend as MWord
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/word.bend as MWord
import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/zip.bend as Zip
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/zip.bend as Zip
import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/rebalance.bend as Rebalance
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/rebalance.bend as Rebalance
import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/stepok.bend as Stepok
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.bend as Stepok
import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/steps.bend as Steps
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/steps.bend as Steps
import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dlist_iterator/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dlist_iterator/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/api.bend as Api
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.bend as Api
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/direct.bend as Direct
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/direct.bend as Direct
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/direct_laws.bend as Direct_laws
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/direct_laws.bend as Direct_laws
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/grow.bend as Grow
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/grow.bend as Grow
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hins.bend as Hins
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/hins.bend as Hins
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hlive.bend as Hlive
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/hlive.bend as Hlive
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hnb.bend as Hnb
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/hnb.bend as Hnb
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hrd.bend as Hrd
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/hrd.bend as Hrd
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/ins.bend as Ins
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ins.bend as Ins
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/insf.bend as Insf
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/insf.bend as Insf
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/insg.bend as Insg
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/insg.bend as Insg
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/insp.bend as Insp
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/insp.bend as Insp
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/link.bend as Link
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/link.bend as Link
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/links.bend as Links
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/links.bend as Links
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/lv.bend as Lv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/lv.bend as Lv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/ok.bend as Ok
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.bend as Ok
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/rel.bend as Rel
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.bend as Rel
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/rm.bend as Rm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rm.bend as Rm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/step.bend as Step
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/step.bend as Step
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/valid.bend as Valid
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/valid.bend as Valid
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/vals.bend as Vals
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/vals.bend as Vals
import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/walk.bend as Walk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/walk.bend as Walk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/clear.bend as Clear
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/clear.bend as Clear
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/closed.bend as Closed
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/closed.bend as Closed
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/growth.bend as Growth
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/growth.bend as Growth
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as Layout
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.bend as Layout
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned.bend as Owned
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/owned.bend as Owned
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned_instances.bend as Owned_instances
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/owned_instances.bend as Owned_instances
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned_swap.bend as Owned_swap
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/owned_swap.bend as Owned_swap
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/steps.bend as Steps
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.bend as Steps
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/walk.bend as Walk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/walk.bend as Walk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/arena.bend as Arena
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/arena.bend as Arena
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/arr.bend as Arr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/arr.bend as Arr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as Buckets
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.bend as Buckets
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as Cyc
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/cyc.bend as Cyc
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/decide.bend as Decide
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/decide.bend as Decide
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/delmv.bend as Delmv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/delmv.bend as Delmv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/delw.bend as Delw
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/delw.bend as Delw
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/get.bend as Get
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/get.bend as Get
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/grow.bend as Grow
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/grow.bend as Grow
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/has.bend as Has
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/has.bend as Has
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/hole.bend as Hole
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/hole.bend as Hole
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insa.bend as Insa
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insa.bend as Insa
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insert.bend as Insert
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insert.bend as Insert
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insf.bend as Insf
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insf.bend as Insf
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insgrow.bend as Insgrow
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insgrow.bend as Insgrow
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as Insm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insm.bend as Insm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insu.bend as Insu
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/insu.bend as Insu
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as Inv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/inv.bend as Inv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as Keys
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keys.bend as Keys
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keysw.bend as Keysw
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/keysw.bend as Keysw
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/lookup.bend as Lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/lookup.bend as Lookup
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/modn.bend as Modn
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/modn.bend as Modn
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/new.bend as New
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/new.bend as New
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/pop.bend as Pop
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/pop.bend as Pop
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/poplem.bend as Poplem
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/poplem.bend as Poplem
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_all.bend as Probe_all
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_all.bend as Probe_all
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_impl.bend as Probe_impl
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/probe_impl.bend as Probe_impl
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/qprobe.bend as Qprobe
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/qprobe.bend as Qprobe
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/rawins.bend as Rawins
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/rawins.bend as Rawins
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/rebuild.bend as Rebuild
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/rebuild.bend as Rebuild
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/rehash.bend as Rehash
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/rehash.bend as Rehash
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/ring.bend as Ring
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/ring.bend as Ring
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/set.bend as MSet
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/set.bend as MSet
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/setins.bend as Setins
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/setins.bend as Setins
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/setok.bend as Setok
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/setok.bend as Setok
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/setv.bend as Setv
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/setv.bend as Setv
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/shift.bend as Shift
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/shift.bend as Shift
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/size.bend as Size
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/size.bend as Size
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/speclem.bend as Speclem
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/speclem.bend as Speclem
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/step.bend as Step
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/step.bend as Step
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/strings.bend as Strings
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/strings.bend as Strings
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as Table
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/table.bend as Table
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as Tools
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/tools.bend as Tools
import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/words.bend as Words
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/words.bend as Words
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/adapter.bend as Adapter
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/adapter.bend as Adapter
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/array_adapter.bend as Array_adapter
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/array_adapter.bend as Array_adapter
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/clear.bend as Clear
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/clear.bend as Clear
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/costs.bend as Costs
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/costs.bend as Costs
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/edits.bend as Edits
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/edits.bend as Edits
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/example.bend as Example
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/example.bend as Example
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/fold.bend as Fold
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/fold.bend as Fold
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/frames.bend as Frames
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/frames.bend as Frames
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/history.bend as History
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/history.bend as History
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/links.bend as Links
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/links.bend as Links
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/shape.bend as Shape
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/shape.bend as Shape
import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/writes.bend as Writes
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/writes.bend as Writes
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/add.bend as Add
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/add.bend as Add
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/basic.bend as Basic
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/basic.bend as Basic
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bump.bend as Bump
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bump.bend as Bump
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bumpk.bend as Bumpk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpk.bend as Bumpk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/bumpsh.bend as Bumpsh
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/bumpsh.bend as Bumpsh
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/contains.bend as Contains
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/contains.bend as Contains
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dellink.bend as Dellink
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/dellink.bend as Dellink
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dll.bend as Dll
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/dll.bend as Dll
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/drop.bend as Drop
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/drop.bend as Drop
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/elfr.bend as Elfr
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/elfr.bend as Elfr
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/ent.bend as Ent
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/ent.bend as Ent
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/evict.bend as Evict
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/evict.bend as Evict
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/evictk.bend as Evictk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/evictk.bend as Evictk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/find.bend as Find
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/find.bend as Find
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/gone.bend as Gone
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/gone.bend as Gone
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/grow.bend as Grow
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/grow.bend as Grow
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/hw.bend as Hw
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/hw.bend as Hw
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as Idx
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/idx.bend as Idx
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/ins.bend as Ins
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/ins.bend as Ins
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/ins1.bend as Ins1
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/ins1.bend as Ins1
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/insp.bend as Insp
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/insp.bend as Insp
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/keys.bend as Keys
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/keys.bend as Keys
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/linktail.bend as Linktail
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/linktail.bend as Linktail
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/lists.bend as Lists
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/lists.bend as Lists
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/meta.bend as Meta
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/meta.bend as Meta
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/miss.bend as Miss
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/miss.bend as Miss
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/new.bend as New
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/new.bend as New
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/perm.bend as Perm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/perm.bend as Perm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/pre.bend as Pre
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/pre.bend as Pre
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/purge.bend as Purge
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/purge.bend as Purge
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/qrm.bend as Qrm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/qrm.bend as Qrm
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/read.bend as Read
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/read.bend as Read
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rebuild.bend as Rebuild
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rebuild.bend as Rebuild
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/remove.bend as Remove
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/remove.bend as Remove
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/repl.bend as Repl
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/repl.bend as Repl
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/resize.bend as Resize
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/resize.bend as Resize
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rmat.bend as Rmat
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmat.bend as Rmat
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rmatk.bend as Rmatk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmatk.bend as Rmatk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rmrb.bend as Rmrb
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/rmrb.bend as Rmrb
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/room.bend as Room
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/room.bend as Room
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/tabsl.bend as Tabsl
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/tabsl.bend as Tabsl
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/tfind.bend as Tfind
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/tfind.bend as Tfind
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touch.bend as Touch
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touch.bend as Touch
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touchsh.bend as Touchsh
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/touchsh.bend as Touchsh
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as Unlink
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/unlink.bend as Unlink
import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/walk.bend as Walk
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/lru/walk.bend as Walk
import bend-collections-laws-containers@1.0.0.0/proofs/containers/priority_queue/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/priority_queue/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/state.bend as State
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.bend as State
import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/steps.bend as Steps
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/steps.bend as Steps
import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/trace.bend as Trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/trace.bend as Trace
import bend-collections-laws-containers@1.0.0.0/proofs/containers/simple_queue/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/simple_queue/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/containers/stack/components.bend as Components
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/components.bend as Components
import bend-collections-laws-containers@1.0.0.0/proofs/containers/stack/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/lib/arith.bend as Arith
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/arith.bend as Arith
import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as MArray
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.bend as MArray
import bend-collections-laws-containers@1.0.0.0/proofs/lib/array2.bend as Array2
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array2.bend as Array2
import bend-collections-laws-containers@1.0.0.0/proofs/lib/array_ext.bend as Array_ext
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array_ext.bend as Array_ext
import bend-collections-laws-containers@1.0.0.0/proofs/lib/flat.bend as Flat
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/flat.bend as Flat
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/absent_read.bend as Absent_read
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/absent_read.bend as Absent_read
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_bindings.bend as Abstraction_bindings
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/abstraction_bindings.bend as Abstraction_bindings
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_identity.bend as Abstraction_identity
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/abstraction_identity.bend as Abstraction_identity
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_lookup.bend as Abstraction_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/abstraction_lookup.bend as Abstraction_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_recency.bend as Abstraction_recency
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/abstraction_recency.bend as Abstraction_recency
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_size.bend as Abstraction_size
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/abstraction_size.bend as Abstraction_size
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/add_refinement.bend as Add_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/add_refinement.bend as Add_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/add_representation.bend as Add_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/add_representation.bend as Add_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as Addition
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/addition.bend as Addition
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend as Addition_bounds
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/addition_bounds.bend as Addition_bounds
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/aggregate_representation.bend as Aggregate_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/aggregate_representation.bend as Aggregate_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_add_capacity.bend as Cache_add_capacity
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_add_capacity.bend as Cache_add_capacity
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_delete_identities.bend as Cache_delete_identities
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_delete_identities.bend as Cache_delete_identities
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_delete_membership.bend as Cache_delete_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_delete_membership.bend as Cache_delete_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_key_identity.bend as Cache_key_identity
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_key_identity.bend as Cache_key_identity
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_oldest_available.bend as Cache_oldest_available
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_oldest_available.bend as Cache_oldest_available
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_order.bend as Cache_order
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_order.bend as Cache_order
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_populated.bend as Cache_populated
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_populated.bend as Cache_populated
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_prepare_capacity.bend as Cache_prepare_capacity
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_prepare_capacity.bend as Cache_prepare_capacity
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_refresh_identity.bend as Cache_refresh_identity
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_refresh_identity.bend as Cache_refresh_identity
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_refresh_membership.bend as Cache_refresh_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_refresh_membership.bend as Cache_refresh_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_storage_preservation.bend as Cache_storage_preservation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_storage_preservation.bend as Cache_storage_preservation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_store_identities.bend as Cache_store_identities
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_store_identities.bend as Cache_store_identities
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_store_identity.bend as Cache_store_identity
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_store_identity.bend as Cache_store_identity
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_store_membership.bend as Cache_store_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_store_membership.bend as Cache_store_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/canonical.bend as Canonical
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/canonical.bend as Canonical
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/canonical_native.bend as Canonical_native
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/canonical_native.bend as Canonical_native
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/canonical_remove.bend as Canonical_remove
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/canonical_remove.bend as Canonical_remove
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/canonical_string.bend as Canonical_string
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/canonical_string.bend as Canonical_string
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/capacity_preservation.bend as Capacity_preservation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/capacity_preservation.bend as Capacity_preservation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/configuration_observations.bend as Configuration_observations
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/configuration_observations.bend as Configuration_observations
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/configuration_representation.bend as Configuration_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/configuration_representation.bend as Configuration_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/constructor_safety.bend as Constructor_safety
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/constructor_safety.bend as Constructor_safety
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/core_refresh_representation.bend as Core_refresh_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/core_refresh_representation.bend as Core_refresh_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend as Counter
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/counter.bend as Counter
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/disabled.bend as Disabled
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/disabled.bend as Disabled
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as Division_bounds
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_bounds.bend as Division_bounds
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend as Division_candidate
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_candidate.bend as Division_candidate
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend as Division_candidate_bound
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_candidate_bound.bend as Division_candidate_bound
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend as Division_invariant
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_invariant.bend as Division_invariant
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend as Division_no_overflow
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_no_overflow.bend as Division_no_overflow
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as Division_quotient
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_quotient.bend as Division_quotient
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend as Division_remainder
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_remainder.bend as Division_remainder
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend as Division_shift
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_shift.bend as Division_shift
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend as Division_value
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/division_value.bend as Division_value
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/duration_refinement.bend as Duration_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/duration_refinement.bend as Duration_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/empty_events.bend as Empty_events
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/empty_events.bend as Empty_events
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/enumeration_suffix.bend as Enumeration_suffix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/enumeration_suffix.bend as Enumeration_suffix
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/evict_then_write.bend as Evict_then_write
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/evict_then_write.bend as Evict_then_write
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/eviction_state.bend as Eviction_state
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/eviction_state.bend as Eviction_state
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/expired_read.bend as Expired_read
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/expired_read.bend as Expired_read
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/extensional_states.bend as Extensional_states
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/extensional_states.bend as Extensional_states
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/full_add.bend as Full_add
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/full_add.bend as Full_add
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/full_add_head.bend as Full_add_head
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/full_add_head.bend as Full_add_head
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Invariants
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.bend as Invariants
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/live_read_state.bend as Live_read_state
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/live_read_state.bend as Live_read_state
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/lookup_refinement.bend as Lookup_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/lookup_refinement.bend as Lookup_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_bits.bend as Map_bits
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_bits.bend as Map_bits
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend as Map_bridge
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_bridge.bend as Map_bridge
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_character_prefix.bend as Map_character_prefix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_character_prefix.bend as Map_character_prefix
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_critbit_parts.bend as Map_critbit_parts
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_critbit_parts.bend as Map_critbit_parts
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete.bend as Map_delete
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete.bend as Map_delete
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_below.bend as Map_delete_below
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_below.bend as Map_delete_below
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_common.bend as Map_delete_common
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_common.bend as Map_delete_common
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_critbit.bend as Map_delete_critbit
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_critbit.bend as Map_delete_critbit
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_frame.bend as Map_delete_frame
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_frame.bend as Map_delete_frame
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_membership.bend as Map_delete_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_membership.bend as Map_delete_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_populated.bend as Map_delete_populated
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_populated.bend as Map_delete_populated
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_prefix.bend as Map_delete_prefix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_prefix.bend as Map_delete_prefix
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_delete_routes.bend as Map_delete_routes
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_routes.bend as Map_delete_routes
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_difference.bend as Map_difference
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_difference.bend as Map_difference
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_difference_char.bend as Map_difference_char
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_difference_char.bend as Map_difference_char
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_difference_order.bend as Map_difference_order
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_difference_order.bend as Map_difference_order
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_enumeration.bend as Map_enumeration
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_enumeration.bend as Map_enumeration
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_index.bend as Map_index
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_index.bend as Map_index
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as Map_insert
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.bend as Map_insert
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_before.bend as Map_insert_before
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_before.bend as Map_insert_before
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_below.bend as Map_insert_below
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_below.bend as Map_insert_below
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_common.bend as Map_insert_common
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_common.bend as Map_insert_common
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_critbit.bend as Map_insert_critbit
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_critbit.bend as Map_insert_critbit
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_descent.bend as Map_insert_descent
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_descent.bend as Map_insert_descent
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_frame.bend as Map_insert_frame
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_frame.bend as Map_insert_frame
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_inverse.bend as Map_insert_inverse
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_inverse.bend as Map_insert_inverse
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_membership.bend as Map_insert_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_membership.bend as Map_insert_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_nonempty.bend as Map_insert_nonempty
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_nonempty.bend as Map_insert_nonempty
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_prefix.bend as Map_insert_prefix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_prefix.bend as Map_insert_prefix
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_insert_routes.bend as Map_insert_routes
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert_routes.bend as Map_insert_routes
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_key_disjoint.bend as Map_key_disjoint
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_key_disjoint.bend as Map_key_disjoint
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_key_lookup.bend as Map_key_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_key_lookup.bend as Map_key_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_key_membership.bend as Map_key_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_key_membership.bend as Map_key_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_key_presence.bend as Map_key_presence
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_key_presence.bend as Map_key_presence
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_keys_unique.bend as Map_keys_unique
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_keys_unique.bend as Map_keys_unique
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_lookup.bend as Map_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_lookup.bend as Map_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_msb.bend as Map_msb
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_msb.bend as Map_msb
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_populated.bend as Map_populated
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_populated.bend as Map_populated
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_populated_inverse.bend as Map_populated_inverse
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_populated_inverse.bend as Map_populated_inverse
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_prefix_algebra.bend as Map_prefix_algebra
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_prefix_algebra.bend as Map_prefix_algebra
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_prefix_bounds.bend as Map_prefix_bounds
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_prefix_bounds.bend as Map_prefix_bounds
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_prefix_join.bend as Map_prefix_join
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_prefix_join.bend as Map_prefix_join
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_prefix_routing.bend as Map_prefix_routing
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_prefix_routing.bend as Map_prefix_routing
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_put_frame.bend as Map_put_frame
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_put_frame.bend as Map_put_frame
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_route_boolean.bend as Map_route_boolean
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_route_boolean.bend as Map_route_boolean
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Map_routing
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_routing.bend as Map_routing
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_seek.bend as Map_seek
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_seek.bend as Map_seek
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_seek_discriminator.bend as Map_seek_discriminator
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_seek_discriminator.bend as Map_seek_discriminator
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_seek_empty.bend as Map_seek_empty
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_seek_empty.bend as Map_seek_empty
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_seek_prefix.bend as Map_seek_prefix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_seek_prefix.bend as Map_seek_prefix
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_seek_routes.bend as Map_seek_routes
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_seek_routes.bend as Map_seek_routes
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_selected_prefix.bend as Map_selected_prefix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_selected_prefix.bend as Map_selected_prefix
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_set_critbit.bend as Map_set_critbit
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_set_critbit.bend as Map_set_critbit
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_set_frame.bend as Map_set_frame
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_set_frame.bend as Map_set_frame
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_set_membership.bend as Map_set_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_set_membership.bend as Map_set_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_shape.bend as Map_shape
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_shape.bend as Map_shape
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_shape_invariants.bend as Map_shape_invariants
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_shape_invariants.bend as Map_shape_invariants
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_splice_critbit.bend as Map_splice_critbit
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_splice_critbit.bend as Map_splice_critbit
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_string_prefix.bend as Map_string_prefix
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_string_prefix.bend as Map_string_prefix
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as Modular_addition
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/modular_addition.bend as Modular_addition
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/modular_negation.bend as Modular_negation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/modular_negation.bend as Modular_negation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as Nat_algebra
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/nat_algebra.bend as Nat_algebra
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as Native_map
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/native_map.bend as Native_map
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/natural_division.bend as Natural_division
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/natural_division.bend as Natural_division
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as Natural_products
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/natural_products.bend as Natural_products
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as Negation_magnitude
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/negation_magnitude.bend as Negation_magnitude
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nonfull_add.bend as Nonfull_add
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/nonfull_add.bend as Nonfull_add
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as Numeric
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/numeric.bend as Numeric
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/oldest_refinement.bend as Oldest_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/oldest_refinement.bend as Oldest_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/ordered_entries.bend as Ordered_entries
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/ordered_entries.bend as Ordered_entries
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/protocol_storage.bend as Protocol_storage
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/protocol_storage.bend as Protocol_storage
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_add.bend as Public_add
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_add.bend as Public_add
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_aggregate.bend as Public_aggregate
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_aggregate.bend as Public_aggregate
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_config.bend as Public_config
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_config.bend as Public_config
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_diagnostics.bend as Public_diagnostics
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_diagnostics.bend as Public_diagnostics
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_drive.bend as Public_drive
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_drive.bend as Public_drive
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_finish.bend as Public_finish
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_finish.bend as Public_finish
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_oldest_ops.bend as Public_oldest_ops
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_oldest_ops.bend as Public_oldest_ops
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_phase_safety.bend as Public_phase_safety
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_phase_safety.bend as Public_phase_safety
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_read.bend as Public_read
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_read.bend as Public_read
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_refresh.bend as Public_refresh
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_refresh.bend as Public_refresh
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_relation.bend as Public_relation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_relation.bend as Public_relation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_requests.bend as Public_requests
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_requests.bend as Public_requests
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_safety.bend as Public_safety
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_safety.bend as Public_safety
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_simple.bend as Public_simple
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_simple.bend as Public_simple
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_trace.bend as Public_trace
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/public_trace.bend as Public_trace
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/read_refinement.bend as Read_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/read_refinement.bend as Read_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/read_representation.bend as Read_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/read_representation.bend as Read_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_bounds.bend as Recency_bounds
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/recency_bounds.bend as Recency_bounds
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_capacity.bend as Recency_capacity
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/recency_capacity.bend as Recency_capacity
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_head_removal.bend as Recency_head_removal
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/recency_head_removal.bend as Recency_head_removal
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_membership.bend as Recency_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/recency_membership.bend as Recency_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_move_inclusion.bend as Recency_move_inclusion
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/recency_move_inclusion.bend as Recency_move_inclusion
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_unique.bend as Recency_unique
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/recency_unique.bend as Recency_unique
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_update_membership.bend as Recency_update_membership
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/recency_update_membership.bend as Recency_update_membership
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refinement.bend as Refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/refinement.bend as Refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refresh_complete_representation.bend as Refresh_complete_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/refresh_complete_representation.bend as Refresh_complete_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refresh_lookup.bend as Refresh_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/refresh_lookup.bend as Refresh_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refresh_representation.bend as Refresh_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/refresh_representation.bend as Refresh_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refresh_state.bend as Refresh_state
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/refresh_state.bend as Refresh_state
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/removal_lookup.bend as Removal_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/removal_lookup.bend as Removal_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/removal_representation.bend as Removal_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/removal_representation.bend as Removal_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/removal_state.bend as Removal_state
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/removal_state.bend as Removal_state
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/remove_refinement.bend as Remove_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/remove_refinement.bend as Remove_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/replacement_refinement.bend as Replacement_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/replacement_refinement.bend as Replacement_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/representation_access.bend as Representation_access
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/representation_access.bend as Representation_access
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/representation_parts.bend as Representation_parts
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/representation_parts.bend as Representation_parts
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/signed_division.bend as Signed_division
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/signed_division.bend as Signed_division
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/size_length.bend as Size_length
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/size_length.bend as Size_length
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_congruence.bend as Spec_congruence
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_congruence.bend as Spec_congruence
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_erase_lookup.bend as Spec_erase_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_erase_lookup.bend as Spec_erase_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_lookup.bend as Spec_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.bend as Spec_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_write_lookup.bend as Spec_write_lookup
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_write_lookup.bend as Spec_write_lookup
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/store_lookup_refinement.bend as Store_lookup_refinement
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/store_lookup_refinement.bend as Store_lookup_refinement
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/store_representation.bend as Store_representation
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/store_representation.bend as Store_representation
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/store_state.bend as Store_state
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/store_state.bend as Store_state
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as String_compare
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/string_compare.bend as String_compare
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_order.bend as String_order
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/string_order.bend as String_order
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/subtraction_bounds.bend as Subtraction_bounds
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/subtraction_bounds.bend as Subtraction_bounds
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as Word_addition
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_addition.bend as Word_addition
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_bounds.bend as Word_bounds
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_bounds.bend as Word_bounds
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_comparison.bend as Word_comparison
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_comparison.bend as Word_comparison
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as Word_multiplication
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_multiplication.bend as Word_multiplication
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as Word_shift
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_shift.bend as Word_shift
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_subtraction.bend as Word_subtraction
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_subtraction.bend as Word_subtraction
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as Word_value
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/word_value.bend as Word_value
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/write_congruence.bend as Write_congruence
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/write_congruence.bend as Write_congruence
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as Cache
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.bend as Cache
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/clock.bend as Clock
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.bend as Clock
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/effectful_aggregate.bend as Effectful_aggregate
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/effectful_aggregate.bend as Effectful_aggregate
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/effectful_operations.bend as Effectful_operations
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/effectful_operations.bend as Effectful_operations
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/equivalence.bend as Equivalence
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.bend as Equivalence
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as Numeric
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.bend as Numeric
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/operations.bend as Operations
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/operations.bend as Operations
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/public_commands.bend as Public_commands
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/public_commands.bend as Public_commands
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/traces.bend as Traces
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/traces.bend as Traces
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/unsigned_division.bend as Unsigned_division
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/unsigned_division.bend as Unsigned_division
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as Cache
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.bend as Cache
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/codec.bend as Codec
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/codec.bend as Codec
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/driver.bend as Driver
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/driver.bend as Driver
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/entry_ops.bend as Entry_ops
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/entry_ops.bend as Entry_ops
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/protocol.bend as Protocol
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/protocol.bend as Protocol
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/public.bend as Public
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/public.bend as Public
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/time.bend as Time
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wide
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/wide.bend as Wide
import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as Model
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.bend as Model
import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as Links
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.bend as Links
import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as MList
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/list.bend as MList
import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as Logic
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/logic.bend as Logic
import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as MNat
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat.bend as MNat
import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as Nat_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.bend as Nat_list
import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as Order
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.bend as Order
import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as Sequence
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/sequence.bend as Sequence
import bend-collections-laws-containers@1.0.0.0/proofs/lib/two_list.bend as Two_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/two_list.bend as Two_list
import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as MU32
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.bend as MU32
import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as U32_tree
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32_tree.bend as U32_tree
import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as U32alg
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32alg.bend as U32alg
import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as U32div
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.bend as U32div
import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32seq.bend as U32seq
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32seq.bend as U32seq
import bend-collections-laws-containers@1.0.0.0/proofs/lib/vec.bend as Vec
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/vec.bend as Vec
import bend-collections-laws-containers@1.0.0.0/proofs/lib/word.bend as MWord
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/word.bend as MWord
import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as Words32
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.bend as Words32
import bend-collections-laws-containers@1.0.0.0/proofs/math/hash/hash.bend as Hash
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/hash/hash.bend as Hash
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/arith.bend as Arith
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/arith.bend as Arith
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/bits.bend as Bits
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/bits.bend as Bits
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/fact.bend as Fact
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/fact.bend as Fact
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/gcd.bend as Gcd
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/gcd.bend as Gcd
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/inverse.bend as Inverse
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/inverse.bend as Inverse
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/lcm.bend as Lcm
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/lcm.bend as Lcm
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/lists.bend as Lists
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/lists.bend as Lists
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/logs.bend as Logs
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/logs.bend as Logs
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/misc.bend as Misc
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/misc.bend as Misc
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/modpow.bend as Modpow
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/modpow.bend as Modpow
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/roots.bend as Roots
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/roots.bend as Roots
import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/sqrtn.bend as Sqrtn
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/sqrtn.bend as Sqrtn
import bend-collections-laws-containers@1.0.0.0/proofs/math/pow2/pow2.bend as Pow2
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/pow2/pow2.bend as Pow2
import bend-collections-laws-containers@1.0.0.0/proofs/math/proof.bend as Proof
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/proof.bend as Proof
import bend-collections-laws-containers@1.0.0.0/proofs/math/u64/u64.bend as U64
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/u64/u64.bend as U64
import bend-collections-laws-containers@1.0.0.0/proofs/math/u64/u64div.bend as U64div
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/u64/u64div.bend as U64div
import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as Main
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.bend as Main
import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/recursive.bend as Recursive
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/recursive.bend as Recursive
import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as Binary_heap
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.bend as Binary_heap
import bend-collections-laws-containers@1.0.0.0/spec/containers/bitlist.bend as Bitlist
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.bend as Bitlist
import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as Bitset
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.bend as Bitset
import bend-collections-laws-containers@1.0.0.0/spec/containers/deque.bend as Deque
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.bend as Deque
import bend-collections-laws-containers@1.0.0.0/spec/containers/dlist_iterator.bend as Dlist_iterator
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dlist_iterator.bend as Dlist_iterator
import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as Doubly_linked_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.bend as Doubly_linked_list
import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as Dynamic_array
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.bend as Dynamic_array
import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as Hash_table
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/hash_table.bend as Hash_table
import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/main.bend as Main
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/main.bend as Main
import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as Model
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.bend as Model
import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/programs.bend as Programs
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.bend as Programs
import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as Lru
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.bend as Lru
import bend-collections-laws-containers@1.0.0.0/spec/containers/priority_queue.bend as Priority_queue
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/priority_queue.bend as Priority_queue
import bend-collections-laws-containers@1.0.0.0/spec/containers/queue.bend as Queue
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/queue.bend as Queue
import bend-collections-laws-containers@1.0.0.0/spec/containers/simple_queue.bend as Simple_queue
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.bend as Simple_queue
import bend-collections-laws-containers@1.0.0.0/spec/containers/stack.bend as Stack
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.bend as Stack
import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as Common
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.bend as Common
import bend-collections-laws-containers@1.0.0.0/spec/lib/numeric.bend as Numeric
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/numeric.bend as Numeric
import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as Order
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.bend as Order
import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as Sequence
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/sequence.bend as Sequence
import bend-collections-laws-containers@1.0.0.0/spec/lib/u32seq.bend as U32seq
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.bend as U32seq
import bend-collections-laws-containers@1.0.0.0/spec/math/hash.bend as Hash
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/hash.bend as Hash
import bend-collections-laws-containers@1.0.0.0/spec/math/natural.bend as Natural
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.bend as Natural
import bend-collections-laws-containers@1.0.0.0/spec/math/pow2.bend as Pow2
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/pow2.bend as Pow2
import bend-collections-laws-containers@1.0.0.0/spec/math/u64.bend as U64
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/u64.bend as U64
import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as Balanced_search_tree
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.bend as Balanced_search_tree
import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as Binary_heap
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.bend as Binary_heap
import bend-collections-laws-containers@1.0.0.0/src/containers/bitlist.bend as Bitlist
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.bend as Bitlist
import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as Bitset
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bend as Bitset
import bend-collections-laws-containers@1.0.0.0/src/containers/deque.bend as Deque
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.bend as Deque
import bend-collections-laws-containers@1.0.0.0/src/containers/dlist_iterator.bend as Dlist_iterator
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.bend as Dlist_iterator
import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as Doubly_linked_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.bend as Doubly_linked_list
import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as Dynamic_array
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.bend as Dynamic_array
import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as Hash_table
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.bend as Hash_table
import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as Dlist_storage
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.bend as Dlist_storage
import bend-collections-laws-containers@1.0.0.0/src/containers/internal/intrusive_list.bend as Intrusive_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/intrusive_list.bend as Intrusive_list
import bend-collections-laws-containers@1.0.0.0/src/containers/internal/vec.bend as Vec
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.bend as Vec
import bend-collections-laws-containers@1.0.0.0/src/containers/intrusive_doubly_linked_list.bend as Intrusive_doubly_linked_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_doubly_linked_list.bend as Intrusive_doubly_linked_list
import bend-collections-laws-containers@1.0.0.0/src/containers/intrusive_links.bend as Intrusive_links
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.bend as Intrusive_links
import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as Lru
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.bend as Lru
import bend-collections-laws-containers@1.0.0.0/src/containers/priority_queue.bend as Priority_queue
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/priority_queue.bend as Priority_queue
import bend-collections-laws-containers@1.0.0.0/src/containers/queue.bend as Queue
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.bend as Queue
import bend-collections-laws-containers@1.0.0.0/src/containers/simple_queue.bend as Simple_queue
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.bend as Simple_queue
import bend-collections-laws-containers@1.0.0.0/src/containers/stack.bend as Stack
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.bend as Stack
import bend-collections-laws-containers@1.0.0.0/src/containers/types/balanced_search_tree.bend as Balanced_search_tree
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/balanced_search_tree.bend as Balanced_search_tree
import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as Binary_heap
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.bend as Binary_heap
import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitlist.bend as Bitlist
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.bend as Bitlist
import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitset.bend as Bitset
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.bend as Bitset
import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as Deque
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.bend as Deque
import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as Doubly_linked_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.bend as Doubly_linked_list
import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as Dynamic_array
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.bend as Dynamic_array
import bend-collections-laws-containers@1.0.0.0/src/containers/types/internal_dlist.bend as Internal_dlist
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.bend as Internal_dlist
import bend-collections-laws-containers@1.0.0.0/src/containers/types/intrusive_doubly_linked_list.bend as Intrusive_doubly_linked_list
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/intrusive_doubly_linked_list.bend as Intrusive_doubly_linked_list
import bend-collections-laws-containers@1.0.0.0/src/containers/types/queue.bend as Queue
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.bend as Queue
import bend-collections-laws-containers@1.0.0.0/src/containers/types/stack.bend as Stack
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.bend as Stack
import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as Hash
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/hash.bend as Hash
import bend-collections-laws-containers@1.0.0.0/src/math/natural.bend as Natural
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.bend as Natural
import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as Pow2
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/pow2.bend as Pow2
import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as U64
import 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.bend as U64

Modules

• laws_containers.bend not loaded
• proofs/END_TO_END.bend 86 declarations, 86 laws
• proofs/PROOF.bend not loaded
• proofs/containers/balanced_search_tree/agree.bend 22 declarations
• proofs/containers/balanced_search_tree/alloc.bend 4 declarations
• proofs/containers/balanced_search_tree/alls.bend 14 declarations
• proofs/containers/balanced_search_tree/api.bend 27 declarations
• proofs/containers/balanced_search_tree/arr.bend 13 declarations
• proofs/containers/balanced_search_tree/attach.bend 8 declarations
• proofs/containers/balanced_search_tree/bk.bend 24 declarations
• proofs/containers/balanced_search_tree/capi.bend 12 declarations
• proofs/containers/balanced_search_tree/ccv.bend 13 declarations
• proofs/containers/balanced_search_tree/cnx.bend 33 declarations
• proofs/containers/balanced_search_tree/components.bend 21 declarations
• proofs/containers/balanced_search_tree/crk.bend 11 declarations
• proofs/containers/balanced_search_tree/crm.bend 28 declarations
• proofs/containers/balanced_search_tree/csv.bend 8 declarations
• proofs/containers/balanced_search_tree/cur.bend 26 declarations
• proofs/containers/balanced_search_tree/da.bend 17 declarations
• proofs/containers/balanced_search_tree/dfix.bend 27 declarations
• proofs/containers/balanced_search_tree/dj.bend 17 declarations
• proofs/containers/balanced_search_tree/dord.bend 6 declarations
• proofs/containers/balanced_search_tree/ends.bend 19 declarations
• proofs/containers/balanced_search_tree/find.bend 13 declarations
• proofs/containers/balanced_search_tree/fix.bend 34 declarations
• proofs/containers/balanced_search_tree/frame.bend 13 declarations
• proofs/containers/balanced_search_tree/hdr.bend 13 declarations
• proofs/containers/balanced_search_tree/idmv.bend 12 declarations
• proofs/containers/balanced_search_tree/ins.bend 6 declarations
• proofs/containers/balanced_search_tree/insf.bend 12 declarations
• proofs/containers/balanced_search_tree/life.bend 5 declarations
• proofs/containers/balanced_search_tree/mirror.bend 275 declarations
• proofs/containers/balanced_search_tree/mk.bend 21 declarations
• proofs/containers/balanced_search_tree/mokx.bend 4 declarations
• proofs/containers/balanced_search_tree/nav.bend 7 declarations
• proofs/containers/balanced_search_tree/navl.bend 10 declarations
• proofs/containers/balanced_search_tree/navm.bend 10 declarations
• proofs/containers/balanced_search_tree/navs.bend 8 declarations
• proofs/containers/balanced_search_tree/nbr.bend 27 declarations
• proofs/containers/balanced_search_tree/nsf.bend 59 declarations
• proofs/containers/balanced_search_tree/nsl.bend 60 declarations
• proofs/containers/balanced_search_tree/nsr.bend 6 declarations
• proofs/containers/balanced_search_tree/ok.bend 7 declarations
• proofs/containers/balanced_search_tree/ord.bend 28 declarations
• proofs/containers/balanced_search_tree/path.bend 27 declarations
• proofs/containers/balanced_search_tree/plug.bend 3 declarations
• proofs/containers/balanced_search_tree/prim.bend 15 declarations
• proofs/containers/balanced_search_tree/proof.bend 103 declarations
• proofs/containers/balanced_search_tree/putf.bend 7 declarations
• proofs/containers/balanced_search_tree/putm.bend 35 declarations
• proofs/containers/balanced_search_tree/range.bend 1 declarations
• proofs/containers/balanced_search_tree/reads.bend 14 declarations
• proofs/containers/balanced_search_tree/rmd.bend 24 declarations
• proofs/containers/balanced_search_tree/rmf.bend 4 declarations
• proofs/containers/balanced_search_tree/rmi.bend 8 declarations
• proofs/containers/balanced_search_tree/rmp.bend 21 declarations
• proofs/containers/balanced_search_tree/rms.bend 18 declarations
• proofs/containers/balanced_search_tree/rmv.bend 22 declarations
• proofs/containers/balanced_search_tree/rot.bend 15 declarations
• proofs/containers/balanced_search_tree/rotm.bend 9 declarations
• proofs/containers/balanced_search_tree/rotn.bend 28 declarations
• proofs/containers/balanced_search_tree/rotp.bend 32 declarations
• proofs/containers/balanced_search_tree/setters.bend 102 declarations
• proofs/containers/balanced_search_tree/sim.bend 525 declarations
• proofs/containers/balanced_search_tree/slot.bend 20 declarations
• proofs/containers/balanced_search_tree/spath.bend 7 declarations
• proofs/containers/balanced_search_tree/state.bend 98 declarations
• proofs/containers/balanced_search_tree/succ.bend 10 declarations
• proofs/containers/balanced_search_tree/tree.bend 21 declarations
• proofs/containers/balanced_search_tree/unl.bend 14 declarations
• proofs/containers/balanced_search_tree/vapi.bend 21 declarations
• proofs/containers/balanced_search_tree/vclr.bend 30 declarations
• proofs/containers/balanced_search_tree/vdef.bend 8 declarations
• proofs/containers/balanced_search_tree/vit.bend 10 declarations
• proofs/containers/balanced_search_tree/vnav.bend 11 declarations
• proofs/containers/balanced_search_tree/vsp.bend 86 declarations
• proofs/containers/balanced_search_tree/vsz.bend 33 declarations
• proofs/containers/balanced_search_tree/vw.bend 24 declarations
• proofs/containers/balanced_search_tree/xtr.bend 3 declarations
• proofs/containers/binary_heap/bag.bend 12 declarations
• proofs/containers/binary_heap/budget.bend 7 declarations
• proofs/containers/binary_heap/down.bend 99 declarations
• proofs/containers/binary_heap/grow.bend 12 declarations
• proofs/containers/binary_heap/idx.bend 43 declarations
• proofs/containers/binary_heap/multiset.bend 8 declarations
• proofs/containers/binary_heap/pop.bend 30 declarations
• proofs/containers/binary_heap/proof.bend 46 declarations
• proofs/containers/binary_heap/push.bend 14 declarations
• proofs/containers/binary_heap/root.bend 21 declarations
• proofs/containers/binary_heap/slots.bend 50 declarations
• proofs/containers/binary_heap/sorted.bend 9 declarations
• proofs/containers/binary_heap/state.bend 24 declarations
• proofs/containers/binary_heap/steps.bend 30 declarations
• proofs/containers/binary_heap/trace.bend 26 declarations
• proofs/containers/binary_heap/u32idx.bend 15 declarations
• proofs/containers/binary_heap/up.bend 84 declarations
• proofs/containers/binary_heap/vals.bend 12 declarations
• proofs/containers/bitlist/bits.bend 29 declarations
• proofs/containers/bitlist/da.bend 65 declarations
• proofs/containers/bitlist/loops.bend 16 declarations
• proofs/containers/bitlist/proof.bend 58 declarations
• proofs/containers/bitlist/state.bend 12 declarations
• proofs/containers/bitlist/steps.bend 62 declarations
• proofs/containers/bitlist/trace.bend 28 declarations
• proofs/containers/bitset/arr.bend 16 declarations
• proofs/containers/bitset/depth.bend 6 declarations
• proofs/containers/bitset/fastcount.bend 10 declarations
• proofs/containers/bitset/index.bend 15 declarations
• proofs/containers/bitset/lists.bend 38 declarations
• proofs/containers/bitset/listx.bend 9 declarations
• proofs/containers/bitset/loops.bend 14 declarations
• proofs/containers/bitset/model.bend 8 declarations
• proofs/containers/bitset/proof.bend 65 declarations
• proofs/containers/bitset/state.bend 59 declarations
• proofs/containers/bitset/steps.bend 68 declarations
• proofs/containers/bitset/trace.bend 21 declarations
• proofs/containers/bitset/walk.bend 8 declarations
• proofs/containers/bitset/word.bend 23 declarations
• proofs/containers/bitset/zip.bend 8 declarations
• proofs/containers/deque/proof.bend 35 declarations
• proofs/containers/deque/rebalance.bend 15 declarations
• proofs/containers/deque/state.bend 8 declarations
• proofs/containers/deque/stepok.bend 2 declarations
• proofs/containers/deque/steps.bend 22 declarations
• proofs/containers/deque/trace.bend 15 declarations
• proofs/containers/dlist_iterator/proof.bend 27 declarations
• proofs/containers/doubly_linked_list/api.bend 19 declarations
• proofs/containers/doubly_linked_list/direct.bend 30 declarations
• proofs/containers/doubly_linked_list/direct_laws.bend 29 declarations
• proofs/containers/doubly_linked_list/grow.bend 9 declarations
• proofs/containers/doubly_linked_list/hins.bend 4 declarations
• proofs/containers/doubly_linked_list/hlive.bend 17 declarations
• proofs/containers/doubly_linked_list/hnb.bend 18 declarations
• proofs/containers/doubly_linked_list/hrd.bend 14 declarations
• proofs/containers/doubly_linked_list/ins.bend 6 declarations
• proofs/containers/doubly_linked_list/insf.bend 5 declarations
• proofs/containers/doubly_linked_list/insg.bend 10 declarations
• proofs/containers/doubly_linked_list/insp.bend 7 declarations
• proofs/containers/doubly_linked_list/link.bend 16 declarations
• proofs/containers/doubly_linked_list/links.bend 7 declarations
• proofs/containers/doubly_linked_list/lv.bend 13 declarations
• proofs/containers/doubly_linked_list/ok.bend 2 declarations
• proofs/containers/doubly_linked_list/proof.bend 88 declarations
• proofs/containers/doubly_linked_list/rel.bend 54 declarations
• proofs/containers/doubly_linked_list/rm.bend 28 declarations
• proofs/containers/doubly_linked_list/state.bend 84 declarations
• proofs/containers/doubly_linked_list/step.bend 24 declarations
• proofs/containers/doubly_linked_list/trace.bend 13 declarations
• proofs/containers/doubly_linked_list/valid.bend 17 declarations
• proofs/containers/doubly_linked_list/vals.bend 36 declarations
• proofs/containers/doubly_linked_list/walk.bend 8 declarations
• proofs/containers/dynamic_array/clear.bend 5 declarations
• proofs/containers/dynamic_array/closed.bend 16 declarations
• proofs/containers/dynamic_array/growth.bend 14 declarations
• proofs/containers/dynamic_array/layout.bend 26 declarations
• proofs/containers/dynamic_array/owned.bend 12 declarations
• proofs/containers/dynamic_array/owned_instances.bend 36 declarations
• proofs/containers/dynamic_array/owned_swap.bend 7 declarations
• proofs/containers/dynamic_array/proof.bend 62 declarations
• proofs/containers/dynamic_array/state.bend 22 declarations
• proofs/containers/dynamic_array/steps.bend 29 declarations
• proofs/containers/dynamic_array/trace.bend 20 declarations
• proofs/containers/dynamic_array/walk.bend 12 declarations
• proofs/containers/hash_table/arena.bend 14 declarations
• proofs/containers/hash_table/arr.bend 5 declarations
• proofs/containers/hash_table/buckets.bend 62 declarations
• proofs/containers/hash_table/cyc.bend 12 declarations
• proofs/containers/hash_table/decide.bend 11 declarations
• proofs/containers/hash_table/delmv.bend 25 declarations
• proofs/containers/hash_table/delw.bend 5 declarations
• proofs/containers/hash_table/get.bend 13 declarations
• proofs/containers/hash_table/grow.bend 50 declarations
• proofs/containers/hash_table/has.bend 6 declarations
• proofs/containers/hash_table/hole.bend 38 declarations
• proofs/containers/hash_table/insa.bend 26 declarations
• proofs/containers/hash_table/insert.bend 38 declarations
• proofs/containers/hash_table/insf.bend 17 declarations
• proofs/containers/hash_table/insgrow.bend 14 declarations
• proofs/containers/hash_table/insm.bend 53 declarations
• proofs/containers/hash_table/insu.bend 11 declarations
• proofs/containers/hash_table/inv.bend 11 declarations
• proofs/containers/hash_table/keys.bend 15 declarations
• proofs/containers/hash_table/keysw.bend 29 declarations
• proofs/containers/hash_table/lookup.bend 18 declarations
• proofs/containers/hash_table/modn.bend 13 declarations
• proofs/containers/hash_table/new.bend 2 declarations
• proofs/containers/hash_table/pop.bend 50 declarations
• proofs/containers/hash_table/poplem.bend 32 declarations
• proofs/containers/hash_table/probe_all.bend 15 declarations
• proofs/containers/hash_table/probe_impl.bend 14 declarations
• proofs/containers/hash_table/proof.bend 55 declarations
• proofs/containers/hash_table/qprobe.bend 17 declarations
• proofs/containers/hash_table/rawins.bend 20 declarations
• proofs/containers/hash_table/rebuild.bend 1 declarations
• proofs/containers/hash_table/rehash.bend 37 declarations
• proofs/containers/hash_table/ring.bend 13 declarations
• proofs/containers/hash_table/set.bend 6 declarations
• proofs/containers/hash_table/setins.bend 20 declarations
• proofs/containers/hash_table/setok.bend 11 declarations
• proofs/containers/hash_table/setv.bend 10 declarations
• proofs/containers/hash_table/shift.bend 108 declarations
• proofs/containers/hash_table/size.bend 6 declarations
• proofs/containers/hash_table/speclem.bend 24 declarations
• proofs/containers/hash_table/state.bend 87 declarations
• proofs/containers/hash_table/step.bend 15 declarations
• proofs/containers/hash_table/strings.bend 13 declarations
• proofs/containers/hash_table/table.bend 12 declarations
• proofs/containers/hash_table/tools.bend 14 declarations
• proofs/containers/hash_table/words.bend 41 declarations
• proofs/containers/intrusive_doubly_linked_list/adapter.bend 8 declarations
• proofs/containers/intrusive_doubly_linked_list/array_adapter.bend not loaded
• proofs/containers/intrusive_doubly_linked_list/clear.bend 6 declarations
• proofs/containers/intrusive_doubly_linked_list/costs.bend 3 declarations
• proofs/containers/intrusive_doubly_linked_list/edits.bend 12 declarations
• proofs/containers/intrusive_doubly_linked_list/example.bend not loaded
• proofs/containers/intrusive_doubly_linked_list/fold.bend 7 declarations
• proofs/containers/intrusive_doubly_linked_list/frames.bend 13 declarations
• proofs/containers/intrusive_doubly_linked_list/history.bend 14 declarations
• proofs/containers/intrusive_doubly_linked_list/links.bend 40 declarations
• proofs/containers/intrusive_doubly_linked_list/proof.bend not loaded
• proofs/containers/intrusive_doubly_linked_list/shape.bend 46 declarations
• proofs/containers/intrusive_doubly_linked_list/writes.bend 7 declarations
• proofs/containers/lru/add.bend 13 declarations
• proofs/containers/lru/basic.bend 17 declarations
• proofs/containers/lru/bump.bend 10 declarations
• proofs/containers/lru/bumpk.bend 3 declarations
• proofs/containers/lru/bumpsh.bend 26 declarations
• proofs/containers/lru/contains.bend 10 declarations
• proofs/containers/lru/dellink.bend 10 declarations
• proofs/containers/lru/dll.bend 18 declarations
• proofs/containers/lru/drop.bend 1 declarations
• proofs/containers/lru/elfr.bend 5 declarations
• proofs/containers/lru/ent.bend 4 declarations
• proofs/containers/lru/evict.bend 11 declarations
• proofs/containers/lru/evictk.bend 5 declarations
• proofs/containers/lru/find.bend 15 declarations
• proofs/containers/lru/gone.bend 6 declarations
• proofs/containers/lru/grow.bend 4 declarations
• proofs/containers/lru/hw.bend 14 declarations
• proofs/containers/lru/idx.bend 20 declarations
• proofs/containers/lru/ins.bend 5 declarations
• proofs/containers/lru/ins1.bend 27 declarations
• proofs/containers/lru/insp.bend 7 declarations
• proofs/containers/lru/keys.bend 21 declarations
• proofs/containers/lru/linktail.bend 6 declarations
• proofs/containers/lru/lists.bend 12 declarations
• proofs/containers/lru/meta.bend 4 declarations
• proofs/containers/lru/miss.bend 20 declarations
• proofs/containers/lru/new.bend 5 declarations
• proofs/containers/lru/perm.bend 10 declarations
• proofs/containers/lru/pre.bend 12 declarations
• proofs/containers/lru/proof.bend 43 declarations
• proofs/containers/lru/purge.bend 27 declarations
• proofs/containers/lru/qrm.bend 4 declarations
• proofs/containers/lru/read.bend 24 declarations
• proofs/containers/lru/rebuild.bend 9 declarations
• proofs/containers/lru/remove.bend 10 declarations
• proofs/containers/lru/repl.bend 10 declarations
• proofs/containers/lru/resize.bend 13 declarations
• proofs/containers/lru/rmat.bend 13 declarations
• proofs/containers/lru/rmatk.bend 7 declarations
• proofs/containers/lru/rmrb.bend 43 declarations
• proofs/containers/lru/room.bend 15 declarations
• proofs/containers/lru/state.bend 159 declarations
• proofs/containers/lru/tabsl.bend 22 declarations
• proofs/containers/lru/tfind.bend 14 declarations
• proofs/containers/lru/touch.bend 8 declarations
• proofs/containers/lru/touchsh.bend 10 declarations
• proofs/containers/lru/trace.bend 28 declarations
• proofs/containers/lru/unlink.bend 22 declarations
• proofs/containers/lru/walk.bend 21 declarations
• proofs/containers/priority_queue/proof.bend 28 declarations
• proofs/containers/queue/proof.bend 25 declarations
• proofs/containers/queue/state.bend 8 declarations
• proofs/containers/queue/steps.bend 18 declarations
• proofs/containers/queue/trace.bend 15 declarations
• proofs/containers/simple_queue/proof.bend 23 declarations
• proofs/containers/stack/components.bend 4 declarations
• proofs/containers/stack/proof.bend 22 declarations
• proofs/lib/arith.bend 22 declarations
• proofs/lib/array.bend 40 declarations
• proofs/lib/array2.bend 6 declarations
• proofs/lib/array_ext.bend 8 declarations
• proofs/lib/flat.bend 21 declarations
• proofs/lib/lemmas/proofs/absent_read.bend 5 declarations
• proofs/lib/lemmas/proofs/abstraction_bindings.bend 11 declarations, 7 laws
• proofs/lib/lemmas/proofs/abstraction_identity.bend 4 declarations
• proofs/lib/lemmas/proofs/abstraction_lookup.bend 5 declarations
• proofs/lib/lemmas/proofs/abstraction_recency.bend 11 declarations, 2 laws
• proofs/lib/lemmas/proofs/abstraction_size.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/add_refinement.bend 5 declarations
• proofs/lib/lemmas/proofs/add_representation.bend 11 declarations
• proofs/lib/lemmas/proofs/addition.bend 9 declarations, 6 laws
• proofs/lib/lemmas/proofs/addition_bounds.bend 3 declarations
• proofs/lib/lemmas/proofs/aggregate_representation.bend 25 declarations
• proofs/lib/lemmas/proofs/cache_add_capacity.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/cache_delete_identities.bend 13 declarations
• proofs/lib/lemmas/proofs/cache_delete_membership.bend 20 declarations, 19 laws
• proofs/lib/lemmas/proofs/cache_key_identity.bend 7 declarations, 3 laws
• proofs/lib/lemmas/proofs/cache_oldest_available.bend 7 declarations, 5 laws
• proofs/lib/lemmas/proofs/cache_order.bend 6 declarations, 4 laws
• proofs/lib/lemmas/proofs/cache_populated.bend 13 declarations, 12 laws
• proofs/lib/lemmas/proofs/cache_prepare_capacity.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/cache_refresh_identity.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/cache_refresh_membership.bend 3 declarations, 3 laws
• proofs/lib/lemmas/proofs/cache_storage_preservation.bend 30 declarations, 28 laws
• proofs/lib/lemmas/proofs/cache_store_identities.bend 7 declarations
• proofs/lib/lemmas/proofs/cache_store_identity.bend 5 declarations
• proofs/lib/lemmas/proofs/cache_store_membership.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/canonical.bend 67 declarations
• proofs/lib/lemmas/proofs/canonical_native.bend 8 declarations
• proofs/lib/lemmas/proofs/canonical_remove.bend 1 declarations
• proofs/lib/lemmas/proofs/canonical_string.bend 11 declarations
• proofs/lib/lemmas/proofs/capacity_preservation.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/configuration_observations.bend 9 declarations
• proofs/lib/lemmas/proofs/configuration_representation.bend 24 declarations
• proofs/lib/lemmas/proofs/constructor_safety.bend 10 declarations
• proofs/lib/lemmas/proofs/core_refresh_representation.bend 7 declarations
• proofs/lib/lemmas/proofs/counter.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/disabled.bend 40 declarations, 36 laws
• proofs/lib/lemmas/proofs/division_bounds.bend 5 declarations
• proofs/lib/lemmas/proofs/division_candidate.bend 5 declarations
• proofs/lib/lemmas/proofs/division_candidate_bound.bend 4 declarations
• proofs/lib/lemmas/proofs/division_invariant.bend 6 declarations
• proofs/lib/lemmas/proofs/division_no_overflow.bend 11 declarations
• proofs/lib/lemmas/proofs/division_quotient.bend 12 declarations
• proofs/lib/lemmas/proofs/division_remainder.bend 4 declarations
• proofs/lib/lemmas/proofs/division_shift.bend 7 declarations
• proofs/lib/lemmas/proofs/division_value.bend 10 declarations
• proofs/lib/lemmas/proofs/duration_refinement.bend 3 declarations
• proofs/lib/lemmas/proofs/empty_events.bend 34 declarations, 31 laws
• proofs/lib/lemmas/proofs/enumeration_suffix.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/evict_then_write.bend 1 declarations
• proofs/lib/lemmas/proofs/eviction_state.bend 4 declarations
• proofs/lib/lemmas/proofs/expired_read.bend 2 declarations
• proofs/lib/lemmas/proofs/extensional_states.bend 22 declarations
• proofs/lib/lemmas/proofs/full_add.bend 4 declarations
• proofs/lib/lemmas/proofs/full_add_head.bend 3 declarations
• proofs/lib/lemmas/proofs/invariants.bend 17 declarations, 3 laws
• proofs/lib/lemmas/proofs/live_read_state.bend 4 declarations
• proofs/lib/lemmas/proofs/lookup_refinement.bend 10 declarations
• proofs/lib/lemmas/proofs/map_bits.bend 13 declarations, 11 laws
• proofs/lib/lemmas/proofs/map_bridge.bend 26 declarations, 18 laws
• proofs/lib/lemmas/proofs/map_character_prefix.bend 3 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_critbit_parts.bend 3 declarations, 2 laws
• proofs/lib/lemmas/proofs/map_delete.bend 11 declarations, 11 laws
• proofs/lib/lemmas/proofs/map_delete_below.bend 8 declarations, 8 laws
• proofs/lib/lemmas/proofs/map_delete_common.bend 8 declarations, 8 laws
• proofs/lib/lemmas/proofs/map_delete_critbit.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_delete_frame.bend 21 declarations, 19 laws
• proofs/lib/lemmas/proofs/map_delete_membership.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_delete_populated.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_delete_prefix.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/map_delete_routes.bend 10 declarations, 10 laws
• proofs/lib/lemmas/proofs/map_difference.bend 14 declarations, 12 laws
• proofs/lib/lemmas/proofs/map_difference_char.bend 11 declarations, 10 laws
• proofs/lib/lemmas/proofs/map_difference_order.bend 10 declarations, 9 laws
• proofs/lib/lemmas/proofs/map_enumeration.bend 7 declarations, 6 laws
• proofs/lib/lemmas/proofs/map_index.bend 9 declarations, 8 laws
• proofs/lib/lemmas/proofs/map_insert.bend 35 declarations, 30 laws
• proofs/lib/lemmas/proofs/map_insert_before.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_insert_below.bend 4 declarations, 4 laws
• proofs/lib/lemmas/proofs/map_insert_common.bend 8 declarations, 7 laws
• proofs/lib/lemmas/proofs/map_insert_critbit.bend 8 declarations, 7 laws
• proofs/lib/lemmas/proofs/map_insert_descent.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_insert_frame.bend 3 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_insert_inverse.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/map_insert_membership.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/map_insert_nonempty.bend 4 declarations, 4 laws
• proofs/lib/lemmas/proofs/map_insert_prefix.bend 6 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_insert_routes.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_key_disjoint.bend 4 declarations, 4 laws
• proofs/lib/lemmas/proofs/map_key_lookup.bend 10 declarations, 8 laws
• proofs/lib/lemmas/proofs/map_key_membership.bend 7 declarations, 7 laws
• proofs/lib/lemmas/proofs/map_key_presence.bend 4 declarations, 4 laws
• proofs/lib/lemmas/proofs/map_keys_unique.bend 10 declarations, 9 laws
• proofs/lib/lemmas/proofs/map_lookup.bend 13 declarations, 10 laws
• proofs/lib/lemmas/proofs/map_msb.bend 26 declarations, 24 laws
• proofs/lib/lemmas/proofs/map_populated.bend 12 declarations, 11 laws
• proofs/lib/lemmas/proofs/map_populated_inverse.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_prefix_algebra.bend 8 declarations, 8 laws
• proofs/lib/lemmas/proofs/map_prefix_bounds.bend 4 declarations, 4 laws
• proofs/lib/lemmas/proofs/map_prefix_join.bend 4 declarations, 4 laws
• proofs/lib/lemmas/proofs/map_prefix_routing.bend 2 declarations, 2 laws
• proofs/lib/lemmas/proofs/map_put_frame.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/map_route_boolean.bend 3 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_routing.bend 18 declarations, 13 laws
• proofs/lib/lemmas/proofs/map_seek.bend 9 declarations, 8 laws
• proofs/lib/lemmas/proofs/map_seek_discriminator.bend 3 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_seek_empty.bend 4 declarations, 4 laws
• proofs/lib/lemmas/proofs/map_seek_prefix.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_seek_routes.bend 4 declarations, 3 laws
• proofs/lib/lemmas/proofs/map_selected_prefix.bend 2 declarations, 2 laws
• proofs/lib/lemmas/proofs/map_set_critbit.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/map_set_frame.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_set_membership.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/map_shape.bend 11 declarations, 9 laws
• proofs/lib/lemmas/proofs/map_shape_invariants.bend 7 declarations, 7 laws
• proofs/lib/lemmas/proofs/map_splice_critbit.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/map_string_prefix.bend 16 declarations, 15 laws
• proofs/lib/lemmas/proofs/modular_addition.bend 13 declarations
• proofs/lib/lemmas/proofs/modular_negation.bend 6 declarations
• proofs/lib/lemmas/proofs/nat_algebra.bend 16 declarations
• proofs/lib/lemmas/proofs/native_map.bend 49 declarations, 44 laws
• proofs/lib/lemmas/proofs/natural_division.bend 6 declarations
• proofs/lib/lemmas/proofs/natural_products.bend 8 declarations
• proofs/lib/lemmas/proofs/negation_magnitude.bend 5 declarations
• proofs/lib/lemmas/proofs/nonfull_add.bend 4 declarations
• proofs/lib/lemmas/proofs/numeric.bend 24 declarations, 23 laws
• proofs/lib/lemmas/proofs/oldest_refinement.bend 4 declarations
• proofs/lib/lemmas/proofs/ordered_entries.bend 10 declarations
• proofs/lib/lemmas/proofs/protocol_storage.bend 10 declarations, 10 laws
• proofs/lib/lemmas/proofs/public_add.bend 27 declarations
• proofs/lib/lemmas/proofs/public_aggregate.bend 43 declarations
• proofs/lib/lemmas/proofs/public_config.bend 6 declarations
• proofs/lib/lemmas/proofs/public_diagnostics.bend 1 declarations
• proofs/lib/lemmas/proofs/public_drive.bend 1 declarations
• proofs/lib/lemmas/proofs/public_finish.bend 9 declarations
• proofs/lib/lemmas/proofs/public_oldest_ops.bend 5 declarations
• proofs/lib/lemmas/proofs/public_phase_safety.bend 63 declarations
• proofs/lib/lemmas/proofs/public_read.bend 5 declarations
• proofs/lib/lemmas/proofs/public_refresh.bend 6 declarations
• proofs/lib/lemmas/proofs/public_relation.bend 3 declarations
• proofs/lib/lemmas/proofs/public_requests.bend 1 declarations
• proofs/lib/lemmas/proofs/public_safety.bend 48 declarations
• proofs/lib/lemmas/proofs/public_simple.bend 1 declarations
• proofs/lib/lemmas/proofs/public_trace.bend 14 declarations
• proofs/lib/lemmas/proofs/read_refinement.bend 3 declarations
• proofs/lib/lemmas/proofs/read_representation.bend 21 declarations
• proofs/lib/lemmas/proofs/recency_bounds.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/recency_capacity.bend 10 declarations, 9 laws
• proofs/lib/lemmas/proofs/recency_head_removal.bend 5 declarations
• proofs/lib/lemmas/proofs/recency_membership.bend 6 declarations, 6 laws
• proofs/lib/lemmas/proofs/recency_move_inclusion.bend 5 declarations, 4 laws
• proofs/lib/lemmas/proofs/recency_unique.bend 20 declarations, 19 laws
• proofs/lib/lemmas/proofs/recency_update_membership.bend 5 declarations, 5 laws
• proofs/lib/lemmas/proofs/refinement.bend 32 declarations, 23 laws
• proofs/lib/lemmas/proofs/refresh_complete_representation.bend 9 declarations
• proofs/lib/lemmas/proofs/refresh_lookup.bend 11 declarations, 9 laws
• proofs/lib/lemmas/proofs/refresh_representation.bend 9 declarations, 3 laws
• proofs/lib/lemmas/proofs/refresh_state.bend 5 declarations
• proofs/lib/lemmas/proofs/removal_lookup.bend 7 declarations
• proofs/lib/lemmas/proofs/removal_representation.bend 20 declarations
• proofs/lib/lemmas/proofs/removal_state.bend 7 declarations
• proofs/lib/lemmas/proofs/remove_refinement.bend 2 declarations
• proofs/lib/lemmas/proofs/replacement_refinement.bend 3 declarations
• proofs/lib/lemmas/proofs/representation_access.bend 10 declarations
• proofs/lib/lemmas/proofs/representation_parts.bend 17 declarations, 9 laws
• proofs/lib/lemmas/proofs/signed_division.bend 5 declarations
• proofs/lib/lemmas/proofs/size_length.bend 13 declarations
• proofs/lib/lemmas/proofs/spec_congruence.bend 51 declarations
• proofs/lib/lemmas/proofs/spec_erase_lookup.bend 6 declarations
• proofs/lib/lemmas/proofs/spec_lookup.bend 14 declarations
• proofs/lib/lemmas/proofs/spec_write_lookup.bend 4 declarations
• proofs/lib/lemmas/proofs/store_lookup_refinement.bend 5 declarations
• proofs/lib/lemmas/proofs/store_representation.bend 1 declarations
• proofs/lib/lemmas/proofs/store_state.bend 7 declarations
• proofs/lib/lemmas/proofs/string_compare.bend 21 declarations, 18 laws
• proofs/lib/lemmas/proofs/string_order.bend 6 declarations
• proofs/lib/lemmas/proofs/subtraction_bounds.bend 7 declarations
• proofs/lib/lemmas/proofs/word_addition.bend 3 declarations
• proofs/lib/lemmas/proofs/word_bounds.bend 2 declarations, 2 laws
• proofs/lib/lemmas/proofs/word_comparison.bend 5 declarations
• proofs/lib/lemmas/proofs/word_multiplication.bend 9 declarations
• proofs/lib/lemmas/proofs/word_shift.bend 6 declarations
• proofs/lib/lemmas/proofs/word_subtraction.bend 5 declarations
• proofs/lib/lemmas/proofs/word_value.bend 19 declarations
• proofs/lib/lemmas/proofs/write_congruence.bend 6 declarations
• proofs/lib/lemmas/spec/cache.bend 53 declarations
• proofs/lib/lemmas/spec/clock.bend 12 declarations
• proofs/lib/lemmas/spec/effectful_aggregate.bend 9 declarations
• proofs/lib/lemmas/spec/effectful_operations.bend 27 declarations
• proofs/lib/lemmas/spec/equivalence.bend 9 declarations
• proofs/lib/lemmas/spec/numeric.bend 17 declarations
• proofs/lib/lemmas/spec/operations.bend 37 declarations
• proofs/lib/lemmas/spec/public_commands.bend 33 declarations
• proofs/lib/lemmas/spec/traces.bend 7 declarations
• proofs/lib/lemmas/spec/unsigned_division.bend 1 declarations
• proofs/lib/lemmas/src/cache.bend 60 declarations, 1 laws
• proofs/lib/lemmas/src/codec.bend 24 declarations, 12 laws
• proofs/lib/lemmas/src/driver.bend 17 declarations
• proofs/lib/lemmas/src/entry_ops.bend 6 declarations
• proofs/lib/lemmas/src/protocol.bend 42 declarations
• proofs/lib/lemmas/src/public.bend 82 declarations
• proofs/lib/lemmas/src/time.bend 8 declarations
• proofs/lib/lemmas/src/wide.bend 27 declarations
• proofs/lib/lemmas/types/model.bend 12 declarations
• proofs/lib/links.bend 10 declarations
• proofs/lib/list.bend 46 declarations
• proofs/lib/logic.bend 24 declarations
• proofs/lib/nat.bend 75 declarations
• proofs/lib/nat_list.bend 39 declarations
• proofs/lib/order.bend 33 declarations
• proofs/lib/sequence.bend 26 declarations
• proofs/lib/two_list.bend 7 declarations
• proofs/lib/u32.bend 43 declarations
• proofs/lib/u32_tree.bend 5 declarations
• proofs/lib/u32alg.bend 36 declarations
• proofs/lib/u32div.bend 28 declarations
• proofs/lib/u32seq.bend 12 declarations
• proofs/lib/vec.bend 18 declarations
• proofs/lib/word.bend 41 declarations
• proofs/lib/words32.bend 13 declarations
• proofs/math/hash/hash.bend 8 declarations
• proofs/math/natural/arith.bend 23 declarations
• proofs/math/natural/bits.bend 14 declarations
• proofs/math/natural/fact.bend 28 declarations
• proofs/math/natural/gcd.bend 18 declarations
• proofs/math/natural/inverse.bend 25 declarations
• proofs/math/natural/lcm.bend 22 declarations
• proofs/math/natural/lists.bend 24 declarations
• proofs/math/natural/logs.bend 17 declarations
• proofs/math/natural/misc.bend 14 declarations
• proofs/math/natural/modpow.bend 8 declarations
• proofs/math/natural/proof.bend 54 declarations
• proofs/math/natural/roots.bend 29 declarations
• proofs/math/natural/sqrtn.bend 13 declarations
• proofs/math/pow2/pow2.bend 2 declarations
• proofs/math/proof.bend 13 declarations
• proofs/math/u64/u64.bend 31 declarations
• proofs/math/u64/u64div.bend 39 declarations
• spec/containers/balanced_search_tree/main.bend 132 declarations
• spec/containers/balanced_search_tree/recursive.bend 18 declarations
• spec/containers/binary_heap.bend 33 declarations
• spec/containers/bitlist.bend 56 declarations
• spec/containers/bitset.bend 53 declarations
• spec/containers/deque.bend 32 declarations
• spec/containers/dlist_iterator.bend 0 declarations
• spec/containers/doubly_linked_list.bend 99 declarations
• spec/containers/dynamic_array.bend 46 declarations
• spec/containers/hash_table.bend 32 declarations
• spec/containers/intrusive_doubly_linked_list/main.bend 9 declarations
• spec/containers/intrusive_doubly_linked_list/model.bend 30 declarations
• spec/containers/intrusive_doubly_linked_list/programs.bend 10 declarations
• spec/containers/lru.bend 86 declarations
• spec/containers/priority_queue.bend 18 declarations
• spec/containers/queue.bend 21 declarations
• spec/containers/simple_queue.bend 14 declarations
• spec/containers/stack.bend 18 declarations
• spec/lib/common.bend 21 declarations
• spec/lib/numeric.bend 15 declarations
• spec/lib/order.bend 2 declarations
• spec/lib/sequence.bend 7 declarations
• spec/lib/u32seq.bend 4 declarations
• spec/math/hash.bend 2 declarations
• spec/math/natural.bend 58 declarations
• spec/math/pow2.bend 1 declarations
• spec/math/u64.bend 9 declarations
• src/containers/balanced_search_tree.bend 383 declarations — Generated by tools/generators/tree_map.py; edit algorithm definitions there.
• src/containers/binary_heap.bend 75 declarations
• src/containers/bitlist.bend 52 declarations
• src/containers/bitset.bend 91 declarations
• src/containers/deque.bend 32 declarations
• src/containers/dlist_iterator.bend 56 declarations
• src/containers/doubly_linked_list.bend 63 declarations
• src/containers/dynamic_array.bend 107 declarations
• src/containers/hash_table.bend 120 declarations
• src/containers/internal/dlist_storage.bend 93 declarations
• src/containers/internal/intrusive_list.bend 139 declarations — Generated by tools/generators/intrusive_list.py; edit that source.
• src/containers/internal/vec.bend 11 declarations
• src/containers/intrusive_doubly_linked_list.bend 42 declarations — Generated by tools/generators/intrusive_list.py; edit that source.
• src/containers/intrusive_links.bend 18 declarations
• src/containers/lru.bend 181 declarations
• src/containers/priority_queue.bend 7 declarations
• src/containers/queue.bend 20 declarations
• src/containers/simple_queue.bend 6 declarations
• src/containers/stack.bend 17 declarations
• src/containers/types/balanced_search_tree.bend 25 declarations
• src/containers/types/binary_heap.bend 14 declarations
• src/containers/types/bitlist.bend 20 declarations
• src/containers/types/bitset.bend 19 declarations
• src/containers/types/deque.bend 16 declarations
• src/containers/types/doubly_linked_list.bend 27 declarations
• src/containers/types/dynamic_array.bend 21 declarations
• src/containers/types/internal_dlist.bend 27 declarations
• src/containers/types/intrusive_doubly_linked_list.bend 14 declarations
• src/containers/types/queue.bend 13 declarations
• src/containers/types/stack.bend 13 declarations
• src/math/hash.bend 4 declarations
• src/math/natural.bend 52 declarations
• src/math/pow2.bend 2 declarations
• src/math/u64.bend 19 declarations

Other files

• LICENSE 1,101 bytes

Dependencies

No imports from other hub packages.

Dependents

• 0x993b989c via laws.bend: import bend-collections-laws-containers@1.0.0.0/laws_containers.bend as Containers

Status on bend 2.0.36

Error:
- expected : a fresh constructor name (duplicate declaration: Ready)
- observed : 'Ready'
Location:
17 | type Root is Data:
18>|   Ready{}
   |   ^^^^^
19 |   Waiting{}

Error:
- expected : a fresh constructor name (duplicate declaration: Ready)
- observed : 'Ready'
Location:
17 | type Root is Data:
18>|   Ready{}
   |   ^^^^^
19 |   Waiting{}

Error:
- expected : a fresh constructor name (duplicate declaration: Ready)
- observed : 'Ready'
Location:
17 | type Root is Data:
18>|   Ready{}
   |   ^^^^^
19 |   Waiting{}

Error:
- expected : a fresh constructor name (duplicate declaration: Ready)
- observed : 'Ready'
Location:
17 | type Root is Data:
18>|   Ready{}
   |   ^^^^^
19 |   Waiting{}

Error:
- expected : a fresh constructor name (duplicate declaration: Ready)
- observed : 'Ready'
Location:
17 | type Root is Data:
18>|   Ready{}
   |   ^^^^^
19 |   Waiting{}