Proof step 12 from proof eq-io-lookup (previous step)

Heuristic conditional left split applied rule or split left

And obtained the following new goals

• Proof step 13:

  ⟨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}⟩ (dent = old_dent ∧ err = err1), asynced ↔ asynced0, dirs1[pageno] = mkdir(m, md, m0, m1, entries), dirs = dirs1, files = files1, p_ino = pageno, pageno ∈ dirs1, links(pageno, dirs1) ≠ ∅ ∨ pageno = ROOT_INO ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0⟩ (dent = old_dent ∧ err = err1), ⟨if dent.name ∈ entries then {dent := mkdentry(dent.name, entries[dent.name]); err := ESUCCESS} else {dent := negdentry(dent.name); err := ENOENT}⟩ (dent = old_dent ∧ err = err1)

• Proof step 24:

  ⟨fail#(; ; err)⟩ (dent = old_dent ∧ err = err1), asynced ↔ asynced0, dirs1[pageno] = mkdir(m, md, m0, m1, entries), dirs = dirs1, files = files1, p_ino = pageno, pageno ∈ dirs1, links(pageno, dirs1) ≠ ∅ ∨ pageno = ROOT_INO ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0⟩ (dent = old_dent ∧ err = err1), ⟨if dent.name ∈ entries then {dent := mkdentry(dent.name, entries[dent.name]); err := ESUCCESS} else {dent := negdentry(dent.name); err := ENOENT}⟩ (dent = old_dent ∧ err = err1)

Rule argument

Additional information