| boolvar2 ↔ boolvar3, boolvar1 ↔ new_dent.dentry?, boolvar0 ↔ old_parent_inode.ino ≠ new_parent_inode.ino, boolvar ↔ old_child_inode.directory, ¬ boolvar0, dirs = abs-dirs(fs, ri), err = err0, files = abs-files(fs, ri), new_child_inode = p_inode2, new_dent = old_dent1, new_parent_inode = p_inode0, old_child_inode = p_inode1, old_dent = old_dent0, old_parent_inode = p_inode, orphans(dirs, files) = abs-keys(ro), fo.inodes?, ro.inodes?, afs-cons(dirs, files), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, ro), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files), replay-cons-strong(fs, ri, ro, fi, fo, log), ri-inj(fi), ri-inj(ri), ubifs-cons(fs, ri, ro, fi, fo, log), asynced → boolvar3 ⊦ ⟪if boolvar1 then aubifs_rename_overwrite_keep_parent# (boolvar, old_child_inode, fi, fo; old_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar2) else aubifs_rename_new_keep_parent#(boolvar, old_child_inode, fi, ro, fo; old_parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar2); new_parent_inode := old_parent_inode⟫ ⟨afs_rename#(; p_inode, p_inode0, p_inode1, p_inode2, old_dent0, old_dent1, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar2)) ∧ old_parent_inode = p_inode ∧ new_parent_inode = p_inode0 ∧ old_child_inode = p_inode1 ∧ new_child_inode = p_inode2 ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) |
boolvar ↔ old_child_inode.directory, boolvar0 ↔ old_parent_inode.ino ≠ new_parent_inode.ino, boolvar1 ↔ new_dent.dentry?, boolvar2 ↔ boolvar3, ¬ boolvar0, boolvar1, dirs = abs-dirs(fs, ri), err = err0, files = abs-files(fs, ri), new_child_inode = p_inode2, new_dent = old_dent1, new_parent_inode = p_inode0, old_child_inode = p_inode1, old_dent = old_dent0, old_parent_inode = p_inode, orphans(dirs, files) = abs-keys(ro), ro.inodes?, fo.inodes?, afs-cons(dirs, files), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, ro), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, ro, fi, fo, log), asynced → boolvar3 ⊦ ⟪aubifs_rename_overwrite_keep_parent# (boolvar, old_child_inode, fi, fo; old_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar2); new_parent_inode := old_parent_inode⟫ ⟨afs_rename#(; p_inode, p_inode0, p_inode1, p_inode2, old_dent0, old_dent1, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar2)) ∧ old_parent_inode = p_inode ∧ new_parent_inode = p_inode0 ∧ old_child_inode = p_inode1 ∧ new_child_inode = p_inode2 ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0)
boolvar ↔ old_child_inode.directory, boolvar0 ↔ old_parent_inode.ino ≠ new_parent_inode.ino, boolvar1 ↔ new_dent.dentry?, boolvar2 ↔ boolvar3, ¬ boolvar0, ¬ boolvar1, dirs = abs-dirs(fs, ri), err = err0, files = abs-files(fs, ri), new_child_inode = p_inode2, new_dent = old_dent1, new_parent_inode = p_inode0, old_child_inode = p_inode1, old_dent = old_dent0, old_parent_inode = p_inode, orphans(dirs, files) = abs-keys(ro), ro.inodes?, fo.inodes?, afs-cons(dirs, files), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, ro), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, ro, fi, fo, log), asynced → boolvar3 ⊦ ⟪aubifs_rename_new_keep_parent#(boolvar, old_child_inode, fi, ro, fo; old_parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar2); new_parent_inode := old_parent_inode⟫ ⟨afs_rename#(; p_inode, p_inode0, p_inode1, p_inode2, old_dent0, old_dent1, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar2)) ∧ old_parent_inode = p_inode ∧ new_parent_inode = p_inode0 ∧ old_child_inode = p_inode1 ∧ new_child_inode = p_inode2 ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0)