Proof step 3 from proof crash-neutral-get (previous step)

key = dentrykey(p_ino, name) ⊦ ⟨if key ∈ dcache then {dent := dcache[key]; cache_sync := true} else cache_sync := false; err := ESUCCESS⟩ true

Heuristic conditional right split applied rule if right

Proof step 4:
key = dentrykey(p_ino, name), key ∈ dcache ⊦ ⟨dent := dcache[key]; cache_sync := true; err := ESUCCESS⟩ true
Proof step 7:
key = dentrykey(p_ino, name) ⊦ ⟨cache_sync := false; err := ESUCCESS⟩ true, key ∈ dcache