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

icache[m] = mkientry(boolvar, mkinode(m0, md0, false, # links(m0, dirs), 0, m4)), files[m0] = mkfile(m1, md1, # links(m0, dirs), content), afs-cons(dirs, files), synced(dirs, icache, pcache), m ∈ icache, m ∈ files, m0 ∈ files, ∀ 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) ) ) ⊦ ∀ ino. (ino ∈ dirs → synced(ino, icache, pcache)) → ino ∈ dirs → synced(ino, icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))], pcache)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 456:
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), ino ∈ dirs, m0 ∈ files, m ∈ files, m ∈ icache, ino ∈ icache → ¬ icache[ino].dirty, ∀ 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 ∈ 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].dirty) ∧ (datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty)

Rule argument

Additional information

Used simplifier rules: ⊦ synced(ino, icache, pcache) ↔ (ino ∈ icache → ¬ icache[ino].dirty) ∧ (∀ n. datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty); (s)