| dirs[m0] = mkdir(m6, md6, # links(m0, dirs), m9, entries1), dirs[m] = mkdir(m2, md4, # links(m, dirs), m5, entries), dirs[entries[str]] = mkdir(m1, md3, # links(entries[str], dirs), m3, ∅), dirs[entries1[str0]] = mkdir(m4, md5, # links(entries1[str0], dirs), m7, entries0), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m0 ∈ dirs, m ∈ dirs, entries1[str0] ∈ dirs, entries[str] ∈ dirs, str0 ∈ entries1, str ∈ entries, asynced → synced(files, icache, pcache), m = m0 → md1 = md2, links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ entries[str] = ROOT_INO, str0 ∈ entries1 ∧ (str0 ∈ entries1 ∧ str0 ∈ entries1) ∧ str ∈ entries ∧ str ∈ entries ∧ str ∈ entries |