Proof step 164 from proof refine-read (previous step)

Heuristic dl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 165:

  abs-files(files)[⌜m3⌝ ] = mkfile(md0, buf), of[fd] = mkfile(m3, mode0, m4), files[m3] = mkfile(m1, md, # links(m3, dirs), content), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, # links(m3, dirs), 0, m1), buf0, buf1, 0, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, # links(m3, dirs), 0, m1), buf0, buf0, 0, dirs, files), fd ∈ of, m3 ∈ files, n ≤ n0, of[fd].pos + n ≤ files[of[fd].ino].size, m4 ≤ m1, n0 ≤ # buf0, psynced → asynced ⊦ ∃ n1. n1 ≤ n0 ∧ of[fd].pos + n1 ≤ files[of[fd].ino].size ∧ ⟨n0 := n1; buf0 := copy(buf, m4, buf0, 0, n0); ofh := abs-of(of[fd, mkfile(m3, mode0, m4 + n0)])⟩ (ofh = abs-of(of[fd, of[fd].pos:= m4]) ∧ (psynced → asynced) ∧ buf1 = buf0 ∧ 0 = n0), mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW

• Proof step 181:

  abs-files(files)[⌜m3⌝ ] = mkfile(md0, buf), of[fd] = mkfile(m3, mode0, m4), files[m3] = mkfile(m1, md, # links(m3, dirs), content), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, # links(m3, dirs), 0, m1), buf0, buf1, 0, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, # links(m3, dirs), 0, m1), buf0, buf0, 0, dirs, files), fd ∈ of, m3 ∈ files, m4 ≤ m1, n0 ≤ # buf0, psynced → asynced ⊦ ⟨n0 := 0⟩ (abs-of(of) = abs-of(of[fd, of[fd].pos:= m4]) ∧ (psynced → asynced) ∧ buf1 = buf0 ∧ 0 = n0), ∃ n1. n1 ≤ n0 ∧ of[fd].pos + n1 ≤ files[of[fd].ino].size ∧ ⟨n0 := n1; buf0 := copy(buf, m4, buf0, 0, n0); ofh := abs-of(of[fd, mkfile(m3, mode0, m4 + n0)])⟩ (ofh = abs-of(of[fd, of[fd].pos:= m4]) ∧ (psynced → asynced) ∧ buf1 = buf0 ∧ 0 = n0), mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW

Rule argument

Additional information