/*
The given program represents the following SMT-model:

(declare-fun b () String)
(declare-fun y () String)
(declare-fun z () String)
(assert (= y (str.replace_all b "bca" "b" ) ))
(assert (= z (str.replace_all y "abba" "aa" ) ))
(assert (not (str.contains z "c")))
(assert (= b (str.++ z "ac") ))
*/

/***********************************************/
/*             initial program                 */
/***********************************************/

$ENTRY Go {(e.z)(e.y)e.b
 = <LogAnd <NCont_c e.z><IsEqual (e.b)(e.z 'ac')><IsEqual (e.y)(<Repl_bca_b e.b>)><IsEqual (e.z)(<Repl_abba_aa e.y>)>>;
}

IsEqual {
    ( )( ) = True;
    (s.1 e.X)(s.1 e.X2) = <IsEqual (e.X)(e.X2)>;
    (e.X)(e.Y) = False;
}

LogAnd {
    False e.Y = False;
    True = True;
    True e.Z = <LogAnd e.Z>;
}

NCont_c {
   e.X 'c' e.Y = False;
   e.Z  = True;
}

Repl_abba_aa {
    e.X 'abba' e.Y = e.X 'aa'<Repl_abba_aa e.Y>;
    e.Z = e.Z;
}

Repl_bca_b {
    e.X 'bca' e.Y = e.X 'b'<Repl_bca_b e.Y>;
    e.Z = e.Z;
}


/***********************************************************/
/*          the residual program (with ~UnAmb)             */
/***********************************************************/
/*
$ENTRY Go {
 (e.x1) (e.x2) e.x3 =  <InputFormat_0 (e.x1) (e.x3) (e.x2)>;
}


InputFormat_0 {
 (e.x1 'c' e.x2) (e.x3) (e.x4) =  False;
 (e.x1) (e.x2) (e.x3) =  <LogAnd_0 (e.x2) (e.x1) (e.x3) ()>;
}


LogAnd_0 {
 (s.z1 e.x1) (s.z1 e.x2) (e.x3) (e.x4) =  <LogAnd_0 (e.x1) (e.x2) (e.x3) (e.x4 s.z1)>;
 ('ac') () (e.x1) (e.x2) =  <LogAnd_1 (e.x1) (e.x2) ()>;
 ('ac' e.x1) () (e.x2) (e.x3) =  False;
 ('a' e.x1) () (e.x2) (e.x3) =  False;
 (e.x1) (e.x2) (e.x3) (e.x4) =  False;
}


LogAnd_1 {
 (s.z1 e.x1) (s.z1 e.x2) (e.x3) =  <LogAnd_1 (e.x1) (e.x2) (e.x3 s.z1)>;
 ('ac') () (e.x1 'abb') =  <LogAnd_2 e.x1>;
 ('ac') () (e.x1 'abba' e.x2) =  <LogAnd_3 (e.x1) (e.x2)>;
 ('ac') () (e.x1) =  <LogAnd_4 e.x1>;
 ('ac' e.x1) () (e.x2) =  False;
 ('a' e.x1) () (e.x2) =  False;
 (e.x1) (e.x2) (e.x3) =  False;
}


LogAnd_2 {
 s.z1 e.x1 =  <LogAnd_2 e.x1>;
 =  False;
 e.x1 =  False;
}


LogAnd_3 {
 (s.z1 e.x1) (e.x2) =  <LogAnd_3 (e.x1) (e.x2)>;
 () (e.x1) =  False;
 (e.x1) (e.x2) =  False;
}


LogAnd_4 {
 s.z1 e.x1 =  <LogAnd_4 e.x1>;
 e.x1 =  False;
}
*/