| dirs0[entries1[str]] = mkdir(m11, md6, m12, m13, entries), dirs0[m] = mkdir(m2 + 1, md2, # links(m, dirs0), m5, entries1), files[entries1[str]] = mkfile(m8, md3, # links(entries1[str], dirs0), content), dirs0[m0] = mkdir(m1, md5, # links(m0, dirs0), m6, entries0), afs-cons(dirs0, files), m0 ∈ dirs0, entries1[str] ∈ files, ROOT_INO ∈ dirs0, str ∈ entries1, m ∈ dirs0, links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO, links(m0, dirs0) ≠ ∅ ∨ m0 = ROOT_INO ⊦ # links(entries1[str], dirs0) = #(links(entries1[str], dirs0) -- mklink(m, str)) + 1, m = m0, entries1[str] ∈ dirs0, str0 ∈ entries0 |
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(m, str) ∈ links(entries1[str], dirs0)