defIsFinite {
\schemaVar \variables any vx ;
\schemaVar \variables int ix ;
\schemaVar \variables Seq s ;
\find ( isFinite ( m ))
\varcond \replacewith ( \exists s ; ( \forall vx ; ( inDomain ( m , vx )<-> ( \exists ix ; ( 0 <= ix & ix < seqLen ( s )& any :: seqGet ( s , ix )= vx )))))
};defined in: mapSize.key Line: 29 Offset :4isFiniteOfMapEmpty {
\find ( isFinite ( mapEmpty ))
\sameUpdateLevel
\replacewith ( true )
\heuristics (simplify )
};defined in: mapSize.key Line: 45 Offset :4isFiniteOfMapRemove {
\find ( isFinite ( mapRemove ( m , key )))
\sameUpdateLevel
\replacewith ( isFinite ( m ))
\heuristics (simplify )
};defined in: mapSize.key Line: 52 Offset :4isFiniteOfMapUpdate {
\find ( isFinite ( mapUpdate ( m , key , value )))
\sameUpdateLevel
\replacewith ( isFinite ( m ))
\heuristics (simplify )
};defined in: mapSize.key Line: 59 Offset :4isFiniteOfMapSingleton {
\find ( isFinite ( mapSingleton ( key , value )))
\sameUpdateLevel
\replacewith ( true )
\heuristics (simplify )
};defined in: mapSize.key Line: 66 Offset :4isFiniteOfSeq2Map {
\schemaVar \term Seq s ;
\find ( isFinite ( seq2map ( s )))
\sameUpdateLevel
\replacewith ( true )
\heuristics (simplify )
};defined in: mapSize.key Line: 73 Offset :4sizeOfMapEmpty {
\find ( mapSize ( mapEmpty ))
\sameUpdateLevel
\replacewith ( 0 )
\heuristics (simplify )
};defined in: mapSize.key Line: 85 Offset :4sizeOfMapUpdate {
\find ( mapSize ( mapUpdate ( m , key , value )))
\add ( isFinite ( m )-> ( mapSize ( mapUpdate ( m , key , value ))= \if ( inDomain ( m , key ))\then ( mapSize ( m ))\else ( mapSize ( m )+ 1 ))==> )
\heuristics (inReachableStateImplication )
};defined in: mapSize.key Line: 105 Offset :4sizeOfMapSingleton {
\find ( mapSize ( mapSingleton ( key , value )))
\sameUpdateLevel
\replacewith ( 1 )
\heuristics (simplify )
};defined in: mapSize.key Line: 114 Offset :4sizeOfSeq2Map {
\schemaVar \term Seq s ;
\find ( mapSize ( seq2map ( s )))
\sameUpdateLevel
\replacewith ( seqLen ( s ))
\heuristics (simplify )
};defined in: mapSize.key Line: 121 Offset :4mapSizeNotNegativeForFiniteMaps {
\find ( mapSize ( m ))
\add ( isFinite ( m )-> ( mapSize ( m )>= 0 )==> )
\heuristics (inReachableStateImplication )
};defined in: mapSize.key Line: 129 Offset :4