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

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 120:

  VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m2, md1, # links(m, dirs), content0), files[m] = mkfile(m3, md0, # links(m, dirs), content1), m2 < m0 + ino, afs-cons (dirs, files1 [m, mkfile(m2, md1, # links(m, dirs), content0[m2 / VFS_PAGE_SIZE, fill(content0[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ]), afs-cons(dirs, files1), of-cons(of, dirs, files1), m ∈ files1, m2 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, m ∈ files, n ≤ # buf0, ⌊err0⌋ ⊦ ⟪err := err0; asynced := ?; if err ≠ ESUCCESS then ino := (m0 ≤ m2 ⊃ m2 - m0;0), err := ESUCCESS; of[fd].pos := m0 + ino⟫ true, m2 % VFS_PAGE_SIZE = 0, ino = 0, n = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

• Proof step 125:

  VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m2, md1, # links(m, dirs), content0), files[m] = mkfile(m3, md0, # links(m, dirs), content1), m2 < m0 + ino, afs-cons (dirs, files1 [m, mkfile(m2, md1, # links(m, dirs), content0[m2 / VFS_PAGE_SIZE, fill(content0[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ]), afs-cons(dirs, files1), of-cons(of, dirs, files1), m ∈ files1, m2 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, m ∈ files, n ≤ # buf0 ⊦ m2 % VFS_PAGE_SIZE = 0, ino = 0, n = 0, ∃ err0. ⌊err0⌋ , mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information