| dirs[entries2[str0]] = mkdir(m6, md3, # links(entries2[str0], dirs), m9, entries), dirs[entries1[str]] = mkdir(m4, md4, # links(entries1[str], dirs), m7, ∅), dirs[m] = mkdir(m2, md0, # links(m, dirs), m5, entries1), dirs[m0] = mkdir(m1, md, # links(m0, dirs), m3, entries2), afs-cons(dirs, files), str ∈ entries1, str0 ∈ entries2, entries1[str] ∈ dirs, entries2[str0] ∈ dirs, m ∈ dirs, m0 ∈ dirs, m = m0 → md1 = md2, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO, links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO ⊦ ⟪choose err0 with ⌊err0⌋ in err := err0; asynced := ?⟫ true, entries1[str] = ROOT_INO |
dirs[m0] = mkdir(m1, md, # links(m0, dirs), m3, entries2), dirs[m] = mkdir(m2, md0, # links(m, dirs), m5, entries1), dirs[entries1[str]] = mkdir(m4, md4, # links(entries1[str], dirs), m7, ∅), dirs[entries2[str0]] = mkdir(m6, md3, # links(entries2[str0], dirs), m9, entries), afs-cons(dirs, files), m0 ∈ dirs, m ∈ dirs, entries2[str0] ∈ dirs, entries1[str] ∈ dirs, str0 ∈ entries2, str ∈ entries1, ⌊err0⌋ , m = m0 → md1 = md2, links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪err := err0; asynced := ?⟫ true, entries1[str] = ROOT_INO
dirs[m0] = mkdir(m1, md, # links(m0, dirs), m3, entries2), dirs[m] = mkdir(m2, md0, # links(m, dirs), m5, entries1), dirs[entries1[str]] = mkdir(m4, md4, # links(entries1[str], dirs), m7, ∅), dirs[entries2[str0]] = mkdir(m6, md3, # links(entries2[str0], dirs), m9, entries), afs-cons(dirs, files), m0 ∈ dirs, m ∈ dirs, entries2[str0] ∈ dirs, entries1[str] ∈ dirs, str0 ∈ entries2, str ∈ entries1, m = m0 → md1 = md2, links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ entries1[str] = ROOT_INO, ∃ err0. ⌊err0⌋