| pageno ∈ content0 ↔ pageno ∈ content, files[m] = mkfile(m0, md0, # links(m, dirs), content0), files0[m] = mkfile(m0, md0, # links(m, dirs), content), content0[pageno] = content[pageno], pageno * VFS_PAGE_SIZE < m2, afs-cons(dirs, files), afs-cons(dirs, files0), pcache-cons(pcache, dirs, files), pcache-cons(pcache1, dirs, files0), m ∈ files, m ∈ files0, ∀ pageno0. (pageno0 < pageno ⊃ (pageno0 ∈ content0 ↔ pageno0 ∈ content ⊕ mkcontent(m, pcache1)) ∧ content0[pageno0] = (content ⊕ mkcontent(m, pcache1))[pageno0] ;(pageno0 ∈ content0 ↔ pageno0 ∈ content) ∧ content0[pageno0] = content[pageno0] ), ∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty) ⊦ content[pageno] = (content ⊕ mkcontent(m, pcache1))[pageno], datakey(m, pageno) ∈ pcache1, datakey(m, pageno) ∈ pcache, (pageno ∈ content → pageno ∈ content ⊕ mkcontent(m, pcache1)) ∧ content[pageno] = (content ⊕ mkcontent(m, pcache1))[pageno] |
pageno ∈ content0 ↔ pageno ∈ content, content0[pageno] = content[pageno], files0[m] = mkfile(m0, md0, # links(m, dirs), content), files[m] = mkfile(m0, md0, # links(m, dirs), content0), pageno * VFS_PAGE_SIZE < m2, afs-cons(dirs, files0), afs-cons(dirs, files), pcache-cons(pcache1, dirs, files0), pcache-cons(pcache, dirs, files), m ∈ files0, m ∈ files, ∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty), ∀ pageno0. (pageno0 < pageno ⊃ (pageno0 ∈ content0 ↔ pageno0 ∈ content ⊕ mkcontent(m, pcache1)) ∧ content0[pageno0] = (content ⊕ mkcontent(m, pcache1))[pageno0] ;(pageno0 ∈ content0 ↔ pageno0 ∈ content) ∧ content0[pageno0] = content[pageno0] ) ⊦ content[pageno] = (content ⊕ mkcontent(m, pcache1))[pageno], datakey(m, pageno) ∈ pcache, datakey(m, pageno) ∈ pcache1