eqSeqEmpty {
\schemaVar \term Seq s ;
\find ( s = seqEmpty )
\replacewith ( seqLen ( s )= 0 )
\heuristics (simplify )
};defined in: seqEq.key Line: 11 Offset :4eqSeqSingleton {
\schemaVar \term Seq s ;
\schemaVar \term any x ;
\find ( s = seqSingleton ( x ))
\replacewith ( seqLen ( s )= 1 & any :: seqGet ( s , 0 )= x )
\heuristics (simplify )
};defined in: seqEq.key Line: 19 Offset :4eqSeqSingleton2 {
\schemaVar \term Seq s , s2 ;
\schemaVar \term any x ;
\assumes ( seqSingleton ( x )= s2 ==> )
\find ( s = s2 )
\replacewith ( seqLen ( s )= 1 & any :: seqGet ( s , 0 )= x )
\heuristics (simplify )
};defined in: seqEq.key Line: 28 Offset :4eqSeqConcat {
\schemaVar \term Seq s , s1 , s2 ;
\find ( s = seqConcat ( s1 , s2 ))
\replacewith ( seqLen ( s )= seqLen ( s1 )+ seqLen ( s2 )& seqSub ( s , 0 , seqLen ( s1 ))= s1 & seqSub ( s , seqLen ( s1 ), seqLen ( s ))= s2 )
\heuristics (simplify_ENLARGING )
};defined in: seqEq.key Line: 38 Offset :4eqSeqConcatEQ {
\schemaVar \term Seq s , s1 , s2 , EQ ;
\assumes ( seqConcat ( s1 , s2 )= EQ ==> )
\find ( s = EQ )
\replacewith ( seqLen ( s )= seqLen ( s1 )+ seqLen ( s2 )& seqSub ( s , 0 , seqLen ( s1 ))= s1 & seqSub ( s , seqLen ( s1 ), seqLen ( s ))= s2 )
\heuristics (no_self_application , simplify_ENLARGING )
};defined in: seqEq.key Line: 51 Offset :4eqSeqConcat2 {
\schemaVar \term Seq s , s1 , s2 ;
\find ( seqConcat ( s , s1 )= seqConcat ( s , s2 ))
\replacewith ( s1 = s2 )
\heuristics (simplify )
};defined in: seqEq.key Line: 65 Offset :4eqSeqConcat2EQ {
\schemaVar \term Seq s , s1 , s2 , EQ ;
\assumes ( seqConcat ( s , s2 )= EQ ==> )
\find ( seqConcat ( s , s1 )= EQ )
\replacewith ( s1 = s2 )
\heuristics (no_self_application , simplify )
};defined in: seqEq.key Line: 74 Offset :4eqSeqConcat3 {
\schemaVar \term Seq s , s1 , s2 ;
\find ( seqConcat ( s1 , s )= seqConcat ( s2 , s ))
\replacewith ( s1 = s2 )
\heuristics (simplify )
};defined in: seqEq.key Line: 84 Offset :4eqSeqConcat3EQ {
\schemaVar \term Seq s , s1 , s2 , EQ ;
\assumes ( seqConcat ( s2 , s )= EQ ==> )
\find ( seqConcat ( s1 , s )= EQ )
\replacewith ( s1 = s2 )
\heuristics (no_self_application , simplify )
};defined in: seqEq.key Line: 93 Offset :4eqSeqConcat4 {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \term any x , y ;
\find ( seqConcat ( s1 , seqSingleton ( x ))= seqConcat ( s2 , seqSingleton ( y )))
\replacewith ( s1 = s2 & x = y )
\heuristics (simplify )
};defined in: seqEq.key Line: 103 Offset :4eqSeqConcat4EQ {
\schemaVar \term Seq s1 , s2 , EQ ;
\schemaVar \term any x , y ;
\assumes ( seqConcat ( s2 , seqSingleton ( x ))= EQ ==> )
\find ( seqConcat ( s1 , seqSingleton ( y ))= EQ )
\replacewith ( s1 = s2 & x = y )
\heuristics (no_self_application , simplify )
};defined in: seqEq.key Line: 113 Offset :4eqSeqConcat5 {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \term any x , y ;
\find ( seqConcat ( seqSingleton ( x ), s1 )= seqConcat ( seqSingleton ( y ), s2 ))
\replacewith ( x = y & s1 = s2 )
\heuristics (simplify )
};defined in: seqEq.key Line: 124 Offset :4eqSeqConcat5EQ {
\schemaVar \term Seq s1 , s2 , EQ ;
\schemaVar \term any x , y ;
\assumes ( seqConcat ( seqSingleton ( x ), s2 )= EQ ==> )
\find ( seqConcat ( seqSingleton ( y ), s1 )= EQ )
\replacewith ( x = y & s1 = s2 )
\heuristics (no_self_application , simplify )
};defined in: seqEq.key Line: 134 Offset :4eqSeqReverse {
\schemaVar \term Seq s , s2 ;
\schemaVar \variables int iv ;
\find ( s = seqReverse ( s2 ))
\varcond \replacewith ( seqLen ( s )= seqLen ( seqReverse ( s2 ))& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s , iv )= any :: seqGet ( seqReverse ( s2 ), iv )))
\heuristics (simplify_enlarging )
};defined in: seqEq.key Line: 145 Offset :4eqSeqReverse2 {
\schemaVar \term Seq s , s2 , t ;
\schemaVar \variables int iv ;
\assumes ( seqReverse ( s2 )= t ==> )
\find ( s = t )
\varcond \replacewith ( seqLen ( s )= seqLen ( seqReverse ( s2 ))& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s , iv )= any :: seqGet ( seqReverse ( s2 ), iv )))
\heuristics (simplify_enlarging , no_self_application )
};defined in: seqEq.key Line: 161 Offset :4eqSeqDef {
\schemaVar \term Seq s ;
\schemaVar \term int l , u ;
\schemaVar \term any a ;
\schemaVar \variables int i , iv ;
\find ( s = seqDef { i ; } ( l , u , a ))
\varcond \replacewith ( seqLen ( s )= seqLen ( seqDef { i ; } ( l , u , a ))& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s , iv )= any :: seqGet ( seqDef { i ; } ( l , u , a ), iv )))
\heuristics (simplify_enlarging )
};defined in: seqEq.key Line: 178 Offset :4eqSeqDef2 {
\schemaVar \term Seq s , t ;
\schemaVar \term int l , u ;
\schemaVar \term any a ;
\schemaVar \variables int i , iv ;
\assumes ( seqDef { i ; } ( l , u , a )= t ==> )
\find ( s = t )
\varcond \replacewith ( seqLen ( s )= seqLen ( seqDef { i ; } ( l , u , a ))& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s , iv )= any :: seqGet ( seqDef { i ; } ( l , u , a ), iv )))
\heuristics (simplify_enlarging )
};defined in: seqEq.key Line: 200 Offset :4\lemma eqSameSeq {
\schemaVar \term Seq seq ;
\schemaVar \term int from , to ;
\schemaVar \variables int iv ;
\find ( seqSub ( seq , from , to )= seq )
\sameUpdateLevel
\varcond \replacewith ( ( from = 0 & seqLen ( seq )= to )| ( to <= from & seqLen ( seq )= 0 )| ( seqLen ( seq )= to - from & \forall iv ; ( 0 <= iv & iv < seqLen ( seq )-> any :: seqGet ( seq , iv )= any :: seqGet ( seq , iv + from ))))
\heuristics (simplify )
};defined in: seqEq.key Line: 224 Offset :4