Proof step 40 from proof inv-recover (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  afs-cons(dirs0, files1) ⊦ (ino ∈ dirs0 ∧ ¬ ino ∈ orphans(dirs0, files1) ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → dirs0[ino].entries = ∅) ∧ ( ino ∈ dirs0 ∧ ¬ ino ∈ orphans(dirs0, files1) → dirs0[ino].nlink = # links(ino, dirs0) ∧ dirs0[ino].nlink ≤ 1 ∧ dirs0[ino].size = # dirs0[ino].entries ∧ dirs0[ino].nsubdirs = # subdirs(ino, dirs0)) ∧ (ino ∈ files1 ∧ ¬ ino ∈ orphans(dirs0, files1) → ¬ ino ∈ dirs0 ∧ files1[ino].nlink = # links(ino, dirs0)) ∧ ( ino ∈ dirs0 ∧ ¬ ino ∈ orphans(dirs0, files1) ∧ name ∈ dirs0[ino].entries → dirs0[ino].entries[name] ∈ dirs0 ∧ ¬ dirs0[ino].entries[name] ∈ orphans(dirs0, files1) ∨ dirs0[ino].entries[name] ∈ files1 ∧ ¬ dirs0[ino].entries[name] ∈ orphans(dirs0, files1)) ∧ (ino ∈ files1 ∧ ¬ ino ∈ orphans(dirs0, files1) ∧ n ∈ files1[ino].content → # files1[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)