| afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, ¬ boolvar, c_inode = p_inode1, err = err0, m0 = cache_dirs[m].nlink, m1 = cache_dirs[m].nsubdirs, m2 = cache_dirs[m].size, m3 = cache_dirs[ino].entries[str], m4 = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m3].nlink, m5 = 0, new_dent = negdentry(str0), p_inode = mkinode(m, md, true, cache_dirs[m].nlink, cache_dirs[m].nsubdirs, cache_dirs[m].size), p_inode1 = mkinode(m3, md0, boolvar, m4, m5, m6), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), 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), m3 ∈ cache_files, m ∈ cache_dirs, str ∈ cache_dirs[ino].entries, ino ∈ cache_dirs, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m3, cache_dirs) ≠ ∅ ∨ m3 = ROOT_INO, links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO, links(ino, cache_dirs) ≠ ∅ ∨ ino = ROOT_INO ⊦ ⟪cache_link#(mkdentry(str, m3); p_inode, c_inode, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨old_dent0 := negdentry(str0); p_inode0 := mkinode(m, md, true, m0, m1, m2); afs_link#(mkdentry(str, m3); p_inode0, p_inode1, old_dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ new_dent = old_dent0 ∧ err = err0), str0 ∈ cache_dirs[m].entries |
afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, c_inode = mkinode(cache_dirs[ino].entries[str], md0, false, ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[ino].entries[str]].nlink, 0, m6), err = err0, m0 = cache_dirs[m].nlink, m1 = cache_dirs[m].nsubdirs, m2 = cache_dirs[m].size, m3 = cache_dirs[ino].entries[str], m4 = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[ino].entries[str]].nlink, new_dent = negdentry(str0), p_inode = mkinode(m, md, true, cache_dirs[m].nlink, cache_dirs[m].nsubdirs, cache_dirs[m].size), 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), ino ∈ cache_dirs, str ∈ cache_dirs[ino].entries, m ∈ cache_dirs, cache_dirs[ino].entries[str] ∈ cache_files, ¬ str0 ∈ cache_dirs[m].entries, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(ino, cache_dirs) ≠ ∅ ∨ ino = ROOT_INO, links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO, links(cache_dirs[ino].entries[str], cache_dirs) ≠ ∅ ∨ cache_dirs[ino].entries[str] = ROOT_INO ⊦ ⟪cache_link#(mkdentry(str, m3); p_inode, c_inode, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨old_dent0 := negdentry(str0); p_inode0 := mkinode(m, md, true, m0, m1, m2); p_inode1 := mkinode(m3, md0, false, m4, 0, m6); afs_link#(mkdentry(str, m3); p_inode0, p_inode1, old_dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ new_dent = old_dent0 ∧ err = err0)