Proof step 88 from proof refine-fsync (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 89:

  files[ino1] = mkfile(m0, md0, # links(ino1, dirs), content0), root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pr(user, md0), px-parent(user, path, ROOT_INO, dirs, files), ino1 ∈ files, ROOT_INO ∈ dirs, ⌊err1⌋ , psynced → asynced0 ⊦ ∃ err0. pre-fsync(path, isdir, err0, user, root, abs-files(files), abs-of(of)) ∧ ⟨err := err0; psynced := ?⟩ ((psynced → err = ESUCCESS) ∧ err1 = err), root[path].dir?, ino1 ∈ dirs

• Proof step 95:

  files[ino1] = mkfile(m0, md0, # links(ino1, dirs), content0), err1 = ESUCCESS, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pr(user, md0), px-parent(user, path, ROOT_INO, dirs, files), ino1 ∈ files, ROOT_INO ∈ dirs, psynced → asynced0 ⊦ ∃ err0. pre-fsync(path, isdir, err0, user, root, abs-files(files), abs-of(of)) ∧ ⟨err := err0; psynced := ?⟩ ((psynced → err = ESUCCESS) ∧ err1 = err), root[path].dir?, ino1 ∈ dirs

Rule argument

Additional information