~/bend-docscommunity

proofs/containers/doubly_linked_list/insg.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/insg.bend as Insg

15 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ./state.bend as ST
import ./links.bend as LK
import ./rel.bend as RL
import ./vals.bend as VA
import ./lv.bend as LV
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LKx
import ../../lib/u32_tree.bend as UT

Definitions

def off_l source · line 22 · raw

@+nn:Nat -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, a) == False{} : Bool}

nn off a ++ b is off a and off b

def off_r source · line 25 · raw

@+nn:Nat -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, b) == False{} : Bool}

def len_is source · line 28 · raw

@-X:Data -> @+xs:List<&2, X> -> @+m:Nat -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(X, xs) == m : Nat} -> @+i:Nat -> @+h:{Nat.is_lt(i, m) == True{} : Bool} -> {Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(X, xs)) == True{} : Bool}

def fst_len source · line 31 · raw

@+b:List<&2, Nat> -> @+xs:List<&2, U32> -> @+m:Nat -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) == m : Nat} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.fstlt(b, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool}

def last_len source · line 34 · raw

@+a:List<&2, Nat> -> @+xs:List<&2, U32> -> @+m:Nat -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) == m : Nat} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.lastlt(a, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool}

Templates

template ig_seg source · line 39 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fr:U32 -> @+free:U32 -> @+d:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+nn:Nat -> @+x:T -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hcap:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+pp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, pT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, nT) == True{} : Bool} -> @+pg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, gT) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap)) == True{} : Bool} -> @+hnf:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool} -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfree:{U32.is_eq(free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(fl, 0)) == True{} : Bool} -> @+hfll:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), fl) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, fl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(fl) == True{} : Bool} -> @+hnfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, fl) == False{} : Bool} -> @+hgz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hlv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, pT, nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)), b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(nn))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, nT, nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)), a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(nn))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, nn <> b), 0, 0) == True{} : Bool}

the links of the new lists, from the list-level theorem

template ig_fll source · line 58 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fr:U32 -> @+free:U32 -> @+d:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+nn:Nat -> @+x:T -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hcap:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+pp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, pT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, nT) == True{} : Bool} -> @+pg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, gT) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap)) == True{} : Bool} -> @+hnf:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool} -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfree:{U32.is_eq(free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(fl, 0)) == True{} : Bool} -> @+hfll:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), fl) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, fl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(fl) == True{} : Bool} -> @+hnfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, fl) == False{} : Bool} -> @+hgz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hlv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, nT, nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)), a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(nn))), fl) == True{} : Bool}

the free stack is off the writes

template ig_sl source · line 71 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fr:U32 -> @+free:U32 -> @+d:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+nn:Nat -> @+x:T -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hcap:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+pp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, pT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, nT) == True{} : Bool} -> @+pg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, gT) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap)) == True{} : Bool} -> @+hnf:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool} -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfree:{U32.is_eq(free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(fl, 0)) == True{} : Bool} -> @+hfll:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), fl) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, fl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(fl) == True{} : Bool} -> @+hnfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, fl) == False{} : Bool} -> @+hgz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hlv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, nn <> b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), nn, Some{x})) == True{} : Bool}

the value facts over the written value list

template ig_lv source · line 82 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fr:U32 -> @+free:U32 -> @+d:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+nn:Nat -> @+x:T -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hcap:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+pp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, pT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, nT) == True{} : Bool} -> @+pg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, gT) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap)) == True{} : Bool} -> @+hnf:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool} -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfree:{U32.is_eq(free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(fl, 0)) == True{} : Bool} -> @+hfll:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), fl) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, fl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(fl) == True{} : Bool} -> @+hnfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, fl) == False{} : Bool} -> @+hgz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hlv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), nn, Some{x}), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, nn <> b)) == True{} : Bool}

template ins_good source · line 87 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fr:U32 -> @+free:U32 -> @+d:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+nn:Nat -> @+x:T -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hcap:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+pp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, pT) == True{} : Bool} -> @+pn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, nT) == True{} : Bool} -> @+pg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, gT) == True{} : Bool} -> @+hfr:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(cap)) == True{} : Bool} -> @+hnf:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+hns:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool} -> @+hsl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfree:{U32.is_eq(free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(fl, 0)) == True{} : Bool} -> @+hfll:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), fl) == True{} : Bool} -> @+hfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, fl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> @+hfnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(fl) == True{} : Bool} -> @+hnfl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(nn, fl) == False{} : Bool} -> @+hgz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fr)) == True{} : Bool} -> @+hlv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fr, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, nn <> b), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, nn <> b), 0), d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, vT, nn, Some{x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, pT, nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)), b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(nn)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, nT, nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)), a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(nn)), gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, nn <> b), fl) == True{} : Bool}

THEOREM: the linked state keeps the invariant