[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 28 from proof writepage-afs-cons (previous step)

# buf2 = VFS_PAGE_SIZE, files[m] = mkfile(m0, md, # links(m, dirs), content), afs-cons(dirs, files), m ∈ files, ino + n ≤ VFS_PAGE_SIZE, ino0 + n ≤ # buf0 ⊦ afs-cons(dirs, files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 29:
⊦ 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 30:
# buf2 = VFS_PAGE_SIZE, files[m] = mkfile(m0, md, # links(m, dirs), content), afs-cons(dirs, files), m ∈ files, ino0 + n ≤ # buf0, ino + n ≤ VFS_PAGE_SIZE ⊦ ∀ ino1, name, n0. ROOT_INO ∈ dirs ∧ (ino1 ∈ dirs ∧ ino1 ≠ ROOT_INO ∧ links(ino1, dirs) = ∅ → dir-empty(ino1, dirs, files)) ∧ ( ino1 ∈ dirs → ¬ ino1 ∈ files ∧ dirs[ino1].nlink = # links(ino1, dirs) ∧ dirs[ino1].nlink ≤ 1 ∧ dirs[ino1].size = # dirs[ino1].entries ∧ dirs[ino1].nsubdirs = # subdirs(ino1, dirs)) ∧ (ino1 ∈ files → ¬ ino1 ∈ dirs ∧ files[ino1].nlink = # links(ino1, dirs)) ∧ (ino1 ∈ dirs ∧ name ∈ dirs[ino1].entries → valid-ino(dirs[ino1].entries[name], dirs, files)) ∧ (ino1 ∈ files ∧ n0 ∈ files[ino1].content → valid-pagesize(ino1, n0, files)) → ROOT_INO ∈ dirs ∧ ( ino1 ∈ dirs ∧ ino1 ≠ ROOT_INO ∧ links(ino1, dirs) = ∅ → dir-empty(ino1, dirs, files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])])) ∧ ( ino1 ∈ dirs → ¬ ino1 ∈ files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])] ∧ dirs[ino1].nlink = # links(ino1, dirs) ∧ dirs[ino1].nlink ≤ 1 ∧ dirs[ino1].size = # dirs[ino1].entries ∧ dirs[ino1].nsubdirs = # subdirs(ino1, dirs)) ∧ ( ino1 ∈ files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])] → ¬ ino1 ∈ dirs ∧ files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])][ino1].nlink = # links(ino1, dirs)) ∧ ( ino1 ∈ dirs ∧ name ∈ dirs[ino1].entries → valid-ino(dirs[ino1].entries[name], dirs, files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])])) ∧ ( ino1 ∈ files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])] ∧ n0 ∈ files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])][ino1].content → valid-pagesize(ino1, n0, files[m, mkfile(m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)])]))

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, files, files [m, mkfile (m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)]) ], dirs] flags: <all paths>

Additional information

Used terms: dirs, files, files [m, mkfile (m0, md, # links(m, dirs), content[pageno, copy(buf0, ino0, buf2, ino, n)]) ], dirs