Proof step 151 from proof inv-create (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 152:

  dcache[key].ino = entries0[dcache[key].name], (m6 = m1 ⊃ mkdir(m0 + 1, md1, # links(m1, dirs0), m4, entries1[str, ino0]);mkdir(m5, md3, # links(m6, dirs0), m7, entries0)) = mkdir(m, md0, m2, m3, entries), dirs0[m1] = mkdir(m0, md2, # links(m1, dirs0), m4, entries1), dirs0[m6] = mkdir(m5, md3, # links(m6, dirs0), m7, entries0), key = dentrykey(m6, dcache[key].name), dcache[key].dentry?, key.dentry?, afs-cons(dirs0[m1, mkdir(m0 + 1, md1, # links(m1, dirs0), m4, entries1[str, ino0])], (files0 ++ ino0)[ino0, mkfile(0, md, 1, ∅)]), afs-cons(dirs0, files0), synced(dirs0, icache0, pcache), dcache[key].name ∈ entries0, m6 ∈ dirs0, key ∈ dcache, m1 ∈ dirs0, asynced1 → synced(files0, icache0, pcache), ∀ key0. key0 ∈ dcache → key0.dentry? ∧ key0.name = dcache[key0].name ∧ key0.ino ∈ dirs0 ∧ (links(key0.ino, dirs0) ≠ ∅ ∨ key0.ino = ROOT_INO) ∧ (dcache[key0].ino ∈ dirs0 ∨ dcache[key0].ino ∈ files0) ∧ dcache[key0].name ∈ dirs0[key0.ino].entries ∧ dcache[key0].ino = dirs0[key0.ino].entries[dcache[key0].name] ∧ dcache[key0].dentry?, dcache[key].ino ∈ dirs0 ∨ dcache[key].ino ∈ files0, links(m6, dirs0) ≠ ∅ ∨ m6 = ROOT_INO, links(m1, dirs0) ≠ ∅ ∨ m1 = ROOT_INO ⊦ ino0 = 0, key = dentrykey(m1, str), str ∈ entries1, ino0 ∈ files0, ino0 ∈ dirs0, (dcache[key].ino ∈ dirs0 ∨ dcache[key].ino = ino0 ∨ dcache[key].ino ∈ files0) ∧ dcache[key].name ∈ entries ∧ dcache[key].ino = entries[dcache[key].name]

Rule argument

Additional information