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

files[new_dent.ino] = mkfile(m10, md4, m11, content0), files[dirs[m4].entries[str]] = mkfile(m5, md3, m9, content), dirs[m] = mkdir(m12, md5, # links(m, dirs), m14, entries), new_child_inode = mkinode(m0, md0, boolvar, m1, m2, m3), new_parent_inode = mkinode(m, md, true, # links(m, dirs), m14, m12), old_child_inode = mkinode(dirs[m4].entries[str], md2, boolvar0, m6, m7, m8), old_dent = mkdentry(str, dirs[m4].entries[str]), old_parent_inode = mkinode(m4, md1, true, dirs[m4].nlink, dirs[m4].nsubdirs, dirs[m4].size), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m ∈ dirs, str ∈ dirs[m4].entries, m4 ∈ dirs, m = m4 → md = md1, asynced → synced(files, icache, pcache), (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ ¬ new_dent.name ∈ entries ∧ new_dent.negdentry? ∨ (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ (new_dent.ino ∈ dirs ∨ new_dent.ino ∈ files) ∧ new_dent.name ∈ entries ∧ new_dent.ino = 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 = m11 ∧ m2 = 0 ∧ ¬ boolvar) ∧ m0 = new_dent.ino ∧ (new_dent.ino ∈ files ↔ dirs[m4].entries[str] ∈ files) ∧ (new_dent.ino ∈ dirs → new_dent.ino ≠ ROOT_INO ∧ dirs[new_dent.ino].entries = ∅), dirs[m4].entries[str] ∈ dirs ∧ m6 = dirs[dirs[m4].entries[str]].nlink ∧ m8 = dirs[dirs[m4].entries[str]].size ∧ m7 = dirs[dirs[m4].entries[str]].nsubdirs ∧ boolvar0 ∨ dirs[m4].entries[str] ∈ files ∧ m6 = m9 ∧ m7 = 0 ∧ ¬ boolvar0, dirs[m4].entries[str] ∈ dirs ∨ dirs[m4].entries[str] ∈ files, links(m4, dirs) ≠ ∅ ∨ m4 = ROOT_INO ⊦ ⟪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 18:
dirs[m] = mkdir(m12, md5, # links(m, dirs), m14, entries), files[entries0[str]] = mkfile(m5, md3, m9, content), files[new_dent.ino] = mkfile(m10, md4, m11, content0), dirs[m4] = mkdir(m13, md6, m15, m16, entries0), new_child_inode = mkinode(m0, md0, boolvar, m1, m2, m3), new_parent_inode = mkinode(m, md, true, # links(m, dirs), m14, m12), old_child_inode = mkinode(entries0[str], md2, boolvar0, m6, m7, m8), old_dent = mkdentry(str, entries0[str]), old_parent_inode = mkinode(m4, md1, true, m15, m16, m13), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m4 ∈ dirs, str ∈ entries0, m ∈ dirs, asynced → synced(files, icache, pcache), m = m4 → md = md1, links(m4, dirs) ≠ ∅ ∨ m4 = ROOT_INO, entries0[str] ∈ dirs ∨ entries0[str] ∈ files, entries0[str] ∈ dirs ∧ m6 = dirs[entries0[str]].nlink ∧ m8 = dirs[entries0[str]].size ∧ m7 = dirs[entries0[str]].nsubdirs ∧ boolvar0 ∨ entries0[str] ∈ files ∧ m6 = m9 ∧ m7 = 0 ∧ ¬ boolvar0, (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ ¬ new_dent.name ∈ entries ∧ new_dent.negdentry? ∨ (links(m, dirs) ≠ ∅ ∨ m = ROOT_INO) ∧ (new_dent.ino ∈ dirs ∨ new_dent.ino ∈ files) ∧ new_dent.name ∈ entries ∧ new_dent.ino = 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 = m11 ∧ m2 = 0 ∧ ¬ boolvar) ∧ m0 = new_dent.ino ∧ (new_dent.ino ∈ files ↔ entries0[str] ∈ 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: abstract-dir name: elim seq: ⊦ ( ((m = ad.size ∧ md = ad.meta) ∧ m0 = ad.nlink) ∧ m1 = ad.nsubdirs) ∧ entries = ad.entries ↔ ad = mkdir(m, md, m0, m1, entries) subst: [ad, m, md, m0, m1, entries] → [dirs[m4], m13, md6, m15, m16, entries0]

Additional information

Used simplifier rules: ⊦ ( ((m = ad.size ∧ md = ad.meta) ∧ m0 = ad.nlink) ∧ m1 = ad.nsubdirs) ∧ entries = ad.entries ↔ ad = mkdir(m, md, m0, m1, entries); (elim) Used terms: dirs[m4], m13, md6, m15, m16, entries0