Proof step 2 from proof inv-write (previous step)

Heuristic weak unfold applied rule call right

And obtained the following new goals

• Proof step 3:

  ⊦

• Proof step 4:

  err0 = err, n0 = n, root.dir?, fids-cons(root, fs, ofh), n ≤ # buf ⊦ ⟪if n0 ≤ # buf then {choose err with pre-write(fd, buf, n0, err, user, root, fs, ofh) in err0 := err; if err0 = ESUCCESS then let fh = ofh[fd] in let f = fs[fh.fid] in choose n with n ≤ n0 in {n0 := n; f.content := splice(buf, 0, f.content, fh.pos, n0); fs[fh.fid] := f; ofh[fd].pos := fh.pos + n0} else n0 := ?; psynced := ?} else abort⟫ fids-cons(root, fs, ofh)

Rule argument

Additional information

Used simplifier rules: write: ⊦ ;