[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 14 from proof write-inv-strong-rec (previous step)

files1 -- ino = files0 -- ino, files1[ino] = mkfile(m, md1, # links(ino, dirs), content), files0[ino] = mkfile(m, md1, m5, content0), afs-cons(dirs, files1), write-inv (n0, n3 + n0 + n, buf, n + min(n3, n2), content0, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]), write-inv(n0, n3 + n0 + n, buf, n, content0, content), ino ∈ files1, ino ∈ files0, n3 + n ≤ # buf, n ≤ # buf, (n0 + n) % VFS_PAGE_SIZE + min(n3, n2) ≤ VFS_PAGE_SIZE, min(n3, n2) ≤ n3 ⊦ afs-cons (dirs, files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 15:
⊦ 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 16:
files1 -- ino = files0 -- ino, files0[ino] = mkfile(m, md1, m5, content0), files1[ino] = mkfile(m, md1, # links(ino, dirs), content), afs-cons(dirs, files1), write-inv(n0, n3 + n0 + n, buf, n, content0, content), write-inv (n0, n3 + n0 + n, buf, n + min(n3, n2), content0, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]), ino ∈ files0, ino ∈ files1, min(n3, n2) ≤ n3, (n0 + n) % VFS_PAGE_SIZE + min(n3, n2) ≤ VFS_PAGE_SIZE, n ≤ # buf, n3 + n ≤ # buf ⊦ ∀ ino0, name, n1. ROOT_INO ∈ dirs ∧ (ino0 ∈ dirs ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → dir-empty(ino0, dirs, files1)) ∧ ( ino0 ∈ dirs → ¬ ino0 ∈ files1 ∧ dirs[ino0].nlink = # links(ino0, dirs) ∧ dirs[ino0].nlink ≤ 1 ∧ dirs[ino0].size = # dirs[ino0].entries ∧ dirs[ino0].nsubdirs = # subdirs(ino0, dirs)) ∧ (ino0 ∈ files1 → ¬ ino0 ∈ dirs ∧ files1[ino0].nlink = # links(ino0, dirs)) ∧ (ino0 ∈ dirs ∧ name ∈ dirs[ino0].entries → valid-ino(dirs[ino0].entries[name], dirs, files1)) ∧ (ino0 ∈ files1 ∧ n1 ∈ files1[ino0].content → valid-pagesize(ino0, n1, files1)) → ROOT_INO ∈ dirs ∧ ( ino0 ∈ dirs ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → dir-empty (ino0, dirs, files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ])) ∧ ( ino0 ∈ dirs → ¬ ino0 ∈ files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ] ∧ dirs[ino0].nlink = # links(ino0, dirs) ∧ dirs[ino0].nlink ≤ 1 ∧ dirs[ino0].size = # dirs[ino0].entries ∧ dirs[ino0].nsubdirs = # subdirs(ino0, dirs)) ∧ ( ino0 ∈ files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ] → ¬ ino0 ∈ dirs ∧ files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ] [ino0 ] .nlink = # links(ino0, dirs)) ∧ ( ino0 ∈ dirs ∧ name ∈ dirs[ino0].entries → valid-ino (dirs[ino0].entries[name], dirs, files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ])) ∧ ( ino0 ∈ files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ] ∧ n1 ∈ files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ] [ino0 ] .content → valid-pagesize (ino0, n1, files1 [ino, mkfile (m, md1, # links(ino, dirs), content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2))]) ]))

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, files1, files1 [ino, mkfile (m, md1, # links(ino, dirs), content [(n0 + n) / VFS_PAGE_SIZE, copy (buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2)) ]) ], dirs] flags: <all paths>

Additional information

Used terms: dirs, files1, files1 [ino, mkfile (m, md1, # links(ino, dirs), content [(n0 + n) / VFS_PAGE_SIZE, copy (buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n3, n2)) ]) ], dirs