Proof step 17 from proof inv-readmeta (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 18:

  err = ESUCCESS, ino = ino2, afs-cons(dirs, files), ispath(p, ROOT_INO, ino2, dirs, files), of-cons(of, dirs, files), pre-iget(ino, dirs, files), px-parent(user, p, ROOT_INO, dirs, files) ⊦ ⟪inode := getinode(ino, dirs, files); err := ESUCCESS; if err = ESUCCESS then if pr(user, inode.meta) then {md := inode.meta, ino0 := inode.size; if inode.directory then ino1 := inode.nsubdirs + 2 else ino1 := inode.nlink} else err := EACCESS⟫ true

• Proof step 27:

  err = ESUCCESS, ino = ino2, afs-cons(dirs, files), ispath(p, ROOT_INO, ino2, dirs, files), of-cons(of, dirs, files), pre-iget(ino, dirs, files), px-parent(user, p, ROOT_INO, dirs, files) ⊦ ⟪fail#(; ; err); if err = ESUCCESS then if pr(user, inode.meta) then {md := inode.meta, ino0 := inode.size; if inode.directory then ino1 := inode.nsubdirs + 2 else ino1 := inode.nlink} else err := EACCESS⟫ true

Rule argument

Additional information