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

m1 + n1 = m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE + VFS_PAGE_SIZE, of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m1, md0, # links(m, dirs), content0), files[m] = mkfile(m2, md, # links(m, dirs), content), m1 = n2 + m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, dom of < ino3, m1 < m0 + ino4, afs-cons(dirs, files), afs-cons(dirs, files1), of-cons(of, dirs, files), of-cons(of, dirs, files1), m ∈ files1, m1 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, m ∈ files, m1 % VFS_PAGE_SIZE + n1 ≤ VFS_PAGE_SIZE, n ≤ # buf0, n2 + n1 ≤ VFS_PAGE_SIZE ⊦ ino4 = 0, n = 0, n2 = 0, err1 = ESUCCESS ∧ ¬ isdir, mode ≠ MODE_W ∧ mode ≠ MODE_RW, of-cons(of[fd, mkfile(m, mode, m0 + ino4)], dirs, files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)]) ∧ afs-cons(dirs, files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 252:
⊦ 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 253:
m1 + n1 = m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE + VFS_PAGE_SIZE, files[m] = mkfile(m2, md, # links(m, dirs), content), files1[m] = mkfile(m1, md0, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), m1 = n2 + m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, m1 < m0 + ino4, dom of < ino3, afs-cons(dirs, files1), afs-cons(dirs, files), of-cons(of, dirs, files1), of-cons(of, dirs, files), m ∈ files, fd ∈ of, m1 / VFS_PAGE_SIZE ∈ content0, m ∈ files1, n2 + n1 ≤ VFS_PAGE_SIZE, n ≤ # buf0, m1 % VFS_PAGE_SIZE + n1 ≤ VFS_PAGE_SIZE ⊦ ino4 = 0, n = 0, n2 = 0, of-cons(of[fd, mkfile(m, mode, m0 + ino4)], dirs, files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)]) ∧ (∀ ino, name, n. ROOT_INO ∈ dirs ∧ (ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dir-empty(ino, dirs, files)) ∧ ( ino ∈ dirs → ¬ ino ∈ files ∧ dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs)) ∧ (ino ∈ files → ¬ ino ∈ dirs ∧ files[ino].nlink = # links(ino, dirs)) ∧ (ino ∈ dirs ∧ name ∈ dirs[ino].entries → valid-ino(dirs[ino].entries[name], dirs, files)) ∧ (ino ∈ files ∧ n ∈ files[ino].content → valid-pagesize(ino, n, files)) → ROOT_INO ∈ dirs ∧ (ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dir-empty(ino, dirs, files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)])) ∧ ( ino ∈ dirs → ¬ ino ∈ files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)] ∧ dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs)) ∧ ( ino ∈ files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)] → ¬ ino ∈ dirs ∧ files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)][ino].nlink = # links(ino, dirs)) ∧ ( ino ∈ dirs ∧ name ∈ dirs[ino].entries → valid-ino(dirs[ino].entries[name], dirs, files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)])) ∧ ( ino ∈ files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)] ∧ n ∈ files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)][ino].content → valid-pagesize(ino, n, files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)]))), mode ≠ MODE_W ∧ mode ≠ MODE_RW, err1 = ESUCCESS ∧ ¬ isdir

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 + ino4, md0, # links(m, dirs), content) ], dirs] flags: <all paths>

Additional information

Used terms: dirs, files, files[m, mkfile(m0 + ino4, md0, # links(m, dirs), content)], dirs