Proof step 85 from proof inv-fsync (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 86:

  asynced0 ↔ true, files0[m] = mkfile(m0, md0, # links(m, dirs), content), files1[m] = mkfile(m1, md1, # links(m, dirs), content0), files = files0, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), afs-cons(dirs, files0), afs-cons(dirs, files1), dcache-cons(dcache, dirs, files0), dcache-cons(dcache, dirs, files1), icache-cons(icache, dirs, files0), icache-cons(icache, dirs, files1), pcache-cons(pcache0, dirs, files0), pcache-cons(pcache, dirs, files1), synced(dirs, icache, pcache0), synced(dirs, icache, pcache), valid-file-inode(inode, dirs, files), m ∈ files0, m ∈ files1 ⊦ ⟪fail_or_success#(; ; err); choose bv with true in asynced := bv⟫ true

• Proof step 114:

  asynced0 ↔ true, files0[m] = mkfile(m0, md0, # links(m, dirs), content), files1[m] = mkfile(m1, md1, # links(m, dirs), content0), files = files0, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), afs-cons(dirs, files0), afs-cons(dirs, files1), dcache-cons(dcache, dirs, files0), dcache-cons(dcache, dirs, files1), icache-cons(icache, dirs, files0), icache-cons(icache, dirs, files1), pcache-cons(pcache0, dirs, files0), pcache-cons(pcache, dirs, files1), synced(dirs, icache, pcache0), synced(dirs, icache, pcache), m ∈ files0, m ∈ files1 ⊦ ⟪abort⟫ true, valid-file-inode(inode, dirs, files)

Rule argument

Additional information