Proof step 38 from proof truncate-greater (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  VFS_PAGE_SIZE = n0 + m3 % VFS_PAGE_SIZE, files0[m0] = mkfile(m, md0, # links(m0, dirs), content0), m3 % VFS_PAGE_SIZE ≠ 0, m3 < n, afs-cons(dirs, files0), m3 / VFS_PAGE_SIZE ∈ content0, m0 ∈ files0 ⊦ [asynced := ?] ( (content0[m3 / VFS_PAGE_SIZE, fill(content0[m3 / VFS_PAGE_SIZE], zero, m3 % VFS_PAGE_SIZE, n0)] upto m3).stream to n = (content0.stream to m3) + (σ⊥ to (n - m3)))

Rule argument

Additional information

Used simplifier rules: ⊦ mkfile(m, md, m0, content).content = content; (s)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)%ino ∈ files ⊦ files[ino, af] -- ino = files -- ino; (s)% ⊦ mkfile(m, md, m0, content).size = m; (s)% ⊦ mkfile(m, md, m0, content).nlink = m0; (s)% ⊦ mkfile(m, md, m0, content).meta = md; (s)% ⊦ mkfile(m, md, m0, content).meta:= md0 = mkfile(m, md0, m0, content); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ files[ino, af][ino, af0] = files[ino, af0]; (s)% ⊦ mkfile(m, md, m0, content).size:= m1 = mkfile(m1, md, m0, content); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ files[ino, af][ino0] = (ino0 = ino ∧ ino ∈ files ⊃ af;files[ino0]); (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)