repeatMatchEmpty {
\schemaVar \term RegEx rexp ;
\schemaVar \term int nTimes1 ;
\find ( match ( repeat ( rexp , nTimes1 ), seqEmpty ))
\replacewith ( nTimes1 = 0 | ( nTimes1 > 0 & match ( rexp , seqEmpty )))
\heuristics (simplify )
};defined in: regExLemmaProven.key Line: 7 Offset :4repeatZero {
\schemaVar \term RegEx rexp ;
\schemaVar \term Seq string ;
\find ( repeat ( rexp , 0 ))
\replacewith ( regEx ( seqEmpty ))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 18 Offset :4repeatOnce {
\schemaVar \term RegEx rexp ;
\find ( repeat ( rexp , 1 ))
\replacewith ( rexp )
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 27 Offset :4optEmpty {
\schemaVar \term RegEx rexp ;
\find ( match ( opt ( rexp ), seqEmpty ))
\replacewith ( true )
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 36 Offset :4regExConcatAltLeft {
\schemaVar \term RegEx rexp1 , rexp2 , rexp3 ;
\schemaVar \term Seq string ;
\find ( match ( regExConcat ( alt ( rexp1 , rexp2 ), rexp3 ), string ))
\replacewith ( match ( regExConcat ( rexp1 , rexp3 ), string )| match ( regExConcat ( rexp2 , rexp3 ), string ))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 46 Offset :4regExConcatAltRight {
\schemaVar \term RegEx rexp1 , rexp2 , rexp3 ;
\schemaVar \term Seq string ;
\find ( match ( regExConcat ( rexp1 , alt ( rexp2 , rexp3 )), string ))
\replacewith ( match ( regExConcat ( rexp1 , rexp2 ), string )| match ( regExConcat ( rexp1 , rexp3 ), string ))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 59 Offset :4regExConcatOptLeft {
\schemaVar \term RegEx rexp1 , rexp2 ;
\schemaVar \term Seq string ;
\find ( match ( regExConcat ( opt ( rexp1 ), rexp2 ), string ))
\replacewith ( match ( rexp2 , string )| match ( regExConcat ( rexp1 , rexp2 ), string ))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 72 Offset :4regExConcatOptRight {
\schemaVar \term RegEx rexp1 , rexp2 ;
\schemaVar \term Seq string ;
\find ( match ( regExConcat ( rexp1 , opt ( rexp2 )), string ))
\replacewith ( match ( rexp1 , string )| match ( regExConcat ( rexp1 , rexp2 ), string ))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 85 Offset :4regExConcatConcreteStringLeft {
\schemaVar \term RegEx rexp ;
\schemaVar \term Seq string , pattern ;
\find ( match ( regExConcat ( regEx ( pattern ), rexp ), string ))
\replacewith ( seqLen ( pattern )<= seqLen ( string )& match ( regEx ( pattern ), seqSub ( string , 0 , seqLen ( pattern )))& match ( rexp , seqSub ( string , seqLen ( pattern ), seqLen ( string ))))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 98 Offset :4regExConcatConcreteStringRight {
\schemaVar \term RegEx rexp ;
\schemaVar \term Seq string , pattern ;
\find ( match ( regExConcat ( rexp , regEx ( pattern )), string ))
\replacewith ( seqLen ( pattern )<= seqLen ( string )& match ( rexp , seqSub ( string , 0 , seqLen ( string )- seqLen ( pattern )))& match ( regEx ( pattern ), seqSub ( string , seqLen ( string )- seqLen ( pattern ), seqLen ( string ))))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 111 Offset :4regExConcatRepeatLeft {
\schemaVar \term RegEx rexp1 , rexp2 ;
\schemaVar \term Seq string ;
\schemaVar \variables Seq string1 , string2 ;
\schemaVar \term int nTimes ;
\find ( match ( regExConcat ( repeat ( rexp1 , nTimes ), rexp2 ), string ))
\varcond \replacewith ( \if ( nTimes = 0 )\then ( match ( rexp2 , string ))\else ( \if ( nTimes < 0 )\then ( false )\else ( \exists string1 ; \exists string2 ; ( match ( repeat ( rexp1 , nTimes ), string1 )& match ( rexp2 , string2 )& string = seqConcat ( string1 , string2 )))))
\heuristics (simplify )
};defined in: regExLemmaProven.key Line: 124 Offset :4regExConcatRepeatRight {
\schemaVar \term RegEx rexp1 , rexp2 ;
\schemaVar \term Seq string ;
\schemaVar \variables Seq string1 , string2 ;
\schemaVar \term int nTimes ;
\find ( match ( regExConcat ( rexp1 , repeat ( rexp2 , nTimes )), string ))
\varcond \replacewith ( \if ( nTimes = 0 )\then ( match ( rexp1 , string ))\else ( \if ( nTimes < 0 )\then ( false )\else ( \exists string1 ; \exists string2 ; ( match ( rexp1 , string1 )& match ( repeat ( rexp2 , nTimes ), string2 )& string = seqConcat ( string1 , string2 )))))
\heuristics (simplify )
};defined in: regExLemmaProven.key Line: 149 Offset :4concatRepeatContraction3 {
\schemaVar \term RegEx rexp ;
\schemaVar \term int nTimes ;
\find ( regExConcat ( repeat ( rexp , nTimes ), regEx ( seqEmpty )))
\replacewith ( repeat ( rexp , nTimes ))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 175 Offset :4concatRepeatContraction3Sym {
\schemaVar \term RegEx rexp ;
\schemaVar \term int nTimes ;
\find ( regExConcat ( regEx ( seqEmpty ), repeat ( rexp , nTimes )))
\replacewith ( repeat ( rexp , nTimes ))
\heuristics (concrete )
};defined in: regExLemmaProven.key Line: 186 Offset :4