Proof step 4 from proof afs-cons-remove-orphans (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  afs-cons(dirs, files) ⊦ (ino ∈ dirs ∧ ¬ ino ∈ orphans(dirs, files) ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dirs[ino].entries = ∅) ∧ ( ino ∈ dirs ∧ ¬ ino ∈ orphans(dirs, 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 ∈ orphans(dirs, files) → ¬ ino ∈ dirs ∧ files[ino].nlink = # links(ino, dirs)) ∧ ( ino ∈ dirs ∧ ¬ ino ∈ orphans(dirs, files) ∧ name ∈ dirs[ino].entries → dirs[ino].entries[name] ∈ dirs ∧ ¬ dirs[ino].entries[name] ∈ orphans(dirs, files) ∨ dirs[ino].entries[name] ∈ files ∧ ¬ dirs[ino].entries[name] ∈ orphans(dirs, files)) ∧ (ino ∈ files ∧ ¬ ino ∈ orphans(dirs, files) ∧ n ∈ files[ino].content → # files[ino].content[n] = VFS_PAGE_SIZE)

Rule argument

Additional information

Used simplifier rules: ⊦ valid-pagesize(ino, n, files) ↔ # files[ino].content[n] = VFS_PAGE_SIZE; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)% ⊦ ino ∈ files ∧ ¬ ino ∈ ns → (files \ ns)[ino] = files[ino]; (s)%⊦ ¬ ino ∈ orphans(dirs, files) → subdirs(ino, dirs \ orphans(dirs, files)) = subdirs(ino, dirs); (s)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)% ⊦ ino ∈ files \ ns ↔ ino ∈ files ∧ ¬ ino ∈ ns; (s)% ⊦ ino ∈ dirs ∧ ¬ ino ∈ ns → (dirs \ ns)[ino] = dirs[ino]; (s)% ⊦ dir-empty(ino, dirs, files) ↔ dirs[ino].entries = ∅; (s)%⊦ afs-cons(dirs, files) → links(ino, dirs \ orphans(dirs, files)) = links(ino, dirs); (s)% ⊦ ¬ ROOT_INO ∈ orphans(dirs, files); (s)% ⊦ afs-cons(dirs, files) → ROOT_INO ∈ dirs; (ss)% ⊦ ino ∈ dirs \ ns ↔ ino ∈ dirs ∧ ¬ ino ∈ ns; (s)