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

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) ) )

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 127:
icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode = mkinode(m6, md2, boolvar1, m7, m8, m9), 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, ino ∈ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))], asynced2 → synced(files, icache, pcache) ⊦ m6 = ino ∧ (icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].dirty ⊃ m6 ∈ files ∧ m7 = files[m6].nlink ∧ m8 = 0 ∧ ¬ boolvar1 ; (ino ∈ dirs ∨ ino ∈ files) ∧ icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))][ino].inode = (m6 ∈ dirs ⊃ mkinode (m6, (m6 = m ⊃ mkdir(m0, md, # links(m6, dirs), m2, entries);dirs[m6]).meta, true, (m6 = m ⊃ mkdir(m0, md, # links(m6, dirs), m2, entries);dirs[m6]).nlink, (m6 = m ⊃ mkdir(m0, md, # links(m6, dirs), m2, entries);dirs[m6]).nsubdirs, (m6 = m ⊃ mkdir(m0, md, # links(m6, dirs), m2, entries);dirs[m6]).size) ;mkinode(m6, files[m6].meta, false, files[m6].nlink, 0, files[m6].size) ) )

Rule argument

spec: inode name: elim seq: ⊦ ( ( ( (m = inode.ino ∧ md = inode.meta) ∧ (boolvar ↔ inode.directory)) ∧ m0 = inode.nlink) ∧ m1 = inode.nsubdirs) ∧ m2 = inode.size ↔ inode = mkinode(m, md, boolvar, m0, m1, m2) subst: [inode, m, md, boolvar, m0, m1, m2] → [icache [m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5)) ] [ino ] .inode, m6, md2, boolvar1, m7, m8, m9]

Additional information

Used simplifier rules: ⊦ ( ( ( (m = inode.ino ∧ md = inode.meta) ∧ (boolvar ↔ inode.directory)) ∧ m0 = inode.nlink) ∧ m1 = inode.nsubdirs) ∧ m2 = inode.size ↔ inode = mkinode(m, md, boolvar, m0, m1, m2); (elim) Used terms: icache[m1, mkientry(false, mkinode(m1, md, boolvar0, m3, m4, m5))] [ino ] .inode, m6, md2, boolvar1, m7, m8, m9