~/bend-docscommunity

proofs/containers/lru/state.bend checks

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

19 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/hash_table.bend as S
import ../../../spec/containers/lru.bend as SP
import ../../lib/u32div.bend as UD
import ../../../src/math/u64.bend as W
import ../../../src/containers/hash_table.bend as H
import ../../../src/containers/lru.bend as LR
import ../hash_table/table.bend as TB
import ../hash_table/buckets.bend as B
import ../hash_table/cyc.bend as CY
import ../hash_table/inv.bend as IV
import ../hash_table/state.bend as HT
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

Types

type Sh source · line 32 · raw

@-V:Data -> Data

type SP1 source · line 78 · raw

@-V:Data -> Data

Definitions

def off source · line 49 · raw

@+s:Nat -> @+o:Nat -> Nat

word o of slot s in lk

def lw source · line 52 · raw

@+ll:List<&2, U32> -> @+s:Nat -> @+o:Nat -> U32

def seg source · line 57 · raw

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

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

def fll source · line 65 · raw

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

the free list: each slot's next is the slot after it (0 for the last)

def isbf source · line 87 · raw

@b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> @+w:U32 -> @+l:U32 -> Bool

b is a full bucket with word w and link l

def anyb source · line 95 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+l:U32 -> @+w:U32 -> Bool

some bucket below m is full with word w and link l

def bslb source · line 103 · raw

@+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk -> Bool

a full bucket's slot is on the recency list and stores the bucket's word

def bsl source · line 110 · raw

@+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+sl:List<&2, Nat> -> @+ll:List<&2, U32> -> @+m:Nat -> Bool

def skey source · line 121 · raw

@+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+s:Nat -> String

the key of slot s: a one-character key is its check word, any other is its stored String

def w64 source · line 139 · raw

@+ml:List<&2, U32> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64

def ctr source · line 142 · raw

@+ml:List<&2, U32> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ctr

Templates

template real source · line 35 · raw

@-V:Data -> @sh:Sh<V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/lru.LRU<&2, V>

template live source · line 73 · raw

@-V:Data -> @+el:List<&2, Maybe<&2, V>> -> @+s:Nat -> Bool

template sent_m source · line 124 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+s:Nat -> @m:Maybe<&2, V> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>

template es source · line 132 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @+el:List<&2, Maybe<&2, V>> -> @sl:List<&2, Nat> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>

the entries of the slots of sl, in order

template modelF source · line 145 · raw

@-V:Data -> @+cap:U32 -> @+mT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V>

template lru_es source · line 149 · raw

@-V:Data -> @l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Ent<V>>

the entries of a model

template model source · line 155 · raw

@-V:Data -> @sh:Sh<V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/lru.Lru<V>

the cache the shadow stands for

template sev source · line 160 · raw

@-V:Data -> @p:SP1<V> -> @+s:Nat -> Bool

template sall source · line 172 · raw

@-V:Data -> @+p:SP1<V> -> @xs:List<&2, Nat> -> Bool

p holds for every slot of xs

template slok source · line 180 · raw

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

every slot of xs is below fr and live

template flok source · line 184 · raw

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

every slot of xs is below fr and vacant

template hasall source · line 188 · raw

@-V:Data -> @+bs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/buckets.Bk> -> @+m:Nat -> @+ll:List<&2, U32> -> @sl:List<&2, Nat> -> Bool

every slot of sl has a bucket with its link and its stored check word

template nokey source · line 192 · raw

@-V:Data -> @+ll:List<&2, U32> -> @+kl:List<&2, String> -> @sl:List<&2, Nat> -> @+key:String -> Bool

no slot of sl has key

template ck source · line 198 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template csdk source · line 201 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpt source · line 204 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpk source · line 207 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpe source · line 210 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpl source · line 213 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cpm source · line 216 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cmask source · line 219 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cbits source · line 222 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template csize source · line 225 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cdepth source · line 228 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfresh source · line 231 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cwell source · line 234 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cclus source · line 237 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cuniq source · line 240 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cn source · line 243 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cload source · line 246 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template ccap source · line 249 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cbsl source · line 252 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template chas source · line 255 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template csl source · line 258 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cnd source · line 261 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template clen source · line 264 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template chead source · line 267 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template ctail source · line 270 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cdll source · line 273 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template ckeys source · line 276 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfree source · line 279 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfll source · line 282 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfl source · line 285 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfnd source · line 288 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template cfcnt source · line 291 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr30 source · line 294 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr29 source · line 297 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr28 source · line 300 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr27 source · line 303 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr26 source · line 306 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr25 source · line 309 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr24 source · line 312 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr23 source · line 315 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr22 source · line 318 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr21 source · line 321 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr20 source · line 324 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr19 source · line 327 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr18 source · line 330 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr17 source · line 333 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr16 source · line 336 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr15 source · line 339 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr14 source · line 342 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr13 source · line 345 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr12 source · line 348 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr11 source · line 351 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr10 source · line 354 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr9 source · line 357 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr8 source · line 360 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr7 source · line 363 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr6 source · line 366 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr5 source · line 369 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr4 source · line 372 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr3 source · line 375 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr2 source · line 378 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template gr1 source · line 381 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template goodF source · line 384 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> Bool

