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

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))]) ]))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 17:
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), ROOT_INO ∈ dirs, ino ∈ files1, ino ∈ files0, n3 + n ≤ # buf, n ≤ # buf, (n0 + n) % VFS_PAGE_SIZE + min(n3, n2) ≤ VFS_PAGE_SIZE, min(n3, n2) ≤ n3, ino0 ∈ files1 → ¬ ino0 ∈ dirs ∧ files1[ino0].nlink = # links(ino0, dirs), ino0 ∈ dirs ∧ ino0 ≠ ROOT_INO ∧ links(ino0, dirs) = ∅ → dirs[ino0].entries = ∅, ino0 ∈ dirs → dirs[ino0].nlink = # links(ino0, dirs) ∧ dirs[ino0].nlink ≤ 1 ∧ dirs[ino0].size = # dirs[ino0].entries ∧ dirs[ino0].nsubdirs = # subdirs(ino0, dirs), ino0 ∈ dirs ∧ name ∈ dirs[ino0].entries → dirs[ino0].entries[name] ∈ dirs ∨ dirs[ino0].entries[name] ∈ files1, ino0 ∈ files1 ∧ n1 ∈ files1[ino0].content → # files1[ino0].content[n1] = VFS_PAGE_SIZE ⊦ ( ino0 ∈ files1 → ¬ ino0 ∈ dirs ∧ (ino0 = 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))]) ;files1[ino0] ) .nlink = # links(ino0, dirs)) ∧ ( ino0 ∈ files1 ∧ n1 ∈ (ino0 = 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))]) ;files1[ino0] ) .content → # (ino0 = 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))]) ;files1[ino0] ) .content [n1 ] = 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)