Proof step 180 from proof inv-rmdir (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 181:

  (entries[str] = ino1 ⊃ mkdir(m - 1, md1, # links(entries[str], dirs0), m2 - 1, entries -- str) ;mkdir(0, md, # links(entries[str], dirs0), m1, ∅) ) = mkdir(m0, md0, m3, m4, entries0), dirs0[entries[str]] = mkdir(0, md, # links(entries[str], dirs0), m1, ∅), dirs0[ino1] = mkdir(m, md1, # links(ino1, dirs0), m2, entries), dirs = dirs0 [ino1, (ino1 = entries[str] ⊃ mkdir(m0, md0, m3 - 1, m4, entries0);mkdir(m - 1, md1, # links(ino1, dirs0), m2 - 1, entries -- str)).meta:= md1 ] [entries[str], (entries[str] = ino1 ⊃ mkdir(m0, md1, m3 - 1, m4, entries0);mkdir(m0, md0, m3 - 1, m4, entries0)).meta:= md ], err = ESUCCESS, entries[str] ≠ ROOT_INO, m ≠ 0, m2 ≠ 0, m3 ≠ 0, dom of < ino0, afs-cons(dirs0, files), afs-cons (dirs0 [ino1, (ino1 = entries[str] ⊃ mkdir(m0, md0, m3 - 1, m4, entries0);mkdir(m - 1, md1, # links(ino1, dirs0), m2 - 1, entries -- str)).meta:= md1 ] [entries[str], (entries[str] = ino1 ⊃ mkdir(m0, md1, m3 - 1, m4, entries0);mkdir(m0, md0, m3 - 1, m4, entries0)).meta:= md ], files), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pw(user, md1), px(user, md1), px-parent(user, q, ROOT_INO, dirs0, files), ino1 ∈ dirs0, str ∈ entries, entries[str] ∈ dirs0, 1 ≤ m, 1 ≤ m2, 1 ≤ m3, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟪vfs_put_inode#(getinode(entries[str], dirs, files), of, asynced; err, dirs, files)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files))

Rule argument

Additional information