Proof step 94 from proof inv-evict (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  # links(m, dirs) = 0, dcache[key].ino = entries0[dcache[key].name], dirs[m3] = mkdir(m1, md0, # links(m3, dirs), m4, entries0), dirs[m] = mkdir(m0, md, 0, m2, entries), key = dentrykey(m3, dcache[key].name), key.dentry?, dcache[key].dentry?, afs-cons(dirs -- m, files), afs-cons(dirs, files), synced(dirs, icache, pcache), m3 ∈ dirs, key ∈ dcache, m ∈ dirs, dcache[key].name ∈ entries0, asynced1 → synced(files, icache, pcache), ∀ key0. key0 ∈ dcache → key0.dentry? ∧ key0.name = dcache[key0].name ∧ key0.ino ∈ dirs ∧ (links(key0.ino, dirs) ≠ ∅ ∨ key0.ino = ROOT_INO) ∧ (dcache[key0].ino ∈ dirs ∨ dcache[key0].ino ∈ files) ∧ dcache[key0].name ∈ dirs[key0.ino].entries ∧ dcache[key0].ino = dirs[key0.ino].entries[dcache[key0].name] ∧ dcache[key0].dentry?, dcache[key].ino ∈ dirs ∨ dcache[key].ino ∈ files, links(m3, dirs) ≠ ∅ ∨ m3 = ROOT_INO ⊦ m = ROOT_INO, m3 ≠ m ∧ (links(m3, dirs -- m) ≠ ∅ ∨ m3 = ROOT_INO) ∧ (dcache[key].ino ≠ m ∧ dcache[key].ino ∈ dirs ∨ dcache[key].ino ∈ files)

Rule argument

Additional information