| # entries0 = m6 + 1, # links(entries0[str], dirs0) = m11 + 1, dirs0[m0] = mkdir(m6 + 1, md6, # links(m0, dirs0), # subdirs(m0, dirs0), entries0), files0[m0] = mkfile(m12, md7, m13, content0), files0[entries0[str]] = mkfile(m5, md0, m11 + 1, content1), files0[entries0[str0]] = mkfile(m1, md3, # links(entries0[str0], dirs0), content), afs-cons(dirs0, files0), name ∈ (entries0 -- str0)[str, entries0[str0]], str0 ∈ entries0, entries0[str0] ∈ files0, str ∈ entries0, m0 ∈ dirs0, entries0[str] ∈ files0, ROOT_INO ∈ dirs0, # links(m0, dirs0) ≤ 1, name ∈ entries0 → entries0[name] ∈ dirs0 ∨ entries0[name] ∈ files0, links(m0, dirs0) ≠ ∅ ∨ m0 = ROOT_INO ⊦ entries0 = ∅, mkdentry(str, entries0[str]) = mkdentry(str0, entries0[str0]), entries0[str0] ∈ dirs0, entries0[str] ∈ dirs0, (entries0 -- str0)[str, entries0[str0]][name] ∈ dirs0, (entries0 -- str0)[str, entries0[str0]][name] ∈ files0, m0 ≠ ROOT_INO ∧ links(m0, dirs0) = ∅ |
Used simplifier rules: ⊦ str ≠ str0 → (str ∈ entries[str0, ino] ↔ str ∈ entries); (s)% ⊦ str ∈ entries -- str0 ↔ str ≠ str0 ∧ str ∈ entries; (s)% ⊦ str ≠ str0 → entries[str0, ino][str] = entries[str]; (s)% ⊦ str ≠ str0 → (entries -- str0)[str] = entries[str]; (s)%⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ str ∈ entries ∧ afs-cons(dirs, files) → (entries[str] ∈ files ↔ ¬ entries[str] ∈ dirs); (ss)% ⊦ str ∈ entries[str, ino]; (s)% ⊦ entries[str, ino][str] = ino; (s) Used formulas: name = str