Proof step 15 from proof inv-read (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 16:

  of[fd] = mkfile(m, mode, m0), err = ESUCCESS, ino = m, dom of < ino2, afs-cons(dirs, files), of-cons(of, dirs, files), fd ∈ of, n ≤ # buf, mode ≠ MODE_R → fd ∈ of ⊦ ⟪inode := getinode(ino, dirs, files); err := ESUCCESS; if err = ESUCCESS then if inode.directory then err := EISDIR else let ino1 = m0, ino0 = m0 + n, ino = 0 in if ino1 ≤ inode.size then {let isdir = false in vfs_read_loop#(ino1, ino0, inode, isdir, dirs, files, asynced; buf, ino, err); if ino ≠ 0 then err := ESUCCESS; of[fd].pos := of[fd].pos + ino; n := ino} else n := 0⟫ (of-cons(of, dirs, files) ∧ dom of < ino2), mode ≠ MODE_R ∧ mode ≠ MODE_RW

• Proof step 45:

  of[fd] = mkfile(m, mode, m0), err = ESUCCESS, ino = m, dom of < ino2, afs-cons(dirs, files), of-cons(of, dirs, files), fd ∈ of, n ≤ # buf, mode ≠ MODE_R → fd ∈ of ⊦ ⟪fail#(; ; err); if err = ESUCCESS then if inode.directory then err := EISDIR else let ino1 = m0, ino0 = m0 + n, ino = 0 in if ino1 ≤ inode.size then {let isdir = false in vfs_read_loop#(ino1, ino0, inode, isdir, dirs, files, asynced; buf, ino, err); if ino ≠ 0 then err := ESUCCESS; of[fd].pos := of[fd].pos + ino; n := ino} else n := 0⟫ (of-cons(of, dirs, files) ∧ dom of < ino2), mode ≠ MODE_R ∧ mode ≠ MODE_RW

Rule argument

Additional information