\lemma bsum_num_of_bounds {
\find ( bsum { uSub ; } ( i0 , i2 , \if ( phi )\then ( 1 )\else ( 0 )))
\varcond \add ( 0 <= bsum { uSub ; } ( i0 , i2 , \if ( phi )\then ( 1 )\else ( 0 )), i0 <= i2 -> bsum { uSub ; } ( i0 , i2 , \if ( phi )\then ( 1 )\else ( 0 ))<= i2 - i0 ==> )
};defined in: bsum.key Line: 60 Offset :4\lemma bsum_num_of_bounds2 {
\find ( bsum { uSub ; } ( i0 , i2 , \if ( phi )\then ( 0 )\else ( 1 )))
\varcond \add ( 0 <= bsum { uSub ; } ( i0 , i2 , \if ( phi )\then ( 0 )\else ( 1 )), i0 <= i2 -> bsum { uSub ; } ( i0 , i2 , \if ( phi )\then ( 0 )\else ( 1 ))<= i2 - i0 ==> )
};defined in: bsum.key Line: 69 Offset :4bsum_split {
\schemaVar \term int low , high ;
\schemaVar \term int middle ;
\find ( bsum { uSub ; } ( low , high , t ))
\varcond \replacewith ( \if ( low <= middle & middle <= high )\then ( bsum { uSub ; } ( low , middle , t )+ bsum { uSub ; } ( middle , high , t ))\else ( bsum { uSub ; } ( low , high , t )))
\heuristics (comprehension_split , triggered )
\trigger { middle } bsum { uSub ; } ( low , middle , t )\avoid middle <= low , middle >= high ;
};defined in: bsum.key Line: 78 Offset :4\lemma bsum_induction_upper_concrete_2 {
\find ( bsum { uSub ; } ( Z ( iz ), Z ( jz ), t ))
\varcond \replacewith ( bsum { uSub ; } ( Z ( iz ), Z ( jz )- 1 , t )+ \if ( Z ( iz )<= Z ( jz )- 1 )\then ( {\subst uSub ; ( Z ( jz )- 1 )} t )\else ( 0 ))
\heuristics (simplify )
};defined in: bsum.key Line: 125 Offset :4bsum_equal_split1 {
\find ( ==> bsum { uSub1 ; } ( i0 , i1 , t1 )= bsum { uSub2 ; } ( i0 , i2 , t2 ))
\varcond \add ( ==> i0 <= i1 & i0 <= i2 & \if ( i1 < i2 )\then ( bsum { uSub1 ; } ( i0 , i1 , t1 - {\subst uSub2 ; uSub1 } t2 )= bsum { uSub2 ; } ( i1 , i2 , t2 ))\else ( bsum { uSub1 ; } ( i2 , i1 , t1 )= bsum { uSub2 ; } ( i0 , i2 , t2 - {\subst uSub1 ; uSub2 } t1 )))
\heuristics (comprehensions )
};defined in: bsum.key Line: 186 Offset :4bsum_equal_split2 {
\assumes ( bsum { uSub1 ; } ( i0 , i1 , t1 )= i ==> )
\find ( ==> bsum { uSub2 ; } ( i0 , i2 , t2 )= i )
\varcond \add ( ==> i0 <= i1 & i0 <= i2 & \if ( i2 < i1 )\then ( bsum { uSub1 ; } ( i2 , i1 , t1 )= bsum { uSub2 ; } ( i0 , i2 , t2 - {\subst uSub1 ; uSub2 } t1 ))\else ( bsum { uSub1 ; } ( i0 , i1 , t1 - {\subst uSub2 ; uSub1 } t2 )= bsum { uSub2 ; } ( i1 , i2 , t2 )))
\heuristics (comprehensions )
};defined in: bsum.key Line: 204 Offset :4bsum_equal_split3 {
\find ( ==> bsum { uSub1 ; } ( i1 , i0 , t1 )= bsum { uSub2 ; } ( i2 , i0 , t2 ))
\varcond \add ( ==> i1 <= i0 & i2 <= i0 & \if ( i1 < i2 )\then ( bsum { uSub1 ; } ( i1 , i2 , t1 )= bsum { uSub2 ; } ( i2 , i0 , t2 - {\subst uSub1 ; uSub2 } t1 ))\else ( bsum { uSub1 ; } ( i1 , i0 , t1 - {\subst uSub2 ; uSub1 } t2 )= bsum { uSub2 ; } ( i2 , i1 , t2 )))
\heuristics (comprehensions )
};defined in: bsum.key Line: 223 Offset :4bsum_equal_split4 {
\assumes ( bsum { uSub1 ; } ( i1 , i0 , t1 )= i ==> )
\find ( ==> bsum { uSub2 ; } ( i2 , i0 , t2 )= i )
\varcond \add ( ==> i1 <= i0 & i2 <= i0 & \if ( i2 < i1 )\then ( bsum { uSub1 ; } ( i1 , i0 , t1 - {\subst uSub2 ; uSub1 } t2 )= bsum { uSub2 ; } ( i2 , i1 , t2 ))\else ( bsum { uSub1 ; } ( i1 , i2 , t1 )= bsum { uSub2 ; } ( i2 , i0 , t2 - {\subst uSub1 ; uSub2 } t1 )))
\heuristics (comprehensions )
};defined in: bsum.key Line: 241 Offset :4bsum_split_in_three {
\find ( bsum { uSub ; } ( i0 , i2 , t ))
\sameUpdateLevel
\varcond "Precondition" : \add ( ==> ( i0 <= i1 & i1 < i2 ));
"Splitted Sum" : \replacewith ( bsum { uSub ; } ( i0 , i1 , t )+ {\subst uSub ; i1 } t + bsum { uSub1 ; } ( i1 + 1 , i2 , {\subst uSub ; uSub1 } t ))
};defined in: bsum.key Line: 260 Offset :4bsum_one_summand_concrete1 {
\find ( bsum { uSub ; } ( i0 , 1 + i0 , t ))
\sameUpdateLevel
\varcond \replacewith ( {\subst uSub ; i0 } t )
\heuristics (concrete )
};defined in: bsum.key Line: 285 Offset :4bsum_one_summand_concrete2 {
\find ( bsum { uSub ; } ( - 1 + i0 , i0 , t ))
\sameUpdateLevel
\varcond \replacewith ( {\subst uSub ; - 1 + i0 } t )
\heuristics (concrete )
};defined in: bsum.key Line: 293 Offset :4bsum_zero {
\find ( bsum { uSub ; } ( i0 , i1 , 0 ))
\varcond \replacewith ( 0 )
\heuristics (concrete )
};defined in: bsum.key Line: 325 Offset :4bsum_lower_equals_upper {
\find ( bsum { uSub ; } ( i0 , i0 , t ))
\sameUpdateLevel
\varcond \replacewith ( 0 )
\heuristics (concrete )
};defined in: bsum.key Line: 333 Offset :4\lemma bsum_positive_lower_bound_element {
\schemaVar \term int index ;
\find ( bsum { uSub ; } ( i0 , i1 , t ))
\sameUpdateLevel
\varcond "Precondition" : \add ( ==> \forall uSub ; ( ( uSub >= i0 & uSub < i1 & uSub != index )-> t >= 0 )& i0 <= index & index < i1 );
"Usage" : \add ( ( {\subst uSub ; index } t )<= bsum { uSub ; } ( i0 , i1 , t )==> )
};defined in: bsum.key Line: 370 Offset :4\lemma bsum_sub_same_index {
\find ( bsum { uSub1 ; } ( i0 , i1 , t1 )- bsum { uSub2 ; } ( i0 , i1 , t2 ))
\sameUpdateLevel
\varcond \add ( bsum { uSub1 ; } ( i0 , i1 , t1 - ( {\subst uSub2 ; uSub1 } t2 ))= bsum { uSub1 ; } ( i0 , i1 , t1 )- bsum { uSub2 ; } ( i0 , i1 , t2 )==> )
};defined in: bsum.key Line: 384 Offset :4\lemma bsum_less_same_index {
\find ( ==> bsum { uSub1 ; } ( i0 , i1 , t1 )< bsum { uSub2 ; } ( i0 , i1 , t2 ))
\sameUpdateLevel
\varcond \add ( ==> \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )-> t1 <= ( {\subst uSub2 ; uSub1 } t2 ))& \exists uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )& t1 < ( {\subst uSub2 ; uSub1 } t2 )))
};defined in: bsum.key Line: 398 Offset :4equal_bsum1 {
\find ( ==> bsum { uSub1 ; } ( i0 , i1 , t1 )= bsum { uSub2 ; } ( i0 , i1 , t2 ))
\varcond \add ( ==> \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )-> t1 = ( {\subst uSub2 ; uSub1 } t2 )))
\heuristics (comprehensions )
\displayname "equal_bsum_same_index"
};defined in: bsum.key Line: 430 Offset :4equal_bsum2 {
\assumes ( bsum { uSub1 ; } ( i0 , i1 , t1 )= i ==> )
\find ( ==> bsum { uSub2 ; } ( i0 , i1 , t2 )= i )
\varcond \add ( ==> \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )-> t1 = ( {\subst uSub2 ; uSub1 } t2 )))
\heuristics (comprehensions )
\displayname "equal_bsum_same_index"
};defined in: bsum.key Line: 444 Offset :4equal_bsum3 {
\assumes ( bsum { uSub1 ; } ( i0 , i1 , t1 )= i , bsum { uSub2 ; } ( i0 , i1 , t2 )= j ==> )
\find ( ==> j = i )
\varcond \add ( ==> \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )-> t1 = ( {\subst uSub2 ; uSub1 } t2 )))
\heuristics (comprehensions )
\displayname "equal_bsum_same_index"
};defined in: bsum.key Line: 459 Offset :4\lemma bsum_equal_except_one_index {
\schemaVar \term int index ;
\find ( ==> bsum { uSub1 ; } ( i0 , i1 , t1 )= bsum { uSub2 ; } ( i0 , i1 , t2 )+ t )
\sameUpdateLevel
\varcond "Precondition" : \add ( ==> i0 <= index & index < i1 & \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 & uSub1 != index )-> t1 = ( {\subst uSub2 ; uSub1 } t2 )));
"Usage" : \add ( ==> t = ( ( {\subst uSub1 ; index } t1 )- ( {\subst uSub2 ; index } t2 )))
};defined in: bsum.key Line: 474 Offset :4equal_bsum5 {
\find ( ==> bsum { uSub1 ; } ( i0 , i1 , t1 )= bsum { uSub2 ; } ( i2 , i3 , t2 ))
\varcond "Equal length" : \add ( ==> i1 - i0 = i3 - i2 );
"Equal elements" : \add ( ==> \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )-> t1 = ( {\subst uSub2 ; uSub1 + i2 - i0 } t2 )))
\heuristics (comprehensions_high_costs )
\displayname "equal_bsum"
};defined in: bsum.key Line: 503 Offset :4\lemma bsum_num_of_lt_max2 {
\assumes ( i2 > i0 & i0 >= 0 ==> )
\find ( \exists uSub ; ( ( uSub >= i0 & uSub < i2 )& ! phi )==> )
\varcond \add ( bsum { uSub ; } ( i0 , i2 , \if ( phi )\then ( 1 )\else ( 0 ))< i2 - i0 ==> )
\heuristics (simplify_enlarging )
};defined in: bsum.key Line: 572 Offset :4equal_bsum_perm2 {
\assumes ( bsum { uSub2 ; } ( i2 , i3 , t2 )= t ==> )
\find ( ==> bsum { uSub1 ; } ( i0 , i1 , t1 )= t )
\varcond \add ( ==> seqPerm ( seqDef { uSub1 ; } ( i0 , i1 , t1 ), seqDef { uSub2 ; } ( i2 , i3 , t2 )))
\displayname "equal_bsum_perm"
};defined in: bsum.key Line: 638 Offset :4bsum_add {
\find ( bsum { uSub1 ; } ( i0 , i1 , t1 )+ bsum { uSub2 ; } ( i2 , i3 , t2 ))
\varcond \replacewith ( bsum { uSub1 ; } ( \if ( i0 < i2 )\then ( i0 )\else ( i2 ), \if ( i1 > i3 )\then ( i1 )\else ( i3 ), {\subst uSub2 ; uSub1 } ( \if ( i0 <= uSub1 & uSub1 < i1 )\then ( t1 )\else ( 0 )+ \if ( i2 <= uSub1 & uSub1 < i3 )\then ( t2 )\else ( 0 ))))
};defined in: bsum.key Line: 698 Offset :4\lemma bsum_add_concrete {
\find ( bsum { uSub1 ; } ( i0 , i1 , t1 )+ bsum { uSub2 ; } ( i1 , i3 , t2 ))
\varcond \add ( ==> i0 <= i1 & i1 <= i3 );
\replacewith ( bsum { uSub1 ; } ( i0 , i3 , {\subst uSub2 ; uSub1 } \if ( uSub1 < i1 )\then ( t1 )\else ( t2 )))
};defined in: bsum.key Line: 712 Offset :4sum_empty {
\schemaVar \variables alpha x ;
\find ( sum { x ; } ( FALSE , t ))
\replacewith ( 0 )
\heuristics (concrete )
};defined in: bsum.key Line: 727 Offset :4sum_zero {
\schemaVar \variables alpha x ;
\schemaVar \term boolean range ;
\find ( sum { x ; } ( range , 0 ))
\replacewith ( 0 )
\heuristics (concrete )
};defined in: bsum.key Line: 734 Offset :4