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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 254:
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)]) ∧ ( ROOT_INO ∈ dirs ∧ (ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dirs[ino].entries = ∅) ∧ ( ino ∈ dirs → 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 → dirs[ino].entries[name] ∈ dirs ∨ dirs[ino].entries[name] ∈ files) ∧ (ino ∈ files ∧ n0 ∈ files[ino].content → # files[ino].content[n0] = VFS_PAGE_SIZE) → (ino ∈ files → ¬ ino ∈ dirs ∧ (ino = m ⊃ mkfile(m0 + ino4, md0, # links(m, dirs), content);files[ino]).nlink = # links(ino, dirs)) ∧ ( ino ∈ files ∧ n0 ∈ (ino = m ⊃ mkfile(m0 + ino4, md0, # links(m, dirs), content);files[ino]).content → # (ino = m ⊃ mkfile(m0 + ino4, md0, # links(m, dirs), content);files[ino]).content[n0] = VFS_PAGE_SIZE))

Rule argument

Additional information

Used simplifier rules: ⊦ of-cons(of, dirs, files) ∧ fd ∈ of ∧ of[fd] = mkfile(ino, mode, n) → ino ∈ files; (ss)% ⊦ 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)