| # links (entries[str], cache_dirs [m8, (m8 = m14 ⊃ mkdir(m0 + 1, md6, m4, m6, entries1[str0, entries[str]]) ;mkdir(m1, md4, cache_dirs[m8].nlink, cache_dirs[m8].nsubdirs, entries -- str) ) .meta:= md0 ] [m14, (m14 = m8 ⊃ mkdir(m0 + 1, md0, m4, m6, entries1[str0, entries[str]]);mkdir(m0 + 1, md6, m4, m6, entries1[str0, entries[str]])).meta:= md5 ]) = # links(entries[str], cache_dirs), # links(m8, cache_dirs) = cache_dirs[m8].nlink, # links(m14, cache_dirs) = cache_dirs[m14].nlink, m1 + 1 = cache_dirs[m8].size, (m14 = m8 ⊃ mkdir(m1, md4, cache_dirs[m8].nlink, cache_dirs[m8].nsubdirs, entries -- str);cache_dirs[m14]) = mkdir(m0, md6, m4, m6, entries1), (m8 = m14 ⊃ mkdir(m0 + 1, md5, m4, m6, entries1[str0, entries[str]]);mkdir(m1, md0, cache_dirs[m8].nlink, cache_dirs[m8].nsubdirs, entries -- str)) = mkdir(m, md, m12, m13, entries0), asynced1 ↔ false, asynced0 ↔ false, cache_dirs[m8] = mkdir(m1 + 1, md4, cache_dirs[m8].nlink, cache_dirs[m8].nsubdirs, entries), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries[str]] = mkfile(m9, md2, # links(entries[str], cache_dirs), content), cache_dirs[m14] = mkdir(cache_dirs[m14].size, md7, cache_dirs[m14].nlink, cache_dirs[m14].nsubdirs, entries2), cache_files[entries[str]] = mkfile(m2, md3, # links(entries[str], cache_dirs), content0), entries[str] = cache_dirs[m8].entries[str], dirs = dirs0[old_ino, dirs0[old_ino].size:= (dirs0[old_ino].size - 1)], dirs0 = cache_dirs[old_ino, cache_dirs[old_ino].entries:= (cache_dirs[old_ino].entries -- mkdentry(str, entries[str]).name)], new_ino = m14, old_dent = mkdentry(str, entries[str]), old_ino = m8, afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), afs-cons (cache_dirs [m8, (m8 = m14 ⊃ mkdir(m0 + 1, md6, m4, m6, entries1[str0, entries[str]]) ;mkdir(m1, md4, cache_dirs[m8].nlink, cache_dirs[m8].nsubdirs, entries -- str) ) .meta:= md0 ] [m14, (m14 = m8 ⊃ mkdir(m0 + 1, md0, m4, m6, entries1[str0, entries[str]]);mkdir(m0 + 1, md6, m4, m6, entries1[str0, entries[str]])).meta:= md5 ], 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), str ∈ entries, entries[str] ∈ cache_files, m14 ∈ cache_dirs, m8 ∈ cache_dirs, str ∈ cache_dirs[m8].entries, dirs0[old_ino].size ≥ 1, cache_sync → synced(cache_files, cache_icache, cache_pcache), m14 = m8 → md5 = md0, links(m8, cache_dirs) ≠ ∅ ∨ m8 = ROOT_INO, links(m14, cache_dirs) ≠ ∅ ∨ m14 = ROOT_INO ⊦ old_dent.dentry?, str0 ∈ cache_dirs[m14].entries, entries[str] ∈ cache_dirs, str0 ∈ entries2 |
Used simplifier rules: ⊦ mkdentry(str, m).dentry?; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ (ad.entries:= entries).size = ad.size; (s)% ⊦ dirs[ino, ad][ino0] = (ino0 = ino ∧ ino ∈ dirs ⊃ ad;dirs[ino0]); (s)% ⊦ mkdentry(str, m).name = str; (s)