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