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

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), m0 ∈ files, m ∈ files, m ∈ icache, ∀ 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) ) ) ⊦ synced(dirs, icache[m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2))], pcache)

Heuristic use patterns applied rule insert rewrite lemma

And obtained the following new goals

Proof step 454:
⊦ synced(dirs, icache, pcache) → (¬ synced(dirs0, icache0, pcache0) ↔ ¬(∀ ino. (ino ∈ dirs → synced(ino, icache, pcache)) → ino ∈ dirs0 → synced(ino, icache0, pcache0)))
Proof step 455:
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)

Rule argument

spec: cache-base name: synced-dirs-variant1 seq: ⊦ synced(dirs, icache, pcache) → ( ¬ synced(dirs0, icache0, pcache0) ↔ ¬ (∀ ino. (ino ∈ dirs → synced(ino, icache, pcache)) → ino ∈ dirs0 → synced(ino, icache0, pcache0))) subst: [dirs, icache, pcache, dirs0, icache0, pcache0] → [dirs, icache, pcache, dirs, icache [m0, mkientry (true, mkinode(m0, md, false, # links(m0, dirs), 0, m2)) ], pcache] flags: <all paths>

Additional information

Used terms: dirs, icache, pcache, dirs, icache [m0, mkientry(true, mkinode(m0, md, false, # links(m0, dirs), 0, m2)) ], pcache