Specification directory-tree

[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,
enrich
   directory-tree-inst
, 
   path
, 
   fidset
with
   

   
   
   functions  . [ . ] : directory-tree × path → directory-tree;
              . [ . ] : directory-tree × path × directory-tree → directory-tree;
              . -- . : directory-tree × path → directory-tree prio 9 left;
              . .fid : directory-tree → fid;
              . .meta : directory-tree → metadata;
              . .entries : directory-tree → entries-tree;
              . .subdirs : directory-tree → stringset;
              . .fid:= . : directory-tree × fid → directory-tree prio 12 left;
              . .meta:= . : directory-tree × metadata → directory-tree prio 12 left;
              . .entries:= . : directory-tree × entries-tree → directory-tree prio 12 left;
              #n . : directory-tree → nat;
              #n . : entries-tree → nat;
   predicates  . ∈ . : path × directory-tree;
               . .dir? : directory-tree;
   
   variables  Ptree : directory-tree → bool;
   
   

   

   axioms count-fnode :  ⊦ #n fnode(fid) = 1;
          used for: s, ls;
          count-dnode :  ⊦ #n dnode(md, sdt) = 1 + #n sdt;
          used for: s, ls;
          count-empty :  ⊦ #n ∅ = 0;
          used for: s, ls;
          count-rec :  ⊦ ¬ str ∈ sdt → #n sdt[str, tree] = #n sdt + #n tree;
          used for: s, ls;
          nil-in :  ⊦ ε ∈ tree;
          used for: s, ls;
          in-fnode :  ⊦ ¬ str ' + p ∈ fnode(fid);
          used for: s, ls;
          in-dnode :  ⊦ str ' + p ∈ dnode(md, sdt) ↔ str ∈ sdt ∧ p ∈ sdt[str];
          used for: s, ls;
          nil-at :  ⊦ tree[ε] = tree;
          used for: s, ls;
          at-dnode :  ⊦ str ∈ sdt → dnode(md, sdt)[str ' + p] = sdt[str][p];
          used for: s, ls;
          nil-put :  ⊦ tree[ε, tree0] = tree0;
          used for: s, ls;
          put-here :  ⊦ dnode(md, sdt)[str ', tree0] = dnode(md, sdt[str, tree0]);
          used for: s, ls;
          put-rec : p ≠ ε ⊦ str ∈ sdt → dnode(md, sdt)[str ' + p, tree0] = dnode(md, sdt[str, sdt[str][p, tree0]]);
          used for: s, ls;
          del-here :  ⊦ dnode(md, sdt) -- str ' = dnode(md, sdt -- str);
          used for: s, ls;
          del-recin : p ≠ ε ⊦ str ∈ sdt → dnode(md, sdt) -- (str ' + p) = dnode(md, sdt[str, sdt[str] -- p]);
          used for: s, ls;
          del-recnotin : p ≠ ε ⊦ ¬ str ∈ sdt → dnode(md, sdt) -- (str ' + p) = dnode(md, sdt);
          used for: s, ls;
          fid :  ⊦ fnode(fid).fid = fid;
          used for: s, ls;
          meta :  ⊦ dnode(md, sdt).meta = md;
          used for: s, ls;
          entries :  ⊦ dnode(md, sdt).entries = sdt;
          used for: s, ls;
          subdirs :  ⊦ str ∈ dnode(md, sdt).subdirs ↔ str ∈ sdt ∧ sdt[str].dir?;
          used for: s, ls;
          isfnode :  ⊦ ¬ fnode(fid).dir?;
          used for: s, ls;
          isdnode :  ⊦ dnode(md, sdt).dir?;
          used for: s, ls;
          setfid :  ⊦ fnode(fid).fid:= fid0 = fnode(fid0);
          used for: s, ls;
          setmeta :  ⊦ dnode(md, sdt).meta:= md0 = dnode(md0, sdt);
          used for: s, ls;
          setentries :  ⊦ dnode(md, sdt).entries:= sdt0 = dnode(md, sdt0);
          used for: s, ls;

   

   
end enrich