| ⟨abort⟩ (err = err0 ∧ dirs = dirs0 ∧ files = files0), asynced ↔ asynced0, files1[m] = mkfile(m3, md0, m4, content), dirs1[m] = mkdir(m5, md1, m6, m7, entries), dirs = dirs1, files = files1, inode = mkinode(m, md, boolvar, m0, m1, m2) ⊦ pre-evict(inode, dirs, files), (m ∈ dirs1 ∧ m0 = m6 ∧ m2 = m5 ∧ m1 = m7 ∧ boolvar ∨ m ∈ files1 ∧ m0 = m4 ∧ m1 = 0 ∧ ¬ boolvar) ∧ m ≠ ROOT_INO |