| # links(entries0[str], dirs0) = m1 + 1, (entries0[str] = ino ⊃ links(entries0[str], dirs0) -- mklink(m, str);links(ino, dirs0)) = ∅, (ino = entries0[str] ⊃ mkfile(m0, md1, m1, content);mkfile(m4, md, m5, content0)) = mkfile(m6, md0, m7, content1), (ino = m ⊃ mkdir(m2, md2, # links(m, dirs0), m3, entries0 -- str) ;mkdir(# entries, md3, # links(ino, dirs0), # subdirs(ino, dirs0), entries) ) = mkdir(m11, md4, m12, m13, entries1), files0[ino] = mkfile(m4, md, m5, content0), files0[entries0[str]] = mkfile(m0, md1, m1 + 1, content), dirs0[m] = mkdir(m2 + 1, md2, # links(m, dirs0), m3, entries0), dirs0[ino] = mkdir(# entries, md3, # links(ino, dirs0), # subdirs(ino, dirs0), entries), afs-cons(dirs0, files0), ino ∈ dirs0, m ∈ dirs0, str ∈ entries0, entries0[str] ∈ files0, ROOT_INO ∈ dirs0, # links(ino, dirs0) ≤ 1, links(ino, dirs0) = ∅ → entries = ∅, name ∈ entries → entries[name] ∈ dirs0 ∨ entries[name] ∈ files0, links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO ⊦ entries1 = ∅, ino = ROOT_INO |
Used simplifier rules: ⊦ afs-cons(dirs, files) → ( links(ino, dirs) = ∅ ↔ (ino ∈ dirs → dirs[ino].nlink = 0) ∧ (ino ∈ files → files[ino].nlink = 0)); (ws)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)%⊦ mkfile(m, md, m0, content) = mkfile(m1, md0, m2, content0) ↔ m = m1 ∧ md = md0 ∧ m0 = m2 ∧ content = content0; (ws)% ⊦ mkdir(m, md, m0, m1, entries).nlink = m0; (s)%size-zero-02: ⊦ # ls = 0 → ls = ∅; (forward) from specification set-basic[alink-set]%size-zero-01: ⊦ ls ≠ ∅ → # ls ≠ 0; (forward) from specification set-basic[alink-set]%afs-cons-dir-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) → # links(ino, dirs) = n; (forward) from specification afs-base% ⊦ # ∅ = 0; (s)% ⊦ ¬ str ∈ ∅; (s)%⊦ mkdir(m, md, m0, m1, entries) = mkdir(m2, md0, m3, m4, entries0) ↔ m = m2 ∧ md = md0 ∧ m0 = m3 ∧ m1 = m4 ∧ entries = entries0; (ws) Used formulas: entries0[str] = ino