proofs/containers/intrusive_doubly_linked_list/history.bend checks

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

4 imports

import Base
import ../../../spec/containers/intrusive_doubly_linked_list/model.bend as G
import ./edits.bend as E
import ../../lib/logic.bend as Logic

Types

type Edit source · line 9 · raw

@-N:Data -> Data

The split fields are proof witnesses, not runtime arguments to remove. They name the old ordered sequence independently of the link algorithm.

Prepend
```
@-N:Data -> @node:N -> Edit<N>
```

RemoveHead

@-N:Data -> @node:N -> @rest:List<&2, N> -> Edit<N>

RemoveAfter

@-N:Data -> @prefix:List<&2, N> -> @previous:N -> @node:N -> @suffix:List<&2, N> -> Edit<N>

Templates

template order source · line 14 · raw

@-N:Data -> @op:Edit<N> -> @xs:List<&2, N> -> List<&2, N>

template step source · line 20 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @r:R -> @op:Edit<N> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P>

template permitted source · line 26 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @op:Edit<N> -> @+xs:List<&2, N> -> Data

template legal source · line 32 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @ops:List<&2, Edit<N>> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+xs:List<&2, N> -> Data

template run source · line 37 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @ops:List<&2, Edit<N>> -> @g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P>

template orders source · line 42 · raw

@-N:Data -> @ops:List<&2, Edit<N>> -> @xs:List<&2, N> -> List<&2, N>

template step_preserves source · line 47 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+op:Edit<N> -> @+xs:List<&2, N> -> @rsame:{req(r, r) == True{} : Bool} -> @pre:permitted(N, R, P, eq, g, op, xs) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, xs) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, step(N, R, P, eq, req, g, r, op), r, order(N, op, xs))

template run_preserves source · line 56 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @-reflex:(@x:N -> {eq(x, x) == True{} : Bool}) -> @+ops:List<&2, Edit<N>> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+xs:List<&2, N> -> @+rsame:{req(r, r) == True{} : Bool} -> @history:legal(N, R, P, eq, req, ops, g, r, xs) -> @good:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, g, r, xs) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.valid(N, R, P, eq, req, run(N, R, P, eq, req, ops, g, r), r, orders(N, ops, xs))

Induction over any finite legal history, not a bound or enumeration.

template step_frame source · line 62 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> @+op:Edit<N> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, step(N, R, P, eq, req, g, r, op)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, g) : P}

template run_frame source · line 68 · raw

@-N:Data -> @-R:Data -> @-P:Data -> @-eq:(@_:N -> @_:N -> Bool) -> @-req:(@_:R -> @_:R -> Bool) -> @+ops:List<&2, Edit<N>> -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<N, R, P> -> @+r:R -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, run(N, R, P, eq, req, ops, g, r)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.frame(N, R, P, g) : P}