| m5 + n1 = m5 / VFS_PAGE_SIZE * VFS_PAGE_SIZE + VFS_PAGE_SIZE, of[n0] = mkfile(m1, mode0, m2), of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m5, md, # links(m, dirs), content0), of[fd, mkfile(m, mode, m0 + (m0 ≤ m5 ⊃ m5 - m0;0))][n0] = mkfile(m3, mode1, m4), m5 = n2 + m5 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, dom of < ino3, m5 < m0 + ino4, afs-cons(dirs, files), afs-cons(dirs, files1), of-cons(of, dirs, files), of-cons(of, dirs, files1), n0 ∈ of, m1 ∈ files, m ∈ files1, m5 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, n0 ∈ of[fd, mkfile(m, mode, m0 + (m5 - m0))], m5 % VFS_PAGE_SIZE + n1 ≤ VFS_PAGE_SIZE, n ≤ # buf0, n2 + n1 ≤ VFS_PAGE_SIZE, ⌊err0⌋ ⊦ ino4 = 0, n = 0, n2 = 0, m3 ∈ files, err1 = ESUCCESS ∧ ¬ isdir, mode ≠ MODE_W ∧ mode ≠ MODE_RW |
m5 + n1 = m5 / VFS_PAGE_SIZE * VFS_PAGE_SIZE + VFS_PAGE_SIZE, of[fd, mkfile(m, mode, m0 + (m0 ≤ m5 ⊃ m5 - m0;0))][n0] = mkfile(m3, mode1, m4), files1[m] = mkfile(m5, md, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), of[n0] = mkfile(m1, mode0, m2), m5 = n2 + m5 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, m5 < m0 + ino4, dom of < ino3, afs-cons(dirs, files1), afs-cons(dirs, files), of-cons(of, dirs, files1), of-cons(of, dirs, files), n0 ∈ of[fd, mkfile(m, mode, m0 + (m5 - m0))], fd ∈ of, m5 / VFS_PAGE_SIZE ∈ content0, m ∈ files1, m1 ∈ files, n0 ∈ of, n2 + n1 ≤ VFS_PAGE_SIZE, n ≤ # buf0, m5 % VFS_PAGE_SIZE + n1 ≤ VFS_PAGE_SIZE, ⌊err0⌋ ⊦ ino4 = 0, n = 0, n2 = 0, m3 ∈ files, mode ≠ MODE_W ∧ mode ≠ MODE_RW, err1 = ESUCCESS ∧ ¬ isdir