| dirs[m] = mkdir(m1, md3, # links(m, dirs), m4, entries), dirs[entries[str]] = mkdir(m0, md2, # links(entries[str], dirs), m2, ∅), c_inode = mkinode(entries[str], md0, true, # links(entries[str], dirs), m2, m0), dent = mkdentry(str, entries[str]), p_inode = mkinode(m, md, true, # links(m, dirs), m4, m1), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m ∈ dirs, str ∈ entries, entries[str] ∈ dirs, asynced1 → synced(files, icache, pcache), links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ [abort] ( afs-cons(dirs, files) → ⟪if err = ESUCCESS then let asynced = false in {icache_set#(c_inode, asynced; err, icache); icache_set#(p_inode, asynced; err, icache); dcache_delete#(p_inode.ino, dent.name; err, dcache)}⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced1 → synced(files, icache, pcache)))), entries[str] = ROOT_INO, pre-rmdir(p_inode, c_inode, dent, dirs, files) |