[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 139 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, zeropage, (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), m ∈ files0, n6 + min(n5, n7) ≤ # buf1, (n0 + n6) % VFS_PAGE_SIZE + min(n5, n7) ≤ VFS_PAGE_SIZE, n5 + n6 ≤ # buf1, n6 ≤ # buf1, min(n5, n7) ≤ n5, ¬ afs-cons (dirs, files0 [m, mkfile(m1, md0, # links(m, dirs), content[(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, zeropage, (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7))]) ]), ¬ (n0 + n6) / VFS_PAGE_SIZE ∈ content, ∀ 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)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 140:
⊦ afs-cons(dirs0, files0) → ( afs-cons(dirs1, files1) ↔ (∀ ino, name, n. ROOT_INO ∈ dirs0 ∧ (ino ∈ dirs0 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → dir-empty(ino, dirs0, files0)) ∧ ( ino ∈ dirs0 → ¬ ino ∈ files0 ∧ dirs0[ino].nlink = # links(ino, dirs0) ∧ dirs0[ino].nlink ≤ 1 ∧ dirs0[ino].size = # dirs0[ino].entries ∧ dirs0[ino].nsubdirs = # subdirs(ino, dirs0)) ∧ (ino ∈ files0 → ¬ ino ∈ dirs0 ∧ files0[ino].nlink = # links(ino, dirs0)) ∧ (ino ∈ dirs0 ∧ name ∈ dirs0[ino].entries → valid-ino(dirs0[ino].entries[name], dirs0, files0)) ∧ (ino ∈ files0 ∧ n ∈ files0[ino].content → valid-pagesize(ino, n, files0)) → ROOT_INO ∈ dirs1 ∧ (ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → dir-empty(ino, dirs1, files1)) ∧ ( ino ∈ dirs1 → ¬ ino ∈ files1 ∧ dirs1[ino].nlink = # links(ino, dirs1) ∧ dirs1[ino].nlink ≤ 1 ∧ dirs1[ino].size = # dirs1[ino].entries ∧ dirs1[ino].nsubdirs = # subdirs(ino, dirs1)) ∧ (ino ∈ files1 → ¬ ino ∈ dirs1 ∧ files1[ino].nlink = # links(ino, dirs1)) ∧ (ino ∈ dirs1 ∧ name ∈ dirs1[ino].entries → valid-ino(dirs1[ino].entries[name], dirs1, files1)) ∧ (ino ∈ files1 ∧ n ∈ files1[ino].content → valid-pagesize(ino, n, files1))))
Proof step 141:
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, zeropage, (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, min(n5, n7) ≤ n5, n6 ≤ # buf1, n5 + n6 ≤ # buf1, (n0 + n6) % VFS_PAGE_SIZE + min(n5, n7) ≤ VFS_PAGE_SIZE, n6 + min(n5, n7) ≤ # 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, zeropage, (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, zeropage, (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, zeropage, (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, zeropage, (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, zeropage, (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, zeropage, (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, zeropage, (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, zeropage, (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, (n0 + n6) / VFS_PAGE_SIZE ∈ content

Rule argument

spec: afs-asm name: afs-cons-reduce seq: ⊦ afs-cons(dirs0, files0) → ( afs-cons(dirs1, files1) ↔ (∀ ino, name, n. ROOT_INO ∈ dirs0 ∧ ( ino ∈ dirs0 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → dir-empty(ino, dirs0, files0)) ∧ ( ino ∈ dirs0 → ¬ ino ∈ files0 ∧ dirs0[ino].nlink = # links(ino, dirs0) ∧ dirs0[ino].nlink ≤ 1 ∧ dirs0[ino].size = # dirs0[ino].entries ∧ dirs0[ino].nsubdirs = # subdirs(ino, dirs0)) ∧ ( ino ∈ files0 → ¬ ino ∈ dirs0 ∧ files0[ino].nlink = # links(ino, dirs0)) ∧ ( ino ∈ dirs0 ∧ name ∈ dirs0[ino].entries → valid-ino (dirs0[ino].entries[name], dirs0, files0)) ∧ ( ino ∈ files0 ∧ n ∈ files0[ino].content → valid-pagesize(ino, n, files0)) → ROOT_INO ∈ dirs1 ∧ ( ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → dir-empty(ino, dirs1, files1)) ∧ ( ino ∈ dirs1 → ¬ ino ∈ files1 ∧ dirs1[ino].nlink = # links(ino, dirs1) ∧ dirs1[ino].nlink ≤ 1 ∧ dirs1[ino].size = # dirs1[ino].entries ∧ dirs1[ino].nsubdirs = # subdirs(ino, dirs1)) ∧ ( ino ∈ files1 → ¬ ino ∈ dirs1 ∧ files1[ino].nlink = # links(ino, dirs1)) ∧ ( ino ∈ dirs1 ∧ name ∈ dirs1[ino].entries → valid-ino (dirs1[ino].entries[name], dirs1, files1)) ∧ ( ino ∈ files1 ∧ n ∈ files1[ino].content → valid-pagesize(ino, n, files1)))) subst: [dirs0, files0, files1, dirs1] → [dirs, files0, files0 [m, mkfile (m1, md0, # links(m, dirs), content [(n0 + n6) / VFS_PAGE_SIZE, copy (buf1, n6, zeropage, (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7)) ]) ], dirs] flags: <all paths>

Additional information

Used terms: dirs, files0, files0 [m, mkfile (m1, md0, # links(m, dirs), content [(n0 + n6) / VFS_PAGE_SIZE, copy(buf1, n6, zeropage, (n0 + n6) % VFS_PAGE_SIZE, min(n5, n7)) ]) ], dirs