proofs/containers/balanced_search_tree/vdef.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vdef.bend as Vdef

7 imports

import Base
import ../../lib/logic.bend as L
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI
import ./ok.bend as OK

Templates

template vmod source · line 15 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.View<K, V>

template vgood source · line 20 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> Bool

template vg_dg source · line 25 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+h:{vgood(K, V, cmp, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.dgv(K, V, w) == True{} : Bool}

template VOK source · line 31 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @sp:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.View<K, V> -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.View<K, V, cmp> -> Type

a view refining a specification's

template VM source · line 35 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @sp:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.View<K, V>, X) -> @mir:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V>, X) -> Type

a mirror view result refining a specification's

template VPOK source · line 39 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @sp:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.View<K, V>, X) -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.View<K, V, cmp>, X) -> Type

an implementation view result refining a specification's

template vm_pok source · line 42 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @-sp:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.View<K, V>, X) -> @-mir:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V>, X) -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.View<K, V, cmp>, X) -> @+hs:{r == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rvp(K, V, cmp, X, mir) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.View<K, V, cmp>, X)} -> @p:VM(K, V, cmp, X, sp, mir) -> VPOK(K, V, cmp, X, sp, r)

template vm_exact source · line 48 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-X:Data -> @-sp:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.View<K, V>, X) -> @-mir:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V>, X) -> @+w2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+o:X -> @+hm:{mir == (w2, o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V>, X)} -> @+hs:{sp == (vmod(K, V, cmp, w2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.View<K, V>, X)} -> @+hg:{vgood(K, V, cmp, w2) == True{} : Bool} -> VM(K, V, cmp, X, sp, mir)

a mirror result given exactly