[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 565 from proof inv-rename-dir-dentry (previous step)

(entries0[str0] = m7 ⊃ mkdir(m1, md2, # links(entries0[str0], dirs0), m4, entries0) ;mkdir(m3, md3, # links(entries0[str0], dirs0), m6, ∅) ) .meta:= md0 = mkdir(m, md4, m8, m9, entries1), (m7 = entries0[str0] ⊃ mkdir(m1, md0, # links(entries0[str0], dirs0), m4, entries0);mkdir(m1, md2, # links(m7, dirs0), m4, entries0)) = mkdir(m0, md, m2, m5, entries), dirs0[m7] = mkdir(m1, md1, # links(m7, dirs0), m4, entries0), dirs0[entries0[str0]] = mkdir(m3, md3, # links(entries0[str0], dirs0), m6, ∅), afs-cons(dirs0, files), afs-cons(dirs0[m7, mkdir(m1, md2, # links(m7, dirs0), m4, entries0)][entries0[str0], mkdir(m, md4, m8, m9, entries1)], files), icache-cons(icache0, dirs0, files), synced(dirs0, icache0, pcache), ino ∈ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))][entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m))], entries0[str0] ∈ dirs0, str0 ∈ entries0, m7 ∈ dirs0, asynced2 → synced(files, icache0, pcache), links(m7, dirs0) ≠ ∅ ∨ m7 = ROOT_INO ⊦ entries0[str0] = ROOT_INO, icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))][entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m))] [ino ] .inode .ino = ino ∧ (icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))][entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m))] [ino ] .dirty ⊃ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ∈ files ∧ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .nlink = files [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] .nlink ∧ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .nsubdirs = 0 ∧ ¬ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .directory ; (ino ∈ dirs0 ∨ ino ∈ files) ∧ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode = ( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ∈ dirs0 ⊃ mkinode (icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino, ( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1) ;( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0) ;dirs0 [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] ) ) .meta, true, ( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1) ;( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0) ;dirs0 [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] ) ) .nlink, ( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1) ;( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0) ;dirs0 [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] ) ) .nsubdirs, ( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1) ;( icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0) ;dirs0 [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] ) ) .size) ;mkinode (icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino, files [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] .meta, false, files [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] .nlink, 0, files [icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode .ino ] .size) ) )

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 566:
icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))][entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m))][ino] .inode = mkinode(m10, md5, boolvar, m11, m12, m13), (entries0[str0] = m7 ⊃ mkdir(m1, md2, # links(entries0[str0], dirs0), m4, entries0) ;mkdir(m3, md3, # links(entries0[str0], dirs0), m6, ∅) ) .meta:= md0 = mkdir(m, md4, m8, m9, entries1), (m7 = entries0[str0] ⊃ mkdir(m1, md0, # links(entries0[str0], dirs0), m4, entries0);mkdir(m1, md2, # links(m7, dirs0), m4, entries0)) = mkdir(m0, md, m2, m5, entries), dirs0[entries0[str0]] = mkdir(m3, md3, # links(entries0[str0], dirs0), m6, ∅), dirs0[m7] = mkdir(m1, md1, # links(m7, dirs0), m4, entries0), afs-cons(dirs0[m7, mkdir(m1, md2, # links(m7, dirs0), m4, entries0)][entries0[str0], mkdir(m, md4, m8, m9, entries1)], files), afs-cons(dirs0, files), icache-cons(icache0, dirs0, files), synced(dirs0, icache0, pcache), m7 ∈ dirs0, str0 ∈ entries0, entries0[str0] ∈ dirs0, ino ∈ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))][entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m))], asynced2 → synced(files, icache0, pcache), links(m7, dirs0) ≠ ∅ ∨ m7 = ROOT_INO ⊦ entries0[str0] = ROOT_INO, m10 = ino ∧ (icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))][entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m))] [ino ] .dirty ⊃ m10 ∈ files ∧ m11 = files[m10].nlink ∧ m12 = 0 ∧ ¬ boolvar ; (ino ∈ dirs0 ∨ ino ∈ files) ∧ icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode = (m10 ∈ dirs0 ⊃ mkinode (m10, (m10 = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1);(m10 = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0);dirs0[m10])).meta, true, (m10 = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1);(m10 = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0);dirs0[m10])) .nlink, (m10 = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1);(m10 = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0);dirs0[m10])) .nsubdirs, (m10 = entries0[str0] ⊃ mkdir(m, md4, m8, m9, entries1);(m10 = m7 ⊃ mkdir(m1, md2, # links(m7, dirs0), m4, entries0);dirs0[m10])).size) ;mkinode(m10, files[m10].meta, false, files[m10].nlink, 0, files[m10].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] → [icache0 [m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0)) ] [entries0[str0], mkientry (false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode, m10, md5, boolvar, m11, m12, m13]

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: icache0[m7, mkientry(false, mkinode(m7, md, true, m2, m5, m0))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md4, true, m8, m9, m)) ] [ino ] .inode, m10, md5, boolvar, m11, m12, m13