[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 173 from proof refine-write_inode (previous step)

(ino = m3 ⊃ mkfile(m2, md, # links(m3, cache_dirs), content0);cache_files[ino]) = mkfile(m8, md4, m9, content1), cache_icache[m3] = mkientry(boolvar, mkinode(m3, md2, false, # links(m3, cache_dirs), 0, m6)), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content), cache_files[m3] = mkfile(m1, md1, # links(m3, cache_dirs), content0), cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2))][ino] = mkientry(boolvar0, mkinode(m, md3, true, m4, m5, m7)), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), synced(cache_files, cache_icache, cache_pcache), m3 ∈ cache_icache, m3 ∈ cache_files, ino ∈ cache_files, ino ∈ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2))], ¬ boolvar → mkinode(m3, md2, false, # links(m3, cache_dirs), 0, m6) = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m1), ∀ ino0. ino0 ∈ cache_icache → cache_icache[ino0].inode.ino = ino0 ∧ (cache_icache[ino0].dirty ⊃ cache_icache[ino0].inode.ino ∈ cache_files ∧ cache_icache[ino0].inode.nlink = cache_files[cache_icache[ino0].inode.ino].nlink ∧ cache_icache[ino0].inode.nsubdirs = 0 ∧ ¬ cache_icache[ino0].inode.directory ; (ino0 ∈ cache_dirs ∨ ino0 ∈ cache_files) ∧ cache_icache[ino0].inode = (cache_icache[ino0].inode.ino ∈ cache_dirs ⊃ mkinode (cache_icache[ino0].inode.ino, cache_dirs[cache_icache[ino0].inode.ino].meta, true, cache_dirs[cache_icache[ino0].inode.ino].nlink, cache_dirs[cache_icache[ino0].inode.ino].nsubdirs, cache_dirs[cache_icache[ino0].inode.ino].size) ;mkinode (cache_icache[ino0].inode.ino, cache_files[cache_icache[ino0].inode.ino].meta, false, cache_files[cache_icache[ino0].inode.ino].nlink, 0, cache_files[cache_icache[ino0].inode.ino].size) ) ) ⊦ (ino = m3 ⊃ mkfile(m2, md, # links(m3, cache_dirs), content);((cache_files ⊕ cache_pcache) ⊕ cache_icache)[ino]) = mkfile(m8, md4, m9, content1 ⊕ mkcontent(ino, cache_pcache)), ino = m3

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 174:
cache_files[ino] = mkfile(m8, md4, # links(ino, cache_dirs), content1), cache_icache[m3] = mkientry(boolvar, mkinode(m3, md2, false, # links(m3, cache_dirs), 0, m6)), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content), cache_files[m3] = mkfile(m1, md1, # links(m3, cache_dirs), content0), cache_icache[ino] = mkientry(boolvar0, mkinode(m, md3, true, m4, m5, m7)), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), synced(cache_files, cache_icache, cache_pcache), ino ∈ cache_icache, m3 ∈ cache_icache, m3 ∈ cache_files, ino ∈ cache_files, ¬ boolvar → mkinode(m3, md2, false, # links(m3, cache_dirs), 0, m6) = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m1), ∀ ino0. ino0 ∈ cache_icache → cache_icache[ino0].inode.ino = ino0 ∧ (cache_icache[ino0].dirty ⊃ cache_icache[ino0].inode.ino ∈ cache_files ∧ cache_icache[ino0].inode.nlink = cache_files[cache_icache[ino0].inode.ino].nlink ∧ cache_icache[ino0].inode.nsubdirs = 0 ∧ ¬ cache_icache[ino0].inode.directory ; (ino0 ∈ cache_dirs ∨ ino0 ∈ cache_files) ∧ cache_icache[ino0].inode = (cache_icache[ino0].inode.ino ∈ cache_dirs ⊃ mkinode (cache_icache[ino0].inode.ino, cache_dirs[cache_icache[ino0].inode.ino].meta, true, cache_dirs[cache_icache[ino0].inode.ino].nlink, cache_dirs[cache_icache[ino0].inode.ino].nsubdirs, cache_dirs[cache_icache[ino0].inode.ino].size) ;mkinode (cache_icache[ino0].inode.ino, cache_files[cache_icache[ino0].inode.ino].meta, false, cache_files[cache_icache[ino0].inode.ino].nlink, 0, cache_files[cache_icache[ino0].inode.ino].size) ) ) ⊦ ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[ino] = mkfile(m8, md4, # links(ino, cache_dirs), content1 ⊕ mkcontent(ino, cache_pcache)), ino = m3

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% ⊦ ino ≠ ino0 → (ino ∈ icache[ino0, ie] ↔ ino ∈ icache); (s)% ⊦ ino ≠ ino0 → icache[ino0, ie][ino] = icache[ino]; (s)