| # links(m, cache_dirs) = m9, # links(entries[str], cache_dirs) = m8, asynced0 ↔ cache_asynced, cache_files[entries[str]] = mkfile(m5, md1, # links(entries[str], cache_dirs), content), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries[str]] = mkfile(m7, md2, # links(entries[str], cache_dirs), content0), cache_dirs[m] = mkdir(m4, md3, # links(m, cache_dirs), m10, entries), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, c_inode = mkinode(entries[str], md0, false, # links(entries[str], cache_dirs), 0, m6), dcache = cache_dcache, dent = mkdentry(str, entries[str]), dirs = cache_dirs, err = err0, files = cache_files, icache = cache_icache, p_inode = mkinode(m, md, true, # links(m, cache_dirs), m10, m4), 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), entries[str] ∈ cache_files, str ∈ entries, 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, entries[str]); p_inode0 := mkinode(m, md, true, m9, m10, m4); p_inode1 := mkinode(entries[str], md0, false, m8, 0, m6); afs_unlink#(; 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)), pre-unlink(p_inode, c_inode, dent, dirs, files) |