| dcache0[key].ino = entries1[str], (m8 = m3 ⊃ mkdir(m1, md2, # links(m8, dirs0), m4, entries);mkdir(m7, md4, # links(m8, dirs0), m9, entries1)) = mkdir(m2, md, m5, m6, entries0), dirs0[m8] = mkdir(m7, md4, # links(m8, dirs0), m9, entries1), files[entries[str0]] = mkfile(m0, md0, # links(entries[str0], dirs0), content), dirs0[m3] = mkdir(m1, md1, # links(m3, dirs0), m4, entries), key = dentrykey(m8, str), str = dcache0[key].name, key.dentry?, dcache0[key].dentry?, afs-cons (dirs0[m3, mkdir(m1, md2, # links(m3, dirs0), m4, entries)], files[entries[str0], mkfile(m, md3, # links(entries[str0], dirs0), content)]), afs-cons(dirs0, files), synced(dirs0, icache0, pcache), entries[str0] ∈ files, str0 ∈ entries, m3 ∈ dirs0, key ∈ dcache0, m8 ∈ dirs0, str ∈ entries1, asynced2 → synced(files, icache0, pcache), ∀ key0. key0 ∈ dcache0 → key0.dentry? ∧ key0.name = dcache0[key0].name ∧ key0.ino ∈ dirs0 ∧ (links(key0.ino, dirs0) ≠ ∅ ∨ key0.ino = ROOT_INO) ∧ (dcache0[key0].ino ∈ dirs0 ∨ dcache0[key0].ino ∈ files) ∧ dcache0[key0].name ∈ dirs0[key0.ino].entries ∧ dcache0[key0].ino = dirs0[key0.ino].entries[dcache0[key0].name] ∧ dcache0[key0].dentry?, links(m3, dirs0) ≠ ∅ ∨ m3 = ROOT_INO, links(m8, dirs0) ≠ ∅ ∨ m8 = ROOT_INO, entries1[str] ∈ dirs0 ∨ entries1[str] ∈ files ⊦ key = dentrykey(m3, str0), entries[str0] ∈ dirs0, str ∈ entries0 ∧ entries1[str] = entries0[str] |
dcache0[key].ino = entries1[dcache0[key].name], (m8 = m3 ⊃ mkdir(m1, md2, # links(m3, dirs0), m4, entries);mkdir(m7, md4, # links(m8, dirs0), m9, entries1)) = mkdir(m2, md, m5, m6, entries0), dirs0[m3] = mkdir(m1, md1, # links(m3, dirs0), m4, entries), files[entries[str0]] = mkfile(m0, md0, # links(entries[str0], dirs0), content), dirs0[m8] = mkdir(m7, md4, # links(m8, dirs0), m9, entries1), key = dentrykey(m8, dcache0[key].name), dcache0[key].dentry?, key.dentry?, afs-cons(dirs0, files), afs-cons (dirs0[m3, mkdir(m1, md2, # links(m3, dirs0), m4, entries)], files[entries[str0], mkfile(m, md3, # links(entries[str0], dirs0), content)]), synced(dirs0, icache0, pcache), dcache0[key].name ∈ entries1, m8 ∈ dirs0, key ∈ dcache0, m3 ∈ dirs0, str0 ∈ entries, entries[str0] ∈ files, asynced2 → synced(files, icache0, pcache), ∀ key0. key0 ∈ dcache0 → key0.dentry? ∧ key0.name = dcache0[key0].name ∧ key0.ino ∈ dirs0 ∧ (links(key0.ino, dirs0) ≠ ∅ ∨ key0.ino = ROOT_INO) ∧ (dcache0[key0].ino ∈ dirs0 ∨ dcache0[key0].ino ∈ files) ∧ dcache0[key0].name ∈ dirs0[key0.ino].entries ∧ dcache0[key0].ino = dirs0[key0.ino].entries[dcache0[key0].name] ∧ dcache0[key0].dentry?, dcache0[key].ino ∈ dirs0 ∨ dcache0[key].ino ∈ files, links(m8, dirs0) ≠ ∅ ∨ m8 = ROOT_INO, links(m3, dirs0) ≠ ∅ ∨ m3 = ROOT_INO ⊦ key = dentrykey(m3, str0), entries[str0] ∈ dirs0, dcache0[key].name ∈ entries0 ∧ dcache0[key].ino = entries0[dcache0[key].name]