| # links(entries0[str], cache_dirs) = m8, # links(m, cache_dirs) = m5, asynced0 ↔ cache_asynced, cache_dirs[m] = mkdir(m1, md1, # links(m, cache_dirs), m7, entries0), cache_dirs[entries0[str]] = mkdir(m0, md3, # links(entries0[str], cache_dirs), m2, ∅), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, c_inode = mkinode(entries0[str], md0, true, # links(entries0[str], cache_dirs), m2, m0), dcache = cache_dcache, dent = mkdentry(str, entries0[str]), dirs = cache_dirs, err = err0, files = cache_files, icache = cache_icache, p_inode = mkinode(m, md, true, # links(m, cache_dirs), m7, m1), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), entries0[str] ∈ cache_dirs, str ∈ entries0, m ∈ cache_dirs, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ [abort] ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(cache_pcache, dirs, files) ∧ synced(dirs, icache, cache_pcache) ∧ (cache_sync → synced(files, icache, cache_pcache)) ∧ afs-cons(dirs, files) → ⟨dent0 := mkdentry(str, entries0[str]); p_inode0 := mkinode(m, md, true, m5, m7, m1); p_inode1 := mkinode(entries0[str], md0, true, m8, m2, m0); afs_rmdir#(; p_inode0, p_inode1, dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( afs_dirs = dirs ∧ afs_files = (files ⊕ cache_pcache) ⊕ icache ∧ (afs_asynced ↔ asynced0) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err0)), entries0[str] = ROOT_INO, pre-rmdir(p_inode, c_inode, dent, dirs, files) |