| cache_dirs[m3] = mkdir(m6, md4, # links(m3, cache_dirs), 0, entries0), cache_dirs[m] = mkdir(m4, md3, # links(m, cache_dirs), m7, entries2), cache_dirs[entries2[str]] = mkdir(m1, md2, # links(entries2[str], cache_dirs), m5, ∅), cache_dirs[entries0[str0]] = mkdir(m0, md1, # links(entries0[str0], cache_dirs), m2, entries), 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), m3 ∈ cache_dirs, m ∈ cache_dirs, entries2[str] ∈ cache_dirs, str ∈ entries2, str0 ∈ entries0, entries0[str0] ∈ cache_dirs, 1 ≤ m6, ⌊err1⌋ , m = m3 → md = md0, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m3, cache_dirs) ≠ ∅ ∨ m3 = ROOT_INO, links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟨asynced := ?⟩ (err1 = err1 ∧ (asynced ↔ asynced2)), ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ (err1 = err ∧ (asynced ↔ asynced2)), entries2[str] = ROOT_INO, m6 = 0, m3 = m ∧ mkdentry(str, entries2[str]) = mkdentry(str0, entries0[str0]) |