| # links(entries2[str], dirs0) = 1, dirs0[m] = mkdir(m8 + 1, md0, # links(m, dirs0), m11 + 1, entries2), dirs0[entries2[str]] = mkdir(0, md6, 1, # subdirs(entries2[str], dirs0), ∅), dirs0[entries2[str0]] = mkdir(m4, md3, # links(entries2[str0], dirs0), m7, entries1), files[entries2[str]] = mkfile(m14, md8, m16, content), afs-cons(dirs0, files), ROOT_INO ∈ dirs0, str0 ∈ entries2, entries2[str0] ∈ dirs0, str ∈ entries2, m ∈ dirs0, entries2[str] ∈ dirs0, links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO ⊦ 0 = #(links(entries2[str], dirs0) -- mklink(m, str)), entries2[str] = ROOT_INO, entries2[str] = m, links(entries2[str], dirs0) = ∅ ++ mklink(m, str), mkdentry(str, entries2[str]) = mkdentry(str0, entries2[str0]) |
Used simplifier rules: lastlink-move: ⊦ # links(entries0[str0], dirs) = 1 ∧ ino0 ∈ dirs ∧ dirs[ino0] = mkdir(m0, md0, n0, n2, entries0) ∧ ino1 ∈ dirs ∧ dirs[ino1] = mkdir(m1, md1, n1, n3, entries1) ∧ str0 ∈ entries0 ∧ str1 ∈ entries1 → (entries0[str0] = entries1[str1] ↔ str0 = str1 ∧ ino0 = ino1);%lastlink-rename: ⊦ # links(entries[str0], dirs) = 1 ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(m, md, n, n0, entries) ∧ str0 ∈ entries ∧ str1 ∈ entries → (entries[str0] = entries[str1] ↔ str0 = str1);% ⊦ ¬ alink ∈ ls → ls -- alink = ls; (s)%⊦ alink ∈ links(ino, dirs) ↔ alink.pino ∈ dirs ∧ alink.name ∈ dirs[alink.pino].entries ∧ ino = dirs[alink.pino].entries[alink.name]; (s)% ⊦ mklink(m, str).pino = m; (s)% ⊦ mklink(m, str).name = str; (s)% ⊦ mkdir(m, md, m0, m1, entries).entries = entries; (s)% ⊦ alink ∈ ls → #(ls -- alink) = # ls - 1; (s) Used formulas: mklink(m, str) ∈ links(entries2[str], dirs0)