[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 7 from proof refine-renam (previous step)

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_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)⟫ ⟨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)

User applied rule apply lemma

And obtained the following new goals

Proof step 8:
old_parent_inode.ino ≠ new_parent_inode.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_reparent# (old_child_inode.directory, old_child_inode, fi, fo ; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0)⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0)
Proof step 9:
boolvar2 ↔ boolvar3, boolvar1 ↔ new_dent.dentry?, boolvar0 ↔ old_parent_inode.ino ≠ new_parent_inode.ino, boolvar ↔ old_child_inode.directory, 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), 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 ⊦ ⟪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)⟫ ⟨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), old_parent_inode.ino ≠ new_parent_inode.ino ∧ valid-dentry(new_parent_inode.ino, new_dent, dirs, files) ∧ old_parent_inode = old_parent_inode ∧ new_parent_inode = new_parent_inode ∧ p_inode1 = old_child_inode ∧ p_inode2 = new_child_inode
Proof step 13:
⟪new_parent_inode0 := new_parent_inode, old_parent_inode0 := old_parent_inode; aubifs_rename_overwrite_reparent# (p_inode1.directory, p_inode1, fi, fo; old_parent_inode, new_parent_inode, p_inode2, old_dent, new_dent, err, ri, ro, fs, log, boolvar3)⟫ ⟨afs_rename#(; old_parent_inode0, new_parent_inode0, old_child_inode, new_child_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar3)) ∧ old_parent_inode = old_parent_inode0 ∧ new_parent_inode = new_parent_inode0 ∧ p_inode1 = old_child_inode ∧ p_inode2 = new_child_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0), boolvar2 ↔ boolvar3, boolvar1 ↔ new_dent.dentry?, boolvar0 ↔ old_parent_inode.ino ≠ new_parent_inode.ino, boolvar ↔ old_child_inode.directory, 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), 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 ⊦ ⟪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)⟫ ⟨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)

Rule argument

spec: <toplevel> name: refine-rename-overwrite-reparent seq: old_parent_inode.ino ≠ new_parent_inode.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename (old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_reparent# (old_child_inode.directory, old_child_inode, fi, fo ; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0)⟫ ⟨afs_rename# (; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files ; boolvar)⟩ ( ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) subst: [old_parent_inode, new_parent_inode, new_dent, dirs, files, old_inode, old_dent, old_dent_inode, new_inode, new_dent_inode, fs, ri, ro, boolvar, boolvar0, fi, fo, log, old_child_inode, new_child_inode, old_dent0, old_dent1, err, err0] → [old_parent_inode, new_parent_inode, new_dent, dirs, files, old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_child_inode, fs, ri, ro, asynced, boolvar3, fi, fo, log, p_inode1, p_inode2, old_dent0, old_dent1, err, err0]

Additional information

Used terms: old_parent_inode, new_parent_inode, new_dent, dirs, files, old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_child_inode, fs, ri, ro, asynced, boolvar3, fi, fo, log, p_inode1, p_inode2, old_dent0, old_dent1, err, err0