| dirs[m0] = mkdir(m3, md2, # links(m0, dirs), m6, entries1), files[entries[str]] = mkfile(m2, md, # links(entries[str], dirs), content0), dirs[m] = mkdir(m1, md3, # links(m, dirs), m4, entries), 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, entries[str] ∈ files, m ∈ dirs, str ∈ entries, ⌊err0⌋ , m0 = m → md1 = md0, asynced0 → synced(files, icache, pcache), links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪skip⟫ (icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced0 → synced(files, icache, pcache))), str0 ∈ entries1 |