Proof step 121 from proof inv-rmdir (previous step)

User applied rule all left

And obtained the following new goals

• Proof step 122:

  dirs[m] = mkdir(m1, md0, # links(m, dirs), 0, entries0), ROOT_INO ∈ dirs, m ∈ dirs, str ∈ entries0, entries0[str] ∈ dirs, m ∈ dirs ∧ m ≠ ROOT_INO ∧ links(m, dirs) = ∅ → dirs[m].entries = ∅, m ∈ dirs → ¬ m ∈ files ∧ dirs[m].nlink = # links(m, dirs) ∧ dirs[m].nlink ≤ 1 ∧ dirs[m].size = # dirs[m].entries ∧ dirs[m].nsubdirs = # subdirs(m, dirs), m ∈ files → ¬ m ∈ dirs ∧ files[m].nlink = # links(m, dirs), ∀ ino. (ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dirs[ino].entries = ∅) ∧ ( ino ∈ dirs → ¬ ino ∈ files ∧ dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs)) ∧ (ino ∈ files → ¬ ino ∈ dirs ∧ files[ino].nlink = # links(ino, dirs)) ∧ (∀ name. ino ∈ dirs ∧ name ∈ dirs[ino].entries → dirs[ino].entries[name] ∈ dirs ∨ dirs[ino].entries[name] ∈ files) ∧ (∀ n. ino ∈ files ∧ n ∈ files[ino].content → # files[ino].content[n] = VFS_PAGE_SIZE), ∀ name. m ∈ dirs ∧ name ∈ dirs[m].entries → dirs[m].entries[name] ∈ dirs ∨ dirs[m].entries[name] ∈ files, ∀ n. m ∈ files ∧ n ∈ files[m].content → # files[m].content[n] = VFS_PAGE_SIZE ⊦

Rule argument

Additional information

Used terms: m