\lemma schiffl_lemma_2 {
\schemaVar \term Seq s , t ;
\schemaVar \variable Seq r ;
\schemaVar \variable int x , y , iv ;
\find ( seqPerm ( s , t )==> )
\varcond \add ( \forall x ; \forall y ; ( any :: seqGet ( s , x )= any :: seqGet ( t , x )& any :: seqGet ( s , y )= any :: seqGet ( t , y )& 0 <= x & x < seqLen ( s )& 0 <= y & y < seqLen ( s )-> \exists r ; ( seqLen ( r )= seqLen ( s )& seqNPerm ( r )& ( \forall iv ; ( 0 <= iv & iv < seqLen ( s )-> any :: seqGet ( s , iv )= any :: seqGet ( t , int :: seqGet ( r , iv ))))& int :: seqGet ( r , x )= x & int :: seqGet ( r , y )= y ))==> )
};defined in: seqPerm2.key Line: 16 Offset :4\lemma schiffl_thm_1 {
\schemaVar \term Seq s , t ;
\schemaVar \term int x , y ;
\schemaVar \term any a , b ;
\schemaVar \variables int idx ;
\find ( seqPerm ( s , t )==> )
\varcond \add ( seqPerm ( s , t )& any :: seqGet ( s , x )= any :: seqGet ( t , x )& any :: seqGet ( s , y )= any :: seqGet ( t , y )& 0 <= x & x < seqLen ( s )& 0 <= y & y < seqLen ( s )-> seqPerm ( seqDef { idx ; } ( 0 , s . length , \if ( idx = y )\then ( b )\else ( \if ( idx = x )\then ( a )\else ( any :: seqGet ( s , idx )))), seqDef { idx ; } ( 0 , s . length , \if ( idx = y )\then ( b )\else ( \if ( idx = x )\then ( a )\else ( any :: seqGet ( t , idx )))))==> )
};defined in: seqPerm2.key Line: 40 Offset :4