~/bend-docscommunity

proofs/lib/lemmas/proofs/map_selected_prefix.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_selected_prefix.bend as Map_selected_prefix

8 imports
import Base
import ./invariants.bend as Inv
import ./map_insert.bend as I
import ./map_seek_prefix.bend as Seek
import ./map_string_prefix.bend as Difference
import ./map_prefix_algebra.bend as A
import ./map_routing.bend as R
import ./map_delete_prefix.bend as P

Laws

law selected_row provedsource · line 12 · raw

@-V:Data -> @tree:Map<&2, V> -> @+whole:Map<&2, V> -> @+key:String -> @+stored:String -> @+limit:Nat -> @+common:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, tree, whole, limit) == True{} : Bool} -> @+found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, whole, key)) == Some{stored} : Maybe<&2, String>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.prefix_against(V, stored, tree, limit) == True{} : Bool}

Extract a row for the actual native seek result from the all-pairs relation. The selected leaf is obtained by seek; no leaf-membership oracle is supplied.

law fresh_difference_prefix provedsource · line 33 · raw

@-V:Data -> @+tree:Map<&2, V> -> @+key:String -> @+stored:String -> @common:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.common_prefix(V, tree, tree, Map.diff(key, stored)) == True{} : Bool} -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(V, Map.seek(&2, V, tree, key)) == Some{stored} : Maybe<&2, String>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.prefix_against(V, key, tree, Map.diff(key, stored)) == True{} : Bool}

Discharge the fresh-key prefix premise at the actual native discriminator.