Proof step 194 from proof inv-write_inode (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 195:

  dcache[key].ino = dirs[m5].entries[dcache[key].name], (m5 = m ⊃ mkdir(m0, md, # links(m, dirs), m2, entries);dirs[m5]) = mkdir(m1, md1, m3, m4, entries0), dirs[m] = mkdir(m0, md0, # links(m, dirs), m2, entries), key = dentrykey(m5, dcache[key].name), key.dentry?, dcache[key].dentry?, afs-cons(dirs, files), afs-cons(dirs[m, mkdir(m0, md, # links(m, dirs), m2, entries)], files), synced(dirs, icache, pcache), m ∈ dirs, key ∈ dcache, m5 ∈ dirs, dcache[key].name ∈ dirs[m5].entries, asynced2 → 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?, links(m5, dirs) ≠ ∅ ∨ m5 = ROOT_INO, dcache[key].ino ∈ dirs ∨ dcache[key].ino ∈ files ⊦ m ∈ icache, dcache[key].name ∈ entries0 ∧ dcache[key].ino = entries0[dcache[key].name]

Rule argument

Additional information