[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 170 from proof refine-link (previous step)

cache_icache[ino] = mkientry(boolvar0, mkinode(m14, md, false, m18, m19, m20)), cache_dirs[ino3] = mkdir(m1, md4, # links(ino3, cache_dirs), m12, entries2), cache_dirs[ino0] = mkdir(m4, md2, # links(ino0, cache_dirs), m10, entries), cache_dirs[ino1] = mkdir(m0, md3, # links(ino1, cache_dirs), m2, entries0), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries2[str]] = mkfile(m5, md1, # links(entries2[str], cache_dirs), content), cache_dirs[m9] = mkdir(m, md7, # links(m9, cache_dirs), m6, entries3), entries0[str] = entries2[str], cache_files[entries2[str]] = mkfile(m3, md6, # links(entries2[str], cache_dirs), content1), entries[str] = entries2[str], cache_dirs[ino2] = mkdir(m7, md5, # links(ino2, cache_dirs), m11, entries1), entries1[str] = entries2[str], cache_icache[m9, mkientry(false, mkinode(m9, md0, true, # links(m9, cache_dirs), m6, m + 1))][ino] = mkientry(boolvar, mkinode(m8, md8, true, m13, m15, m16)), cache_files[ino] = mkfile(m17, md9, # links(ino, cache_dirs), content0), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), m9 ∈ cache_dirs, str ∈ entries0, str ∈ entries, ino1 ∈ cache_dirs, ino0 ∈ cache_dirs, ino2 ∈ cache_dirs, str ∈ entries1, entries2[str] ∈ cache_files, ino3 ∈ cache_dirs, str ∈ entries2, ino ∈ cache_files, ino ∈ cache_icache[m9, mkientry(false, mkinode(m9, md0, true, # links(m9, cache_dirs), m6, m + 1))], ino ∈ cache_icache, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m9, cache_dirs) ≠ ∅ ∨ m9 = ROOT_INO, links(ino1, cache_dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino0, cache_dirs) ≠ ∅ ∨ ino0 = ROOT_INO, links(ino2, cache_dirs) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino3, cache_dirs) ≠ ∅ ∨ ino3 = ROOT_INO ⊦ ino = entries2[str], mkfile(m20, md, m18, content0 ⊕ mkcontent(ino, cache_pcache)) = mkfile(m17, md9, # links(ino, cache_dirs), content0 ⊕ mkcontent(ino, cache_pcache)), str0 ∈ entries3

Heuristic use patterns applied rule insert rewrite lemma

And obtained the following new goals

Proof step 171:
⊦ mkfile(m, md, m0, content) = mkfile(m1, md0, m2, content0) ↔ m = m1 ∧ md = md0 ∧ m0 = m2 ∧ content = content0
Proof step 172:
cache_files[ino] = mkfile(m17, md9, # links(ino, cache_dirs), content0), cache_icache[m9, mkientry(false, mkinode(m9, md0, true, # links(m9, cache_dirs), m6, m + 1))][ino] = mkientry(boolvar, mkinode(m8, md8, true, m13, m15, m16)), entries1[str] = entries2[str], cache_dirs[ino2] = mkdir(m7, md5, # links(ino2, cache_dirs), m11, entries1), entries[str] = entries2[str], cache_files[entries2[str]] = mkfile(m3, md6, # links(entries2[str], cache_dirs), content1), entries0[str] = entries2[str], cache_dirs[m9] = mkdir(m, md7, # links(m9, cache_dirs), m6, entries3), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries2[str]] = mkfile(m5, md1, # links(entries2[str], cache_dirs), content), cache_dirs[ino1] = mkdir(m0, md3, # links(ino1, cache_dirs), m2, entries0), cache_dirs[ino0] = mkdir(m4, md2, # links(ino0, cache_dirs), m10, entries), cache_dirs[ino3] = mkdir(m1, md4, # links(ino3, cache_dirs), m12, entries2), cache_icache[ino] = mkientry(boolvar0, mkinode(m14, md, false, m18, m19, m20)), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), ino ∈ cache_icache, ino ∈ cache_icache[m9, mkientry(false, mkinode(m9, md0, true, # links(m9, cache_dirs), m6, m + 1))], ino ∈ cache_files, str ∈ entries2, ino3 ∈ cache_dirs, entries2[str] ∈ cache_files, str ∈ entries1, ino2 ∈ cache_dirs, ino0 ∈ cache_dirs, ino1 ∈ cache_dirs, str ∈ entries, str ∈ entries0, m9 ∈ cache_dirs, cache_sync → synced(cache_files, cache_icache, cache_pcache), links(ino3, cache_dirs) ≠ ∅ ∨ ino3 = ROOT_INO, links(ino2, cache_dirs) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino0, cache_dirs) ≠ ∅ ∨ ino0 = ROOT_INO, links(ino1, cache_dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(m9, cache_dirs) ≠ ∅ ∨ m9 = ROOT_INO ⊦ ino = entries2[str], str0 ∈ entries3, m20 = m17 ∧ md = md9 ∧ m18 = # links(ino, cache_dirs) ∧ content0 ⊕ mkcontent(ino, cache_pcache) = content0 ⊕ mkcontent(ino, cache_pcache)

Rule argument

spec: abstract-file name: inj seq: ⊦ mkfile(m, md, m0, content) = mkfile(m1, md0, m2, content0) ↔ m = m1 ∧ md = md0 ∧ m0 = m2 ∧ content = content0 subst: [m, md, m0, content, m1, md0, m2, content0] → [m20, md, m18, content0 ⊕ mkcontent(ino, cache_pcache), m17, md9, # links(ino, cache_dirs), content0 ⊕ mkcontent(ino, cache_pcache)] flags: <all paths>

Additional information

Used terms: m20, md, m18, content0 ⊕ mkcontent(ino, cache_pcache), m17, md9, # links(ino, cache_dirs), content0 ⊕ mkcontent(ino, cache_pcache)