proofs/containers/intrusive_doubly_linked_list/links.bend checks

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

11 imports

import Base
import ../../../spec/containers/intrusive_doubly_linked_list/model.bend as G
import ./adapter.bend as A
import ../../../spec/containers/intrusive_doubly_linked_list/programs.bend as Spec
import ../../lib/array.bend as AR
import ../../lib/logic.bend as LG
import ../../lib/list.bend as LL
import ../../lib/u32.bend as U
import ../../lib/u32alg.bend as UA
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/intrusive_links.bend as K

Types

type Depth source · line 36 · raw

Data

The graph's frame carries the table's sizes; no operation changes it.

Depth
```
@nodes:Nat -> @roots:Nat -> Depth
```

Definitions

def ueq source · line 25 · raw

@a:U32 -> @b:U32 -> Bool

def tn source · line 28 · raw

@+d:Nat -> @bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>

def real_at source · line 39 · raw

@ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @f:Depth -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links

def real source · line 44 · raw

@g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<U32, U32, Depth> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links

def dn_of source · line 48 · raw

@g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<U32, U32, Depth> -> Nat

def dr_of source · line 53 · raw

@g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<U32, U32, Depth> -> Nat

def bound source · line 58 · raw

@+d:Nat -> @+x:U32 -> Data

def keys_ok source · line 61 · raw

@+d:Nat -> @bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> Data

def gok source · line 68 · raw

@g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<U32, U32, Depth> -> Data

def nz source · line 74 · raw

@m:Maybe<&2, U32> -> Data

A link that is read: absent, or a nonzero id.

def inb source · line 82 · raw

@+d:Nat -> @m:Maybe<&2, U32> -> Data

A link that is written through: absent, or an id in range.

def tn_perfect source · line 91 · raw

@+d:Nat -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tn(d, bs)) == True{} : Bool}

def nth_rep source · line 98 · raw

@+m:Nat -> @+i:Nat -> @+h:{Nat.is_lt(i, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, m, 0), i) == Some{0} : Maybe<&2, U32>}

def eq_nat source · line 109 · raw

@+a:U32 -> @+b:U32 -> {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}

def ne_nat source · line 113 · raw

@+a:U32 -> @+b:U32 -> @+e:{U32.is_eq(a, b) == False{} : Bool} -> {Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) == False{} : Bool}

def lt_len source · line 118 · raw

@+d:Nat -> @+n:U32 -> @+xs:List<&2, U32> -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat} -> @+hn:bound(d, n) -> {Nat.is_lt(U32.to_nat(n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool}

def nth_bind source · line 123 · raw

@+d:Nat -> @+k:U32 -> @+v:Maybe<&2, U32> -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+n:U32 -> @+xs:List<&2, U32> -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat} -> @+hn:bound(d, n) -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, U32.to_nat(n)) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.encode(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, n, rest, None{}))} : Maybe<&2, U32>} -> @+b:Bool -> @+eb:{U32.is_eq(k, n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, xs, U32.to_nat(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.encode(v)), U32.to_nat(n)) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.encode(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.choose(Maybe<&2, U32>, b, v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, n, rest, None{})))} : Maybe<&2, U32>}

After a binding (k, v): the slot of n is v when k is n, else unchanged.

def tn_len source · line 132 · raw

@+d:Nat -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tn(d, bs))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat}

def tn_nth source · line 136 · raw

@+d:Nat -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+n:U32 -> @+hn:bound(d, n) -> @+hk:keys_ok(d, bs) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tn(d, bs)), U32.to_nat(n)) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.encode(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, n, bs, None{}))} : Maybe<&2, U32>}

Reading slot n of a realized tree gives the model's value for n.

def dec_enc source · line 145 · raw

@+m:Maybe<&2, U32> -> @+hz:nz(m) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.decode(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.encode(m)) == m : Maybe<&2, U32>}

def next_read source · line 156 · raw

@+n:U32 -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hn:bound(dn, n) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> @+hz:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, n, ns, None{})) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.next(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), n) == (real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, n, ns, None{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links, Maybe<&2, U32>)}

def prev_read source · line 161 · raw

@+n:U32 -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hn:bound(dn, n) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> @+hz:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, n, ps, None{})) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.prev(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), n) == (real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, n, ps, None{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links, Maybe<&2, U32>)}

def head_read source · line 167 · raw

@+r:U32 -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hr:bound(dr, r) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> @+hz:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, r, rs, None{})) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.get_head(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), r) == (real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.lookup(U32, Maybe<&2, U32>, ueq, r, rs, None{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links, Maybe<&2, U32>)}

def set_tree source · line 174 · raw

@+d:Nat -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+x:U32 -> @+v:Maybe<&2, U32> -> @+hd0:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hx:bound(d, x) -> @+kb:keys_ok(d, bs) -> {Array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tn(d, bs)), x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.encode(v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tn(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding{x, v} <> bs)) : Array<U32>}

def sn_law source · line 177 · raw

@+n:U32 -> @+v:Maybe<&2, U32> -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hn:bound(dn, n) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.set_next(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), n, v) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sn(U32, U32, Depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, n, v)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

