| entries1[str] = entries2[str], cache_files[entries2[str]] = mkfile(m3, md6, # links(entries2[str], cache_dirs), content1), entries0[str] = entries2[str], cache_dirs[m] = mkdir(m1, md7, # links(m, cache_dirs), m9, entries3), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries2[str]] = mkfile(m5, md1, # links(entries2[str], cache_dirs), content), cache_dirs[ino3] = mkdir(m0, md3, # links(ino3, cache_dirs), m2, entries0), cache_dirs[ino0] = mkdir(m4, md2, # links(ino0, cache_dirs), m10, entries), entries[str] = entries2[str], cache_dirs[ino1] = mkdir(m7, md5, # links(ino1, cache_dirs), m11, entries1), cache_dirs[ino2] = mkdir(m8, md4, # links(ino2, cache_dirs), m13, entries2), 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), str ∈ entries2, ino2 ∈ cache_dirs, str ∈ entries, ino0 ∈ cache_dirs, ino3 ∈ cache_dirs, m ∈ cache_dirs, entries2[str] ∈ cache_files, ino1 ∈ cache_dirs, str ∈ entries1, str ∈ entries0, ⌊err1⌋ , cache_sync → synced(cache_files, cache_icache, cache_pcache), links(ino2, cache_dirs) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino0, cache_dirs) ≠ ∅ ∨ ino0 = ROOT_INO, links(ino3, cache_dirs) ≠ ∅ ∨ ino3 = ROOT_INO, links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO, links(ino1, cache_dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨asynced := ?⟩ ((asynced ↔ asynced0) ∧ err1 = err1), str0 ∈ entries3 |