Proof step 21 from proof inv-lookup (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 22:

  asynced ↔ asynced0, err = ESUCCESS, name = dent.name, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), p_ino ∈ dirs, asynced1 → synced(files, icache, pcache), links(p_ino, dirs) ≠ ∅ ∨ p_ino = ROOT_INO ⊦ ⟪if dent.name ∈ dirs[p_ino].entries then {dent := mkdentry(dent.name, dirs[p_ino].entries[dent.name]); err := ESUCCESS} else {dent := negdentry(dent.name); err := ENOENT}; if err = ESUCCESS then dcache_set#(p_ino, name, dent; err, dcache)⟫ dcache-cons(dcache, dirs, files), dentrykey(p_ino, dent.name) ∈ dcache

• Proof step 49:

  asynced ↔ asynced0, err = ESUCCESS, name = dent.name, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), p_ino ∈ dirs, asynced1 → synced(files, icache, pcache), links(p_ino, dirs) ≠ ∅ ∨ p_ino = ROOT_INO ⊦ ⟪fail#(; ; err); if err = ESUCCESS then dcache_set#(p_ino, name, dent; err, dcache)⟫ dcache-cons(dcache, dirs, files), dentrykey(p_ino, dent.name) ∈ dcache

Rule argument

Additional information