| (entries[str] = m ⊃ mkdir(m0, md2, # links(entries[str], cache_dirs), m1, entries -- str) ;mkdir(m2, md1, # links(entries[str], cache_dirs), m4, ∅) ) = mkdir(m3, md, m5, m6, entries0), cache_dirs[entries[str]] = mkdir(m2, md1, # links(entries[str], cache_dirs), m4, ∅), cache_dirs[m] = mkdir(m0 + 1, md2, # links(m, cache_dirs), m1 + 1, entries), 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), str ∈ entries, m ∈ cache_dirs, entries[str] ∈ cache_dirs, 1 ≤ m5, ⌊err1⌋ , cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ ((asynced ↔ asynced0) ∧ err1 = err), entries[str] = ROOT_INO, m5 = 0 |
(entries[str] = m ⊃ mkdir(m0, md2, # links(entries[str], cache_dirs), m1, entries -- str) ;mkdir(m2, md1, # links(entries[str], cache_dirs), m4, ∅) ) = mkdir(m3, md, m5, m6, entries0), cache_dirs[m] = mkdir(m0 + 1, md2, # links(m, cache_dirs), m1 + 1, entries), cache_dirs[entries[str]] = mkdir(m2, md1, # links(entries[str], cache_dirs), m4, ∅), entries[str] ≠ ROOT_INO, m5 ≠ 0, 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), entries[str] ∈ cache_dirs, m ∈ cache_dirs, str ∈ entries, 1 ≤ m5, ⌊err1⌋ , cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ ((asynced ↔ asynced0) ∧ err1 = err)