[forall u in UsedInode], u.inodestatus=literal(Used);
[],sizeof(RootDirectoryInode)=1;