Proof step 2 from proof abs-nlinks-h (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  links(ino1, dirs) = ∅, abs(tree, ino0)(dirs), ino1 ∈ files, ino0 ∈ dirs, ⌜ino1⌝ ∈ tree.fids, ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files ⊦

• Proof step 45:

  abs(tree, ino0)(dirs), ino1 ∈ files, ino0 ∈ dirs, ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files ⊦ links(ino1, dirs) = ∅, ⌜ino1⌝ ∈ tree.fids

Rule argument

Additional information