Proof step 22 from proof writepage-prepost (previous step)

User applied rule if right

And obtained the following new goals

• Proof step 23:

  err0 = ESUCCESS, files0 = files, ⌜buf0⌝ = (σ from n3 * VFS_PAGE_SIZE) to VFS_PAGE_SIZE, ((m0 =>mkfile(n2, md, m1, σ) * F))(files), afs-cons(dirs, files), m0 ∈ files, n0 + n1 ≤ VFS_PAGE_SIZE, m + n1 ≤ # buf1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [buf0 := copy(buf1, m, buf0, n0, n1); afs_writepage#(mkinode(m0, md0, boolvar, m2, m3, m4), n3, buf0, dirs; err0, files; asynced)] ( err0 = ESUCCESS ∧ ((m0 =>mkfile(n2, md, m1, (σ to n3 * VFS_PAGE_SIZE + n0) + ((⌜buf1⌝ from m) to n1) + (σ from n3 * VFS_PAGE_SIZE + n0 + n1)) * F))(files) ∨ ⌊err0⌋ ∧ files0 = files)

• Proof step 65:

  files0 = files, ⌜buf0⌝ = (σ from n3 * VFS_PAGE_SIZE) to VFS_PAGE_SIZE, ((m0 =>mkfile(n2, md, m1, σ) * F))(files), afs-cons(dirs, files), m0 ∈ files, n0 + n1 ≤ VFS_PAGE_SIZE, m + n1 ≤ # buf1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [skip] ( err0 = ESUCCESS ∧ ((m0 =>mkfile(n2, md, m1, (σ to n3 * VFS_PAGE_SIZE + n0) + ((⌜buf1⌝ from m) to n1) + (σ from n3 * VFS_PAGE_SIZE + n0 + n1)) * F))(files) ∨ ⌊err0⌋ ∧ files0 = files), err0 = ESUCCESS

Rule argument

Additional information