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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 115:

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

Rule argument

Additional information