| dirs[m] = mkdir(m0, md0, # links(m, dirs), m2, entries), files[ino0] = mkfile(m1, md1, m3, content), dirs[ino0] = mkdir(# entries1, md2, # links(ino0, dirs), # subdirs(ino0, dirs), entries1), (dirs[m, mkdir(m0 + 1, md0, # links(m, dirs), m2 + 1, entries[str, ino])] ++ ino)[ino0] = mkdir(m4, md, m5, m6, entries0), afs-cons(dirs, files), ino0 ∈ dirs, m ∈ dirs, ROOT_INO ∈ dirs, # links(ino0, dirs) ≤ 1, ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → entries1 = ∅, name ∈ entries1 → entries1[name] ∈ dirs ∨ entries1[name] ∈ files, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ # subdirs(ino0, dirs) = # subdirs(ino0, dirs[m, mkdir(m0 + 1, md0, # links(m, dirs), m2 + 1, entries[str, ino])] ++ ino), str0 ∈ entries1 ∧ entries1[str0] ∈ dirs ↔ str0 ∈ entries0 ∧ (entries0[str0] = ino ∨ entries0[str0] ∈ dirs), ino = 0, ino0 = m, ino ∈ dirs, ino ∈ files, str ∈ entries |
Used simplifier rules: ⊦ ino ∈ dirs[ino0, ad] ↔ ino ∈ dirs; (s)%ino ∈ dirs, ino0 ≠ 0, ¬ ino0 ∈ dirs ⊦ ino ≠ ino0 → (dirs ++ ino0)[ino] = dirs[ino]; (s)% ⊦ dirs[ino, ad][ino0] = (ino0 = ino ∧ ino ∈ dirs ⊃ ad;dirs[ino0]); (s)%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%⊦ mkdir(m, md, m0, m1, entries) = mkdir(m2, md0, m3, m4, entries0) ↔ m = m2 ∧ md = md0 ∧ m0 = m3 ∧ m1 = m4 ∧ entries = entries0; (ws)% ⊦ # ∅ = 0; (s)% ⊦ ¬ str ∈ ∅; (s)%⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ str ∈ entries → entries[str] ≠ 0; (s)%⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ str ∈ entries ∧ afs-cons(dirs, files) → (entries[str] ∈ files ↔ ¬ entries[str] ∈ dirs); (ss) Used formulas: ino0 = ino