proofs/lib/lemmas/proofs/public_add.bend checks

import Base
import ../src/cache.bend as C
import ../src/codec.bend as Codec
import ../src/time.bend as Time
import ../src/public.bend as Pub
import ../src/driver.bend as D
import ../spec/cache.bend as S
import ../spec/clock.bend as Clock
import ../spec/numeric.bend as N
import ../spec/operations.bend as O
import ../spec/effectful_operations.bend as Eff
import ../spec/public_commands.bend as PC
import ../spec/equivalence.bend as E
import ../types/model.bend as T
import ./refinement.bend as F
import ./invariants.bend as Inv
import ./disabled.bend as Disabled
import ./spec_lookup.bend as Lookup
import ./public_relation.bend as R
import ./public_finish.bend as Finish
import ./extensional_states.bend as Ext
import ./empty_events.bend as Events
import ./add_refinement.bend as AddRefinement
import ./eviction_state.bend as Eviction
import ./lookup_refinement.bend as L
import ./abstraction_bindings.bend as B
import ./abstraction_recency.bend as Recency
import ./string_order.bend as Order
import ./cache_key_identity.bend as Key
import ./representation_access.bend as Access
import ./configuration_observations.bend as Config
import ./duration_refinement.bend as Duration
import ./numeric.bend as Numeric
import ./map_routing.bend as Routing