Proof step 7 from proof write-inode-inv (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 8:

  files1[ino].meta = md, files = files1, inode = mkinode(ino, files1[ino].meta, false, m, n0, m0 + n), pre-write-inode(inode, dirs, files), write-inv(n0, n1, mkinode(ino, files1[ino].meta, false, m, n0, m0), buf, n, dirs, files0, files1), ino ∈ files1 ⊦ [if inode.directory then dirs[inode.ino].meta := inode.meta else {files[inode.ino].meta := inode.meta; files[inode.ino].size := inode.size}; err := ESUCCESS; asynced := ?; if err = ESUCCESS then files0[ino].size := m0 + n] write-inv(n0, n1, mkinode(ino, md, false, m, n0, files0[ino].size), buf, n, dirs, files0, files)

• Proof step 37:

  files1[ino].meta = md, files = files1, inode = mkinode(ino, files1[ino].meta, false, m, n0, m0 + n), pre-write-inode(inode, dirs, files), write-inv(n0, n1, mkinode(ino, files1[ino].meta, false, m, n0, m0), buf, n, dirs, files0, files1), ino ∈ files1 ⊦ [fail#(; ; err); asynced := ?; if err = ESUCCESS then files0[ino].size := m0 + n] write-inv(n0, n1, mkinode(ino, md, false, m, n0, files0[ino].size), buf, n, dirs, files0, files)

Rule argument

Additional information