[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 37 from proof refine-unlink (previous step)

cache_files[cache_dirs[m].entries[str]] = mkfile(m5, md1, m7, content), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, c_inode = mkinode(cache_dirs[m].entries[str], md0, false, ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[m].entries[str]].nlink, 0, m6), dent = mkdentry(str, cache_dirs[m].entries[str]), err = err0, m0 = cache_dirs[m].nlink, m1 = cache_dirs[m].nsubdirs, m2 = cache_dirs[m].size, m3 = cache_dirs[m].entries[str], m4 = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[m].entries[str]].nlink, m7 = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[m].entries[str]].nlink, p_inode = mkinode(m, md, true, cache_dirs[m].nlink, cache_dirs[m].nsubdirs, cache_dirs[m].size), 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), cache_dirs[m].entries[str] ∈ cache_files, str ∈ cache_dirs[m].entries, m ∈ cache_dirs, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ [cache_unlink#(; p_inode, c_inode, dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)] ( icache-cons(cache_icache, cache_dirs, cache_files) ∧ dcache-cons(cache_dcache, cache_dirs, cache_files) ∧ pcache-cons(cache_pcache, cache_dirs, cache_files) ∧ synced(cache_dirs, cache_icache, cache_pcache) ∧ (cache_sync → synced(cache_files, cache_icache, cache_pcache)) ∧ afs-cons(cache_dirs, cache_files) → ⟨dent0 := mkdentry(str, m3); p_inode0 := mkinode(m, md, true, m0, m1, m2); p_inode1 := mkinode(m3, md0, false, m4, 0, m6); afs_unlink#(; p_inode0, p_inode1, dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err0))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 38:
# links(cache_dirs[m].entries[str], cache_dirs) = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[m].entries[str]].nlink, cache_files[cache_dirs[m].entries[str]] = mkfile(m5, md1, ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[m].entries[str]].nlink, content), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, c_inode = mkinode(cache_dirs[m].entries[str], md0, false, ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[m].entries[str]].nlink, 0, m6), dent = mkdentry(str, cache_dirs[m].entries[str]), err = err0, m0 = cache_dirs[m].nlink, m1 = cache_dirs[m].nsubdirs, m2 = cache_dirs[m].size, m3 = cache_dirs[m].entries[str], m4 = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[cache_dirs[m].entries[str]].nlink, p_inode = mkinode(m, md, true, cache_dirs[m].nlink, cache_dirs[m].nsubdirs, cache_dirs[m].size), 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_dirs, str ∈ cache_dirs[m].entries, cache_dirs[m].entries[str] ∈ cache_files, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ [cache_unlink#(; p_inode, c_inode, dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)] ( icache-cons(cache_icache, cache_dirs, cache_files) ∧ dcache-cons(cache_dcache, cache_dirs, cache_files) ∧ pcache-cons(cache_pcache, cache_dirs, cache_files) ∧ synced(cache_dirs, cache_icache, cache_pcache) ∧ (cache_sync → synced(cache_files, cache_icache, cache_pcache)) ∧ afs-cons(cache_dirs, cache_files) → ⟨dent0 := mkdentry(str, m3); p_inode0 := mkinode(m, md, true, m0, m1, m2); p_inode1 := mkinode(m3, md0, false, m4, 0, m6); afs_unlink#(; p_inode0, p_inode1, dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err0))

Rule argument

Additional information

Used simplifier rules: afs-cons-file-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ files ∧ files[ino] = mkfile(m, md, n, content) → # links(ino, dirs) = n; (forward) from specification afs-base