Proof step 192 from proof fsync-inode-inv (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 193:

  asynced0 ↔ false, files[m] = mkfile(m0, md0, # links(m, dirs), content), err = ESUCCESS, ino = m, ino0 = m, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m ∈ files ⊦ ⟪asynced := false; icache_set_status#(ino, asynced; err, icache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ inode.ino ∈ files ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory), ino0 ∈ icache

• Proof step 200:

  asynced0 ↔ false, files[m] = mkfile(m0, md0, # links(m, dirs), content), ino = m, ino0 = m, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m ∈ files ⊦ ⟪skip⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ inode.ino ∈ files ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory), err = ESUCCESS, ino0 ∈ icache

Rule argument

Additional information