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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 98:

  VFS_PAGE_SIZE = n1 + m5 % VFS_PAGE_SIZE, files[m] = mkfile(m1, md, # links(m, dirs), content), files1[m] = mkfile(m5, md0, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), err = err0, m5 < m0 + ino, afs-cons(dirs, files1), afs-cons (dirs, files1 [m, mkfile(m5, md0, # links(m, dirs), content0[m5 / VFS_PAGE_SIZE, fill(content0[m5 / VFS_PAGE_SIZE], zero, m5 % VFS_PAGE_SIZE, n1)] upto m5) ]), of-cons(of, dirs, files1), m ∈ files, fd ∈ of, m5 / VFS_PAGE_SIZE ∈ content0, m ∈ files1, n ≤ # buf0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪dirs0 := dirs; err1 := err; if err1 = ESUCCESS then afs_write_inode# ( (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode (m, files1 [m, files1 [m, files1 [m, mkfile (m5, md0, # links(m, dirs), content0[m5 / VFS_PAGE_SIZE, fill(content0[m5 / VFS_PAGE_SIZE], zero, m5 % VFS_PAGE_SIZE, n1)] upto m5) ] [m ] .size:= m5 ] [m ] .meta:= md0 ] [m ] .meta, false, files1 [m, files1 [m, files1 [m, mkfile (m5, md0, # links(m, dirs), content0[m5 / VFS_PAGE_SIZE, fill(content0[m5 / VFS_PAGE_SIZE], zero, m5 % VFS_PAGE_SIZE, n1)] upto m5) ] [m ] .size:= m5 ] [m ] .meta:= md0 ] [m ] .nlink, 0, files1 [m, files1 [m, files1 [m, mkfile (m5, md0, # links(m, dirs), content0[m5 / VFS_PAGE_SIZE, fill(content0[m5 / VFS_PAGE_SIZE], zero, m5 % VFS_PAGE_SIZE, n1)] upto m5) ] [m ] .size:= m5 ] [m ] .meta:= md0 ] [m ] .size) ) .size:= (m0 + ino) ; err1, dirs, files ; asynced); if err1 ≠ ESUCCESS then ino := (m0 ≤ m5 ⊃ m5 - m0;0), err1 := ESUCCESS; of[fd].pos := m0 + ino⟫ (dirs0 = dirs), m5 % VFS_PAGE_SIZE = 0, ino = 0, n = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information