[], true => literal(0) in SuperBlock [], true => literal(1) in GroupBlock [], d.g.InodeTableBlock < d.s.NumberofBlocks => d.g.InodeTableBlock in InodeTableBlock [], d.g.InodeBitmapBlock < d.s.NumberofBlocks => d.g.InodeBitmapBlock in InodeBitmapBlock [], d.g.BlockBitmapBlock < d.s.NumberofBlocks => d.g.BlockBitmapBlock in BlockBitmapBlock [], d.s.RootDirectoryInode < d.s.NumberofInodes => d.s.RootDirectoryInode in RootDirectoryInode delay [for j=literal(0) to d.s.NumberofInodes-literal(1)], !(j in UsedInode) => j in FreeInode delay [for j=literal(0) to d.s.NumberofBlocks-literal(1)], !(j in UsedBlock) => j in FreeBlock [forall di in DirectoryInode, forall itb in InodeTableBlock, for j=literal(0) to (d.s.blocksize/literal(128))-literal(1), for k=literal(0) to literal(11)], cast(InodeTable,d.b[itb]).itable[di].Blockptr[k] < d.s.NumberofBlocks => cast(DirectoryBlock,d.b[cast(InodeTable,d.b[itb]).itable[di].Blockptr[k]]).de[j] in DirectoryEntry [forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)], !cast(InodeTable,d.b[itb]).itable[i].Blockptr[j]=literal(0) => in contents [forall i in UsedInode, forall itb in InodeTableBlock, for j=literal(0) to literal(11)], cast(InodeTable,d.b[itb]).itable[i].Blockptr[j] cast(InodeTable,d.b[itb]).itable[i].Blockptr[j] in FileDirectoryBlock [for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock], cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(false) => in inodestatus [for j=literal(0) to d.s.NumberofInodes-literal(1), forall ibb in InodeBitmapBlock], cast(InodeBitmap,d.b[ibb]).inodebitmap[j]=literal(true) => in inodestatus [forall de in DirectoryEntry], de.inodenumber de.inodenumber in FileInode [forall de in DirectoryEntry], de.inodenumber in inodeof [forall j in UsedInode, forall itb in InodeTableBlock], true => in referencecount [forall j in UsedInode, forall itb in InodeTableBlock], true => in filesize [for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock], cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(false) => in blockstatus [for j=literal(0) to d.s.NumberofBlocks-literal(1), forall bbb in BlockBitmapBlock], cast(BlockBitmap,d.b[bbb]).blockbitmap[j]=literal(true) => in blockstatus