seqNPermDefReplace {
\schemaVar \term Seq s1 ;
\schemaVar \variables int iv , jv ;
\find ( seqNPerm ( s1 ))
\varcond \replacewith ( ( \forall iv ; ( 0 <= iv & iv < seqLen ( s1 )-> \exists jv ; ( 0 <= jv & jv < seqLen ( s1 )& any :: seqGet ( s1 , jv )= iv ))))
};defined in: seqPerm.key Line: 32 Offset :4seqNPermDefLeft {
\schemaVar \term Seq s1 ;
\schemaVar \variables int iv , jv ;
\find ( seqNPerm ( s1 )==> )
\varcond \add ( ( \forall iv ; ( 0 <= iv & iv < seqLen ( s1 )-> \exists jv ; ( 0 <= jv & jv < seqLen ( s1 )& any :: seqGet ( s1 , jv )= iv )))==> )
};defined in: seqPerm.key Line: 44 Offset :4seqPermDefLeft {
\schemaVar \term Seq s1 , s2 , s3 ;
\schemaVar \variables int iv ;
\schemaVar \variables Seq s ;
\find ( seqPerm ( s1 , s2 )==> )
\varcond \add ( seqLen ( s1 )= seqLen ( s2 )& ( \exists s ; ( seqLen ( s )= seqLen ( s1 )& seqNPerm ( s )& ( \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s1 , iv )= any :: seqGet ( s2 , int :: seqGet ( s , iv ))))))==> )
};defined in: seqPerm.key Line: 56 Offset :4seqPermDef {
\schemaVar \term Seq s1 , s2 , s3 ;
\schemaVar \variables int iv ;
\schemaVar \variables Seq s ;
\find ( seqPerm ( s1 , s2 ))
\varcond \replacewith ( seqLen ( s1 )= seqLen ( s2 )& ( \exists s ; ( seqLen ( s )= seqLen ( s1 )& seqNPerm ( s )& ( \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s1 , iv )= any :: seqGet ( s2 , int :: seqGet ( s , iv )))))))
};defined in: seqPerm.key Line: 75 Offset :4defOfSeqSwap {
\schemaVar \term Seq s ;
\schemaVar \term int iv , jv ;
\schemaVar \variables int uSub ;
\find ( seqSwap ( s , iv , jv ))
\varcond \replacewith ( seqDef { uSub ; } ( 0 , seqLen ( s ), \if ( ! ( 0 <= iv & 0 <= jv & iv < seqLen ( s )& jv < seqLen ( s )))\then ( any :: seqGet ( s , uSub ))\else ( \if ( uSub = iv )\then ( any :: seqGet ( s , jv ))\else ( \if ( uSub = jv )\then ( any :: seqGet ( s , iv ))\else ( any :: seqGet ( s , uSub ))))))
};defined in: seqPerm.key Line: 94 Offset :4defOfSeqRemove {
\schemaVar \term Seq s ;
\schemaVar \term int iv ;
\schemaVar \variables int uSub ;
\find ( seqRemove ( s , iv ))
\varcond \replacewith ( \if ( iv < 0 | seqLen ( s )<= iv )\then ( s )\else ( seqDef { uSub ; } ( 0 , seqLen ( s )- 1 , \if ( uSub < iv )\then ( any :: seqGet ( s , uSub ))\else ( any :: seqGet ( s , uSub + 1 )))))
};defined in: seqPerm.key Line: 115 Offset :4defOfSeqNPermInv {
\schemaVar \term Seq s ;
\schemaVar \variables int uSub ;
\find ( seqNPermInv ( s ))
\varcond \replacewith ( seqDef { uSub ; } ( 0 , seqLen ( s ), seqIndexOf ( s , uSub )))
};defined in: seqPerm.key Line: 138 Offset :4lenOfNPermInv {
\schemaVar \term Seq s1 ;
\find ( seqLen ( seqNPermInv ( s1 )))
\replacewith ( seqLen ( s1 ))
\heuristics (simplify )
};defined in: seqPerm.key Line: 156 Offset :4\lemma getAnyOfNPermInv {
\schemaVar \term Seq s1 ;
\schemaVar \term int i3 ;
\find ( any :: seqGet ( seqNPermInv ( s1 ), i3 ))
\replacewith ( int :: seqGet ( seqNPermInv ( s1 ), i3 ));
\add ( ==> 0 <= i3 & i3 < seqLen ( s1 ))
\heuristics (simplify )
};defined in: seqPerm.key Line: 164 Offset :4getOfNPermInv {
\schemaVar \term Seq s1 ;
\schemaVar \term int i3 ;
\schemaVar \skolemTerm int jsk ;
\find ( int :: seqGet ( seqNPermInv ( s1 ), i3 ))
\varcond \replacewith ( jsk ) \add ( int :: seqGet ( s1 , jsk )= i3 & 0 <= jsk & jsk < seqLen ( s1 )==> );
\add ( ==> 0 <= i3 & i3 < seqLen ( s1 )& seqNPerm ( s1 ))
\heuristics (simplify )
};defined in: seqPerm.key Line: 175 Offset :4lenOfSwap {
\schemaVar \term Seq s1 ;
\schemaVar \term int iv1 , iv2 ;
\find ( seqLen ( seqSwap ( s1 , iv1 , iv2 )))
\replacewith ( seqLen ( s1 ))
\heuristics (simplify )
};defined in: seqPerm.key Line: 189 Offset :4getOfSwap {
\schemaVar \term Object o ;
\schemaVar \term Seq s1 ;
\schemaVar \term int iv , jv , idx ;
\schemaVar \term Heap h ;
\find ( alpha :: seqGet ( seqSwap ( s1 , iv , jv ), idx ))
\replacewith ( \if ( ! ( 0 <= iv & 0 <= jv & iv < seqLen ( s1 )& jv < seqLen ( s1 )))\then ( alpha :: seqGet ( s1 , idx ))\else ( \if ( idx = iv )\then ( alpha :: seqGet ( s1 , jv ))\else ( \if ( idx = jv )\then ( alpha :: seqGet ( s1 , iv ))\else ( alpha :: seqGet ( s1 , idx )))))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 198 Offset :4lenOfRemove {
\schemaVar \term Seq s1 ;
\schemaVar \term int iv1 ;
\find ( seqLen ( seqRemove ( s1 , iv1 )))
\replacewith ( \if ( 0 <= iv1 & iv1 < seqLen ( s1 ))\then ( seqLen ( s1 )- 1 )\else ( seqLen ( s1 )))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 219 Offset :4getOfRemoveAny {
\schemaVar \term Seq s1 ;
\schemaVar \term int i3 , i2 ;
\find ( alpha :: seqGet ( seqRemove ( s1 , i2 ), i3 ))
\replacewith ( \if ( i2 < 0 | seqLen ( s1 )<= i2 )\then ( alpha :: seqGet ( s1 , i3 ))\else ( \if ( i3 < i2 )\then ( alpha :: seqGet ( s1 , i3 ))\else ( \if ( i2 <= i3 & i3 < seqLen ( s1 )- 1 )\then ( alpha :: seqGet ( s1 , i3 + 1 ))\else ( (alpha ) seqGetOutside ))))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 235 Offset :4getOfRemoveInt {
\schemaVar \term Seq s1 ;
\schemaVar \term int i3 , i2 ;
\find ( int :: seqGet ( seqRemove ( s1 , i2 ), i3 ))
\replacewith ( \if ( i2 < 0 | seqLen ( s1 )<= i2 )\then ( int :: seqGet ( s1 , i3 ))\else ( \if ( i3 < i2 )\then ( int :: seqGet ( s1 , i3 ))\else ( \if ( i2 <= i3 & i3 < seqLen ( s1 )- 1 )\then ( int :: seqGet ( s1 , i3 + 1 ))\else ( (int ) seqGetOutside ))))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 251 Offset :4lenOfRemoveConcrete1 {
\schemaVar \term Seq s1 ;
\assumes ( seqLen ( s1 )>= 1 ==> )
\find ( seqLen ( seqRemove ( s1 , seqLen ( s1 )- 1 )))
\replacewith ( seqLen ( s1 )- 1 )
\heuristics (simplify )
};defined in: seqPerm.key Line: 267 Offset :4lenOfRemoveConcrete2 {
\schemaVar \term Seq s1 ;
\assumes ( seqLen ( s1 )>= 1 ==> )
\find ( seqLen ( seqRemove ( s1 , 0 )))
\replacewith ( seqLen ( s1 )- 1 )
\heuristics (simplify )
};defined in: seqPerm.key Line: 277 Offset :4getOfRemoveAnyConcrete1 {
\schemaVar \term Seq s1 ;
\schemaVar \term int i3 , i2 ;
\assumes ( seqLen ( s1 )>= 1 ==> )
\find ( alpha :: seqGet ( seqRemove ( s1 , seqLen ( s1 )- 1 ), i3 ))
\replacewith ( \if ( i3 < seqLen ( s1 )- 1 )\then ( alpha :: seqGet ( s1 , i3 ))\else ( (alpha ) seqGetOutside ))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 290 Offset :4getOfRemoveAnyConcrete2 {
\schemaVar \term Seq s1 ;
\schemaVar \term int i3 , i2 ;
\assumes ( seqLen ( s1 )>= 1 ==> )
\find ( alpha :: seqGet ( seqRemove ( s1 , 0 ), i3 ))
\replacewith ( \if ( 0 <= i3 & i3 < seqLen ( s1 )- 1 )\then ( alpha :: seqGet ( s1 , i3 + 1 ))\else ( (alpha ) seqGetOutside ))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 305 Offset :4\lemma seqNPermRange {
\schemaVar \term Seq s ;
\schemaVar \variables int iv ;
\find ( seqNPerm ( s )==> )
\varcond \add ( \forall iv ; ( ( 0 <= iv & iv < seqLen ( s ))-> ( 0 <= int :: seqGet ( s , iv )& int :: seqGet ( s , iv )< seqLen ( s )& int :: instance ( any :: seqGet ( s , iv ))= TRUE ))==> )
};defined in: seqPerm.key Line: 339 Offset :4seqNPermInjective {
\schemaVar \term Seq s ;
\schemaVar \variables int iv , jv ;
\find ( seqNPerm ( s )==> )
\varcond \add ( \forall iv ; ( \forall jv ; ( ( 0 <= iv & iv < seqLen ( s )& 0 <= jv & jv < seqLen ( s )& int :: seqGet ( s , iv )= int :: seqGet ( s , jv ))-> iv = jv ))==> )
};defined in: seqPerm.key Line: 358 Offset :4\lemma seqPermRefl {
\schemaVar \term Seq s ;
\find ( seqPerm ( s , s ))
\replacewith ( true )
\heuristics (concrete )
};defined in: seqPerm.key Line: 382 Offset :4seqPermEmpty1 {
\schemaVar \term Seq s ;
\find ( seqPerm ( seqEmpty , s ))
\replacewith ( seqEmpty = s )
\heuristics (simplify )
\displayname "seqPermEmpty"
};defined in: seqPerm.key Line: 390 Offset :4seqPermEmpty2 {
\schemaVar \term Seq s ;
\find ( seqPerm ( s , seqEmpty ))
\replacewith ( seqEmpty = s )
\heuristics (simplify )
\displayname "seqPermEmpty"
};defined in: seqPerm.key Line: 398 Offset :4seqNPermSwapNPerm {
\schemaVar \term Seq s1 ;
\schemaVar \variables int iv , jv ;
\find ( seqNPerm ( s1 )==> )
\varcond \add ( \forall iv ; ( \forall jv ; ( ( 0 <= iv & 0 <= jv & iv < seqLen ( s1 )& jv < seqLen ( s1 ))-> seqNPerm ( seqSwap ( s1 , iv , jv ))))==> )
};defined in: seqPerm.key Line: 406 Offset :4seqNPermEmpty {
\find ( seqNPerm ( seqEmpty ))
\replacewith ( true )
\heuristics (concrete )
};defined in: seqPerm.key Line: 420 Offset :4seqNPermSingletonConrete {
\find ( seqNPerm ( seqSingleton ( 0 )))
\replacewith ( true )
\heuristics (concrete )
};defined in: seqPerm.key Line: 427 Offset :4seqNPermSingleton {
\schemaVar \term int si ;
\find ( seqNPerm ( seqSingleton ( si )))
\replacewith ( si = 0 )
\heuristics (simplify )
};defined in: seqPerm.key Line: 434 Offset :4seqNPermComp {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \variables int u ;
\assumes ( seqNPerm ( s2 )& seqLen ( s1 )= seqLen ( s2 )==> )
\find ( seqNPerm ( s1 )==> )
\varcond \add ( seqNPerm ( seqDef { u ; } ( 0 , seqLen ( s1 ), int :: seqGet ( s1 , int :: seqGet ( s2 , u ))))==> )
};defined in: seqPerm.key Line: 441 Offset :4seqNPermInvNPermLeft {
\schemaVar \term Seq s1 ;
\find ( seqNPerm ( s1 )==> )
\add ( seqNPerm ( seqNPermInv ( s1 ))==> )
};defined in: seqPerm.key Line: 465 Offset :4seqPermSym {
\schemaVar \term Seq s1 , s2 ;
\find ( seqPerm ( s1 , s2 ))
\replacewith ( seqPerm ( s2 , s1 ))
};defined in: seqPerm.key Line: 473 Offset :4seqNPermInvNPermReplace {
\schemaVar \term Seq s1 ;
\find ( seqNPerm ( seqNPermInv ( s1 )))
\replacewith ( seqNPerm ( s1 ))
};defined in: seqPerm.key Line: 479 Offset :4seqnormalizeDef {
\schemaVar \term Seq s1 ;
\schemaVar \term int le , ri ;
\schemaVar \term any t ;
\schemaVar \variables int u ;
\find ( seqDef { u ; } ( le , ri , t ))
\varcond \replacewith ( \if ( le < ri )\then ( seqDef { u ; } ( 0 , ( ri - le ), ( {\subst u ; ( u + le )} t )))\else ( seqEmpty ))
};defined in: seqPerm.key Line: 511 Offset :4\lemma seqNPermRight {
\schemaVar \term Seq s ;
\schemaVar \variables int iv , jv ;
\find ( ==> seqNPerm ( s ))
\varcond \add ( ==> \forall iv ; ( \forall jv ; ( ( 0 <= iv & iv < seqLen ( s )& 0 <= jv & jv < seqLen ( s )& int :: seqGet ( s , iv )= int :: seqGet ( s , jv ))-> iv = jv ))& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> 0 <= int :: seqGet ( s , iv )& int :: seqGet ( s , iv )< seqLen ( s ))& \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> int :: instance ( any :: seqGet ( s , iv ))= TRUE ))
};defined in: seqPerm.key Line: 525 Offset :4\lemma seqPermFromSwap {
\schemaVar \term Seq s1 , s2 , t1 , t2 ;
\schemaVar \variables int iv , jv ;
\assumes ( seqPerm ( s1 , t1 )==> )
\find ( ==> seqPerm ( s2 , t2 ))
\varcond \replacewith ( ==> t1 = t2 & \exists iv ; \exists jv ; ( 0 <= iv & 0 <= jv & iv < s2 . length & jv < s2 . length & s1 = seqSwap ( s2 , iv , jv )))
};defined in: seqPerm.key Line: 540 Offset :4\lemma seqSwapPreservesSeqPerm {
\schemaVar \term Seq s ;
\schemaVar \term int x ;
\schemaVar \term int y ;
\find ( ==> seqPerm ( s , seqSwap ( s , x , y )))
\add ( ==> 0 <= x & x < seqLen ( s )& 0 <= y & y < seqLen ( s ))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 561 Offset :4\lemma seqSwapPreservesSeqPermEQ {
\schemaVar \term Seq s ;
\schemaVar \term Seq EQ ;
\schemaVar \term int x ;
\schemaVar \term int y ;
\assumes ( seqSwap ( s , x , y )= EQ ==> )
\find ( ==> seqPerm ( s , EQ ))
\add ( ==> 0 <= x & x < seqLen ( s )& 0 <= y & y < seqLen ( s ))
\heuristics (simplify_enlarging )
};defined in: seqPerm.key Line: 572 Offset :4\lemma seqPermTransAlt0 {
\schemaVar \term Seq s1 , s2 , s3 , x , y ;
\assumes ( seqPerm ( s2 , s3 )==> seqPerm ( x , y ))
\find ( seqPerm ( s1 , s2 )==> )
\add ( seqPerm ( s1 , s3 )==> )
\heuristics (inReachableStateImplication )
\displayname "seqPermTrans"
};defined in: seqPerm.key Line: 595 Offset :4\lemma seqPermTransAlt1 {
\schemaVar \term Seq a , b , c , x , y ;
\assumes ( seqPerm ( a , b )==> seqPerm ( x , y ))
\find ( seqPerm ( a , c )==> )
\add ( seqPerm ( b , c )==> )
\heuristics (inReachableStateImplication )
\displayname "seqPermTrans"
};defined in: seqPerm.key Line: 606 Offset :4\lemma seqPermTransAlt2 {
\schemaVar \term Seq a , b , c , x , y ;
\assumes ( seqPerm ( a , c )==> seqPerm ( x , y ))
\find ( seqPerm ( b , c )==> )
\add ( seqPerm ( a , b )==> )
\heuristics (inReachableStateImplication )
\displayname "seqPermTrans"
};defined in: seqPerm.key Line: 617 Offset :4\lemma seqPermTransAlt3 {
\schemaVar \term Seq a , b , c , x , y ;
\assumes ( seqPerm ( a , c )==> seqPerm ( x , y ))
\find ( seqPerm ( b , a )==> )
\add ( seqPerm ( b , c )==> )
\heuristics (inReachableStateImplication )
\displayname "seqPermTrans"
};defined in: seqPerm.key Line: 628 Offset :4seqPermCountsInt {
\schemaVar \term Seq s1 , s2 ;
\schemaVar \variables int iv ;
\schemaVar \variables any element ;
\find ( seqPerm ( s1 , s2 ))
\varcond \replacewith ( ( \forall element ; bsum { iv ; } ( 0 , s1 . length , \if ( any :: seqGet ( s1 , iv )= element )\then ( 1 )\else ( 0 ))= bsum { iv ; } ( 0 , s2 . length , \if ( any :: seqGet ( s2 , iv )= element )\then ( 1 )\else ( 0 ))))
};defined in: seqPerm.key Line: 640 Offset :4\lemma seqPermForall {
\schemaVar \term Seq s1 ;
\schemaVar \term Seq s2 ;
\schemaVar \formula phi ;
\schemaVar \variable int iv ;
\schemaVar \variable any x ;
\assumes ( seqPerm ( s1 , s2 )==> )
\varcond \add ( \forall iv ; ( 0 <= iv & iv < seqLen ( s1 )-> {\subst x ; any :: seqGet ( s1 , iv )} phi )<-> \forall iv ; ( 0 <= iv & iv < seqLen ( s1 )-> {\subst x ; any :: seqGet ( s2 , iv )} phi )==> )
};defined in: seqPerm.key Line: 660 Offset :4\lemma seqPermExists {
\schemaVar \term Seq s1 ;
\schemaVar \term Seq s2 ;
\schemaVar \formula phi ;
\schemaVar \variable int iv ;
\schemaVar \variable any x ;
\assumes ( seqPerm ( s1 , s2 )==> )
\varcond \add ( \exists iv ; ( 0 <= iv & iv < seqLen ( s1 )& {\subst x ; any :: seqGet ( s1 , iv )} phi )<-> \exists iv ; ( 0 <= iv & iv < seqLen ( s1 )& {\subst x ; any :: seqGet ( s2 , iv )} phi )==> )
};defined in: seqPerm.key Line: 674 Offset :4