| dirs[m0].entries = ∅, boolvar, c_inode = mkinode(m0, md0, boolvar, m1, m2, m3), dent = mkdentry(str, m0), m0 = dirs[m].entries[str], m1 = dirs[m0].nlink, m2 = dirs[m0].nsubdirs, m3 = dirs[m0].size, p_inode = mkinode(m, md, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size), 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 ∈ dirs[m].entries, m0 ∈ dirs, asynced → synced(files, icache, pcache), links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪cache_rmdir#(; p_inode, c_inode, dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files)), m0 = ROOT_INO |
dirs[dirs[m].entries[str]].entries = ∅, c_inode = mkinode(dirs[m].entries[str], md0, true, dirs[dirs[m].entries[str]].nlink, dirs[dirs[m].entries[str]].nsubdirs, dirs[dirs[m].entries[str]].size), dent = mkdentry(str, dirs[m].entries[str]), p_inode = mkinode(m, md, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size), dirs[m].entries[str] ≠ ROOT_INO, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), dirs[m].entries[str] ∈ dirs, str ∈ dirs[m].entries, m ∈ dirs, asynced → synced(files, icache, pcache), links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪cache_rmdir#(; p_inode, c_inode, dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files))