~/bend-docscommunity

proofs/containers/intrusive_doubly_linked_list/frames.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/frames.bend as Frames

3 imports
import Base
import ../../../spec/containers/intrusive_doubly_linked_list/model.bend as G
import ./shape.bend as S

Templates

template separated source · line 6 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @at:Maybe<&2, N> -> @xs:List<&2, N> -> Data

template optional_frame source · line 11 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+at:Maybe<&2, N> -> @+v:Maybe<&2, N> -> @+xs:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @sep:separated(N, eq, at, xs) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, xs, q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.optional_prev(N, R, P, g, at, v), p, xs, q)

template remove_segment_frame source · line 18 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+before:Maybe<&2, N> -> @+after:Maybe<&2, N> -> @+xs:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @+an:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, xs) -> @ap:separated(N, eq, before, xs) -> @aq:separated(N, eq, after, xs) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, xs, q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, before, after), p, xs, q)

Any other chain disjoint from the edited node and its two neighbours keeps every next/prev link. It may be another root in the same association.

template prepend_segment_frame source · line 27 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+head:Maybe<&2, N> -> @+xs:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @an:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, xs) -> @ah:separated(N, eq, head, xs) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, xs, q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.attach(N, R, P, g, r, n, head), p, xs, q)

template root_effect source · line 30 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @p:Maybe<&2, N> -> @q:Maybe<&2, N> -> @+x:R -> Maybe<&2, N>

template remove_root_effect source · line 35 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @+x:R -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, p, q), x) == root_effect(N, R, P, req, g, r, p, q, x) : Maybe<&2, N>}

template root_effect_other source · line 42 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @+x:R -> @neq:{req(r, x) == False{} : Bool} -> {root_effect(N, R, P, req, g, r, p, q, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, x) : Maybe<&2, N>}

template remove_other_root source · line 49 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @+x:R -> @neq:{req(r, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, p, q), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, x) : Maybe<&2, N>}

template prepend_root_effect source · line 52 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+h:Maybe<&2, N> -> @+x:R -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.attach(N, R, P, g, r, n, h), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.choose(Maybe<&2, N>, req(r, x), Some{n}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, x)) : Maybe<&2, N>}

template prepend_other_root source · line 57 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+h:Maybe<&2, N> -> @+x:R -> @neq:{req(r, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.attach(N, R, P, g, r, n, h), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, x) : Maybe<&2, N>}

template removed_next source · line 62 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @same:{eq(n, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, p, q), n) == None{} : Maybe<&2, N>}

template removed_nonhead_prev source · line 67 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+p:N -> @+q:Maybe<&2, N> -> @same:{eq(n, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, Some{p}, q), n) == None{} : Maybe<&2, N>}

template removed_head_prev source · line 70 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+n:N -> @+q:Maybe<&2, N> -> @hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, n) == None{} : Maybe<&2, N>} -> @aq:separated(N, eq, q, [n]) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.cut(N, R, P, g, r, n, None{}, q), n) == None{} : Maybe<&2, N>}