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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 101:

  VFS_PAGE_SIZE = n1 + m5 % VFS_PAGE_SIZE, of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m5, md0, # links(m, dirs), content0), files[m] = mkfile(m1, md, # links(m, dirs), content), dirs0 = dirs, err = err0, err1 = ESUCCESS, err1 = err, m5 < m0 + ino, 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) ]), afs-cons(dirs, files1), of-cons(of, dirs, files1), m ∈ files1, m5 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, m ∈ files, n ≤ # buf0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪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

• Proof step 128:

  VFS_PAGE_SIZE = n1 + m5 % VFS_PAGE_SIZE, of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m5, md0, # links(m, dirs), content0), files[m] = mkfile(m1, md, # links(m, dirs), content), dirs0 = dirs, err = err0, err1 = err, m5 < m0 + ino, 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) ]), afs-cons(dirs, files1), of-cons(of, dirs, files1), m ∈ files1, m5 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, m ∈ files, n ≤ # buf0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪skip; if err1 ≠ ESUCCESS then ino := (m0 ≤ m5 ⊃ m5 - m0;0), err1 := ESUCCESS; of[fd].pos := m0 + ino⟫ (dirs0 = dirs), m5 % VFS_PAGE_SIZE = 0, err1 = ESUCCESS, ino = 0, n = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information