[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 150 from proof refine-truncate-buff-none-uncached (previous step)

VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, cache_files[m1] = mkfile(m3, md1, # links(m1, cache_dirs), content1), ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m1] = mkfile(m4, md2, # links(m1, cache_dirs), content), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache0, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache0), m2 / VFS_PAGE_SIZE ∈ content1, m2 / VFS_PAGE_SIZE ∈ content, m1 ∈ cache_files, m2 ≤ m, VFS_PAGE_SIZE ≤ # content[m2 / VFS_PAGE_SIZE], cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ m2 % VFS_PAGE_SIZE = 0, datakey(m1, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache )[m1, mkfile (m, md, # links(m1, cache_dirs), content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] = ( cache_files [m1, mkfile (m, md, # links(m1, cache_dirs), content1[m2 / VFS_PAGE_SIZE, fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ⊕ truncate(m1, m2, cache_pcache0) [datakey(m1, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)) ]) ⊕ cache_icache[m1, mkientry(false, mkinode(m1, md, false, # links(m1, cache_dirs), 0, m))] ∧ fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1) = fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)

Heuristic use patterns applied rule cut formula

And obtained the following new goals

Proof step 151:
VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m1] = mkfile(m4, md2, # links(m1, cache_dirs), content), cache_files[m1] = mkfile(m3, md1, # links(m1, cache_dirs), content1), fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1) = fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ 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_pcache0, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache0), m1 ∈ cache_files, m2 / VFS_PAGE_SIZE ∈ content, m2 / VFS_PAGE_SIZE ∈ content1, VFS_PAGE_SIZE ≤ # content[m2 / VFS_PAGE_SIZE], m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ m2 % VFS_PAGE_SIZE = 0, datakey(m1, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache )[m1, mkfile (m, md, # links(m1, cache_dirs), content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] = ( cache_files [m1, mkfile (m, md, # links(m1, cache_dirs), content1[m2 / VFS_PAGE_SIZE, fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ⊕ truncate(m1, m2, cache_pcache0) [datakey(m1, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)) ]) ⊕ cache_icache[m1, mkientry(false, mkinode(m1, md, false, # links(m1, cache_dirs), 0, m))] ∧ fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1) = fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)
Proof step 761:
VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m1] = mkfile(m4, md2, # links(m1, cache_dirs), content), cache_files[m1] = mkfile(m3, md1, # links(m1, cache_dirs), content1), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ 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_pcache0, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache0), m1 ∈ cache_files, m2 / VFS_PAGE_SIZE ∈ content, m2 / VFS_PAGE_SIZE ∈ content1, VFS_PAGE_SIZE ≤ # content[m2 / VFS_PAGE_SIZE], m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ m2 % VFS_PAGE_SIZE = 0, fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1) = fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1), datakey(m1, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache )[m1, mkfile (m, md, # links(m1, cache_dirs), content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] = ( cache_files [m1, mkfile (m, md, # links(m1, cache_dirs), content1[m2 / VFS_PAGE_SIZE, fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ⊕ truncate(m1, m2, cache_pcache0) [datakey(m1, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)) ]) ⊕ cache_icache[m1, mkientry(false, mkinode(m1, md, false, # links(m1, cache_dirs), 0, m))] ∧ fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1) = fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)

Rule argument

fma: fill (content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1) = fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)

Additional information

Used formulas: fill(content1[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1) = fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)