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

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 61:

  VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, files1[m] = mkfile(m2, md0, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), dirs0 = dirs, files = files0, files0 = files1 [m, mkfile(m2, md0, # links(m, dirs), content0[m2 / VFS_PAGE_SIZE, fill(content0[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ], ino = inode.ino, inode = mkinode(m, md0, false, # links(m, dirs), 0, m2), inode0 = mkinode(m, md0, false, # links(m, dirs), 0, m2), afs-cons(dirs, files1), of-cons(of, dirs, files1), fd ∈ of, m ∈ files1, m2 / VFS_PAGE_SIZE ∈ content0, n0 ≤ # buf0 ⊦ [if ino ∈ files then {files[ino].size := inode.size; files[ino].meta := inode.meta} else if ino ∈ dirs then dirs[ino].meta := inode.meta; inode0 := (inode0.ino ∈ dirs ⊃ mkinode(inode0.ino, dirs[inode0.ino].meta, true, dirs[inode0.ino].nlink, dirs[inode0.ino].nsubdirs, dirs[inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ); err := ESUCCESS; asynced := ?] ( afs-cons(dirs, files) → ⟪ino3 := 0; files0 := files; if err = ESUCCESS then vfs_write_loop#(m0, inode0, m0 + n0, buf0, dirs; ino3, err, files0, asynced); if ino3 ≠ 0 then err := ESUCCESS; if err = ESUCCESS then let ino = inode0.size in {n0 := ino3, ino1 := m0 + ino3; if ino3 ≠ 0 ∧ ino < ino1 then {inode0.size := ino1; afs_check_commit#(dirs, files0; err; asynced); if err = ESUCCESS then afs_write_inode#(inode0; err, dirs, files0; asynced)}; if err ≠ ESUCCESS then n0 := (m0 ≤ ino ⊃ ino - m0;0), err := ESUCCESS; of[fd].pos := m0 + n0}⟫ (dirs0 = dirs)), m2 % VFS_PAGE_SIZE = 0, n0 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information