| asynced ↔ asynced2, asynced0 ↔ asynced1, ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m] = mkfile(m0, md0, # links(m, cache_dirs), content), cache_files[m] = mkfile(m3, md1, # links(m, cache_dirs), content0), ¬ asynced1, ¬ asynced2, err = ESUCCESS, ino = m, key = datakey(ino, pageno), pageno = m2 / VFS_PAGE_SIZE, pcache = cache_pcache, afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), m ∈ cache_files, key ∈ pcache, cache_sync → synced(cache_files, cache_icache, cache_pcache) ⊦ ⟪asynced := pcache[key].dirty; pageno := m2 / VFS_PAGE_SIZE; asynced1 := true; if err = ESUCCESS ∧ asynced1 then pcache_get#(m, pageno, cache_pcache; asynced1, buf, err); buf-opt := none; if err = ESUCCESS ∧ asynced1 then buf-opt := some(buf); size := m2; inode := mkinode(m, md, false, # links(m, cache_dirs), 0, m2); afs_files := (cache_files ⊕ cache_pcache) ⊕ cache_icache; afs_dirs := cache_dirs; afs_asynced := cache_asynced; asynced := asynced5; m1 := # links(m, cache_dirs); if err = ESUCCESS then afs_truncate#(n, pageno; buf-opt, inode, asynced, err, cache_dirs, cache_files, cache_asynced); if err = ESUCCESS then let asynced0 = false in {icache_set#(inode, asynced0; err, cache_icache); pcache_truncate#(inode.ino, size, n; err, cache_pcache); if asynced then pcache_set#(inode.ino, pageno, buf-opt.buf, asynced0; err, cache_pcache)}; if ¬ asynced ∨ err ≠ ESUCCESS then buf-opt := none⟫ ⟨buf-opt0 := none; inode0 := mkinode(m, md, false, m1, 0, m2); afs_truncate#(n, m2 / VFS_PAGE_SIZE; buf-opt0, inode0, asynced5, err0, afs_dirs, afs_files, afs_asynced)⟩ ( afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced) ∧ buf-opt = buf-opt0 ∧ inode = inode0 ∧ (asynced ↔ asynced5) ∧ err = err0), VFS_PAGE_SIZE = 0, datakey(m, m2 / VFS_PAGE_SIZE) ∈ cache_pcache |