Proof step 11 from proof inv-close (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 12:

  ofh0[fd] = mkfh(fid, mode, m), root.dir?, fids-cons(root, fs, ofh0), fd ∈ ofh0 ⊦ ⟪fs := fs -- fid⟫ fids-cons(root, fs, ofh0 -- fd), fid ∈ root.fids, fid ∈ (ofh0 -- fd).fids

• Proof step 31:

  ofh0[fd] = mkfh(fid, mode, m), root.dir?, fids-cons(root, fs, ofh0), fd ∈ ofh0 ⊦ ⟪skip⟫ fids-cons(root, fs, ofh0 -- fd), ¬ fid ∈ (ofh0 -- fd).fids ∧ ¬ fid ∈ root.fids

Rule argument

Additional information