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

root[q + str '] = dnode(md1, ∅), dirs0[ino1] = mkdir(# entries, md, # links(ino1, dirs0), m1, entries), dirs0[entries[str]] = mkdir(0, md0, # links(entries[str], dirs0), m2, ∅), c_inode = p_inode0, dent = mkdentry(str, entries[str]), err = ESUCCESS, fs = abs-files(files), ino = dent.ino, inode = mkinode(ino1, md, true, # links(ino1, dirs0), m1, # entries), p_ino = p_inode.ino, p_inode = inode, p_inode0 = mkinode(entries[str], md0, true, # links(entries[str], dirs0), m2, 0), dent.dentry?, 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-rmdir(p_inode, c_inode, dent, dirs0, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs0, files), entries[str] ∈ dirs0, ino1 ∈ dirs0, str ∈ entries, dirs ≡ dirs2[p_ino, dirs2[p_ino].nsubdirs:= (dirs2[p_ino].nsubdirs - 1)], dirs1 ≡ dirs0[p_ino, dirs0[p_ino].entries:= (dirs0[p_ino].entries -- dent.name)], dirs2 ≡ dirs1[p_ino, dirs1[p_ino].size:= (dirs1[p_ino].size - 1)], dirs2[p_ino].nsubdirs ≥ 1, dirs1[p_ino].size ≥ 1, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [afs_drop_nlink#(ino; dirs, files); dent := negdentry(dent.name); afs_inode_sync#(p_inode; dirs, files); afs_inode_sync#(c_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(c_inode.ino, dirs, files); err := ESUCCESS; asynced := ?; vfs_put_inode#(c_inode, of, asynced; err, dirs, files)] ( 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) ∧ err = err1))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Used simplifier rules: abs-acyclic: ⊦ abs(tree, ROOT_INO)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n, md, m, m0, entries) ∧ str ∈ entries ∧ ispath(p, ROOT_INO, ino, dirs, files) → entries[str] ≠ ROOT_INO;%path-in: ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → p ∈ tree ∧ (tree[p].dir? ↔ m ∈ dirs);%dir-empty: ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ m ∈ dirs ∧ dirs[m] = mkdir(m0, md, n0, n1, entries) ∧ str ∈ entries ∧ entries[str] ∈ dirs → (dirs[entries[str]].entries = ∅ ↔ tree[p + str '].entries = ∅);%dir-entry: ⊦ ispath(p, ino, m, dirs, files) ∧ px-parent(user, p, ino, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ m ∈ dirs ∧ dirs[m] = mkdir(m0, md, n0, n1, entries) ∧ str ∈ entries → (entries[str] ∈ dirs ↔ tree[p + str '].dir?);%path-in-eq: ⊦ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (p ∈ tree ↔ ispath(p, ino, dirs, files));% ⊦ dnode(md, sdt).dir?; (s)% ⊦ (ad.entries:= entries).nsubdirs = ad.nsubdirs; (s)% ⊦ (ad.size:= m).nsubdirs = ad.nsubdirs; (s)% ⊦ # entries = 0 ↔ entries = ∅; (s)% ⊦ dnode(md, sdt).entries = sdt; (s)% ⊦ dirs[ino, ad][ino, ad0] = dirs[ino, ad0]; (s)% ⊦ ispath(p, n, m, dirs, files) → ispath(p, n, dirs, files); (s)% ⊦ (ad.entries:= entries).size = ad.size; (s)% ⊦ dirs[ino, ad][ino0] = (ino0 = ino ∧ ino ∈ dirs ⊃ ad;dirs[ino0]); (s)%afs-cons-dir-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) → # links(ino, dirs) = n; (forward) from specification afs-base%not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat%⊦ 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)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs = m1; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nlink = m0; (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)% ⊦ dir-empty(ino, dirs, files) ↔ dirs[ino].entries = ∅; (s)% ⊦ mkdentry(str, m).dentry?; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)%⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO); (s)%⊦ valid-dentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ valid-ino(dent.ino, dirs, files) ∧ dent.name ∈ dirs[ino].entries ∧ dent.ino = dirs[ino].entries[dent.name] ∧ dent.dentry?; (s)% ⊦ mkdentry(str, m).ino = m; (s)%⊦ pre-rmdir(p_inode, c_inode, dent, dirs, files) ↔ dent.ino ≠ ROOT_INO ∧ valid-dentry(p_inode.ino, dent, dirs, files) ∧ dir-empty(dent.ino, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files) ∧ valid-dir-inode(c_inode, dirs, files) ∧ c_inode.ino = dent.ino; (s)%⊦ ino ∈ dirs ∧ dirs0 ≡ dirs1[ino, ad] → (dirs1 ≡ dirs[ino, ad0] ↔ dirs1 = dirs[ino, ad0]); (s)% ⊦ mkdentry(str, m).name = str; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)