What does it really mean here? Do you want me to compress the code? I can see there is a way to do it, but it will not gain that much. 

```
     rule write-specific(Loc:SymLoc, V:CValue, T:Type)
          => writeBytes(Loc, splitBytes(tv(V, T)), T)
          when (bitSizeofType(T) %Int cfg:bitsPerByte ==Int 0)
               andBool (isBitfieldType(T) =/=K true)
               andBool (hasUnionMarker(T) =/=K true)
          [structural]

     rule write-specific(Loc:SymLoc, V:CValue,
               t(SetItem(M:Modifier) S:Set, ST:SimpleType))
	  => midWriteSpecific(M,Loc,V,S,.Set, ST)
	  when (bitSizeofType(t(SetItem(M) S,ST)) %Int cfg:bitsPerByte =/=Int 0)
               orBool (isBitfieldType(t(SetItem(M) S,ST)) ==K true)
               orBool (hasUnionMarker(t(SetItem(M) S,ST)) ==K true)
	  [structural]


     rule midWriteSpecific(fromUnion(UnionLoc:SymLoc, 
		F:CId, Fields:FieldInfo),Loc:SymLoc,
		V:CValue,.Set,NoUnionSet:Set,ST:SimpleType)
		=> (makeUnknown(UnionLoc, F, Fields)
		   ~> write-specific(Loc, V, t(NoUnionSet,ST)))
	  [structural]

     rule midWriteSpecific(M:Modifier,Loc:SymLoc,
		V:CValue,.Set,NoUnionSet:Set
		,ST:SimpleType) => 
		write-specific(Loc, V, t(SetItem(M) NoUnionSet,ST))
	  when hasUnionMarker(t(SetItem(M),ST)) =/=K true
	  [structural]
     rule write-specific(Loc:SymLoc,
               agg(ListItem(V:CValue) ListItem(V':CValue) L:List),
               T:Type)
          => writeBytes(Loc, dataList(ListItem(V) ListItem(V') L), T)
          when (bitSizeofType(T) %Int cfg:bitsPerByte ==Int 0)
               andBool notBool isBitfieldType(T)
          [structural]

     rule write-specific(Loc:SymLoc, I:Int, T:Type)
          => write-specific(Loc, justBits(I, T), T)
          when (bitSizeofType(T) %Int cfg:bitsPerByte =/=Int 0
               orBool isBitfieldType(T))
               andBool (I <Int 0)
          [structural]
     
     rule write-specific(Loc:SymLoc, V:Int, T:Type)
          => writeBytes(Loc,
               calculateNewBytes(piece(V, bitSizeofType(T)),
                    readBytes(Loc, byteSizeofType(T), T)), T)
          when (bitSizeofType(T) %Int cfg:bitsPerByte =/=Int 0)
               orBool (isBitfieldType(T) andBool notBool hasUnionMarker(T))
               andBool (V >=Int 0)
          [structural]
```

From this set of rules which related to write-specific currently, if we want to compress it more, then it will have certain assumptions. Do you know what is the assumptions related to the write-specific function. For example, the relation among the "Loc:SymLoc, I:Int and T:Type" arguments, the specific form of the "T:Type" input argument.

Are one of these three condition always true?
```
(bitSizeofType(T) %Int cfg:bitsPerByte ==Int 0)
               andBool (isBitfieldType(T) =/=K true)
               andBool (hasUnionMarker(T) =/=K true)
```