Proof step 9 from proof inv-link (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ino = ROOT_INO, p ≠ ε, p3 ≠ ε, afs-cons(dirs, files), of-cons(of, dirs, files) ⊦ ⟪vfs_walk#(parent(p3), user, dirs, files, asynced; ino, err); dent := negdentry(p3.last); if err = ESUCCESS then vfs_may_link#(ino, user, dirs, files, asynced; inode, dent, err); c_inode := inode; old_dent := dent; if err = ESUCCESS then let ino = ROOT_INO, dent = negdentry(p.last), p0 = parent(p) in {vfs_walk#(p0, user, dirs, files, asynced; ino, err); if err = ESUCCESS then vfs_may_create#(ino, dent, user, dirs, files, asynced; inode, err); new_inode := inode, new_dent := dent}; if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced); if err = ESUCCESS then afs_link#(old_dent; new_inode, c_inode, new_dent, err, dirs, files; asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files))

Rule argument

Additional information