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

Heuristic conditional left split applied rule if left

And obtained the following new goals

• Proof step 19:

  ⟨err := ESUCCESS; let ino = inode.ino in if ino ∈ dirs then if dirs[ino].nlink = 0 then dirs := dirs -- ino else if files[ino].nlink = 0 then files := files -- ino⟩ (err = 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, inode = mkinode(m, md, boolvar, m0, m1, m2), pre-evict(inode, dirs, files), 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 28:

  ⟨abort⟩ (err = 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, inode = mkinode(m, md, boolvar, m0, m1, m2), m ∈ dirs1, m0 = 0 ∧ m2 = m5 ∧ m1 = m7 ∧ boolvar ∨ m ∈ files1 ∧ m0 = m4 ∧ m1 = 0 ∧ ¬ boolvar ⊦ m = ROOT_INO, pre-evict(inode, dirs, files), ESUCCESS = err0 ∧ dirs1 -- m = dirs0 ∧ files1 = files0

Rule argument

Additional information