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

icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino] = mkientry(boolvar2, inode0), pcache[datakey(ino, n)] = mkpentry(boolvar0, buf), files[m0] = mkfile(m1, md1, # links(m0, dirs), content), icache[m] = mkientry(boolvar, mkinode(m0, md0, false, # links(m0, dirs), 0, m4)), icache[ino] = mkientry(boolvar1, inode), afs-cons(dirs, files), synced(dirs, icache, pcache), ino ∈ dirs, m0 ∈ files, m ∈ files, m ∈ icache, ino ∈ icache → ¬ boolvar1, ∀ ino. ino ∈ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))] → icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino = ino ∧ (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].dirty ⊃ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino ∈ files ∧ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.nlink = files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nlink ∧ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.nsubdirs = 0 ∧ ¬ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.directory ; (ino ∈ dirs ∨ ino ∈ files) ∧ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode = (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino ∈ dirs ⊃ mkinode (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].meta, true, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nlink, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nsubdirs, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].size) ;mkinode (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino, files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].meta, false, files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nlink, 0, files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].size) ) ), ∀ n. datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty ⊦ ino = m0, (ino ∈ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))] → ¬ boolvar2) ∧ (datakey(ino, n) ∈ pcache → ¬ boolvar0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 461:
icache[ino] = mkientry(boolvar1, inode), pcache[datakey(ino, n)] = mkpentry(true, buf), files[m0] = mkfile(m1, md1, # links(m0, dirs), content), icache[m] = mkientry(boolvar, mkinode(m0, md0, false, # links(m0, dirs), 0, m4)), afs-cons(dirs, files), synced(dirs, icache, pcache), datakey(ino, n) ∈ pcache, ino ∈ dirs, m0 ∈ files, m ∈ files, m ∈ icache, ino ∈ icache → ¬ boolvar1, ∀ ino. ino ∈ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))] → icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino = ino ∧ (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].dirty ⊃ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino ∈ files ∧ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.nlink = files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nlink ∧ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.nsubdirs = 0 ∧ ¬ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.directory ; (ino ∈ dirs ∨ ino ∈ files) ∧ icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode = (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino ∈ dirs ⊃ mkinode (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].meta, true, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nlink, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nsubdirs, dirs[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].size) ;mkinode (icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino, files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].meta, false, files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].nlink, 0, files[icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))][ino].inode.ino].size) ) ), ∀ n. datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty ⊦ ino = m0

Rule argument

Additional information

Used simplifier rules: ⊦ mkientry(boolvar, inode) = mkientry(boolvar0, inode0) ↔ (boolvar ↔ boolvar0) ∧ inode = inode0; (ws)% ⊦ ino ≠ ino0 → (ino ∈ icache[ino0, ie] ↔ ino ∈ icache); (s)% ⊦ ino ≠ ino0 → icache[ino0, ie][ino] = icache[ino]; (s)