| boolvar2 ↔ boolvar, 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 → boolvar ⊦ ⟪let boolvar1 = new_dent.dentry?, boolvar0 = old_parent_inode.ino ≠ new_parent_inode.ino, boolvar = old_child_inode.directory in if boolvar0 then if boolvar1 then aubifs_rename_overwrite_reparent# (boolvar, old_child_inode, fi, fo ; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar2) else aubifs_rename_new_reparent# (boolvar, old_child_inode, fi, ro, fo; old_parent_inode, new_parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar2) else {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, 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 ⊦ ⟪if boolvar0 then if boolvar1 then aubifs_rename_overwrite_reparent# (boolvar, old_child_inode, fi, fo ; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar2) else aubifs_rename_new_reparent# (boolvar, old_child_inode, fi, ro, fo; old_parent_inode, new_parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar2) else {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)