lenNonNegative {
\schemaVar \term Seq seq ;
\find ( seqLen ( seq ))
\sameUpdateLevel
\add ( 0 <= seqLen ( seq )==> )
\heuristics (inReachableStateImplication )
};defined in: seqCoreRules.key Line: 23 Offset :4equalityToSeqGetAndSeqLen {
\schemaVar \term Seq left , right ;
\schemaVar \variables int iv ;
\find ( left = right )
\varcond \replacewith ( seqLen ( left )= seqLen ( right )& \forall iv ; ( 0 <= iv & iv < seqLen ( left )-> any :: seqGet ( left , iv )= any :: seqGet ( right , iv )))
\heuristics (defOpsSeqEquality )
};defined in: seqCoreRules.key Line: 38 Offset :4getOfSeqDef {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( alpha :: seqGet ( seqDef { uSub ; } ( from , to , t ), idx ))
\varcond \replacewith ( \if ( 0 <= idx & idx < ( to - from ))\then ( (alpha ) {\subst uSub ; ( idx + from )} t )\else ( (alpha ) seqGetOutside ))
\heuristics (simplify )
};defined in: seqCoreRules.key Line: 55 Offset :4lenOfSeqDef {
\schemaVar \term int from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqLen ( seqDef { uSub ; } ( from , to , t )))
\replacewith ( \if ( from < to )\then ( ( to - from ))\else ( 0 ))
\heuristics (simplify )
};defined in: seqCoreRules.key Line: 70 Offset :4