[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 67 from proof write-loop-term (previous step)

VFS_PAGE_SIZE = n7 + (n0 + n6) % VFS_PAGE_SIZE, files0[m] = mkfile(m1, md0, # links(m, dirs), content), err = ESUCCESS, files = files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ], inode = mkinode(m, md, false, # links(m, dirs), 0, m2), ¬ isdir, n = n6 + min(n5, n7), n1 = n5 + n0 + n6, afs-cons(dirs, files0), m ∈ files0, (n0 + n6) / VFS_PAGE_SIZE ∈ content, min(n5, n7) ≤ n5, n6 + min(n5, n7) ≤ # buf1, (n0 + n6) % VFS_PAGE_SIZE + min(n5, n7) ≤ VFS_PAGE_SIZE, n5 + n6 ≤ # buf1, n6 ≤ # buf1, ∃ ino, name, n. ¬ ( ROOT_INO ∈ dirs ∧ (ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dir-empty(ino, dirs, files0)) ∧ ( ino ∈ dirs → ¬ ino ∈ files0 ∧ dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs)) ∧ (ino ∈ files0 → ¬ ino ∈ dirs ∧ files0[ino].nlink = # links(ino, dirs)) ∧ (ino ∈ dirs ∧ name ∈ dirs[ino].entries → valid-ino(dirs[ino].entries[name], dirs, files0)) ∧ (ino ∈ files0 ∧ n ∈ files0[ino].content → valid-pagesize(ino, n, files0)) → ROOT_INO ∈ dirs ∧ ( ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dir-empty (ino, dirs, files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ])) ∧ ( ino ∈ dirs → ¬ ino ∈ files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ] ∧ dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs)) ∧ ( ino ∈ files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ] → ¬ ino ∈ dirs ∧ files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ] [ino ] .nlink = # links(ino, dirs)) ∧ ( ino ∈ dirs ∧ name ∈ dirs[ino].entries → valid-ino (dirs[ino].entries[name], dirs, files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ])) ∧ ( ino ∈ files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ] ∧ n ∈ files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ] [ino ] .content → valid-pagesize (ino, n, files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ]))), ∀ n2, n3, n4, files, m, m1, md0, dirs, content, inode, md, m2, isdir, buf, err, asynced. n2 - n3 + n4 < n5 → files[m] = mkfile(m1, md0, # links(m, dirs), content) ∧ inode = mkinode(m, md, false, # links(m, dirs), 0, m2) ∧ ¬ isdir ∧ afs-cons(dirs, files) ∧ m ∈ files ∧ n4 ≤ # buf ∧ n3 + n4 ≤ n2 ∧ n2 ≤ # buf + n3 → ⟪while err = ESUCCESS ∧ ¬ isdir do vfs_write_block#(n3, inode, buf, n2, dirs; n4, isdir, err, files, asynced)⟫ (m ∈ files ∧ # links(m, dirs) = files[m].nlink) ⊦ ⟪while err = ESUCCESS ∧ ¬ isdir do vfs_write_block#(n0, inode, buf1, n1, dirs; n, isdir, err, files, asynced)⟫ (m ∈ files ∧ # links(m, dirs) = files[m].nlink), min(n5, n7) = 0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 68:
VFS_PAGE_SIZE = n7 + (n0 + n6) % VFS_PAGE_SIZE, files0[m] = mkfile(m1, md0, # links(m, dirs), content), err = ESUCCESS, files = files0 [m, mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ], inode = mkinode(m, md, false, # links(m, dirs), 0, m2), ¬ isdir, n = n6 + min(n5, n7), n1 = n5 + n0 + n6, min(n5, n7) ≠ 0, afs-cons(dirs, files0), ROOT_INO ∈ dirs, (n0 + n6) / VFS_PAGE_SIZE ∈ content, m ∈ files0, n6 ≤ # buf1, n5 + n6 ≤ # buf1, (n0 + n6) % VFS_PAGE_SIZE + min(n5, n7) ≤ VFS_PAGE_SIZE, n6 + min(n5, n7) ≤ # buf1, min(n5, n7) ≤ n5, ino ∈ files0 → ¬ ino ∈ dirs ∧ files0[ino].nlink = # links(ino, dirs), ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dirs[ino].entries = ∅, ino ∈ dirs → dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs), ino ∈ dirs ∧ name ∈ dirs[ino].entries → dirs[ino].entries[name] ∈ dirs ∨ dirs[ino].entries[name] ∈ files0, ino ∈ files0 ∧ n2 ∈ files0[ino].content → # files0[ino].content[n2] = VFS_PAGE_SIZE, ∀ n2, n3, n4, files, m, m1, md0, dirs, content, inode, md, m2, isdir, buf, err, asynced. n2 - n3 + n4 < n5 → files[m] = mkfile(m1, md0, # links(m, dirs), content) ∧ inode = mkinode(m, md, false, # links(m, dirs), 0, m2) ∧ ¬ isdir ∧ afs-cons(dirs, files) ∧ m ∈ files ∧ n4 ≤ # buf ∧ n3 + n4 ≤ n2 ∧ n2 ≤ # buf + n3 → ⟪while err = ESUCCESS ∧ ¬ isdir do vfs_write_block#(n3, inode, buf, n2, dirs; n4, isdir, err, files, asynced)⟫ (m ∈ files ∧ # links(m, dirs) = files[m].nlink) ⊦ ⟪while err = ESUCCESS ∧ ¬ isdir do vfs_write_block#(n0, inode, buf1, n1, dirs; n, isdir, err, files, asynced)⟫ (m ∈ files ∧ # links(m, dirs) = files[m].nlink), ( ino ∈ files0 → ¬ ino ∈ dirs ∧ (ino = m ⊃ mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ;files0[ino] ) .nlink = # links(ino, dirs)) ∧ ( ino ∈ files0 ∧ n2 ∈ (ino = m ⊃ mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ;files0[ino] ) .content → # (ino = m ⊃ mkfile (m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, content[(n0 + n6) / VFS_PAGE_SIZE], (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ;files0[ino] ) .content [n2 ] = VFS_PAGE_SIZE)

Rule argument

Additional information

Used simplifier rules: ⊦ files[ino, af][ino0] = (ino0 = ino ∧ ino ∈ files ⊃ af;files[ino0]); (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)% ⊦ afs-cons(dirs, files) → ROOT_INO ∈ dirs; (ss)%⊦ valid-pagesize(ino, n, files) ↔ # files[ino].content[n] = VFS_PAGE_SIZE; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)% ⊦ dir-empty(ino, dirs, files) ↔ dirs[ino].entries = ∅; (s)