Proof step 37 from proof truncate-smaller (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

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

Rule argument

Additional information

Used simplifier rules: ⊦ (content upto m).stream to m = content.stream to m; (s)% ⊦ 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)