[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification nat-basic

nat-basic/a is used by size-consp, plinks-fids,
nat-basic/c is used by size-consp, plinks-fids,
nat-basic/eq-01 is used by size-consp, plinks-fids,
nat-basic/oz is used by size-consp,
nat-basic/ref is used by size-consp, plinks-fids,
nat-basic/s-04 is used by size-consp, plinks-fids,

Used from specification bag-union

bag-union/fidbag/union is used by plinks-fids,
bag-union/fidbag/count-one is used by plinks-fids,

Used from specification directory-tree-base

directory-tree-base/At-other is used by plinksd+,
directory-tree-base/At-same is used by plinksd+, plinks-fids,
directory-tree-base/In-insert is used by plinksd+, plinks-fids,
directory-tree-base/Size-insert is used by plinks-fids,
directory-tree-base/disj is used by plinksd+, linksd0,
directory-tree-base/fnode-inj is used by links1,

Used from specification store

store/directory-tree-inst/exnotempty is used by plinks-fids,
store/directory-tree-inst/At-in-out is used by plinksd+, plinks-fids,
store/directory-tree-inst/insin is used by plinksd+, plinks-fids,

Used from specification directory-tree

directory-tree/tree-induction is used by plinks-fids,
directory-tree/at-dnode is used by plinksd+,
directory-tree/at-dnode-same is used by plinksd+,
directory-tree/fnode-notin is used by links1,
directory-tree/in-dnode is used by plinksd+, plinks-fids,
directory-tree/in-dnode-empty is used by linksd0,
directory-tree/nil-at is used by plinksd+, linksd0, links1,

Used from specification set-union

set-union/pathset/size-union is used by plinks-fids,
set-union/pathset/unrax is used by plinksd+,
set-union/pathset/Intersect is used by plinks-fids,
set-union/pathset/One is used by plinks-fids, links1,
set-union/pathset/int-a is used by plinks-fids,
set-union/pathset/int-c is used by plinks-fids,

Used from specification bag-basic

bag-basic/fidbag/count-empty is used by plinks-fids,

Used from specification directory-tree-fids

directory-tree-fids/fids-dnode is used by plinks-fids,
directory-tree-fids/fids-emp is used by plinks-fids,
directory-tree-fids/fids-fnode is used by plinks-fids,
directory-tree-fids/fids-ins is used by plinks-fids,

Used from specification set-basic

set-basic/pathset/Extension is used by size-consp, plinksd+, plinks-fids, linksd0, links1, insert-consp, empty-consp,
set-basic/pathset/Size-insert is used by size-consp,
set-basic/pathset/indef is used by size-consp,
set-basic/pathset/In-empty is used by size-consp, plinks-fids, linksd0, empty-consp,
set-basic/pathset/In-insert is used by insert-consp,
set-basic/pathset/Size-empty is used by size-consp, plinks-fids,
set-basic/pathset/eq is used by size-consp,
set-basic/pathset/in-04 is used by links1,
set-basic/pathset/ne is used by links1,
set-basic/pathset/ne-01 is used by links1,
set-basic/pathset/size-one-01 is used by plinks-fids,
set-basic/pathset/size-zero is used by size-consp, plinks-fids, linksd0,
set-basic/pathset/size-zero-01 is used by size-consp, plinks-fids, linksd0,

Used from specification list-data

list-data/path/elim-list-c is used by plinksd+, plinks-fids,

Used from specification list

list/path/a is used by size-consp, plinksd+, plinks-fids, insert-consp,
list/path/c is used by plinksd+, plinks-fids,
list/path/c-07 is used by size-consp, insert-consp,
list/path/c-08 is used by size-consp, insert-consp,
list/path/e-01 is used by size-consp, plinksd+, plinks-fids, insert-consp,
list/path/fr is used by insert-consp,
list/path/in-14 is used by insert-consp,