template good source · line 387 · raw

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

template gp1 source · line 392 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr1(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp2 source · line 395 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr2(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp3 source · line 398 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr3(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp4 source · line 401 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr4(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp5 source · line 404 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr5(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp6 source · line 407 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr6(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp7 source · line 410 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr7(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp8 source · line 413 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr8(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp9 source · line 416 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr9(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp10 source · line 419 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr10(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp11 source · line 422 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr11(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp12 source · line 425 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr12(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp13 source · line 428 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr13(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp14 source · line 431 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr14(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp15 source · line 434 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr15(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp16 source · line 437 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr16(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp17 source · line 440 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr17(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp18 source · line 443 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr18(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp19 source · line 446 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr19(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp20 source · line 449 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr20(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp21 source · line 452 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr21(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp22 source · line 455 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr22(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp23 source · line 458 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr23(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp24 source · line 461 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr24(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp25 source · line 464 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr25(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp26 source · line 467 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr26(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp27 source · line 470 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr27(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp28 source · line 473 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr28(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp29 source · line 476 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr29(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp30 source · line 479 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {gr30(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template gp31 source · line 482 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cfcnt(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_ck source · line 485 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {ck(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_csdk source · line 488 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {csdk(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cpt source · line 491 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cpt(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cpk source · line 494 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cpk(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cpe source · line 497 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cpe(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cpl source · line 500 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cpl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cpm source · line 503 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cpm(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cmask source · line 506 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cmask(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cbits source · line 509 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cbits(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_csize source · line 512 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {csize(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cdepth source · line 515 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cdepth(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cfresh source · line 518 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cfresh(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cwell source · line 521 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cwell(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cclus source · line 524 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cclus(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cuniq source · line 527 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cuniq(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cn source · line 530 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cn(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cload source · line 533 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cload(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_ccap source · line 536 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {ccap(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cbsl source · line 539 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cbsl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_chas source · line 542 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {chas(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_csl source · line 545 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {csl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cnd source · line 548 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cnd(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_clen source · line 551 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {clen(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_chead source · line 554 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {chead(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_ctail source · line 557 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {ctail(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cdll source · line 560 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cdll(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_ckeys source · line 563 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {ckeys(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cfree source · line 566 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cfree(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cfll source · line 569 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cfll(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cfl source · line 572 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cfl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cfnd source · line 575 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cfnd(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template g_cfcnt source · line 578 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+g:{goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {cfcnt(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

template good_intro source · line 582 · raw

@-V:Data -> @+cap:U32 -> @+n:U32 -> @+head:U32 -> @+tail:U32 -> @+free:U32 -> @+fr:U32 -> @+msz:U32 -> @+mdp:U32 -> @+mmk:U32 -> @+mbt:U32 -> @+pm:Bool -> @+k:Nat -> @+sd:Nat -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+eT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+lkT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+h_ck:{ck(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_csdk:{csdk(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cpt:{cpt(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cpk:{cpk(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cpe:{cpe(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cpl:{cpl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cpm:{cpm(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cmask:{cmask(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cbits:{cbits(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_csize:{csize(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cdepth:{cdepth(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cfresh:{cfresh(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cwell:{cwell(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cclus:{cclus(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cuniq:{cuniq(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cn:{cn(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cload:{cload(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_ccap:{ccap(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cbsl:{cbsl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_chas:{chas(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_csl:{csl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cnd:{cnd(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_clen:{clen(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_chead:{chead(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_ctail:{ctail(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cdll:{cdll(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_ckeys:{ckeys(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cfree:{cfree(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cfll:{cfll(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cfl:{cfl(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cfnd:{cfnd(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> @+h_cfcnt:{cfcnt(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool} -> {goodF(V, cap, n, head, tail, free, fr, msz, mdp, mmk, mbt, pm, k, sd, tabT, kl, pk, eT, lkT, sl, fl) == True{} : Bool}

the invariant from its components