Proof step 3 from proof crash-neutral-set-status (previous step)

key = datakey(ino, pageno) ⊦ ⟨if key ∈ pcache then {pe := pcache[key]; pe := mkpentry(boolvar, pe.page); pcache[key] := pe} else err := EFAIL⟩ true

Heuristic conditional right split applied rule if right

Proof step 4:
key = datakey(ino, pageno), key ∈ pcache ⊦ ⟨pe := pcache[key]; pe := mkpentry(boolvar, pe.page); pcache[key] := pe⟩ true
Proof step 7:
key = datakey(ino, pageno) ⊦ ⟨err := EFAIL⟩ true, key ∈ pcache