[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 8 from proof inv-renam (previous step)

old_child_inode.ino = dirs[old_parent_inode.ino].entries[str], old_parent_inode.nlink = dirs[old_parent_inode.ino].nlink, old_parent_inode.nsubdirs = dirs[old_parent_inode.ino].nsubdirs, old_parent_inode.size = dirs[old_parent_inode.ino].size, new_child_inode = mkinode(m0, md0, boolvar, m1, m2, m3), new_parent_inode = mkinode(m, md, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size), old_dent = mkdentry(str, old_child_inode.ino), old_parent_inode.directory, afs-cons(dirs, files), old_parent_inode.ino ∈ dirs, str ∈ dirs[old_parent_inode.ino].entries, m ∈ dirs, m = old_parent_inode.ino → md = old_parent_inode.meta, links(old_parent_inode.ino, dirs) ≠ ∅ ∨ old_parent_inode.ino = ROOT_INO, old_child_inode.ino ∈ dirs ∨ old_child_inode.ino ∈ files, old_child_inode.ino ∈ dirs ∧ old_child_inode.nlink = dirs[old_child_inode.ino].nlink ∧ old_child_inode.size = dirs[old_child_inode.ino].size ∧ old_child_inode.nsubdirs = dirs[old_child_inode.ino].nsubdirs ∧ old_child_inode.directory ∨ old_child_inode.ino ∈ files ∧ old_child_inode.nlink = files[old_child_inode.ino].nlink ∧ old_child_inode.nsubdirs = 0 ∧ ¬ old_child_inode.directory, (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ ¬ new_dent.name ∈ dirs[m].entries ∧ new_dent.negdentry? ∨ (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ (new_dent.ino ∈ dirs ∨ new_dent.ino ∈ files) ∧ new_dent.name ∈ dirs[m].entries ∧ new_dent.ino = dirs[m].entries[new_dent.name] ∧ new_dent.dentry? ∧ ( new_dent.ino ∈ dirs ∧ m1 = dirs[new_dent.ino].nlink ∧ m3 = dirs[new_dent.ino].size ∧ m2 = dirs[new_dent.ino].nsubdirs ∧ boolvar ∨ new_dent.ino ∈ files ∧ m1 = files[new_dent.ino].nlink ∧ m2 = 0 ∧ ¬ boolvar) ∧ m0 = new_dent.ino ∧ (new_dent.ino ∈ files ↔ old_child_inode.ino ∈ files) ∧ (new_dent.ino ∈ dirs → new_dent.ino ≠ ROOT_INO ∧ dirs[new_dent.ino].entries = ∅) ⊦ ⟪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 elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 9:
old_child_inode.ino = dirs[m4].entries[str], boolvar0, m5 = dirs[m4].nlink, m6 = dirs[m4].nsubdirs, m7 = dirs[m4].size, new_child_inode = mkinode(m0, md0, boolvar, m1, m2, m3), new_parent_inode = mkinode(m, md, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size), old_dent = mkdentry(str, old_child_inode.ino), old_parent_inode = mkinode(m4, md1, boolvar0, m5, m6, m7), afs-cons(dirs, files), m ∈ dirs, str ∈ dirs[m4].entries, m4 ∈ dirs, m = m4 → md = md1, (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ ¬ new_dent.name ∈ dirs[m].entries ∧ new_dent.negdentry? ∨ (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ (new_dent.ino ∈ dirs ∨ new_dent.ino ∈ files) ∧ new_dent.name ∈ dirs[m].entries ∧ new_dent.ino = dirs[m].entries[new_dent.name] ∧ new_dent.dentry? ∧ ( new_dent.ino ∈ dirs ∧ m1 = dirs[new_dent.ino].nlink ∧ m3 = dirs[new_dent.ino].size ∧ m2 = dirs[new_dent.ino].nsubdirs ∧ boolvar ∨ new_dent.ino ∈ files ∧ m1 = files[new_dent.ino].nlink ∧ m2 = 0 ∧ ¬ boolvar) ∧ m0 = new_dent.ino ∧ (new_dent.ino ∈ files ↔ old_child_inode.ino ∈ files) ∧ (new_dent.ino ∈ dirs → new_dent.ino ≠ ROOT_INO ∧ dirs[new_dent.ino].entries = ∅), old_child_inode.ino ∈ dirs ∧ old_child_inode.nlink = dirs[old_child_inode.ino].nlink ∧ old_child_inode.size = dirs[old_child_inode.ino].size ∧ old_child_inode.nsubdirs = dirs[old_child_inode.ino].nsubdirs ∧ old_child_inode.directory ∨ old_child_inode.ino ∈ files ∧ old_child_inode.nlink = files[old_child_inode.ino].nlink ∧ old_child_inode.nsubdirs = 0 ∧ ¬ old_child_inode.directory, old_child_inode.ino ∈ dirs ∨ old_child_inode.ino ∈ files, links(m4, dirs) ≠ ∅ ∨ m4 = ROOT_INO ⊦ ⟪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

spec: inode name: elim seq: ⊦ ( ( ( (m = inode.ino ∧ md = inode.meta) ∧ (boolvar ↔ inode.directory)) ∧ m0 = inode.nlink) ∧ m1 = inode.nsubdirs) ∧ m2 = inode.size ↔ inode = mkinode(m, md, boolvar, m0, m1, m2) subst: [inode, m, md, boolvar, m0, m1, m2] → [old_parent_inode, m4, md1, boolvar0, m5, m6, m7]

Additional information

Used simplifier rules: ⊦ ( ( ( (m = inode.ino ∧ md = inode.meta) ∧ (boolvar ↔ inode.directory)) ∧ m0 = inode.nlink) ∧ m1 = inode.nsubdirs) ∧ m2 = inode.size ↔ inode = mkinode(m, md, boolvar, m0, m1, m2); (elim) Used terms: old_parent_inode, m4, md1, boolvar0, m5, m6, m7