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

User applied rule call right

And obtained the following new goals

• Proof step 4:

  ⊦

• Proof step 5:

  ino1 = ino, afs-cons(dirs, files), of-cons(of, dirs, files) ⊦ ⟪let ino = ROOT_INO in {vfs_walk#(p, user, dirs, files, asynced; ino, err); if err = ESUCCESS then choose inode with true in {afs_iget#(ino, dirs, files, asynced; inode, 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

Used simplifier rules: readmeta: ⊦ ;