| (m = m9 ⊃ mkdir(m1, md, # links(m9, dirs0), m2, entries0 -- str);mkdir(m8, md5, # links(m, dirs0), m10, entries3)) = mkdir(m4, md3, m6, m7, entries2), (m9 = m ⊃ mkdir(m4 + 1, md4, m6, m7 + 1, entries2[str0, entries0[str]]);mkdir(m1, md0, # links(m9, dirs0), m2, entries0 -- str)) = mkdir(m0, md1, m11, m12, entries1), (m = m9 ⊃ mkdir(m4 + 1, md0, m6, m7 + 1, entries2[str0, entries0[str]]);mkdir(m4 + 1, md3, m6, m7 + 1, entries2[str0, entries0[str]])) = mkdir(m13, md6, m14, m15, entries4), icache0[m9, mkientry(false, mkinode(m9, md1, true, m11, m12, m0))][ino] = mkientry(true, inode0), icache0[ino] = mkientry(false, inode), dirs0[entries0[str]] = mkdir(m3, md2, # links(entries0[str], dirs0), m5, entries), dirs0[m] = mkdir(m8, md5, # links(m, dirs0), m10, entries3), dirs0[m9] = mkdir(m1 + 1, md, # links(m9, dirs0), m2 + 1, entries0), pcache[datakey(ino, n)] = mkpentry(boolvar, buf), afs-cons(dirs0, files), afs-cons (dirs0 [m9, (m9 = m ⊃ mkdir(m4 + 1, md3, m6, m7 + 1, entries2[str0, entries0[str]]);mkdir(m1, md, # links(m9, dirs0), m2, entries0 -- str)).meta:= md0 ] [m, mkdir(m13, md4, m14, m15, entries4) ], files), synced(dirs0, icache0, pcache), ino ∈ icache0, ino ∈ dirs0, entries0[str] ∈ dirs0, m ∈ dirs0, str ∈ entries0, m9 ∈ dirs0, m = m9 → md4 = md0, asynced2 → synced(files, icache0, pcache), datakey(ino, n) ∈ pcache → ¬ boolvar, ∀ n. datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty, links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO, links(m9, dirs0) ≠ ∅ ∨ m9 = ROOT_INO ⊦ ino = m, str0 ∈ entries3 |
Used simplifier rules: ⊦ ino ≠ ino0 → icache[ino0, ie][ino] = icache[ino]; (s)%⊦ mkientry(boolvar, inode) = mkientry(boolvar0, inode0) ↔ (boolvar ↔ boolvar0) ∧ inode = inode0; (ws)% ⊦ icache[ino, ie][ino] = ie; (s) Used formulas: ino = m9