\generic alpha, beta;defined in: seqRules.key Line: 12 Offset :4\generic alpha, beta;defined in: seqRules.key Line: 12 Offset :4defOfEmpty {
\schemaVar \term any te ;
\schemaVar \variables int uSub ;
\find ( seqEmpty )
\varcond \replacewith ( seqDef { uSub ; } ( 0 , 0 , te ))
};defined in: seqRules.key Line: 26 Offset :4defOfSeqSingleton {
\schemaVar \term any x ;
\schemaVar \variables int uSub ;
\find ( seqSingleton ( x ))
\varcond \replacewith ( seqDef { uSub ; } ( 0 , 1 , x ))
};defined in: seqRules.key Line: 36 Offset :4defOfSeqConcat {
\schemaVar \term Seq seq1 , seq2 ;
\schemaVar \variables int uSub ;
\find ( seqConcat ( seq1 , seq2 ))
\varcond \replacewith ( seqDef { uSub ; } ( 0 , seqLen ( seq1 )+ seqLen ( seq2 ), \if ( uSub < seqLen ( seq1 ))\then ( any :: seqGet ( seq1 , uSub ))\else ( any :: seqGet ( seq2 , uSub - seqLen ( seq1 )))))
};defined in: seqRules.key Line: 46 Offset :4defOfSeqSub {
\schemaVar \term Seq seq ;
\schemaVar \term int from , to ;
\schemaVar \variables int uSub ;
\find ( seqSub ( seq , from , to ))
\varcond \replacewith ( seqDef { uSub ; } ( from , to , any :: seqGet ( seq , uSub )))
};defined in: seqRules.key Line: 70 Offset :4defOfSeqReverse {
\schemaVar \term Seq seq ;
\schemaVar \variables int uSub ;
\find ( seqReverse ( seq ))
\varcond \replacewith ( seqDef { uSub ; } ( 0 , seqLen ( seq ), any :: seqGet ( seq , seqLen ( seq )- uSub - 1 )))
};defined in: seqRules.key Line: 83 Offset :4defOfSeqUpd {
\schemaVar \term Seq seq ;
\schemaVar \term int idx ;
\schemaVar \term any value ;
\schemaVar \variables int uSub ;
\find ( seqUpd ( seq , idx , value ))
\varcond \replacewith ( seqDef { uSub ; } ( 0 , seqLen ( seq ), \if ( uSub = idx )\then ( value )\else ( any :: seqGet ( seq , uSub ))))
};defined in: seqRules.key Line: 94 Offset :4seqIndexOf {
\schemaVar \term Seq s ;
\schemaVar \term any t ;
\schemaVar \skolemTerm int jsk ;
\schemaVar \variables int n , m ;
\find ( seqIndexOf ( s , t ))
\varcond \add ( ( \exists n ; ( 0 <= n & n < seqLen ( s )& any :: seqGet ( s , n )= t ))-> ( 0 <= seqIndexOf ( s , t )& seqIndexOf ( s , t )< seqLen ( s )& any :: seqGet ( s , seqIndexOf ( s , t ))= t & \forall m ; ( ( 0 <= m & m < seqIndexOf ( s , t ))-> any :: seqGet ( s , m )!= t ))==> )
};defined in: seqRules.key Line: 114 Offset :4\lemma seqSelfDefinition {
\schemaVar \term Seq seq ;
\schemaVar \variables Seq s ;
\schemaVar \variables int u ;
\find ( seq )
\add ( \forall s ; ( s = seqDef { u ; } ( 0 , seqLen ( s ), any :: seqGet ( s , u )))==> )
};defined in: seqRules.key Line: 146 Offset :4\lemma seqOutsideValue {
\schemaVar \variables Seq s ;
\schemaVar \variables int iv ;
\find ( seqGetOutside )
\add ( \forall s ; ( \forall iv ; ( ( iv < 0 | seqLen ( s )<= iv )-> any :: seqGet ( s , iv )= seqGetOutside ))==> )
};defined in: seqRules.key Line: 155 Offset :4\lemma castedGetAny {
\schemaVar \term Seq seq ;
\schemaVar \term int idx ;
\find ( (beta ) any :: seqGet ( seq , idx ))
\replacewith ( beta :: seqGet ( seq , idx ))
\heuristics (simplify )
};defined in: seqRules.key Line: 168 Offset :4\lemma getOfSeqSingleton {
\schemaVar \term any x ;
\schemaVar \term int idx ;
\find ( alpha :: seqGet ( seqSingleton ( x ), idx ))
\replacewith ( \if ( idx = 0 )\then ( (alpha ) x )\else ( (alpha ) seqGetOutside ))
\heuristics (simplify )
};defined in: seqRules.key Line: 194 Offset :4\lemma getOfSeqSingletonConcrete {
\schemaVar \term any x ;
\find ( alpha :: seqGet ( seqSingleton ( x ), 0 ))
\replacewith ( (alpha ) x )
\heuristics (concrete )
};defined in: seqRules.key Line: 208 Offset :4\lemma getOfSeqConcat {
\schemaVar \term Seq seq , seq2 ;
\schemaVar \term int idx ;
\find ( alpha :: seqGet ( seqConcat ( seq , seq2 ), idx ))
\replacewith ( \if ( idx < seqLen ( seq ))\then ( alpha :: seqGet ( seq , idx ))\else ( alpha :: seqGet ( seq2 , idx - seqLen ( seq ))))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 216 Offset :4\lemma getOfSeqSub {
\schemaVar \term Seq seq ;
\schemaVar \term int idx , from , to ;
\find ( alpha :: seqGet ( seqSub ( seq , from , to ), idx ))
\replacewith ( \if ( 0 <= idx & idx < ( to - from ))\then ( alpha :: seqGet ( seq , idx + from ))\else ( (alpha ) seqGetOutside ))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 230 Offset :4\lemma getOfSeqReverse {
\schemaVar \term Seq seq ;
\schemaVar \term int idx ;
\find ( alpha :: seqGet ( seqReverse ( seq ), idx ))
\replacewith ( alpha :: seqGet ( seq , seqLen ( seq )- 1 - idx ))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 244 Offset :4\lemma getOfSeqUpd {
\schemaVar \term Seq seq ;
\schemaVar \term int idx , jdx ;
\schemaVar \term any value ;
\find ( alpha :: seqGet ( seqUpd ( seq , idx , value ), jdx ))
\replacewith ( \if ( 0 <= jdx & jdx < seqLen ( seq )& idx = jdx )\then ( (alpha ) value )\else ( alpha :: seqGet ( seq , jdx )))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 256 Offset :4\lemma lenOfSeqEmpty {
\find ( seqLen ( seqEmpty ))
\replacewith ( 0 )
\heuristics (concrete )
};defined in: seqRules.key Line: 271 Offset :4\lemma lenOfSeqSingleton {
\schemaVar \term alpha x ;
\find ( seqLen ( seqSingleton ( x )))
\replacewith ( 1 )
\heuristics (concrete )
};defined in: seqRules.key Line: 280 Offset :4\lemma lenOfSeqConcat {
\schemaVar \term Seq seq , seq2 ;
\find ( seqLen ( seqConcat ( seq , seq2 )))
\replacewith ( seqLen ( seq )+ seqLen ( seq2 ))
\heuristics (simplify )
};defined in: seqRules.key Line: 291 Offset :4\lemma lenOfSeqSub {
\schemaVar \term Seq seq ;
\schemaVar \term int from , to ;
\find ( seqLen ( seqSub ( seq , from , to )))
\replacewith ( \if ( from < to )\then ( to - from )\else ( 0 ))
\heuristics (simplify )
};defined in: seqRules.key Line: 302 Offset :4\lemma lenOfSeqReverse {
\schemaVar \term Seq seq ;
\find ( seqLen ( seqReverse ( seq )))
\replacewith ( seqLen ( seq ))
\heuristics (simplify )
};defined in: seqRules.key Line: 314 Offset :4\lemma lenOfSeqUpd {
\schemaVar \term Seq seq ;
\schemaVar \term int idx ;
\schemaVar \term any value ;
\find ( seqLen ( seqUpd ( seq , idx , value )))
\replacewith ( seqLen ( seq ))
\heuristics (simplify )
};defined in: seqRules.key Line: 325 Offset :4\lemma equalityToSeqGetAndSeqLenLeft {
\schemaVar \term Seq s , s2 ;
\schemaVar \variables int iv ;
\find ( s = s2 ==> )
\varcond \add ( seqLen ( s )= seqLen ( s2 )& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s , iv )= any :: seqGet ( s2 , iv ))==> )
\heuristics (inReachableStateImplication )
};defined in: seqRules.key Line: 341 Offset :4\lemma equalityToSeqGetAndSeqLenRight {
\schemaVar \term Seq s , s2 ;
\schemaVar \variables int iv ;
\find ( ==> s = s2 )
\varcond \replacewith ( ==> seqLen ( s )= seqLen ( s2 )& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s , iv )= any :: seqGet ( s2 , iv )))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 357 Offset :4\lemma getOfSeqSingletonEQ {
\schemaVar \term any x ;
\schemaVar \term int idx ;
\schemaVar \term Seq EQ ;
\assumes ( seqSingleton ( x )= EQ ==> )
\find ( alpha :: seqGet ( EQ , idx ))
\sameUpdateLevel
\replacewith ( \if ( idx = 0 )\then ( (alpha ) x )\else ( (alpha ) seqGetOutside ))
\heuristics (no_self_application , simplify_enlarging )
\displayname "getOfSeqSingleton"
};defined in: seqRules.key Line: 372 Offset :4\lemma getOfSeqConcatEQ {
\schemaVar \term Seq seq , seq2 ;
\schemaVar \term int idx ;
\schemaVar \term Seq EQ ;
\assumes ( seqConcat ( seq , seq2 )= EQ ==> )
\find ( alpha :: seqGet ( EQ , idx ))
\sameUpdateLevel
\replacewith ( \if ( idx < seqLen ( seq ))\then ( alpha :: seqGet ( seq , idx ))\else ( alpha :: seqGet ( seq2 , idx - seqLen ( seq ))))
\heuristics (no_self_application , simplify_enlarging )
\displayname "getOfSeqConcat"
};defined in: seqRules.key Line: 390 Offset :4\lemma getOfSeqSubEQ {
\schemaVar \term Seq seq ;
\schemaVar \term int idx , from , to ;
\schemaVar \term Seq EQ ;
\assumes ( seqSub ( seq , from , to )= EQ ==> )
\find ( alpha :: seqGet ( EQ , idx ))
\sameUpdateLevel
\replacewith ( \if ( 0 <= idx & idx < ( to - from ))\then ( alpha :: seqGet ( seq , idx + from ))\else ( (alpha ) seqGetOutside ))
\heuristics (no_self_application , simplify_enlarging )
\displayname "getOfSeqSub"
};defined in: seqRules.key Line: 408 Offset :4\lemma getOfSeqReverseEQ {
\schemaVar \term Seq seq ;
\schemaVar \term int idx ;
\schemaVar \term Seq EQ ;
\assumes ( seqReverse ( seq )= EQ ==> )
\find ( alpha :: seqGet ( EQ , idx ))
\sameUpdateLevel
\replacewith ( alpha :: seqGet ( seq , seqLen ( seq )- 1 - idx ))
\heuristics (no_self_application , simplify_enlarging )
\displayname "getOfSeqReverse"
};defined in: seqRules.key Line: 426 Offset :4\lemma lenOfSeqEmptyEQ {
\schemaVar \term alpha x ;
\schemaVar \term Seq EQ ;
\assumes ( seqEmpty = EQ ==> )
\find ( seqLen ( EQ ))
\sameUpdateLevel
\replacewith ( 0 )
\heuristics (concrete )
\displayname "lenOfSeqEmpty"
};defined in: seqRules.key Line: 442 Offset :4\lemma lenOfSeqSingletonEQ {
\schemaVar \term alpha x ;
\schemaVar \term Seq EQ ;
\assumes ( seqSingleton ( x )= EQ ==> )
\find ( seqLen ( EQ ))
\sameUpdateLevel
\replacewith ( 1 )
\heuristics (concrete )
\displayname "lenOfSeqSingleton"
};defined in: seqRules.key Line: 456 Offset :4\lemma lenOfSeqConcatEQ {
\schemaVar \term Seq seq , seq2 ;
\schemaVar \term Seq EQ ;
\assumes ( seqConcat ( seq , seq2 )= EQ ==> )
\find ( seqLen ( EQ ))
\sameUpdateLevel
\replacewith ( seqLen ( seq )+ seqLen ( seq2 ))
\heuristics (simplify )
\displayname "lenOfSeqConcat"
};defined in: seqRules.key Line: 470 Offset :4\lemma lenOfSeqSubEQ {
\schemaVar \term Seq seq ;
\schemaVar \term int from , to ;
\schemaVar \term Seq EQ ;
\assumes ( seqSub ( seq , from , to )= EQ ==> )
\find ( seqLen ( EQ ))
\sameUpdateLevel
\replacewith ( \if ( from < to )\then ( to - from )\else ( 0 ))
\heuristics (simplify , find_term_not_in_assumes )
\displayname "lenOfSeqSub"
};defined in: seqRules.key Line: 485 Offset :4\lemma lenOfSeqReverseEQ {
\schemaVar \term Seq seq ;
\schemaVar \term Seq EQ ;
\assumes ( seqReverse ( seq )= EQ ==> )
\find ( seqLen ( EQ ))
\sameUpdateLevel
\replacewith ( seqLen ( seq ))
\heuristics (simplify )
\displayname "lenOfSeqReverse"
};defined in: seqRules.key Line: 501 Offset :4\lemma getOfSeqDefEQ {
\schemaVar \term int idx , from , to ;
\schemaVar \term Seq EQ ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\assumes ( seqDef { uSub ; } ( from , to , t )= EQ ==> )
\find ( alpha :: seqGet ( EQ , idx ))
\sameUpdateLevel
\varcond \replacewith ( \if ( 0 <= idx & idx < ( to - from ))\then ( (alpha ) {\subst uSub ; ( idx + from )} t )\else ( (alpha ) seqGetOutside ))
\heuristics (simplify_enlarging )
\displayname "getOfSeqDef"
};defined in: seqRules.key Line: 516 Offset :4\lemma lenOfSeqDefEQ {
\schemaVar \term int from , to ;
\schemaVar \term Seq EQ ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\assumes ( seqDef { uSub ; } ( from , to , t )= EQ ==> )
\find ( seqLen ( EQ ))
\sameUpdateLevel
\replacewith ( \if ( from <= to )\then ( ( to - from ))\else ( 0 ))
\heuristics (simplify )
\displayname "lenOfSeqDef"
};defined in: seqRules.key Line: 536 Offset :4\lemma seqConcatWithSeqEmpty1 {
\schemaVar \term Seq seq ;
\find ( seqConcat ( seq , seqEmpty ))
\replacewith ( seq )
\heuristics (concrete )
\displayname "seqConcatWithEmpty"
};defined in: seqRules.key Line: 557 Offset :4\lemma seqConcatWithSeqEmpty2 {
\schemaVar \term Seq seq ;
\find ( seqConcat ( seqEmpty , seq ))
\replacewith ( seq )
\heuristics (concrete )
\displayname "seqConcatWithEmpty"
};defined in: seqRules.key Line: 569 Offset :4\lemma seqReverseOfSeqEmpty {
\find ( seqReverse ( seqEmpty ))
\replacewith ( seqEmpty )
\heuristics (concrete )
};defined in: seqRules.key Line: 581 Offset :4subSeqCompleteSeqDef {
\schemaVar \term int u ;
\schemaVar \term any a ;
\schemaVar \variables int i ;
\find ( seqSub ( seqDef { i ; } ( 0 , u , a ), 0 , u ))
\replacewith ( seqDef { i ; } ( 0 , u , a ))
\heuristics (concrete )
};defined in: seqRules.key Line: 594 Offset :4\lemma subSeqComplete {
\schemaVar \term Seq seq ;
\find ( seqSub ( seq , 0 , seqLen ( seq )))
\replacewith ( seq )
\heuristics (concrete )
};defined in: seqRules.key Line: 605 Offset :4subSeqCompleteSeqDefEQ {
\schemaVar \term int u ;
\schemaVar \term any a ;
\schemaVar \variables int i ;
\schemaVar \term Seq EQ ;
\assumes ( seqDef { i ; } ( 0 , u , a )= EQ ==> )
\find ( seqSub ( EQ , 0 , u ))
\replacewith ( seqDef { i ; } ( 0 , u , a ))
\heuristics (no_self_application , concrete )
};defined in: seqRules.key Line: 614 Offset :4subSeqEmpty {
\schemaVar \term Seq seq ;
\schemaVar \term int i ;
\find ( seqSub ( seq , i , i ))
\replacewith ( seqEmpty )
\heuristics (concrete )
};defined in: seqRules.key Line: 626 Offset :4\lemma subSeqTailR {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\find ( seqSub ( seqConcat ( seqSingleton ( x ), seq ), 1 , seqLen ( seq )+ 1 ))
\replacewith ( seq )
\heuristics (concrete )
\displayname "subSeqTail"
};defined in: seqRules.key Line: 634 Offset :4\lemma subSeqTailL {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\find ( seqSub ( seqConcat ( seqSingleton ( x ), seq ), 1 , 1 + seqLen ( seq )))
\replacewith ( seq )
\heuristics (concrete )
\displayname "subSeqTail"
};defined in: seqRules.key Line: 647 Offset :4subSeqSingleton {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\find ( seqSub ( seqSingleton ( x ), 0 , 1 ))
\replacewith ( seqSingleton ( x ))
\heuristics (concrete )
};defined in: seqRules.key Line: 660 Offset :4subSeqSingletonEQ {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\schemaVar \term Seq EQ ;
\assumes ( seqSingleton ( x )= EQ ==> )
\find ( seqSub ( EQ , 0 , 1 ))
\replacewith ( seqSingleton ( x ))
\heuristics (concrete )
};defined in: seqRules.key Line: 671 Offset :4\lemma subSeqTailEQR {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\schemaVar \term int EQ ;
\assumes ( seqLen ( seq )= EQ ==> )
\find ( seqSub ( seqConcat ( seqSingleton ( x ), seq ), 1 , EQ + 1 ))
\sameUpdateLevel
\replacewith ( seq )
\heuristics (concrete )
\displayname "subSeqTail"
};defined in: seqRules.key Line: 684 Offset :4\lemma subSeqTailEQL {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\schemaVar \term int EQ ;
\assumes ( seqLen ( seq )= EQ ==> )
\find ( seqSub ( seqConcat ( seqSingleton ( x ), seq ), 1 , 1 + EQ ))
\sameUpdateLevel
\replacewith ( seq )
\heuristics (concrete )
\displayname "subSeqTail"
};defined in: seqRules.key Line: 700 Offset :4subSeqSingleton2 {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\schemaVar \term int l , u ;
\find ( seqSub ( seqSingleton ( x ), l , u ))
\replacewith ( seqConcat ( seqSub ( seqEmpty , \if ( l < 0 )\then ( l )\else ( 0 ), \if ( u < 0 )\then ( u )\else ( 0 )), seqConcat ( \if ( l <= 0 & u >= 1 )\then ( seqSingleton ( x ))\else ( seqEmpty ), seqSub ( seqEmpty , \if ( l > 0 )\then ( l )\else ( 1 ), \if ( u > 0 )\then ( u )\else ( 1 )))))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 716 Offset :4subSeqSingleton2EQ {
\schemaVar \term Seq seq ;
\schemaVar \term any x ;
\schemaVar \term int l , u ;
\schemaVar \term Seq EQ ;
\assumes ( seqSingleton ( x )= EQ ==> )
\find ( seqSub ( EQ , l , u ))
\replacewith ( seqConcat ( seqSub ( seqEmpty , \if ( l < 0 )\then ( l )\else ( 0 ), \if ( u < 0 )\then ( u )\else ( 0 )), seqConcat ( \if ( l <= 0 & u >= 1 )\then ( seqSingleton ( x ))\else ( seqEmpty ), seqSub ( seqEmpty , \if ( l > 0 )\then ( l )\else ( 1 ), \if ( u > 0 )\then ( u )\else ( 1 )))))
\heuristics (no_self_application , simplify_enlarging )
};defined in: seqRules.key Line: 736 Offset :4subSeqConcat {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \term int l , u ;
\find ( seqSub ( seqConcat ( s1 , s2 ), l , u ))
\replacewith ( seqConcat ( seqSub ( s1 , l , \if ( seqLen ( s1 )< u )\then ( seqLen ( s1 ))\else ( u )), seqSub ( s2 , \if ( l < seqLen ( s1 ))\then ( 0 )\else ( l - seqLen ( s1 )), u - seqLen ( s1 ))))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 758 Offset :4subSeqConcatEQ {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \term int l , u ;
\schemaVar \term Seq EQ ;
\assumes ( seqConcat ( s1 , s2 )= EQ ==> )
\find ( seqSub ( EQ , l , u ))
\replacewith ( seqConcat ( seqSub ( s1 , l , \if ( seqLen ( s1 )< u )\then ( seqLen ( s1 ))\else ( u )), seqSub ( s2 , \if ( l < seqLen ( s1 ))\then ( 0 )\else ( l - seqLen ( s1 )), u - seqLen ( s1 ))))
\heuristics (no_self_application , simplify_enlarging )
};defined in: seqRules.key Line: 771 Offset :4subSeqHeadSeqDef {
\schemaVar \term Seq seq ;
\schemaVar \term any a ;
\schemaVar \term int u ;
\schemaVar \variables int i ;
\find ( seqSub ( seqConcat ( seqDef { i ; } ( 0 , u , a ), seq ), 0 , u ))
\replacewith ( seqDef { i ; } ( 0 , u , a ))
\heuristics (concrete )
};defined in: seqRules.key Line: 785 Offset :4subSeqHeadSeqDefEQ {
\schemaVar \term Seq seq ;
\schemaVar \term any a ;
\schemaVar \term int u ;
\schemaVar \variables int i ;
\schemaVar \term Seq EQ ;
\assumes ( seqDef { i ; } ( 0 , u , a )= EQ ==> )
\find ( seqSub ( seqConcat ( EQ , seq ), 0 , u ))
\replacewith ( seqDef { i ; } ( 0 , u , a ))
\heuristics (concrete )
};defined in: seqRules.key Line: 796 Offset :4\lemma seqDef_split {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( from , to , t ))
\varcond \replacewith ( \if ( from <= idx & idx < to )\then ( seqConcat ( seqDef { uSub ; } ( from , idx , t ), seqDef { uSub1 ; } ( idx , to , {\subst uSub ; uSub1 } t )))\else ( seqDef { uSub ; } ( from , to , t )))
};defined in: seqRules.key Line: 815 Offset :4\lemma seqDef_induction_upper {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( from , to , t ))
\varcond \replacewith ( seqConcat ( seqDef { uSub ; } ( from , to - 1 , t ), \if ( from < to )\then ( seqSingleton ( {\subst uSub ; ( to - 1 )} t ))\else ( seqEmpty )))
};defined in: seqRules.key Line: 837 Offset :4\lemma seqDef_induction_upper_concrete {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( from , 1 + to , t ))
\varcond \replacewith ( seqConcat ( seqDef { uSub ; } ( from , to , t ), \if ( from <= to )\then ( seqSingleton ( {\subst uSub ; ( to )} t ))\else ( seqEmpty )))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 852 Offset :4\lemma seqDef_induction_lower {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( from , to , t ))
\varcond \replacewith ( seqConcat ( \if ( from < to )\then ( seqSingleton ( {\subst uSub ; ( from )} t ))\else ( seqEmpty ), seqDef { uSub ; } ( from + 1 , to , t )))
};defined in: seqRules.key Line: 868 Offset :4\lemma seqDef_induction_lower_concrete {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( - 1 + from , to , t ))
\varcond \replacewith ( seqConcat ( \if ( - 1 + from < to )\then ( seqSingleton ( {\subst uSub ; ( - 1 + from )} t ))\else ( seqEmpty ), seqDef { uSub ; } ( from , to , t )))
\heuristics (simplify )
};defined in: seqRules.key Line: 883 Offset :4\lemma seqDef_split_in_three {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( from , to , t ))
\sameUpdateLevel
\varcond "Precondition" : \add ( ==> ( from <= idx & idx < to ));
"Splitted SeqDef" : \replacewith ( seqConcat ( seqDef { uSub ; } ( from , idx , t ), seqConcat ( seqSingleton ( {\subst uSub ; idx } t ), seqDef { uSub1 ; } ( idx + 1 , to , {\subst uSub ; uSub1 } t ))))
};defined in: seqRules.key Line: 899 Offset :4\lemma seqDef_empty {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( from , idx , t ))
\sameUpdateLevel
\varcond "Precondition" : \add ( ==> idx <= from );
"Empty SeqDef" : \replacewith ( seqEmpty )
};defined in: seqRules.key Line: 922 Offset :4\lemma seqDef_one_summand {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( from , idx , t ))
\sameUpdateLevel
\varcond \replacewith ( \if ( from + 1 = idx )\then ( seqSingleton ( {\subst uSub ; from } t ))\else ( seqDef { uSub ; } ( from , idx , t )))
};defined in: seqRules.key Line: 938 Offset :4\lemma seqDef_lower_equals_upper {
\schemaVar \term int idx , from , to ;
\schemaVar \term any t ;
\schemaVar \variables int uSub , uSub1 , uSub2 ;
\find ( seqDef { uSub ; } ( idx , idx , t ))
\sameUpdateLevel
\varcond \replacewith ( seqEmpty )
\heuristics (simplify )
};defined in: seqRules.key Line: 953 Offset :4\lemma seqDefOfSeq {
\schemaVar \term int x ;
\schemaVar \term Seq s ;
\schemaVar \variables int u , v ;
\find ( seqDef { u ; } ( 0 , x , any :: seqGet ( s , u )))
\varcond \replacewith ( \if ( seqLen ( s )= x )\then ( s )\else ( \if ( seqLen ( s )> x )\then ( seqSub ( s , 0 , x ))\else ( seqConcat ( s , seqDef { v ; } ( seqLen ( s ), x , seqGetOutside )))))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 966 Offset :4\lemma seqSelfDefinitionEQ2 {
\schemaVar \term Seq s ;
\schemaVar \term int x ;
\schemaVar \variables int u ;
\assumes ( seqLen ( s )= x ==> )
\find ( seqDef { u ; } ( 0 , x , any :: seqGet ( s , u )))
\sameUpdateLevel
\varcond \replacewith ( s )
\heuristics (simplify )
\displayname "seqSelfDefinition"
};defined in: seqRules.key Line: 989 Offset :4\lemma indexOfSeqSingleton {
\schemaVar \term any x ;
\find ( seqIndexOf ( seqSingleton ( x ), x ))
\sameUpdateLevel
\replacewith ( 0 )
\heuristics (concrete )
};defined in: seqRules.key Line: 1023 Offset :4\lemma indexOfSeqConcatFirst {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \term any x ;
\schemaVar \variables int idx ;
\find ( seqIndexOf ( seqConcat ( s1 , s2 ), x ))
\sameUpdateLevel
\varcond \replacewith ( seqIndexOf ( s1 , x ));
\add ( ==> \exists idx ; ( 0 <= idx & idx < seqLen ( s1 )& any :: seqGet ( s1 , idx )= x ))
};defined in: seqRules.key Line: 1032 Offset :4\lemma indexOfSeqConcatSecond {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \term any x ;
\schemaVar \variables int idx ;
\find ( seqIndexOf ( seqConcat ( s1 , s2 ), x ))
\sameUpdateLevel
\varcond \replacewith ( add ( seqIndexOf ( s2 , x ), seqLen ( s1 )));
\add ( ==> ( ! \exists idx ; ( 0 <= idx & idx < seqLen ( s1 )& any :: seqGet ( s1 , idx )= x )& \exists idx ; ( 0 <= idx & idx < seqLen ( s2 )& any :: seqGet ( s2 , idx )= x )))
};defined in: seqRules.key Line: 1045 Offset :4\lemma indexOfSeqSub {
\schemaVar \term Seq s ;
\schemaVar \term int from , to , n ;
\schemaVar \term any x ;
\schemaVar \variables int nx ;
\find ( seqIndexOf ( seqSub ( s , from , to ), x ))
\sameUpdateLevel
\varcond \replacewith ( sub ( seqIndexOf ( s , x ), from ));
\add ( ==> from <= seqIndexOf ( s , x )& seqIndexOf ( s , x )< to & 0 <= from & \exists nx ; ( ( 0 <= nx & nx < seqLen ( s )& any :: seqGet ( s , nx )= x )))
};defined in: seqRules.key Line: 1060 Offset :4definitionSeqdefWorkaround {
\schemaVar \term int lower ;
\schemaVar \term int upper ;
\schemaVar \term Object array ;
\schemaVar \term Heap h ;
\schemaVar \variables int j ;
\find ( seq_def_workaround ( h , lower , upper , array ))
\varcond \replacewith ( seqDef { j ; } ( lower , upper , any :: select ( h , array , arr ( j ))))
\heuristics (concrete )
};defined in: seqRules.key Line: 1083 Offset :4definitionSeqdefWorkaround2 {
\schemaVar \term int lower ;
\schemaVar \term int upper ;
\schemaVar \term Object array , o ;
\schemaVar \term Heap h ;
\schemaVar \term Field f ;
\schemaVar \variables int j ;
\find ( seq_def_workaround2 ( h , lower , upper , array , singleton ( o , f )))
\varcond \replacewith ( seqDef { j ; } ( lower , upper , any :: select ( h , Object :: select ( h , array , arr ( j )), f )))
\heuristics (concrete )
};defined in: seqRules.key Line: 1110 Offset :4array2seqDef {
\schemaVar \term Object a ;
\schemaVar \term Heap h ;
\schemaVar \variables int u ;
\find ( array2seq ( h , a ))
\varcond \replacewith ( seqDef { u ; } ( 0 , length ( a ), any :: select ( h , a , arr ( u ))))
\heuristics (simplify_enlarging )
};defined in: seqRules.key Line: 1147 Offset :4\lemma lenOfArray2seq {
\schemaVar \term Object a ;
\schemaVar \term Heap h ;
\find ( seqLen ( array2seq ( h , a )))
\replacewith ( length ( a ))
};defined in: seqRules.key Line: 1161 Offset :4\lemma getAnyOfArray2seq {
\schemaVar \term Object a ;
\schemaVar \term int idx ;
\schemaVar \term Heap h ;
\find ( any :: seqGet ( array2seq ( h , a ), idx ))
\replacewith ( any :: select ( h , a , arr ( idx )));
\add ( ==> 0 <= idx & idx < length ( a ))
};defined in: seqRules.key Line: 1169 Offset :4\lemma getOfArray2seq {
\schemaVar \term Object a ;
\schemaVar \term int idx ;
\schemaVar \term Heap h ;
\find ( alpha :: seqGet ( array2seq ( h , a ), idx ))
\replacewith ( alpha :: select ( h , a , arr ( idx )));
\add ( ==> 0 <= idx & idx < length ( a ))
};defined in: seqRules.key Line: 1179 Offset :4