Proof step 206 from proof write-term (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 207:

  files0[m] = mkfile(m2, md0, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m1, md, # links(m, dirs), content), dirs0 = dirs, err = ESUCCESS, files = files1, inode = mkinode(m, md0, false, # links(m, dirs), 0, m0 + ino), m2 < m0 + ino, afs-cons(dirs, files0[m, mkfile(m2, md0, # links(m, dirs), content0 upto m2)]), afs-cons(dirs, files0), of-cons(of, dirs, files0), pre-write-inode(inode, dirs, files), m ∈ files1, fd ∈ of, m ∈ files0, 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; asynced := ?; if err ≠ ESUCCESS then ino := (m0 ≤ m2 ⊃ m2 - m0;0), err := ESUCCESS; of[fd].pos := m0 + ino⟫ (dirs0 = dirs), ino = 0, n = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content0

• Proof step 215:

  files0[m] = mkfile(m2, md0, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m1, md, # links(m, dirs), content), dirs0 = dirs, err = ESUCCESS, files = files1, inode = mkinode(m, md0, false, # links(m, dirs), 0, m0 + ino), m2 < m0 + ino, afs-cons(dirs, files0[m, mkfile(m2, md0, # links(m, dirs), content0 upto m2)]), afs-cons(dirs, files0), of-cons(of, dirs, files0), pre-write-inode(inode, dirs, files), m ∈ files1, fd ∈ of, m ∈ files0, n ≤ # buf0 ⊦ ⟪fail#(; ; err); asynced := ?; if err ≠ ESUCCESS then ino := (m0 ≤ m2 ⊃ m2 - m0;0), err := ESUCCESS; of[fd].pos := m0 + ino⟫ (dirs0 = dirs), ino = 0, n = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content0

Rule argument

Additional information