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

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 79:

  files[m] = mkfile(m1, md, # links(m, dirs), content), of0[fd] = mkfile(m, mode, m0), 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), fids-cons(root, abs-files(files), abs-of(of0)), of-cons(of0, dirs, files), of-cons(of0 -- fd, dirs, files), fd ∈ ofh, m ∈ files, fd ∈ of0, 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) ∧ (psynced → asynced) ∧ ESUCCESS = err0), # links(m, dirs) = 0, links(m, dirs) = ∅, m = ROOT_INO, is-open(m, of0 -- fd)

• Proof step 85:

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

Rule argument

Additional information