| # links(entries0[str], dirs0) = m12 + 1, (ino = m0 ⊃ mkdir(m8, md1, # links(m0, dirs0), m11, (entries0 -- str0)[str, entries0[str0]]) ;mkdir(# entries4, md9, # links(ino, dirs0), # subdirs(ino, dirs0), entries4) ) = mkdir(m20, md10, m21, m22, entries5), (entries0[str0] = ino ⊃ (links(entries0[str0], dirs0) -- mklink(m0, str0)) ++ mklink(m0, str);links(ino, dirs0)) = ∅, dirs0[ino] = mkdir(# entries4, md9, # links(ino, dirs0), # subdirs(ino, dirs0), entries4), files[ino] = mkfile(m14, md8, m16, content), dirs0[entries0[str0]] = mkdir(m4, md3, # links(entries0[str0], dirs0), m7, entries1), dirs0[entries0[str]] = mkdir(m13, md6, m12 + 1, m15, ∅), dirs0[m0] = mkdir(m8 + 1, md5, # links(m0, dirs0), m11 + 1, entries0), afs-cons(dirs0, files), ino ∈ dirs0, str ∈ entries0, entries0[str0] ∈ dirs0, str0 ∈ entries0, m0 ∈ dirs0, entries0[str] ∈ dirs0, ROOT_INO ∈ dirs0, # links(ino, dirs0) ≤ 1, links(ino, dirs0) = ∅ → entries4 = ∅, name ∈ entries4 → entries4[name] ∈ dirs0 ∨ entries4[name] ∈ files, links(m0, dirs0) ≠ ∅ ∨ m0 = ROOT_INO ⊦ entries0[str] = m0, entries0[str] = ROOT_INO, entries5 = ∅, ino = entries0[str], ino = ROOT_INO, mkdentry(str, entries0[str]) = mkdentry(str0, entries0[str0]) |
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)% ⊦ 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)% ⊦ ∅ ≠ ls ++ alink; (s) Used formulas: entries0[str0] = ino