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

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), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), old_parent_inode.ino ∈ dirs, old_dent.name ∈ dirs[old_parent_inode.ino].entries, new_parent_inode.ino ∈ dirs, asynced → synced(files, icache, pcache), 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 ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files))

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 4:
old_child_inode.ino = m, new_parent_inode.nlink = dirs[new_parent_inode.ino].nlink, old_parent_inode.nlink = dirs[old_parent_inode.ino].nlink, new_parent_inode.nsubdirs = dirs[new_parent_inode.ino].nsubdirs, old_parent_inode.nsubdirs = dirs[old_parent_inode.ino].nsubdirs, new_parent_inode.size = dirs[new_parent_inode.ino].size, old_parent_inode.size = dirs[old_parent_inode.ino].size, m = dirs[old_parent_inode.ino].entries[str], old_dent = mkdentry(str, m), old_dent.dentry?, new_parent_inode.directory, old_parent_inode.directory, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), new_parent_inode.ino ∈ dirs, str ∈ dirs[old_parent_inode.ino].entries, old_parent_inode.ino ∈ dirs, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, asynced → synced(files, icache, pcache), m ∈ dirs ∧ old_child_inode.nlink = dirs[m].nlink ∧ old_child_inode.size = dirs[m].size ∧ old_child_inode.nsubdirs = dirs[m].nsubdirs ∧ old_child_inode.directory ∨ m ∈ files ∧ old_child_inode.nlink = files[m].nlink ∧ old_child_inode.nsubdirs = 0 ∧ ¬ old_child_inode.directory, m ∈ dirs ∨ m ∈ files, links(old_parent_inode.ino, dirs) ≠ ∅ ∨ old_parent_inode.ino = ROOT_INO, (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 ↔ m ∈ files) ∧ (new_dent.ino ∈ dirs → new_dent.ino ≠ ROOT_INO ∧ dirs[new_dent.ino].entries = ∅) ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files, icache, dcache, asynced0)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache)) ∧ afs-cons(dirs, files))

Rule argument

spec: dentry name: elim seq: ⊦ dent.dentry? → (str = dent.name ∧ m = dent.ino ↔ dent = mkdentry(str, m)) subst: [dent, str, m] → [old_dent, str, m]

Additional information

Used simplifier rules: ⊦ dent.dentry? → (str = dent.name ∧ m = dent.ino ↔ dent = mkdentry(str, m)); (elim) Used terms: old_dent, str, m