[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 329 from proof refine-rmdir (previous step)

# entries0 = m + 1, (entries0[str] ∈ dirs ⊃ mkinode(entries0[str], dirs[entries0[str]].meta, true, dirs[entries0[str]].nlink, dirs[entries0[str]].nsubdirs, dirs[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, boolvar, m6, m7, m8), root[q + str '] = dnode(md1, ∅), dirs0[ino1] = mkdir(m + 1, md2, # links(ino1, dirs0), m2, entries0), dirs0[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs0), m3, ∅), dirs1[entries0[str]] = mkdir(m0, md0, m1, m4, entries), err = ESUCCESS, fs = abs-files(files), ino = inode.ino, inode = getinode(entries0[str], dirs, files), root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pre-evict(inode, dirs, files), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), entries0[str] ∈ dirs1, entries0[str] ∈ dirs0, ino1 ∈ dirs0, str ∈ entries0, ino1 ∈ dirs2, entries0[str] ∈ dirs3, dirs ≡ dirs3[entries0[str], dirs3[entries0[str]].meta:= md], dirs3 ≡ dirs2[ino1, dirs2[ino1].meta:= md2], dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], dirs2 ≡ dirs1[entries0[str], mkdir(m0, md0, m1 - 1, m4, entries)], 1 ≤ m2, 1 ≤ m1, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [if files[ino].nlink = 0 then files := files -- ino] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err1, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err1)), entries0 = ∅, m1 = 0, m2 = 0, is-open(m5, of), ino ∈ dirs

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 330:
# entries0 = m + 1, (entries0[str] ∈ dirs ⊃ mkinode(entries0[str], dirs[entries0[str]].meta, true, dirs[entries0[str]].nlink, dirs[entries0[str]].nsubdirs, dirs[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, false, files[m5].nlink, 0, m8), dirs1[entries0[str]] = mkdir(m0, md0, m1, m4, entries), dirs0[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs0), m3, ∅), dirs0[ino1] = mkdir(m + 1, md2, # links(ino1, dirs0), m2, entries0), root[q + str '] = dnode(md1, ∅), fs = abs-files(files), entries0 ≠ ∅, m1 ≠ 0, m2 ≠ 0, m5 ≠ ROOT_INO, root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), m5 ∈ files, entries0[str] ∈ dirs3, ino1 ∈ dirs2, str ∈ entries0, ino1 ∈ dirs0, entries0[str] ∈ dirs0, entries0[str] ∈ dirs1, dirs2 ≡ dirs1[entries0[str], mkdir(m0, md0, m1 - 1, m4, entries)], dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], dirs3 ≡ dirs2[ino1, dirs2[ino1].meta:= md2], dirs ≡ dirs3[entries0[str], dirs3[entries0[str]].meta:= md], 1 ≤ m1, 1 ≤ m2, ¬ is-open(m5, of), ¬ m5 ∈ dirs, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [if files[m5].nlink = 0 then files := files -- m5] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err1, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err1))

Rule argument

Additional information

Used simplifier rules: ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nlink = m0; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs = m1; (s)% ⊦ valid-file-ino(ino, dirs, files) ↔ ino ∈ files; (s)%⊦ valid-file-inode(inode, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory; (s)% ⊦ valid-dir-ino(ino, dirs, files) ↔ ino ∈ dirs; (s)%⊦ valid-dir-inode(inode, dirs, files) ↔ valid-dir-ino(inode.ino, dirs, files) ∧ inode.nlink = dirs[inode.ino].nlink ∧ inode.size = dirs[inode.ino].size ∧ inode.nsubdirs = dirs[inode.ino].nsubdirs ∧ inode.directory; (s)%⊦ valid-wb-inode(inode, dirs, files) ↔ valid-dir-inode(inode, dirs, files) ∨ valid-file-inode(inode, dirs, files); (s)%⊦ pre-evict(inode, dirs, files) ↔ valid-wb-inode(inode, dirs, files) ∧ inode.ino ≠ ROOT_INO; (s)%⊦ getinode(ino, dirs, files) = (ino ∈ dirs ⊃ mkinode (ino, dirs[ino].meta, true, dirs[ino].nlink, dirs[ino].nsubdirs, dirs[ino].size) ;mkinode (ino, files[ino].meta, false, files[ino].nlink, 0, files[ino].size) ); (s)