def sp_law source · line 181 · raw

@+n:U32 -> @+v:Maybe<&2, U32> -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hn:bound(dn, n) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.set_prev(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), n, v) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sp(U32, U32, Depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, n, v)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

def sh_law source · line 185 · raw

@+r:U32 -> @+v:Maybe<&2, U32> -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hr:bound(dr, r) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.set_head(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), r, v) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.sh(U32, U32, Depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, r, v)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

def tgt source · line 192 · raw

@+dn:Nat -> @+dr:Nat -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<U32, U32> -> Data

def tgts source · line 203 · raw

@+dn:Nat -> @+dr:Nat -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<U32, U32>> -> Data

def laws_of source · line 211 · raw

@+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.Edit<U32, U32>> -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> @+ht:tgts(dn, dr, es) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/intrusive_doubly_linked_list/adapter.laws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links, U32, U32, Depth, U32, real, i => i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.set_next, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.set_prev, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.set_head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.set_head_nonempty, es, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}})

Every edit program whose targets are in range is carried out exactly.

def rm_tgts source · line 224 · raw

@+dn:Nat -> @+dr:Nat -> @+r:U32 -> @+n:U32 -> @+p:Maybe<&2, U32> -> @+q:Maybe<&2, U32> -> @+hn:bound(dn, n) -> @+hr:bound(dr, r) -> @+bp:inb(dn, p) -> @+bq:inb(dn, q) -> tgts(dn, dr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.remove(U32, U32, r, n, p, q))

def pp_tgts source · line 235 · raw

@+dn:Nat -> @+dr:Nat -> @+r:U32 -> @+n:U32 -> @+h:Maybe<&2, U32> -> @+hn:bound(dn, n) -> @+hr:bound(dr, r) -> @+bh:inb(dn, h) -> tgts(dn, dr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/programs.prepend(U32, U32, r, n, h))

def remove_c source · line 245 · raw

@+r:U32 -> @+n:U32 -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hn:bound(dn, n) -> @+hr:bound(dr, r) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> @+zp:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, n)) -> @+zq:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, n)) -> @+bp:inb(dn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, n)) -> @+bq:inb(dn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, n)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.remove(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), r, n) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.remove(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, r, n)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

def prepend_c source · line 248 · raw

@+r:U32 -> @+n:U32 -> @+ns:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+ps:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+rs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Binding<U32, Maybe<&2, U32>>> -> @+dn:Nat -> @+dr:Nat -> @+hd:{Nat.is_lt(dn, 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr, 32n) == True{} : Bool} -> @+hn:bound(dn, n) -> @+hr:bound(dr, r) -> @+kn:keys_ok(dn, ns) -> @+kp:keys_ok(dn, ps) -> @+kr:keys_ok(dr, rs) -> @+zh:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, r)) -> @+bh:inb(dn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, r)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.prepend(real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}), r, n) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prepend(U32, U32, Depth, ueq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{ns, ps, rs, Depth{dn, dr}}, r, n)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

def remove_refines source · line 255 · raw

@+r:U32 -> @+n:U32 -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<U32, U32, Depth> -> @+hd:{Nat.is_lt(dn_of(g), 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr_of(g), 32n) == True{} : Bool} -> @+hk:gok(g) -> @+hn:bound(dn_of(g), n) -> @+hr:bound(dr_of(g), r) -> @+zp:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(U32, U32, Depth, ueq, g, n)) -> @+zq:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(U32, U32, Depth, ueq, g, n)) -> @+bp:inb(dn_of(g), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prev(U32, U32, Depth, ueq, g, n)) -> @+bq:inb(dn_of(g), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.next(U32, U32, Depth, ueq, g, n)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.remove(real(g), r, n) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.remove(U32, U32, Depth, ueq, g, r, n)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

The exported remove is the model's remove, for every table size.

def prepend_refines source · line 261 · raw

@+r:U32 -> @+n:U32 -> @+g:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph<U32, U32, Depth> -> @+hd:{Nat.is_lt(dn_of(g), 32n) == True{} : Bool} -> @+hdr:{Nat.is_lt(dr_of(g), 32n) == True{} : Bool} -> @+hk:gok(g) -> @+hn:bound(dn_of(g), n) -> @+hr:bound(dr_of(g), r) -> @+zh:nz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(U32, U32, Depth, ueq, g, r)) -> @+bh:inb(dn_of(g), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.head(U32, U32, Depth, ueq, g, r)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.prepend(real(g), r, n) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.prepend(U32, U32, Depth, ueq, g, r, n)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

The exported prepend is the model's prepend, for every table size.

def new_real source · line 267 · raw

@+dn:Nat -> @+dr:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.new(dn, dr) == real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{[], [], [], Depth{dn, dr}}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/intrusive_links.Links}

A fresh table is the empty model graph of its size.

def new_ok source · line 274 · raw

@+dn:Nat -> @+dr:Nat -> gok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/intrusive_doubly_linked_list/model.Graph{[], [], [], Depth{dn, dr}})

The empty graph satisfies every premise about keys.