(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR a b x x' y) (DATATYPES A = µX.< S(X), 0, True, False >) (SIGNATURES monus :: [A x A] -> A gcd :: [A x A] -> A equal0 :: [A x A] -> A < :: [A x A] -> A gcd[Ite] :: [A x A x A] -> A gcd[False][Ite] :: [A x A x A] -> A equal0[Ite] :: [A x A x A] -> A equal0[True][Ite] :: [A x A x A] -> A) (RULES monus(S(x'),S(x)) -> monus(x',x) gcd(x,y) -> gcd[Ite](equal0(x,y) ,x ,y) equal0(a,b) -> equal0[Ite](<(a ,b) ,a ,b) <(S(x),S(y)) ->= <(x,y) <(0(),S(y)) ->= True() <(x,0()) ->= False() gcd[Ite](False(),x,y) ->= gcd[False][Ite](<(x,y),x,y) gcd[Ite](True(),x,y) ->= x gcd[False][Ite](False(),x,y) ->= gcd(y,monus(y,x)) gcd[False][Ite](True(),x,y) ->= gcd(monus(x,y),y) equal0[Ite](False(),a,b) ->= False() equal0[Ite](True(),a,b) ->= equal0[True][Ite](<(b,a),a,b) equal0[True][Ite](False() ,a ,b) ->= False() equal0[True][Ite](True() ,a ,b) ->= True())