[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,

Lemma dependency for Specification directory-tree

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
same-inprovedall subs proved one-inf, put-here, one-at, one-ind, same-at, split-put, split-in, nil-put, nil-in,
in-modprovedall subs proved fnode-notin, one-at, one-ind, put-here, nil-at, put-rec, split-in, nil-in, at-dnode, in-dnode, dnode-elim-strong, again-put,
same-atprovedall subs proved one-inf, one-at, one-ind, at-dnode-same, put-here, split-put, split-in, nil-at, nil-put,
again-putprovedall subs proved one-inf, nil-put, nil-at, one-at, one-ind, put-here, split-put, split-at, split-in,
split-delprovedall subs proved one-inf, one-at, del-recin, one-ind, put-here, split-put, split-at, split-in, nil-put, nil-at,
same-putprovedall subs proved one-inf, put-rec, one-at, one-ind, put-here, split-put, split-in, nil-put,
at-putprovedall subs proved fnode-notin, one-at, one-ind, split-at, split-in, split-put, put-rec, at-dnode, in-dnode, nil-in, put-here, nil-put, nil-at, dnode-elim-strong, split-restn, one-restn,
split-putprovedall subs proved one-inf, nil-in, put-here, put-rec, one-at, one-ind, split-at, split-in, nil-put, nil-at,
notin-delprovedall subs proved in-del,
at-modprovedall subs proved fnode-notin, at-dnode-same, one-at, one-ind, put-here, put-rec, split-at, split-in, at-dnode, in-dnode, nil-in, nil-put, nil-at, dnode-elim-strong,
at-delprovedall subs proved one-inf, del-recin, at-dnode, nil-in, del-here, split-at, nil-at, one-at, one-ind, in-del, split-in,
in-delprovedall subs proved one-inf, fnode-notin, del-recin, del-here, in-dnode, nil-in, one-at, one-ind, split-in,
split-atprovedall subs proved one-inf, one-at, at-dnode, one-ind, split-in, nil-at,
same-put-oneprovedall subs proved one-at, dir-elimput,
next-atprovedall subs proved at-dnode-same, dir-elimput,
dnode-oneinprovedall subs proved one-inf, one-ind,
dir-put2provedall subs proved put-fnode, fnode-elim-strong, dnode-elim-strong,
dir-putprovedall subs proved put-fnode, fnode-elim-strong, dnode-elim-strong,
dir-delprovedall subs proved dnode-del, fnode-elim-strong, dnode-elim-strong, notdir-notin,
dir-elimputprovedall subs proved entries, meta, put-here, dnode-elim-strong,
put-fnodeprovedall subs proved fnode-notin, put-here, put-rec, in-dnode, nil-in, nil-put,
notdir-notinprovedall subs proved fnode-notin, fnode-elim-strong, nil-in,
one-infprovedall subs proved fnode-notin,
tree-extprovedall subs proved at-dnode, in-dnode, one-at, one-ind, meta, isdnode, fnode-elim-strong, fid, isfnode, nil-at, nil-in, fnode-notin, tree-induction,
setmeta-elimprovedall subs proved entries, setmeta, dnode-elim-strong,
setfid-elimprovedall subs proved setfid, fnode-elim-strong,
setentries-elimprovedall subs proved meta, setentries, dnode-elim-strong,
in-putprovedall subs proved fnode-notin, one-at, one-ind, put-here, put-rec, split-in, at-dnode, in-dnode, nil-in, nil-put, nil-at, dnode-elim-strong, one-restn,
fnode-elimprovedall subs proved fnode-elim-strong, fid,
dnode-elimprovedall subs proved dnode-elim-strong, entries, meta,
dir-put3provedall subs proved put-here, in-dnode, put-rec, fnode-elim-strong, dnode-elim-strong,
del-fnodeprovedall subs proved dnode-del, dnode-elim-strong,
tree-inductionprovedall subs proved count-rec, count-dnode,
fnode-elim-strongprovedall subs proved isdnode, isfnode,
dnode-delprovedall subs proved del-recnotin, del-here, del-recin,
split-restnprovedall subs proved one-restn,
dnode-elim-strongprovedall subs proved isfnode, isdnode,
at-dnode-sameprovedall subs proved at-dnode,
fnode-notinprovedall subs proved in-fnode, nil-in,
split-inprovedall subs proved in-fnode, at-dnode, in-dnode, nil-at, nil-in,
one-indprovedall subs proved nil-in, in-dnode,
one-atprovedall subs proved nil-at, at-dnode,
in-dnode-emptyprovedall subs proved in-dnode, nil-in,
count-dnodeaxiom
count-recaxiom
setmetaaxiom
setfidaxiom
setentriesaxiom
in-fnodeaxiom
fidaxiom
isdnodeaxiom
isfnodeaxiom
del-recnotinaxiom
metaaxiom
entriesaxiom
one-restnprovedall subs proved
in-dnodeaxiom
put-recaxiom
del-hereaxiom
nil-inaxiom
at-dnodeaxiom
del-recinaxiom
put-hereaxiom
nil-ataxiom
nil-putaxiom