Proof step 1 from proof inv-read (conclusion)

Heuristic weak unfold applied rule call right

And obtained the following new goals

• Proof step 2:

  ⊦

• Proof step 3:

  err0 = err, n0 = n, root.dir?, fids-cons(root, fs, ofh), n ≤ # buf ⊦ ⟪if n0 ≤ # buf then {choose err with pre-read(fd, 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 ∧ fh.pos + n ≤ # f.content in {n0 := n; buf := copy(f.content, fh.pos, buf, 0, n0); ofh[fd].pos := fh.pos + n0} ifnone n0 := 0 else n0 := ?} else abort⟫ fids-cons(root, fs, ofh)

Rule argument

Additional information

Used simplifier rules: read: ⊦ ;