proofs/containers/doubly_linked_list/state.bend checks

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

13 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/doubly_linked_list.bend as E
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

Types

type Sh source · line 21 · raw

@-T:Data -> Data

LS

@-T:Data -> @tag:U32 -> @cap:U32 -> @fresh:U32 -> @free:U32 -> @head:U32 -> @tail:U32 -> @depth: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> -> @sl:List<&2, Nat> -> @fl:List<&2, Nat> -> Sh<T>

Definitions

def seg source · line 38 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @sl:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> Bool

the segment sl: its first id's prev is p, its last id's next is q, and consecutive ids are linked both ways

def fll source · line 46 · raw

@+nl:List<&2, U32> -> @fl:List<&2, Nat> -> Bool

the free stack: each id's next is the id after it (0 for the last)

def some_b source · line 53 · raw

@-T:Data -> @m:Maybe<&2, T> -> Bool

def live source · line 60 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+x:Nat -> Bool

def gz source · line 80 · raw

@gl:List<&2, U32> -> @+fr:Nat -> Bool

every generation from index fr on is 0 (the ids not issued yet)

Templates

template real source · line 24 · raw

@-T:Data -> @sh:Sh<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>

template model source · line 29 · raw

@-T:Data -> @sh:Sh<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>

template slok source · line 64 · raw

@-T:Data -> @xs:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> Bool

every id of xs is below fr and live

template flok source · line 72 · raw

@-T:Data -> @xs:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> Bool

every id of xs is below fr and vacant

template lvin source · line 90 · raw

@-T:Data -> @vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+sl:List<&2, Nat> -> Bool

every live value slot (index k on) is an id of sl

template cdep source · line 99 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template ccap source · line 102 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpv source · line 105 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpp source · line 108 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpn source · line 111 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpg source · line 114 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfr source · line 117 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cseg source · line 120 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template chead source · line 123 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template ctail source · line 126 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cnd source · line 129 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template csl source · line 132 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfree source · line 135 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfll source · line 138 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfl source · line 141 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfnd source · line 144 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cgz source · line 147 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template clv source · line 150 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr16 source · line 153 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr15 source · line 156 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr14 source · line 159 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr13 source · line 162 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr12 source · line 165 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr11 source · line 168 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr10 source · line 171 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr9 source · line 174 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr8 source · line 177 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr7 source · line 180 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr6 source · line 183 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr5 source · line 186 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr4 source · line 189 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr3 source · line 192 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr2 source · line 195 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr1 source · line 198 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template goodF source · line 201 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template good source · line 204 · raw

@-T:Data -> @sh:Sh<T> -> Bool

template gp1 source · line 209 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr1(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp2 source · line 212 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr2(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp3 source · line 215 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr3(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp4 source · line 218 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr4(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp5 source · line 221 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr5(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp6 source · line 224 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr6(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp7 source · line 227 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr7(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp8 source · line 230 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr8(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp9 source · line 233 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr9(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp10 source · line 236 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr10(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp11 source · line 239 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr11(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp12 source · line 242 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr12(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp13 source · line 245 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr13(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp14 source · line 248 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr14(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp15 source · line 251 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr15(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp16 source · line 254 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {gr16(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template gp17 source · line 257 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {clv(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cdep source · line 260 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cdep(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_ccap source · line 263 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {ccap(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cpv source · line 266 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cpv(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cpp source · line 269 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cpp(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cpn source · line 272 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cpn(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cpg source · line 275 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cpg(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cfr source · line 278 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cfr(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cseg source · line 281 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cseg(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_chead source · line 284 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {chead(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_ctail source · line 287 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {ctail(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cnd source · line 290 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cnd(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_csl source · line 293 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {csl(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cfree source · line 296 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cfree(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cfll source · line 299 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cfll(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cfl source · line 302 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cfl(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cfnd source · line 305 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cfnd(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_cgz source · line 308 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {cgz(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template g_clv source · line 311 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {clv(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

template good_intro source · line 315 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth: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> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+h_cdep:{cdep(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_ccap:{ccap(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cpv:{cpv(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cpp:{cpp(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cpn:{cpn(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cpg:{cpg(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cfr:{cfr(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cseg:{cseg(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_chead:{chead(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_ctail:{ctail(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cnd:{cnd(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_csl:{csl(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cfree:{cfree(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cfll:{cfll(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cfl:{cfl(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cfnd:{cfnd(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_cgz:{cgz(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h_clv:{clv(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}

the invariant from its components