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

cache_files[m3] = mkfile(m1, md1, # links(m3, cache_dirs), content0), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content), cache_icache[m3] = mkientry(boolvar, mkinode(m3, md2, boolvar0, m4, m5, m6)), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_files, cache_icache, cache_pcache), synced(cache_dirs, cache_icache, cache_pcache), ino ∈ cache_files, m3 ∈ cache_files, m3 ∈ cache_icache, (boolvar ⊃ m4 = # links(m3, cache_dirs) ∧ m5 = 0 ∧ ¬ boolvar0 ;mkinode(m3, md2, boolvar0, m4, m5, 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]) = ( (cache_files[m3, mkfile(m2, md, # links(m3, cache_dirs), content0)] ⊕ cache_pcache) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, boolvar0, m4, m5, m2))] )[ino ]

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

Proof step 159:
cache_icache[m3] = mkientry(boolvar, mkinode(m3, md2, boolvar0, m4, m5, 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), m4 = # links(m3, cache_dirs), 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, (boolvar ⊃ m4 = # links(m3, cache_dirs) ∧ m5 = 0 ∧ ¬ boolvar0 ;mkinode(m3, md2, boolvar0, m4, m5, 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]) = ( (cache_files[m3, mkfile(m2, md, # links(m3, cache_dirs), content0)] ⊕ cache_pcache) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, boolvar0, m4, m5, m2))] )[ino ]

Rule argument

fma: m4 = # links(m3, cache_dirs)

Additional information

Used simplifier rules: ⊦ mkinode(m, md, boolvar, m0, m1, m2) = mkinode(m3, md0, boolvar0, m4, m5, m6) ↔ m = m3 ∧ md = md0 ∧ (boolvar ↔ boolvar0) ∧ m0 = m4 ∧ m1 = m5 ∧ m2 = m6; (ws) Used formulas: m4 = # links(m3, cache_dirs)