Proof step 41 from proof refine-write (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 42:

  files0 -- m2 = files -- m2, (content.stream to m).buf = splice(buf, 0, (content0.stream to m1).buf, m3, n1), files[m2] = mkfile(m1, md, # links(m2, dirs), content0), files0[m2] = mkfile(m, md, m0, content), of[fd] = mkfile(m2, mode, m3), root.dir?, dom of < ino, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), m2 ∈ files0, fd ∈ of, m2 ∈ files, n1 ≤ n0, n0 ≤ # buf, n1 ≤ # buf, finp(content0.stream) → ⌜m1⌝ < # content0.stream ∨ ⌜m1⌝ = # content0.stream, psynced → asynced, mode = MODE_W ∨ mode = MODE_RW ⊦ ⟨psynced := ?⟩ ( abs-of(of[fd, mkfile(m2, mode, m3 + n1)]) = abs-of(of[fd, of[fd].pos:= (m3 + n1)]) ∧ abs-files(files)[⌜m2⌝ , mkfile(md, splice(buf, 0, (content0.stream to m1).buf, m3, n1))] = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n1)

Rule argument

Additional information