[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 1 from proof inv-renam (conclusion)

afs-cons(dirs, files), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files) ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 2:
old_dent.ino = dirs[old_parent_inode.ino].entries[old_dent.name], old_child_inode.ino = old_dent.ino, old_parent_inode.nlink = dirs[old_parent_inode.ino].nlink, new_parent_inode.nlink = dirs[new_parent_inode.ino].nlink, old_parent_inode.nsubdirs = dirs[old_parent_inode.ino].nsubdirs, new_parent_inode.nsubdirs = dirs[new_parent_inode.ino].nsubdirs, old_parent_inode.size = dirs[old_parent_inode.ino].size, new_parent_inode.size = dirs[new_parent_inode.ino].size, old_dent.dentry?, old_parent_inode.directory, new_parent_inode.directory, afs-cons(dirs, files), old_parent_inode.ino ∈ dirs, old_dent.name ∈ dirs[old_parent_inode.ino].entries, new_parent_inode.ino ∈ dirs, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, (links(new_parent_inode.ino, dirs) ≠ ∅ ∨ new_parent_inode.ino = ROOT_INO) ∧ ¬ new_dent.name ∈ dirs[new_parent_inode.ino].entries ∧ new_dent.negdentry? ∨ (links(new_parent_inode.ino, dirs) ≠ ∅ ∨ new_parent_inode.ino = ROOT_INO) ∧ (new_dent.ino ∈ dirs ∨ new_dent.ino ∈ files) ∧ new_dent.name ∈ dirs[new_parent_inode.ino].entries ∧ new_dent.ino = dirs[new_parent_inode.ino].entries[new_dent.name] ∧ new_dent.dentry? ∧ ( new_child_inode.ino ∈ dirs ∧ new_child_inode.nlink = dirs[new_child_inode.ino].nlink ∧ new_child_inode.size = dirs[new_child_inode.ino].size ∧ new_child_inode.nsubdirs = dirs[new_child_inode.ino].nsubdirs ∧ new_child_inode.directory ∨ new_child_inode.ino ∈ files ∧ new_child_inode.nlink = files[new_child_inode.ino].nlink ∧ new_child_inode.nsubdirs = 0 ∧ ¬ new_child_inode.directory) ∧ new_child_inode.ino = new_dent.ino ∧ (new_dent.ino ∈ files ↔ old_dent.ino ∈ files) ∧ (new_dent.ino ∈ dirs → new_dent.ino ≠ ROOT_INO ∧ dirs[new_dent.ino].entries = ∅), links(old_parent_inode.ino, dirs) ≠ ∅ ∨ old_parent_inode.ino = ROOT_INO, old_dent.ino ∈ dirs ∨ old_dent.ino ∈ files, old_dent.ino ∈ dirs ∧ old_child_inode.nlink = dirs[old_dent.ino].nlink ∧ old_child_inode.size = dirs[old_dent.ino].size ∧ old_child_inode.nsubdirs = dirs[old_dent.ino].nsubdirs ∧ old_child_inode.directory ∨ old_dent.ino ∈ files ∧ old_child_inode.nlink = files[old_dent.ino].nlink ∧ old_child_inode.nsubdirs = 0 ∧ ¬ old_child_inode.directory ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files)

Rule argument

Additional information

Used simplifier rules: ⊦ dir-empty(ino, dirs, files) ↔ dirs[ino].entries = ∅; (s)% ⊦ valid-file-ino(ino, dirs, files) ↔ ino ∈ files; (s)%⊦ valid-file-inode(inode, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory; (s)% ⊦ valid-dir-ino(ino, dirs, files) ↔ ino ∈ dirs; (s)%⊦ valid-dir-inode(inode, dirs, files) ↔ valid-dir-ino(inode.ino, dirs, files) ∧ inode.nlink = dirs[inode.ino].nlink ∧ inode.size = dirs[inode.ino].size ∧ inode.nsubdirs = dirs[inode.ino].nsubdirs ∧ inode.directory; (s)%⊦ valid-wb-inode(inode, dirs, files) ↔ valid-dir-inode(inode, dirs, files) ∨ valid-file-inode(inode, dirs, files); (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)%⊦ valid-dentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ valid-ino(dent.ino, dirs, files) ∧ dent.name ∈ dirs[ino].entries ∧ dent.ino = dirs[ino].entries[dent.name] ∧ dent.dentry?; (s)%⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO); (s)%⊦ valid-negdentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ ¬ dent.name ∈ dirs[ino].entries ∧ dent.negdentry?; (s)%⊦ pre-rename (old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files) ↔ ( valid-negdentry(new_parent_inode.ino, new_dent, dirs, files) ∨ valid-dentry(new_parent_inode.ino, new_dent, dirs, files) ∧ valid-wb-inode(new_child_inode, dirs, files) ∧ new_child_inode.ino = new_dent.ino ∧ ( valid-file-ino(new_dent.ino, dirs, files) ↔ valid-file-ino(old_dent.ino, dirs, files)) ∧ ( valid-dir-ino(new_dent.ino, dirs, files) → new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, dirs, files))) ∧ valid-dentry(old_parent_inode.ino, old_dent, dirs, files) ∧ valid-dir-inode(old_parent_inode, dirs, files) ∧ valid-dir-inode(new_parent_inode, dirs, files) ∧ ( new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta) ∧ valid-wb-inode(old_child_inode, dirs, files) ∧ old_child_inode.ino = old_dent.ino; (s)