Proof step 1547 from proof inv-renam (previous step)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 1548:

  dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m3, entries0), dom of < ino2, afs-cons(dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md0), px(user, md0), px-parent(user, q0, ROOT_INO, dirs, files), px-parent(user, q, ROOT_INO, dirs, files), str ∈ entries0, ino1 ∈ dirs, entries0[str] ∈ files, ino ∈ dirs ∨ ino ∈ files, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟪choose err0 with ⌊err0⌋ in err := err0; inode := mkinode(ino1, md0, true, # links(ino1, dirs), m3, m0); if err = ESUCCESS then if ¬ inode.directory then err := ENOENT else if ¬ px(user, inode.meta) then err := EACCESS; p_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); dent := negdentry((q0 + str0 ').last); err0 := err; if err0 = ESUCCESS then {afs_lookup#(ino, dirs, files, asynced; dent, err0); if err0 = ENOENT then vfs_may_create#(ino, dent, user, dirs, files, asynced; inode, err0) else if err0 = ESUCCESS then {isdir := false; vfs_may_delete_check#(ino, user, dirs, files, asynced; inode, isdir, dent, p_inode, err0)}}; new_inode := inode; new_dent := dent; new_dent_inode := p_inode; if err0 = ESUCCESS then afs_check_commit#(dirs, files; err0; asynced); if err0 = ESUCCESS then let dent = new_dent in {old_inode := (ino1 ∈ dirs ⊃ mkinode(ino1, md0, true, # links(ino1, dirs), m3, m0) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); old_dent := mkdentry(str, entries0[str]); old_dent_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent, new_dent, err0, dirs, files; asynced); if dent.dentry? then vfs_put_inode#(new_dent_inode, of, asynced; err0, dirs, files)}⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), entries0[str] ∈ dirs, q + str ' ⊑ q0 + str0 '

Rule argument

Additional information

Used simplifier rules: fail#(; ; ERR){choose ERR0 with ⌊ERR0⌋ in ERR := ERR0};