proofs/containers/intrusive_doubly_linked_list/shape.bend checks

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

2 imports

import Base
import ../../../spec/containers/intrusive_doubly_linked_list/model.bend as G

Templates

template next_sn source · line 8 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+x:N -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sn(N, R, P, g, n, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.choose(Maybe<&2, N>, eq(n, x), v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, g, x)) : Maybe<&2, N>}

template prev_sn source · line 12 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+x:N -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sn(N, R, P, g, n, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, x) : Maybe<&2, N>}

template next_sp source · line 16 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+x:N -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sp(N, R, P, g, n, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, g, x) : Maybe<&2, N>}

template prev_sp source · line 20 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+x:N -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sp(N, R, P, g, n, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.choose(Maybe<&2, N>, eq(n, x), v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, x)) : Maybe<&2, N>}

template next_sh source · line 24 · 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 -> @+v:Maybe<&2, N> -> @+x:N -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sh(N, R, P, g, r, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, g, x) : Maybe<&2, N>}

template prev_sh source · line 28 · 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 -> @+v:Maybe<&2, N> -> @+x:N -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sh(N, R, P, g, r, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, x) : Maybe<&2, N>}

template next_sn_other source · line 32 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+x:N -> @neq:{eq(n, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sn(N, R, P, g, n, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, g, x) : Maybe<&2, N>}

template prev_sp_other source · line 37 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+x:N -> @neq:{eq(n, x) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sp(N, R, P, g, n, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, x) : Maybe<&2, N>}

template next_sn_self source · line 42 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v: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.sn(N, R, P, g, n, v), n) == v : Maybe<&2, N>}

template prev_sp_self source · line 47 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v: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.sp(N, R, P, g, n, v), n) == v : Maybe<&2, N>}

template segment_sn_frame source · line 52 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+xs:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @away:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, 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.sn(N, R, P, g, n, v), p, xs, q)

template segment_sp_frame source · line 60 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> @+xs:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @away:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, 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.sp(N, R, P, g, n, v), p, xs, q)

template segment_sh_frame source · line 68 · 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 -> @+v:Maybe<&2, N> -> @+xs:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @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.sh(N, R, P, g, r, v), p, xs, q)

template segment_first_prev source · line 77 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+x:N -> @+rest:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @+v:Maybe<&2, N> -> @same:{eq(x, x) == True{} : Bool} -> @away:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, x, rest) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, x <> rest, q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sp(N, R, P, g, x, v), v, x <> rest, q)

Changing a segment's first predecessor preserves its entire suffix.

template away_at source · line 84 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+prefix:List<&2, N> -> @+n:N -> @+suffix:List<&2, N> -> @+x:N -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, n <> suffix)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.both({eq(x, n) == False{} : Bool}, {eq(n, x) == False{} : Bool})

template away_delete source · line 89 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+prefix:List<&2, N> -> @+n:N -> @+suffix:List<&2, N> -> @+x:N -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, n <> suffix)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, suffix))

template unique_delete source · line 94 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+prefix:List<&2, N> -> @+n:N -> @+suffix:List<&2, N> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, n <> suffix)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, suffix))

template swapped source · line 99 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:N -> @+b:N -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.both({eq(a, b) == False{} : Bool}, {eq(b, a) == False{} : Bool}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.both({eq(b, a) == False{} : Bool}, {eq(a, b) == False{} : Bool})

template deleted_away source · line 103 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+prefix:List<&2, N> -> @+n:N -> @+suffix:List<&2, N> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, n <> suffix)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, suffix))

template first_append source · line 108 · raw

@-N:Data -> @+a:List<&2, N> -> @+b:List<&2, N> -> @+q:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, b, q)) : Maybe<&2, N>}

template first_end source · line 113 · raw

@-N:Data -> @+a:List<&2, N> -> @+n:N -> @+q:Maybe<&2, N> -> @+v:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [n]), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [n]), v) : Maybe<&2, N>}

template segment_last_next source · line 118 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+prefix:List<&2, N> -> @+n:N -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @+v:Maybe<&2, N> -> @+same:{eq(n, n) == True{} : Bool} -> @unique:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, [n])) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, [n]), q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sn(N, R, P, g, n, v), p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, [n]), v)

template segment_join source · line 127 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+b:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @ga:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, b, q)) -> @gb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.last(N, a, p), b, q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b), q)

template away_join source · line 133 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+b:List<&2, N> -> @+n:N -> @ga:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, a) -> @gb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b))

template unique_join source · line 138 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+b:List<&2, N> -> @ua:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, a) -> @+ub:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, b) -> @dis:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.disjoint(N, eq, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b))

template disjoint_last source · line 143 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+prefix:List<&2, N> -> @+n:N -> @+suffix:List<&2, N> -> @dis:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.disjoint(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, prefix, [n]), suffix) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, suffix)

template disjoint_head source · line 148 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+prefix:List<&2, N> -> @+n:N -> @+suffix:List<&2, N> -> @dis:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.disjoint(N, eq, prefix, n <> suffix) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, prefix)

template last_end source · line 153 · raw

@-N:Data -> @+a:List<&2, N> -> @+n:N -> @+p:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.last(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, [n]), p) == Some{n} : Maybe<&2, N>}

template first_middle source · line 160 · raw

@-N:Data -> @+a:List<&2, N> -> @+n:N -> @+b:List<&2, N> -> @+q:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, n <> b), q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, a, Some{n}) : Maybe<&2, N>}

A prefix/suffix split is the ordinary witness for removing a known member. The following lemmas extract the representation facts from the whole chain.

template prefix_segment source · line 165 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+b:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, n <> b), q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, a, Some{n})

template member_prev source · line 171 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+b:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, n <> b), q) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(N, R, P, eq, g, n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.last(N, a, p) : Maybe<&2, N>}

template member_next source · line 176 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+b:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, n <> b), q) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(N, R, P, eq, g, n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.first(N, b, q) : Maybe<&2, N>}

template suffix_segment source · line 181 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+b:List<&2, N> -> @+p:Maybe<&2, N> -> @+q:Maybe<&2, N> -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, n <> b), q) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.segment(N, R, P, eq, g, Some{n}, b, q)

template head_sn source · line 186 · raw

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

template head_sp source · line 190 · raw

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

template frame_sn source · line 194 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sn(N, R, P, g, n, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, g) : P}

template frame_sp source · line 198 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+n:N -> @+v:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sp(N, R, P, g, n, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, g) : P}

template frame_sh source · line 202 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+v:Maybe<&2, N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sh(N, R, P, g, r, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, g) : P}

template head_sh source · line 206 · 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 -> @+v: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.sh(N, R, P, g, r, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.choose(Maybe<&2, N>, req(r, x), v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, x)) : Maybe<&2, N>}

template head_sh_self source · line 210 · 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 -> @+v:Maybe<&2, N> -> @same:{req(r, r) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sh(N, R, P, g, r, v), r) == v : Maybe<&2, N>}

template head_sh_other source · line 215 · 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 -> @+v: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.sh(N, R, P, g, r, v), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(N, R, P, req, g, x) : Maybe<&2, N>}

template away_left source · line 220 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+b:List<&2, N> -> @+n:N -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, a)

template away_right source · line 225 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+b:List<&2, N> -> @+n:N -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.away(N, eq, n, b)

template unique_left source · line 230 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+b:List<&2, N> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, a)

template unique_right source · line 235 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+b:List<&2, N> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, b)

template disjoint_unique source · line 240 · raw

@-N:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+a:List<&2, N> -> @+b:List<&2, N> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.unique(N, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.append(N, a, b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.disjoint(N, eq, a, b)