[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 23 from proof crash-neutral-rmdir (previous step)

# links(m, dirs) = dirs[m].nlink, # links(entries[str], dirs) = c_inode.nlink, c_inode.ino = entries[str], entries[str] = dirs[m].entries[str], dirs[m] = mkdir(dirs[m].size, md0, dirs[m].nlink, dirs[m].nsubdirs, entries), dirs[entries[str]] = mkdir(c_inode.size, md1, c_inode.nlink, c_inode.nsubdirs, ∅), dirs1 = dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size - 1) ] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size - 1) ] [p_ino ] .nsubdirs:= ( dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size - 1) ] [p_ino ] .nsubdirs - 1) ], files0 = files, files1 = files, ino = mkdentry(str, entries[str]).ino, p_ino = m, mkdentry(str, entries[str]).dentry?, c_inode.directory, afs-cons(dirs, files), str ∈ dirs[m].entries, entries[str] ∈ dirs, m ∈ dirs, str ∈ entries, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size - 1) ] [p_ino ] .nsubdirs ≥ 1, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size ≥ 1, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟨afs_drop_nlink#(ino; dirs1, files); dent := negdentry(mkdentry(str, entries[str]).name); afs_inode_sync#(mkinode(m, md, true, # links(m, dirs), dirs[m].nsubdirs, dirs[m].size); dirs1, files); afs_inode_sync#(c_inode; dirs1, files); p_inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); c_inode := (c_inode.ino ∈ dirs1 ⊃ mkinode(c_inode.ino, dirs1[c_inode.ino].meta, true, dirs1[c_inode.ino].nlink, dirs1[c_inode.ino].nsubdirs, dirs1[c_inode.ino].size) ;mkinode(c_inode.ino, files[c_inode.ino].meta, false, files[c_inode.ino].nlink, 0, files[c_inode.ino].size) ); err := ESUCCESS; asynced := ?⟩ (asynced ∧ dirs \ orphans(dirs, files0) = dirs1 \ orphans(dirs1, files) ∧ files1 \ orphans(dirs, files1) = files \ orphans(dirs1, files)), ⟨fail#(; ; err); asynced := ?⟩ asynced, entries[str] = ROOT_INO

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 24:
# links(entries[str], dirs) = c_inode.nlink, # links(m, dirs) = dirs[m].nlink, c_inode.ino = entries[str], dirs[entries[str]] = mkdir(c_inode.size, md1, c_inode.nlink, c_inode.nsubdirs, ∅), dirs[m] = mkdir(dirs[m].size, md0, dirs[m].nlink, dirs[m].nsubdirs, entries), entries[str] = dirs[m].entries[str], dirs1 = dirs[m, ((dirs[m].entries:= (dirs[m].entries -- str)).size:= (dirs[m].size - 1)).nsubdirs:= (dirs[m].nsubdirs - 1)], files0 = files, dirs[m].nsubdirs ≠ 0, dirs[m].size ≠ 0, entries[str] ≠ ROOT_INO, c_inode.directory, afs-cons(dirs, files), str ∈ entries, m ∈ dirs, entries[str] ∈ dirs, str ∈ dirs[m].entries, 1 ≤ dirs[m].size, 1 ≤ dirs[m].nsubdirs, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟨afs_drop_nlink#(mkdentry(str, entries[str]).ino; dirs1, files); dent := negdentry(mkdentry(str, entries[str]).name); afs_inode_sync#(mkinode(m, md, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size); dirs1, files); afs_inode_sync#(c_inode; dirs1, files); p_inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); c_inode := (c_inode.ino ∈ dirs1 ⊃ mkinode(c_inode.ino, dirs1[c_inode.ino].meta, true, dirs1[c_inode.ino].nlink, dirs1[c_inode.ino].nsubdirs, dirs1[c_inode.ino].size) ;mkinode(c_inode.ino, files[c_inode.ino].meta, false, files[c_inode.ino].nlink, 0, files[c_inode.ino].size) ); err := ESUCCESS; asynced := ?⟩ (asynced ∧ dirs \ orphans(dirs, files0) = dirs1 \ orphans(dirs1, files) ∧ files0 \ orphans(dirs, files0) = files \ orphans(dirs1, files)), ⟨fail#(; ; err); asynced := ?⟩ asynced

Rule argument

Additional information

Used simplifier rules: not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat% ⊦ mkdentry(str, m).dentry?; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ (ad.entries:= entries).nsubdirs = ad.nsubdirs; (s)% ⊦ (ad.size:= m).nsubdirs = ad.nsubdirs; (s)% ⊦ dirs[ino, ad][ino, ad0] = dirs[ino, ad0]; (s)% ⊦ (ad.entries:= entries).size = ad.size; (s)% ⊦ dirs[ino, ad][ino0] = (ino0 = ino ∧ ino ∈ dirs ⊃ ad;dirs[ino0]); (s)% ⊦ mkdentry(str, m).name = str; (s)