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

(entries0[str] = m5 ⊃ mkdir(m0 - 1, md1, # links(entries0[str], dirs0), m2 - 1, entries0 -- str) ;mkdir(m1, md3, # links(entries0[str], dirs0), m4, ∅) ) = mkdir(m3, md2, m7 + 1, m6, entries), (entries0[str] = m5 ⊃ mkdir(m3, md, m7, m6, entries);mkdir(m3, md2, m7, m6, entries)) = mkdir(m, md4, m8, m9, entries1), (m5 = entries0[str] ⊃ mkdir(m3, md0, m7, m6, entries);mkdir(m0 - 1, md, # links(m5, dirs0), m2 - 1, entries0 -- str)) = mkdir(m10, md5, m11, m12, entries2), dirs0[entries0[str]] = mkdir(m1, md3, # links(entries0[str], dirs0), m4, ∅), dirs0[m5] = mkdir(m0, md1, # links(m5, dirs0), m2, entries0), afs-cons(dirs0, files), afs-cons (dirs0[m5, (m5 = entries0[str] ⊃ mkdir(m3, md2, m7, m6, entries);mkdir(m0 - 1, md1, # links(m5, dirs0), m2 - 1, entries0 -- str)).meta:= md] [entries0[str], mkdir(m, md0, m8, m9, entries1) ], files), dcache-cons(dcache, dirs0, files), synced(dirs0, icache0, pcache), entries0[str] ∈ dirs0, str ∈ entries0, m5 ∈ dirs0, 1 ≤ m2, 1 ≤ m0, asynced1 → synced(files, icache0, pcache), links(m5, dirs0) ≠ ∅ ∨ m5 = ROOT_INO ⊦ entries0[str] = ROOT_INO, m0 = 0, m2 = 0, ∀ key. key ∈ dcache -- dentrykey(m5, str) → key.dentry? ∧ key.name = (dcache -- dentrykey(m5, str))[key].name ∧ valid-dentry (key.ino, (dcache -- dentrykey(m5, str))[key], dirs0 [m5, (m5 = entries0[str] ⊃ mkdir(m3, md2, m7, m6, entries);mkdir(m0 - 1, md1, # links(m5, dirs0), m2 - 1, entries0 -- str)).meta:= md ] [entries0[str], mkdir(m, md0, m8, m9, entries1) ], files)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 168:
(m5 = entries0[str] ⊃ mkdir(m3, md0, m7, m6, entries);mkdir(m0 - 1, md, # links(m5, dirs0), m2 - 1, entries0 -- str)) = mkdir(m10, md5, m11, m12, entries2), (entries0[str] = m5 ⊃ mkdir(m3, md, m7, m6, entries);mkdir(m3, md2, m7, m6, entries)) = mkdir(m, md4, m8, m9, entries1), (entries0[str] = m5 ⊃ mkdir(m0 - 1, md1, # links(entries0[str], dirs0), m2 - 1, entries0 -- str) ;mkdir(m1, md3, # links(entries0[str], dirs0), m4, ∅) ) = mkdir(m3, md2, m7 + 1, m6, entries), dirs0[m5] = mkdir(m0, md1, # links(m5, dirs0), m2, entries0), dirs0[entries0[str]] = mkdir(m1, md3, # links(entries0[str], dirs0), m4, ∅), afs-cons (dirs0[m5, (m5 = entries0[str] ⊃ mkdir(m3, md2, m7, m6, entries);mkdir(m0 - 1, md1, # links(m5, dirs0), m2 - 1, entries0 -- str)).meta:= md] [entries0[str], mkdir(m, md0, m8, m9, entries1) ], files), afs-cons(dirs0, files), dcache-cons(dcache, dirs0, files), synced(dirs0, icache0, pcache), m5 ∈ dirs0, str ∈ entries0, entries0[str] ∈ dirs0, key ∈ dcache, 1 ≤ m0, 1 ≤ m2, asynced1 → synced(files, icache0, pcache), links(m5, dirs0) ≠ ∅ ∨ m5 = ROOT_INO ⊦ entries0[str] = ROOT_INO, key = dentrykey(m5, str), m0 = 0, m2 = 0, key.dentry? ∧ key.name = dcache[key].name ∧ key.ino ∈ dirs0 ∧ ( links (key.ino, dirs0 [m5, (m5 = entries0[str] ⊃ mkdir(m3, md2, m7, m6, entries);mkdir(m0 - 1, md1, # links(m5, dirs0), m2 - 1, entries0 -- str)).meta:= md ] [entries0[str], mkdir(m, md0, m8, m9, entries1) ]) ≠ ∅ ∨ key.ino = ROOT_INO) ∧ (dcache[key].ino ∈ dirs0 ∨ dcache[key].ino ∈ files) ∧ dcache[key].name ∈ (key.ino = entries0[str] ⊃ mkdir(m, md0, m8, m9, entries1) ;(key.ino = m5 ⊃ mkdir(m0 - 1, md, # links(key.ino, dirs0), m2 - 1, entries0 -- str);dirs0[key.ino]) ) .entries ∧ dcache[key].ino = (key.ino = entries0[str] ⊃ mkdir(m, md0, m8, m9, entries1) ;(key.ino = m5 ⊃ mkdir(m0 - 1, md, # links(key.ino, dirs0), m2 - 1, entries0 -- str);dirs0[key.ino]) ) .entries [dcache[key].name ] ∧ dcache[key].dentry?

Rule argument

Additional information

Used simplifier rules: ⊦ mkdir(m, md, m0, m1, entries).meta:= md0 = mkdir(m, md0, m0, m1, entries); (s)% ⊦ dirs[ino, ad][ino0] = (ino0 = ino ∧ ino ∈ dirs ⊃ ad;dirs[ino0]); (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)% ⊦ ino ∈ dirs[ino0, ad] ↔ ino ∈ dirs; (s)%⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO); (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)% ⊦ key ≠ key0 → (dcache -- key0)[key] = dcache[key]; (s)% ⊦ key ∈ dcache -- key0 ↔ key ≠ key0 ∧ key ∈ dcache; (s)