[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 76 from proof truncate-greater (previous step)

VFS_PAGE_SIZE = n0 + m3 % VFS_PAGE_SIZE, files0[m0] = mkfile(m, md0, # links(m0, dirs), content0), files = files1, files1 = files0 [m0, mkfile(m, md0, # links(m0, dirs), content0[m3 / VFS_PAGE_SIZE, fill(content0[m3 / VFS_PAGE_SIZE], zero, m3 % VFS_PAGE_SIZE, n0)] upto m3) ], ino = inode.ino, inode = mkinode(m0, md, false, # links(m0, dirs), 0, n), inode0 = mkinode(m0, md, false, # links(m0, dirs), 0, m3), m3 < n, afs-cons(dirs, files0), m3 / VFS_PAGE_SIZE ∈ content0, m0 ∈ files0, ino ∈ dirs ⊦ [asynced := ?] (ESUCCESS = ESUCCESS ⊃ files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .content .stream to files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size = ( files0 [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .content .stream to m3) + ( σ⊥ to ( files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size - m3)) ∧ (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ∈ files ∧ n = files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size ∧ files0 [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .nlink = files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .nlink ∧ files0 -- (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino = files -- (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ;⌊ESUCCESS⌋ ∧ files0 = files ), m3 % VFS_PAGE_SIZE = 0, ino ∈ files

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)