Proof step 4 from proof inv-iget (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 5:

  afs-cons(dirs, files), ino ∈ dirs ∨ ino ∈ files ⊦ ⟪inode := getinode(ino, dirs, files); err := ESUCCESS⟫ true

• Proof step 7:

  afs-cons(dirs, files), ino ∈ dirs ∨ ino ∈ files ⊦ ⟪fail#(; ; err)⟫ true

Rule argument

Additional information