| (m6 = m1 ⊃ mkdir(m0 + 1, md1, # links(m1, dirs0), m4, entries1[str, ino0]);mkdir(m5, md3, # links(m6, dirs0), m7, entries0)) = mkdir(m, md0, m2, m3, entries), dirs0[m6] = mkdir(m5, md3, # links(m6, dirs0), m7, entries0), dirs0[m1] = mkdir(m0, md2, # links(m1, dirs0), m4, entries1), dcache[dentrykey(m6, str0)] = mkdentry(str0, entries0[str0]), afs-cons(dirs0, files0), afs-cons(dirs0[m1, mkdir(m0 + 1, md1, # links(m1, dirs0), m4, entries1[str, ino0])], (files0 ++ ino0)[ino0, mkfile(0, md, 1, ∅)]), synced(dirs0, icache0, pcache), m1 ∈ dirs0, dentrykey(m6, str0) ∈ dcache, m6 ∈ dirs0, str0 ∈ entries0, asynced1 → synced(files0, icache0, pcache), ∀ key0. key0 ∈ dcache → key0.dentry? ∧ key0.name = dcache[key0].name ∧ key0.ino ∈ dirs0 ∧ (links(key0.ino, dirs0) ≠ ∅ ∨ key0.ino = ROOT_INO) ∧ (dcache[key0].ino ∈ dirs0 ∨ dcache[key0].ino ∈ files0) ∧ dcache[key0].name ∈ dirs0[key0.ino].entries ∧ dcache[key0].ino = dirs0[key0.ino].entries[dcache[key0].name] ∧ dcache[key0].dentry?, links(m1, dirs0) ≠ ∅ ∨ m1 = ROOT_INO, links(m6, dirs0) ≠ ∅ ∨ m6 = ROOT_INO, entries0[str0] ∈ dirs0 ∨ entries0[str0] ∈ files0 ⊦ dentrykey(m6, str0) = dentrykey(m1, str), ino0 = 0, ino0 ∈ dirs0, ino0 ∈ files0, str ∈ entries1, (entries0[str0] ∈ dirs0 ∨ entries0[str0] = ino0 ∨ entries0[str0] ∈ files0) ∧ str0 ∈ entries ∧ entries0[str0] = entries[str0] |
Used simplifier rules: ⊦ mkdir(m, md, m0, m1, entries) = mkdir(m2, md0, m3, m4, entries0) ↔ m = m2 ∧ md = md0 ∧ m0 = m3 ∧ m1 = m4 ∧ entries = entries0; (ws)%⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ str ∈ entries ∧ afs-cons(dirs, files) → (entries[str] ∈ files ↔ ¬ entries[str] ∈ dirs); (ss)%⊦ str ∈ entries ∧ ¬ str0 ∈ entries → entries[str0, ino][str] = entries[str]; (s)% ⊦ str ∈ entries[str0, ino] ↔ str = str0 ∨ str ∈ entries; (ws) Used formulas: m6 = m1