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

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

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

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

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[m9, mkientry(false, mkinode(m9, md1, true, m11, m12, m0))] [m, mkientry(false, mkinode(m, md4, true, m14, m15, m13)) ] [ino ] .inode, m16, md7, boolvar, m17, m18, m19