translate0 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 0 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '0' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 13 Offset :4translate1 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 1 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '1' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 20 Offset :4translate2 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 2 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '2' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 27 Offset :4translate3 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 3 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '3' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 34 Offset :4translate4 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 4 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '4' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 41 Offset :4translate5 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 5 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '5' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 48 Offset :4translate6 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 6 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '6' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 55 Offset :4translate7 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 7 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '7' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 62 Offset :4translate8 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 8 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '8' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 69 Offset :4translate9 {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( 9 ( iz ))))
\replacewith ( seqConcat ( clTranslateInt ( Z ( iz )), seqSingleton ( '9' )))
\heuristics (integerToString )
};defined in: charListRules.key Line: 76 Offset :4translate# {
\find ( clTranslateInt ( Z ( #)))
\replacewith ( seqEmpty )
\heuristics (integerToString )
};defined in: charListRules.key Line: 83 Offset :4translateNegLit {
\schemaVar \term numbers iz ;
\find ( clTranslateInt ( Z ( neglit ( iz ))))
\replacewith ( seqConcat ( seqSingleton ( '-' ), clTranslateInt ( Z ( iz ))))
\heuristics (integerToString )
};defined in: charListRules.key Line: 89 Offset :4removeZeros {
\schemaVar \term Seq l ;
\find ( clRemoveZeros ( l ))
\replacewith ( \if ( l = seqEmpty | int :: seqGet ( l , 0 )= '0' )\then ( l )\else ( clRemoveZeros ( seqSub ( l , 1 , seqLen ( l )))))
\heuristics (integerToString )
};defined in: charListRules.key Line: 100 Offset :4containsAxiomAntec {
\schemaVar \term Seq searchString , textString ;
\schemaVar \variables int iv ;
\find ( clContains ( textString , searchString )==> )
\varcond \replacewith ( \exists iv ; ( iv >= 0 & iv + seqLen ( searchString )<= seqLen ( textString )& seqSub ( textString , iv , iv + seqLen ( searchString ))= searchString )==> )
\heuristics (stringsExpandDefNormalOp )
};defined in: charListRules.key Line: 116 Offset :4containsAxiomSucc {
\schemaVar \term Seq searchString , textString ;
\schemaVar \variables int iv ;
\find ( ==> clContains ( textString , searchString ))
\varcond \replacewith ( ==> \exists iv ; ( iv >= 0 & iv + seqLen ( searchString )<= seqLen ( textString )& seqSub ( textString , iv , iv + seqLen ( searchString ))= searchString ))
\heuristics (stringsExpandDefNormalOp )
};defined in: charListRules.key Line: 129 Offset :4contains {
\schemaVar \term Seq searchString , textStringTail ;
\schemaVar \term int fstTextCharacter ;
\schemaVar \skolemTerm int newSym ;
\find ( clContains ( seqConcat ( seqSingleton ( fstTextCharacter ), textStringTail ), searchString ))
\sameUpdateLevel
\varcond \replacewith ( newSym < seqLen ( textStringTail )& ( seqSub ( seqConcat ( seqSingleton ( fstTextCharacter ), textStringTail ), 0 , newSym )= searchString | clContains ( textStringTail , searchString ))) \add ( seqLen ( searchString )= newSym ==> )
\heuristics (stringsContainsDefInline , stringsIntroduceNewSym )
};defined in: charListRules.key Line: 142 Offset :4indexOf {
\schemaVar \term Seq l ;
\schemaVar \term int c ;
\schemaVar \term int i ;
\schemaVar \variables int iv ;
\find ( clIndexOfChar ( l , c , i ))
\varcond \replacewith ( \ifEx iv ; ( i >= 0 & iv >= i & iv < seqLen ( l )& int :: seqGet ( l , iv )= c )\then ( iv )\else ( - 1 ))
\heuristics (stringsExpandDefNormalOp )
};defined in: charListRules.key Line: 162 Offset :4replaceEmpty {
\schemaVar \term int searchChar , replChar ;
\find ( clReplace ( seqEmpty , searchChar , replChar ))
\replacewith ( seqEmpty )
\heuristics (stringsSimplify )
};defined in: charListRules.key Line: 185 Offset :4replaceSingleton {
\schemaVar \term Seq str ;
\schemaVar \term int searchChar , replChar , fstChar ;
\find ( clReplace ( seqSingleton ( fstChar ), searchChar , replChar ))
\replacewith ( \if ( searchChar = fstChar )\then ( seqSingleton ( replChar ))\else ( seqSingleton ( fstChar )))
\heuristics (stringsSimplify )
};defined in: charListRules.key Line: 193 Offset :4replaceCons {
\schemaVar \term Seq str ;
\schemaVar \term int searchChar , replChar , fstChar ;
\find ( clReplace ( seqConcat ( seqSingleton ( fstChar ), str ), searchChar , replChar ))
\replacewith ( \if ( searchChar = fstChar )\then ( seqConcat ( seqSingleton ( replChar ), clReplace ( str , searchChar , replChar )))\else ( seqConcat ( seqSingleton ( fstChar ), clReplace ( str , searchChar , replChar ))))
\heuristics (defOpsReplaceInline )
};defined in: charListRules.key Line: 204 Offset :4replaceDef {
\schemaVar \term Seq str ;
\schemaVar \skolemTerm Seq newSym ;
\schemaVar \term int searchChar , replChar ;
\schemaVar \variables int pos ;
\find ( clReplace ( str , searchChar , replChar ))
\sameUpdateLevel
\varcond \add ( clReplace ( str , searchChar , replChar )= newSym & seqDef { pos ; } ( 0 , seqLen ( str ), \if ( int :: seqGet ( str , pos )= searchChar )\then ( replChar )\else ( int :: seqGet ( str , pos )))= newSym ==> )
\heuristics (defOpsReplace , stringsIntroduceNewSym )
};defined in: charListRules.key Line: 217 Offset :4endsWith {
\schemaVar \term Seq sourceStr , searchStr ;
\find ( clEndsWith ( sourceStr , searchStr ))
\replacewith ( \if ( seqLen ( searchStr )> seqLen ( sourceStr ))\then ( false )\else ( seqSub ( sourceStr , seqLen ( sourceStr )- seqLen ( searchStr ), seqLen ( sourceStr ))= searchStr ))
\heuristics (defOpsStartsEndsWith )
};defined in: charListRules.key Line: 242 Offset :4startsWith {
\schemaVar \term Seq sourceStr , searchStr ;
\find ( clStartsWith ( sourceStr , searchStr ))
\replacewith ( \if ( seqLen ( searchStr )> seqLen ( sourceStr ))\then ( false )\else ( seqSub ( sourceStr , 0 , seqLen ( searchStr ))= searchStr ))
\heuristics (defOpsStartsEndsWith )
};defined in: charListRules.key Line: 259 Offset :4indexOfStr {
\schemaVar \term Seq searchStr , sourceStr ;
\schemaVar \term int i ;
\schemaVar \variables int iv ;
\find ( clIndexOfCl ( sourceStr , i , searchStr ))
\varcond \replacewith ( \ifEx iv ; ( iv >= i & iv >= 0 & iv + seqLen ( searchStr )<= seqLen ( sourceStr )& ( seqSub ( sourceStr , iv , iv + seqLen ( searchStr ))= searchStr ))\then ( iv )\else ( - 1 ))
\heuristics (stringsExpandDefNormalOp )
};defined in: charListRules.key Line: 272 Offset :4lastIndexOf {
\schemaVar \term Seq sourceStr ;
\schemaVar \term int c ;
\schemaVar \term int i ;
\schemaVar \variables int iv ;
\find ( clLastIndexOfChar ( sourceStr , c , i ))
\varcond \replacewith ( \ifEx iv ; ( iv > 0 & i >= iv & i - iv < seqLen ( sourceStr )& int :: seqGet ( sourceStr , i - iv )= c )\then ( i - iv )\else ( - 1 ))
\heuristics (stringsExpandDefNormalOp )
};defined in: charListRules.key Line: 290 Offset :4lastIndexOfStr {
\schemaVar \term Seq searchStr , sourceStr ;
\schemaVar \term int i ;
\schemaVar \variables int iv ;
\find ( clLastIndexOfCl ( sourceStr , i , searchStr ))
\varcond \replacewith ( \ifEx iv ; ( iv > 0 & i - iv >= 0 & seqLen ( searchStr )+ i - iv <= seqLen ( sourceStr )& ( seqSub ( sourceStr , i - iv , seqLen ( searchStr )+ i - iv )= searchStr ))\then ( i - iv )\else ( - 1 ))
\heuristics (stringsExpandDefNormalOp )
};defined in: charListRules.key Line: 309 Offset :4hashCodeBase {
\find ( clHashCode ( seqEmpty ))
\replacewith ( 0 )
\heuristics (simplify_literals )
};defined in: charListRules.key Line: 327 Offset :4lengthReplace {
\schemaVar \term Seq str , newStr ;
\schemaVar \term int searchChar , replaceChar ;
\find ( seqLen ( clReplace ( str , searchChar , replaceChar )))
\replacewith ( seqLen ( str ))
\heuristics (stringsSimplify )
};defined in: charListRules.key Line: 341 Offset :4lengthReplaceEQ {
\schemaVar \term Seq str , newStr ;
\schemaVar \term int searchChar , replaceChar ;
\assumes ( clReplace ( str , searchChar , replaceChar )= newStr ==> )
\find ( seqLen ( newStr ))
\sameUpdateLevel
\replacewith ( seqLen ( str ))
\heuristics (stringsSimplify )
};defined in: charListRules.key Line: 350 Offset :4substringSubstring {
\schemaVar \term Seq str ;
\schemaVar \skolemTerm Seq newSym ;
\schemaVar \term int outerStartIdx , outerEndIdx , innerStartIdx , innerEndIdx ;
\find ( seqSub ( seqSub ( str , innerStartIdx , innerEndIdx ), outerStartIdx , outerEndIdx ))
\sameUpdateLevel
\varcond \add ( ( innerStartIdx >= 0 & innerEndIdx >= innerStartIdx & innerEndIdx <= seqLen ( str )& outerStartIdx >= 0 & outerEndIdx >= outerStartIdx & outerEndIdx <= innerEndIdx - innerStartIdx )-> ( seqSub ( seqSub ( str , innerStartIdx , innerEndIdx ), outerStartIdx , outerEndIdx )= newSym & seqSub ( str , outerStartIdx + innerStartIdx , innerStartIdx + outerEndIdx )= newSym )==> )
\heuristics (stringsReduceSubstring , stringsIntroduceNewSym )
};defined in: charListRules.key Line: 364 Offset :4substringSubstring2 {
\schemaVar \term Seq str , innerSub ;
\schemaVar \skolemTerm Seq newSym ;
\schemaVar \term int outerStartIdx , outerEndIdx , innerStartIdx , innerEndIdx ;
\assumes ( seqSub ( str , innerStartIdx , innerEndIdx )= innerSub ==> )
\find ( seqSub ( innerSub , outerStartIdx , outerEndIdx ))
\sameUpdateLevel
\varcond \add ( ( innerStartIdx >= 0 & innerEndIdx >= innerStartIdx & innerEndIdx <= seqLen ( str )& outerStartIdx >= 0 & outerEndIdx >= outerStartIdx & outerEndIdx <= innerEndIdx - innerStartIdx )-> ( seqSub ( innerSub , outerStartIdx , outerEndIdx )= newSym & seqSub ( str , outerStartIdx + innerStartIdx , innerStartIdx + outerEndIdx )= newSym )==> )
\heuristics (stringsReduceSubstring , stringsIntroduceNewSym )
};defined in: charListRules.key Line: 390 Offset :4equalCharacters {
\schemaVar \term numbers iz1 , iz2 ;
\find ( C ( iz1 )= C ( iz2 ))
\replacewith ( Z ( iz1 )= Z ( iz2 ))
\heuristics (stringsSimplify )
};defined in: charListRules.key Line: 415 Offset :4replaceSubstring {
\schemaVar \term Seq str , subStr ;
\schemaVar \term int searchChar , replaceChar ;
\schemaVar \term int startIdx , endIdx ;
\assumes ( seqSub ( str , startIdx , endIdx )= subStr ==> )
\find ( clReplace ( subStr , searchChar , replaceChar ))
\sameUpdateLevel
\replacewith ( \if ( startIdx >= 0 & endIdx >= startIdx & endIdx <= seqLen ( str ))\then ( seqSub ( clReplace ( str , searchChar , replaceChar ), startIdx , endIdx ))\else ( clReplace ( subStr , searchChar , replaceChar )))
\heuristics (stringsMoveReplaceInside )
\displayname "replaceSubstring"
};defined in: charListRules.key Line: 422 Offset :4replaceConcat {
\schemaVar \term Seq leftStr , rightStr ;
\schemaVar \term int searchChar , replaceChar ;
\find ( clReplace ( seqConcat ( leftStr , rightStr ), searchChar , replaceChar ))
\replacewith ( seqConcat ( clReplace ( leftStr , searchChar , replaceChar ), clReplace ( rightStr , searchChar , replaceChar )))
\heuristics (stringsMoveReplaceInside )
};defined in: charListRules.key Line: 443 Offset :4