| (ino = m ⊃ mkdir(m4 + 1, md1, # links(m, dirs0), m7 + 1, (entries3 -- str)[str0, entries3[str]]) ;mkdir(# entries, md6, # links(ino, dirs0), # subdirs(ino, dirs0), entries) ) = mkdir(m15, md7, m16, m17, entries4), (entries3[str] = ino ⊃ (links(entries3[str], dirs0) -- mklink(m, str)) ++ mklink(m, str0);links(ino, dirs0)) = ∅, dirs0[entries3[str]] = mkdir(m3, md4, # links(entries3[str], dirs0), m5, entries1), dirs0[m] = mkdir(m4 + 1, md5, # links(m, dirs0), m7 + 1, entries3), files[ino] = mkfile(m9, md2, m11, content), dirs0[ino] = mkdir(# entries, md6, # links(ino, dirs0), # subdirs(ino, dirs0), entries), afs-cons(dirs0, files), ino ∈ dirs0, ROOT_INO ∈ dirs0, entries3[str] ∈ dirs0, str ∈ entries3, m ∈ dirs0, # links(ino, dirs0) ≤ 1, name ∈ entries → entries[name] ∈ dirs0 ∨ entries[name] ∈ files, links(ino, dirs0) = ∅ → entries = ∅, links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO ⊦ entries4 = ∅, ino = ROOT_INO, str0 ∈ entries3 |
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)%⊦ mkdir(m, md, m0, m1, entries) = mkdir(m2, md0, m3, m4, entries0) ↔ m = m2 ∧ md = md0 ∧ m0 = m3 ∧ m1 = m4 ∧ entries = entries0; (ws)% ⊦ ¬ str ∈ ∅; (s)% ⊦ ∅ ≠ ls ++ alink; (s) Used formulas: entries3[str] = ino