| # links(entries0[str], dirs0) = m11 + 1, (entries0[str0] = entries0[str] ⊃ mkfile(m2, md, m11, content1);mkfile(m1, md3, # links(entries0[str0], dirs0), content)) = mkfile(m14, md8, m15, content2), files0[entries0[str]] = mkfile(m5, md0, m11 + 1, content1), files0[entries0[str0]] = mkfile(m1, md3, # links(entries0[str0], dirs0), content), dirs0[entries0[str0]] = mkdir(m16, md9, m17, m18, entries2), dirs0[m] = mkdir(m6 + 1, md6, # links(m, dirs0), m8, entries0), afs-cons(dirs0, files0), ROOT_INO ∈ dirs0, entries0[str] ∈ files0, m ∈ dirs0, str ∈ entries0, entries0[str0] ∈ files0, str0 ∈ entries0, links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO ⊦ m15 = #(links(entries0[str0], dirs0) -- mklink(m, str0)) + 1, mkdentry(str, entries0[str]) = mkdentry(str0, entries0[str0]), entries0[str] ∈ dirs0, entries0[str0] ∈ dirs0, mklink(m, str) ≠ mklink(m, str0) ∧ entries0[str0] = entries0[str] |
Used simplifier rules: ⊦ ¬ 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)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ m < 1 ↔ m = 0; (s)%size-zero-02: ⊦ # ls = 0 → ls = ∅; (forward) from specification set-basic[alink-set]%⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries → links(entries[str], dirs) ≠ ∅; (s)%n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s)% ⊦ m + n = m + n0 ↔ n = n0; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ mklink(m, str) = mklink(m0, str0) ↔ m = m0 ∧ str = str0; (ws)% ⊦ mkdentry(str, m) = mkdentry(str0, m0) ↔ str = str0 ∧ m = m0; (ws)%⊦ mkfile(m, md, m0, content) = mkfile(m1, md0, m2, content0) ↔ m = m1 ∧ md = md0 ∧ m0 = m2 ∧ content = content0; (ws) Used formulas: mklink(m, str0) ∈ links(entries0[str0], dirs0)