| # links(entries[str], dirs0) = m11 + 1, files0[entries[str]] = mkfile(m5, md0, m11 + 1, content1), dirs0[m] = mkdir(m6, md6, # links(m, dirs0), m10, entries), files0[entries1[str0]] = mkfile(m1, md3, # links(entries1[str0], dirs0), content), dirs0[entries1[str0]] = mkdir(m16, md9, m17, m18, entries2), dirs0[m0] = mkdir(m3 + 1, md4, # links(m0, dirs0), m7, entries1), afs-cons(dirs0, files0), ROOT_INO ∈ dirs0, entries[str] ∈ files0, m0 ∈ dirs0, str ∈ entries, str0 ∈ entries1, entries1[str0] ∈ files0, m ∈ dirs0, links(m0, dirs0) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO ⊦ # links(entries1[str0], dirs0) = #(links(entries1[str0], dirs0) -- mklink(m0, str0)) + 1, entries1[str0] = entries[str], m0 = m, mklink(m, str) = mklink(m0, str0), entries[str] ∈ dirs0, entries1[str0] ∈ dirs0 |
Used simplifier rules: ⊦ ¬ alink ∈ ls → ls -- alink = ls; (s)% ⊦ m = m + n ↔ n = 0; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%⊦ 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) Used formulas: mklink(m0, str0) ∈ links(entries1[str0], dirs0)