Proof step 44 from proof refine-seek (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 45:

  of[fd] = mkfile(m, mode, m0), err = ESUCCESS, ino = m, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), fd ∈ of, psynced → asynced ⊦ ⟪inode := getinode(ino, dirs, files); err := ESUCCESS; n := n0; if err = ESUCCESS then n := inode.size + n; ofh := abs-of(of); if err = ESUCCESS then of[fd].pos := n⟫ ⟨posix_seek#(fd, SEEK_END, user, root, abs-files(files); n0, err0, ofh)⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ n = n0 ∧ err = err0)

• Proof step 69:

  of[fd] = mkfile(m, mode, m0), err = ESUCCESS, ino = m, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), fd ∈ of, psynced → asynced ⊦ ⟪fail#(; ; err); n := n0; if err = ESUCCESS then n := inode.size + n; ofh := abs-of(of); if err = ESUCCESS then of[fd].pos := n⟫ ⟨posix_seek#(fd, SEEK_END, user, root, abs-files(files); n0, err0, ofh)⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ n = n0 ∧ err = err0)

Rule argument

Additional information