| files[m1] = mkfile(m5, md1, m6, content0), files[m] = mkfile(m0, md0, # links(m, dirs), content), icache[m] = mkientry(true, mkinode(m1, md, boolvar, m2, m3, m4)), dirs[m1] = mkdir(m7, md2, m8, m9, entries), err = ESUCCESS, inode = mkinode(m1, md, boolvar, m2, m3, m4), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m ∈ files, m ∈ icache, m1 ∈ dirs ∧ m2 = m8 ∧ m4 = m7 ∧ m3 = m9 ∧ boolvar ∨ m1 ∈ files ∧ m2 = m6 ∧ m3 = 0 ∧ ¬ boolvar ⊦ [abort] ( afs-cons(dirs, files) → ⟪inode := mkinode(m1, md, boolvar, m2, m3, m4); if err = ESUCCESS then {asynced := false; icache_set_status#(m, asynced; err, icache)}⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ inode.ino ∈ files ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory)), pre-write-inode(inode, dirs, files) |