Proof step 135 from proof inv-writepage (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 136:

  # buf = VFS_PAGE_SIZE, files[m] = mkfile(m0, md, # links(m, dirs), content), icache[m1] = mkientry(boolvar0, mkinode(m1, md0, false, # links(m1, dirs), 0, m4)), files[m1] = mkfile(m2, md1, # links(m1, dirs), content0), afs-cons(dirs, files), afs-cons(dirs, files[m, mkfile(m0, md, # links(m, dirs), content[pageno, buf])]), synced(dirs, icache, pcache), synced(files, icache, pcache), m1 ∈ files, m ∈ files, m1 ∈ icache, ¬ boolvar0 → mkinode(m1, md0, false, # links(m1, dirs), 0, m4) = mkinode(m1, md1, false, # links(m1, dirs), 0, m2), ∀ ino0. ino0 ∈ icache → icache[ino0].inode.ino = ino0 ∧ (icache[ino0].dirty ⊃ icache[ino0].inode.ino ∈ files ∧ icache[ino0].inode.nlink = files[icache[ino0].inode.ino].nlink ∧ icache[ino0].inode.nsubdirs = 0 ∧ ¬ icache[ino0].inode.directory ; (ino0 ∈ dirs ∨ ino0 ∈ files) ∧ icache[ino0].inode = (icache[ino0].inode.ino ∈ dirs ⊃ mkinode (icache[ino0].inode.ino, dirs[icache[ino0].inode.ino].meta, true, dirs[icache[ino0].inode.ino].nlink, dirs[icache[ino0].inode.ino].nsubdirs, dirs[icache[ino0].inode.ino].size) ;mkinode (icache[ino0].inode.ino, files[icache[ino0].inode.ino].meta, false, files[icache[ino0].inode.ino].nlink, 0, files[icache[ino0].inode.ino].size) ) ) ⊦ (boolvar0 ⊃ # links(m1, dirs) = (m1 = m ⊃ mkfile(m0, md, # links(m, dirs), content[pageno, buf]);mkfile(m2, md1, # links(m1, dirs), content0)).nlink ; mkinode(m1, md0, false, # links(m1, dirs), 0, m4) = mkinode (m1, (m1 = m ⊃ mkfile(m0, md, # links(m, dirs), content[pageno, buf]);mkfile(m2, md1, # links(m1, dirs), content0)).meta, false, (m1 = m ⊃ mkfile(m0, md, # links(m, dirs), content[pageno, buf]);mkfile(m2, md1, # links(m1, dirs), content0)).nlink, 0, (m1 = m ⊃ mkfile(m0, md, # links(m, dirs), content[pageno, buf]);mkfile(m2, md1, # links(m1, dirs), content0)).size) )

Rule argument

Additional information