Proof step 22 from proof eq-io-evict (previous step)

Heuristic conditional left split applied rule if left

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

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

Rule argument

Additional information