| ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries1[str0]] = mkfile(m12, md3, # links(entries1[str0], cache_dirs), content), cache_dirs[m] = mkdir(m0, md, # links(m, cache_dirs), m3, entries1), cache_files[entries1[str0]] = mkfile(m1, md5, # links(entries1[str0], cache_dirs), content2), 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), entries1[str0] ∈ cache_files, m ∈ cache_dirs, str0 ∈ entries1, ⌊err1⌋ , cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟨asynced := ?⟩ (err1 = err1 ∧ (asynced ↔ asynced2)), ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ (err1 = err ∧ (asynced ↔ asynced2)), entries1[str0] ∈ cache_dirs |