bprod_empty {
\find ( bprod { uSub ; } ( i0 , i1 , t ))
\sameUpdateLevel
\varcond "Precondition" : \add ( ==> i1 <= i0 );
"Empty Sum" : \replacewith ( 1 )
};defined in: bprod.key Line: 21 Offset :4bprod_find {
\schemaVar \term int low , high , middle ;
\find ( bprod { uSub ; } ( low , high , t ))
\varcond \replacewith ( \if ( low <= middle & middle <= high )\then ( bprod { uSub ; } ( low , middle , t )* bprod { uSub ; } ( middle , high , t ))\else ( bprod { uSub ; } ( low , high , t )))
\heuristics (comprehension_split , triggered )
\trigger { middle } bprod { uSub ; } ( low , middle , t )\avoid middle <= low , middle >= high ;
};defined in: bprod.key Line: 41 Offset :4bprod_one_factor_concrete1 {
\find ( bprod { uSub ; } ( i0 , 1 + i0 , t ))
\sameUpdateLevel
\varcond \replacewith ( {\subst uSub ; i0 } t )
\heuristics (concrete )
};defined in: bprod.key Line: 137 Offset :4bprod_one_factor_concrete2 {
\find ( bprod { uSub ; } ( - 1 + i0 , i0 , t ))
\sameUpdateLevel
\varcond \replacewith ( {\subst uSub ; - 1 + i0 } t )
\heuristics (concrete )
};defined in: bprod.key Line: 146 Offset :4bprod_one {
\find ( bprod { uSub ; } ( i0 , i1 , 1 ))
\varcond \replacewith ( 1 )
\heuristics (concrete )
};defined in: bprod.key Line: 164 Offset :4bprod_lower_equals_upper {
\find ( bprod { uSub ; } ( i0 , i0 , t ))
\sameUpdateLevel
\varcond \replacewith ( 1 )
\heuristics (concrete )
};defined in: bprod.key Line: 173 Offset :4equal_bprod1 {
\find ( ==> bprod { uSub1 ; } ( i0 , i1 , t1 )= bprod { uSub2 ; } ( i0 , i1 , t2 ))
\varcond \add ( ==> \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )-> t1 = ( {\subst uSub2 ; uSub1 } t2 )))
\heuristics (comprehensions )
\displayname "equal_bprod_same_index"
};defined in: bprod.key Line: 181 Offset :4equal_bprod2 {
\assumes ( bprod { uSub1 ; } ( i0 , i1 , t1 )= i ==> )
\find ( ==> bprod { uSub2 ; } ( i0 , i1 , t2 )= i )
\varcond \add ( ==> \forall uSub1 ; ( ( uSub1 >= i0 & uSub1 < i1 )-> t1 = ( {\subst uSub2 ; uSub1 } t2 )))
\heuristics (comprehensions )
\displayname "equal_bprod_same_index"
};defined in: bprod.key Line: 196 Offset :4equal_bprod3 {
\assumes ( bprod { uSub1 ; } ( i0 , i1 , t1 )= i , bprod { 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_bprod_same_index"
};defined in: bprod.key Line: 212 Offset :4equal_bprod5 {
\find ( ==> bprod { uSub1 ; } ( i0 , i1 , t1 )= bprod { 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_bprod"
};defined in: bprod.key Line: 228 Offset :4equal_bprod_perm2 {
\assumes ( bprod { uSub2 ; } ( i2 , i3 , t2 )= t ==> )
\find ( ==> bprod { uSub1 ; } ( i0 , i1 , t1 )= t )
\varcond \add ( ==> seqPerm ( seqDef { uSub1 ; } ( i0 , i1 , t1 ), seqDef { uSub2 ; } ( i2 , i3 , t2 )))
\displayname "equal_bprod_perm"
};defined in: bprod.key Line: 284 Offset :4\lemma bprod_split {
\schemaVar \term int middle ;
\find ( bprod { uSub ; } ( i0 , i1 , t1 ))
\varcond \replacewith ( \if ( i0 <= middle & middle <= i1 )\then ( bprod { uSub ; } ( i0 , middle , t1 )* bprod { uSub ; } ( middle , i1 , t1 ))\else ( bprod { uSub ; } ( i0 , i1 , t1 )))
};defined in: bprod.key Line: 311 Offset :4prod_empty {
\schemaVar \variables alpha x ;
\find ( prod { x ; } ( FALSE , t ))
\replacewith ( 1 )
\heuristics (concrete )
};defined in: bprod.key Line: 329 Offset :4prod_one {
\schemaVar \variables alpha x ;
\schemaVar \term boolean range ;
\find ( prod { x ; } ( range , 1 ))
\replacewith ( 1 )
\heuristics (concrete )
};defined in: bprod.key Line: 336 Offset :4