| afs_asynced ↔ cache_asynced, asynced1 ↔ false, asynced0 ↔ asynced3, asynced4 ↔ asynced2, asynced ↔ asynced5, cache_files[m] = mkfile(m3, md1, # links(m, cache_dirs), content0), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m] = mkfile(m0, md0, # links(m, cache_dirs), content), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, ¬ asynced2, ¬ asynced3, buf-opt = none, err = ESUCCESS, ino = m, inode = mkinode(m, md, false, # links(m, cache_dirs), 0, m2), key = datakey(ino, pageno0), m1 = # links(m, cache_dirs), pageno = m2 / VFS_PAGE_SIZE, pageno0 = m2 / VFS_PAGE_SIZE, pcache = cache_pcache, afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), 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, datakey(m, m2 / VFS_PAGE_SIZE) ∈ cache_pcache, cache_sync → synced(cache_files, cache_icache, cache_pcache) ⊦ ⟪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, m2, 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, key ∈ pcache |