Proof step 327 from proof refine-write_inode (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 328:

  cache_icache[m3] = mkientry(boolvar, mkinode(m3, md2, boolvar0, # links(m3, cache_dirs), 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), 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), m3 ∈ cache_files, m3 ∈ cache_icache, (boolvar ⊃ m5 = 0 ∧ ¬ boolvar0 ;mkinode(m3, md2, boolvar0, # links(m3, cache_dirs), m5, m6) = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m1) ) ⊦ ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m3, mkfile(m2, md, # links(m3, cache_dirs), content)] = (cache_files ⊕ cache_pcache) ⊕ cache_icache[m3, mkientry(true, mkinode(m3, md, boolvar0, # links(m3, cache_dirs), m5, m2))]

Rule argument

Additional information