Proof step 58 from proof refine-close (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 59:

  # links(m, dirs) = 0, of0[fd] = mkfile(m, mode, m0), files[m] = mkfile(m1, md, 0, content), err0 = ESUCCESS, fid = ofh[fd].fid, fs = abs-files(files), ofh = abs-of(of0), root.dir?, dom of0 < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), afs-cons(dirs, files -- m), fids-cons(root, abs-files(files), abs-of(of0)), of-cons(of0 -- fd, dirs, files -- m), of-cons(of0, dirs, files), fd ∈ ofh, fd ∈ of0, m ∈ files, psynced → asynced ⊦ ⟨ofh := ofh -- fd; if ¬ fid ∈ ofh.fids ∧ ¬ fid ∈ root.fids then fs := fs -- fid⟩ (ofh = abs-of(of0 -- fd) ∧ fs = abs-files(files -- m) ∧ (psynced → asynced) ∧ ESUCCESS = err0), m = ROOT_INO, is-open(m, of0 -- fd)

• Proof step 66:

  # links(m, dirs) = 0, of0[fd] = mkfile(m, mode, m0), files[m] = mkfile(m1, md, 0, content), err0 = ESUCCESS, fs = abs-files(files), ofh = abs-of(of0), root.dir?, dom of0 < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), afs-cons(dirs, files -- m), fids-cons(root, abs-files(files), abs-of(of0)), of-cons(of0 -- fd, dirs, files -- m), of-cons(of0, dirs, files), fd ∈ of0, m ∈ files, psynced → asynced ⊦ m = ROOT_INO, is-open(m, of0 -- fd), fd ∈ ofh

Rule argument

Additional information