Proof step 226 from proof eq-io-truncate (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 227:

  files1[m] = mkfile(m0, md0, m1, content0), dirs = dirs1, dirs0 = dirs1, files = files1[m, mkfile(m0, md0, m1, content0 upto min(n0, m2))], ino = inode.ino, inode = mkinode(m, md, false, m1, 0, n0), ino ∈ dirs, m ∈ files1, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE ⊦ ⟨dirs[ino].meta := inode.meta; inode := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS; asynced := ?⟩ ( inode = (m ∈ dirs0 ⊃ mkinode(m, dirs0[m].meta, true, dirs0[m].nlink, dirs0[m].nsubdirs, dirs0[m].size);mkinode(m, md, false, m1, 0, n0)) ∧ err = ESUCCESS ∧ dirs = dirs0 ∧ files = files1[m, mkfile(n0, md, m1, content0 upto min(n0, m2))]), ino ∈ files, m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content0 ∨ buf-opt0.some?)

• Proof step 231:

  files1[m] = mkfile(m0, md0, m1, content0), dirs = dirs1, dirs0 = dirs1, files = files1[m, mkfile(m0, md0, m1, content0 upto min(n0, m2))], ino = inode.ino, inode = mkinode(m, md, false, m1, 0, n0), m ∈ files1, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE ⊦ ⟨skip; inode := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS; asynced := ?⟩ ( inode = (m ∈ dirs0 ⊃ mkinode(m, dirs0[m].meta, true, dirs0[m].nlink, dirs0[m].nsubdirs, dirs0[m].size);mkinode(m, md, false, m1, 0, n0)) ∧ err = ESUCCESS ∧ dirs = dirs0 ∧ files = files1[m, mkfile(n0, md, m1, content0 upto min(n0, m2))]), ino ∈ files, ino ∈ dirs, m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content0 ∨ buf-opt0.some?)

Rule argument

Additional information