bend-collections-laws-containers@1.0.0.0

0x5c489f5d9646d7cc9aa3dd8137e9dc07

Files (582)

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