Proof step 514 from proof inv-write (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 515:

  of[fd] = mkfile(m, mode, m0), files0[m] = mkfile(m1, md, # links(m, dirs), content0), dirs1 = dirs, err = err0, err0 = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m0 + ino4), m1 < m0 + ino4, dom of < ino3, afs-cons(dirs, files), afs-cons(dirs, files0), of-cons(of, dirs, files), of-cons(of, dirs, files0), pre-write-inode(inode, dirs, files), m ∈ files0, fd ∈ of, n ≤ # buf0 ⊦ [ {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} or fail#(; ; err); asynced := ?; if err ≠ ESUCCESS then ino4 := (m0 ≤ m1 ⊃ m1 - m0;0), err0 := ESUCCESS; of[fd].pos := m0 + ino4] (dirs1 = dirs → of-cons(of, dirs, files) ∧ dom of < ino3 ∧ afs-cons(dirs, files)), ino4 = 0, n = 0, err1 = ESUCCESS ∧ ¬ isdir, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

• Proof step 563:

  of[fd] = mkfile(m, mode, m0), files0[m] = mkfile(m1, md, # links(m, dirs), content0), dirs1 = dirs, err = err0, err0 = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m0 + ino4), m1 < m0 + ino4, dom of < ino3, afs-cons(dirs, files), afs-cons(dirs, files0), of-cons(of, dirs, files), of-cons(of, dirs, files0), m ∈ files0, fd ∈ of, n ≤ # buf0 ⊦ [abort; if err ≠ ESUCCESS then ino4 := (m0 ≤ m1 ⊃ m1 - m0;0), err0 := ESUCCESS; of[fd].pos := m0 + ino4] (dirs1 = dirs → of-cons(of, dirs, files) ∧ dom of < ino3 ∧ afs-cons(dirs, files)), ino4 = 0, n = 0, pre-write-inode(inode, dirs, files), err1 = ESUCCESS ∧ ¬ isdir, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information