[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 2 from proof refine-rename-overwrite-reparent-file (previous step)

dirs = abs-dirs(fs, ri), err = err0, files = abs-files(fs, ri), new_child_inode = new_dent_inode, new_dent = old_dent1, new_parent_inode = new_inode, old_child_inode = old_dent_inode, old_dent = old_dent0, old_parent_inode = old_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_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_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), valid-dentry(new_parent_inode.ino, new_dent, dirs, files), boolvar → boolvar0 ⊦ ⟪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), old_parent_inode.ino = new_parent_inode.ino, new_dent_inode.directory

User applied rule apply lemma

And obtained the following new goals

Proof step 3:
⊦ dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ afs-cons(dirs, files) ∧ ro.inodes? ∧ file-node-cons(fs, ri) ∧ log-cons(log, fs) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ ri-inj(ri) ∧ ri-inj(fi) ∧ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ 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)
Proof step 4:
dirs = abs-dirs(fs, ri), err = err0, files = abs-files(fs, ri), new_child_inode = new_dent_inode, new_dent = old_dent1, new_parent_inode = new_inode, old_child_inode = old_dent_inode, old_dent = old_dent0, old_parent_inode = old_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_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), replay-cons-strong(fs, ri, ro, fi, fo, log), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, ro, fi, fo, log), valid-dentry(new_parent_inode.ino, new_dent, dirs, files), boolvar → boolvar0, dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ afs-cons(dirs, files) ∧ ro.inodes? ∧ file-node-cons(fs, ri) ∧ log-cons(log, fs) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ ri-inj(ri) ∧ ri-inj(fi) ∧ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files) → pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, fs, ri, ro) ⊦ ⟪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), old_parent_inode.ino = new_parent_inode.ino, new_dent_inode.directory

Rule argument

spec: <toplevel> name: rename-precond-abs seq: ⊦ dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ afs-cons(dirs, files) ∧ ro.inodes? ∧ file-node-cons(fs, ri) ∧ log-cons(log, fs) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ ri-inj(ri) ∧ ri-inj(fi) ∧ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ 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) subst: [dirs, fs, ri, files, ro, log, fi, fo, old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode] → [dirs, fs, ri, files, ro, log, fi, fo, old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode]

Additional information

Used terms: dirs, fs, ri, files, ro, log, fi, fo, old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode