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

dirs[m] = mkdir(m0, md0, # links(m, dirs), m2, entries), icache[m] = mkientry(boolvar, mkinode(m1, md1, boolvar0, m3, m4, m5)), afs-cons(dirs, files), afs-cons(dirs[m, mkdir(m0, md, # links(m, dirs), m2, entries)], files), icache-cons(icache, dirs, files), synced(dirs, icache, pcache), m ∈ dirs, m ∈ icache, asynced2 → synced(files, icache, pcache) ⊦ ∀ ino. ino ∈ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))] → icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino = ino ∧ (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].dirty ⊃ valid-file-inode (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode, dirs[m, mkdir(m0, md, # links(m, dirs), m2, entries)], files) ; valid-ino(ino, dirs[m, mkdir(m0, md, # links(m, dirs), m2, entries)], files) ∧ valid-inode (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode, dirs[m, mkdir(m0, md, # links(m, dirs), m2, entries)], files) )

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 126:
icache[m] = mkientry(boolvar, mkinode(m1, md1, boolvar0, m3, m4, m5)), dirs[m] = mkdir(m0, md0, # links(m, dirs), m2, entries), afs-cons(dirs[m, mkdir(m0, md, # links(m, dirs), m2, entries)], files), afs-cons(dirs, files), icache-cons(icache, dirs, files), synced(dirs, icache, pcache), ino ∈ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))], m ∈ icache, m ∈ dirs, asynced2 → synced(files, icache, pcache) ⊦ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino = ino ∧ (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].dirty ⊃ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino ∈ files ∧ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.nlink = files[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino].nlink ∧ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.nsubdirs = 0 ∧ ¬ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.directory ; (ino ∈ dirs ∨ ino ∈ files) ∧ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode = (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino ∈ dirs ⊃ mkinode (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino, (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino = m ⊃ mkdir(m0, md, # links(icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino, dirs), m2, entries) ;dirs[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino] ) .meta, true, (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino = m ⊃ mkdir(m0, md, # links(icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino, dirs), m2, entries) ;dirs[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino] ) .nlink, (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino = m ⊃ mkdir(m0, md, # links(icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino, dirs), m2, entries) ;dirs[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino] ) .nsubdirs, (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino = m ⊃ mkdir(m0, md, # links(icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino, dirs), m2, entries) ;dirs[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino] ) .size) ;mkinode (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino, files[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino].meta, false, files[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino].nlink, 0, files[icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode.ino].size) ) )

Rule argument

Additional information

Used simplifier rules: ⊦ dirs[ino, ad][ino0] = (ino0 = ino ∧ ino ∈ dirs ⊃ ad;dirs[ino0]); (s)%⊦ 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)%⊦ valid-inode(inode, dirs, files) ↔ inode = getinode(inode.ino, dirs, files); (s)% ⊦ ino ∈ dirs[ino0, ad] ↔ ino ∈ dirs; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)% ⊦ valid-file-ino(ino, dirs, files) ↔ ino ∈ files; (s)%⊦ valid-file-inode(inode, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory; (s)