MAYBE Time: 18.201 Problem: Equations: TRS: 1() -> s_(0()) 2() -> s_(s_(0())) 3() -> s_(s_(s_(0()))) 4() -> s_(s_(s_(s_(0())))) 5() -> s_(s_(s_(s_(s_(0()))))) 6() -> s_(s_(s_(s_(s_(s_(0())))))) 7() -> s_(s_(s_(s_(s_(s_(s_(0()))))))) U101(tt(),M,N) -> dC(N,M) U11(tt()) -> 0() U111(tt()) -> 0() U121(tt(),M',N') -> U122(equal(_>_(N',M'),true()),M',N') U122(tt(),M',N') -> gcdC(dC(N',M'),M') U131(tt(),N') -> N' U141(tt(),V1,V2) -> U142(isNat(V1),V2) U142(tt(),V2) -> U143(isNat(V2)) U143(tt()) -> tt() U151(tt(),V1,V2) -> U152(isNat(V1),V2) U152(tt(),V2) -> U153(isNat(V2)) U153(tt()) -> tt() U161(tt(),V) -> U162(isNzNat(V)) U162(tt()) -> tt() U171(tt(),V1,V2) -> U172(isNat(V1),V2) U172(tt(),V2) -> U173(isNat(V2)) U173(tt()) -> tt() U181(tt(),V1,V2) -> U182(isNat(V1),V2) U182(tt(),V2) -> U183(isNat(V2)) U183(tt()) -> tt() U191(tt(),V1,V2) -> U192(isNat(V1),V2) U192(tt(),V2) -> U193(isNat(V2)) U193(tt()) -> tt() U201(tt(),V1,V2) -> U202(isNat(V1),V2) U202(tt(),V2) -> U203(isNat(V2)) U203(tt()) -> tt() U21(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M)))) U211(tt(),V1) -> U212(isNzNat(V1)) U212(tt()) -> tt() U221(tt(),V1,V2) -> U222(isNat(V1),V2) U222(tt(),V2) -> U223(isNzNat(V2)) U223(tt()) -> tt() U231(tt(),V1,V2) -> U232(isNzNat(V1),V2) U232(tt(),V2) -> U233(isNzNat(V2)) U233(tt()) -> tt() U241(tt(),V1,V2) -> U242(isNzNat(V1),V2) U242(tt(),V2) -> U243(isNzNat(V2)) U243(tt()) -> tt() U251(tt(),V1) -> U252(isNat(V1)) U252(tt()) -> tt() U261(tt(),N) -> N U271(tt()) -> s_(0()) U281(tt(),M',N) -> U282(equal(_>_(M',N),true())) U282(tt()) -> 0() U291(tt(),M',N) -> U292(equal(_>_(N,M'),true()),M',N) U292(tt(),M',N) -> s_(quot(dC(N,M'),M')) U31(tt(),N) -> N U41(tt(),M,N) -> s_(s_(_+_C(N,M))) U51(tt(),M,N) -> _>_(M,N) U61(tt()) -> false() U71(tt()) -> true() U81(tt(),M,N) -> _>_(N,M) U91(tt(),N) -> N _*_C(N,0()) -> U11(and(isNat(N),isNatKind(N))) _*_C(s_(N),s_(M)) -> U21(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _+_C(N,0()) -> U31(and(isNat(N),isNatKind(N)),N) _+_C(s_(N),s_(M)) -> U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _<_(N,M) -> U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _>_(0(),M) -> U61(and(isNat(M),isNatKind(M))) _>_(N',0()) -> U71(and(isNzNat(N'),isNatKind(N'))) _>_(s_(N),s_(M)) -> U81(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) and(tt(),X) -> X dC(0(),N) -> U91(and(isNat(N),isNatKind(N)),N) dC(s_(N),s_(M)) -> U101(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) equal(X,X) -> tt() gcdC(0(),N) -> U111(and(isNat(N),isNatKind(N))) gcdC(N',M') -> U121(and(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'),isNatKind(N'))),M',N') gcdC(N',N') -> U131(and(isNzNat(N'),isNatKind(N')),N') isBoolean(false()) -> tt() isBoolean(true()) -> tt() isBoolean(_<_(V1,V2)) -> U141(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBoolean(_>_(V1,V2)) -> U151(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBooleanKind(false()) -> tt() isBooleanKind(true()) -> tt() isBooleanKind(_<_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isBooleanKind(_>_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNat(0()) -> tt() isNat(V) -> U161(isNatKind(V),V) isNat(_*_C(V1,V2)) -> U171(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(_+_C(V1,V2)) -> U181(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(dC(V1,V2)) -> U191(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(gcdC(V1,V2)) -> U201(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(p_(V1)) -> U211(isNatKind(V1),V1) isNat(quot(V1,V2)) -> U221(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNatKind(0()) -> tt() isNatKind(1()) -> tt() isNatKind(2()) -> tt() isNatKind(3()) -> tt() isNatKind(4()) -> tt() isNatKind(5()) -> tt() isNatKind(6()) -> tt() isNatKind(7()) -> tt() isNatKind(_*_C(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(_+_C(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(dC(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(gcdC(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(p_(V1)) -> isNatKind(V1) isNatKind(quot(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(s_(V1)) -> isNatKind(V1) isNzNat(1()) -> tt() isNzNat(2()) -> tt() isNzNat(3()) -> tt() isNzNat(4()) -> tt() isNzNat(5()) -> tt() isNzNat(6()) -> tt() isNzNat(7()) -> tt() isNzNat(_*_C(V1,V2)) -> U231(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat(gcdC(V1,V2)) -> U241(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat(s_(V1)) -> U251(isNatKind(V1),V1) p_(s_(N)) -> U261(and(isNat(N),isNatKind(N)),N) quot(M',M') -> U271(and(isNzNat(M'),isNatKind(M'))) quot(N,M') -> U281(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) quot(N,M') -> U291(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) Proof: DP Processor: Equations#: DPs: U101#(tt(),M,N) -> d{C,#}(N,M) U121#(tt(),M',N') -> _>_#(N',M') U121#(tt(),M',N') -> equal#(_>_(N',M'),true()) U121#(tt(),M',N') -> U122#(equal(_>_(N',M'),true()),M',N') U122#(tt(),M',N') -> d{C,#}(N',M') U122#(tt(),M',N') -> gcd{C,#}(dC(N',M'),M') U141#(tt(),V1,V2) -> isNat#(V1) U141#(tt(),V1,V2) -> U142#(isNat(V1),V2) U142#(tt(),V2) -> isNat#(V2) U142#(tt(),V2) -> U143#(isNat(V2)) U151#(tt(),V1,V2) -> isNat#(V1) U151#(tt(),V1,V2) -> U152#(isNat(V1),V2) U152#(tt(),V2) -> isNat#(V2) U152#(tt(),V2) -> U153#(isNat(V2)) U161#(tt(),V) -> isNzNat#(V) U161#(tt(),V) -> U162#(isNzNat(V)) U171#(tt(),V1,V2) -> isNat#(V1) U171#(tt(),V1,V2) -> U172#(isNat(V1),V2) U172#(tt(),V2) -> isNat#(V2) U172#(tt(),V2) -> U173#(isNat(V2)) U181#(tt(),V1,V2) -> isNat#(V1) U181#(tt(),V1,V2) -> U182#(isNat(V1),V2) U182#(tt(),V2) -> isNat#(V2) U182#(tt(),V2) -> U183#(isNat(V2)) U191#(tt(),V1,V2) -> isNat#(V1) U191#(tt(),V1,V2) -> U192#(isNat(V1),V2) U192#(tt(),V2) -> isNat#(V2) U192#(tt(),V2) -> U193#(isNat(V2)) U201#(tt(),V1,V2) -> isNat#(V1) U201#(tt(),V1,V2) -> U202#(isNat(V1),V2) U202#(tt(),V2) -> isNat#(V2) U202#(tt(),V2) -> U203#(isNat(V2)) U21#(tt(),M,N) -> _*_{C,#}(N,M) U21#(tt(),M,N) -> _+_{C,#}(M,_*_C(N,M)) U21#(tt(),M,N) -> _+_{C,#}(N,_+_C(M,_*_C(N,M))) U211#(tt(),V1) -> isNzNat#(V1) U211#(tt(),V1) -> U212#(isNzNat(V1)) U221#(tt(),V1,V2) -> isNat#(V1) U221#(tt(),V1,V2) -> U222#(isNat(V1),V2) U222#(tt(),V2) -> isNzNat#(V2) U222#(tt(),V2) -> U223#(isNzNat(V2)) U231#(tt(),V1,V2) -> isNzNat#(V1) U231#(tt(),V1,V2) -> U232#(isNzNat(V1),V2) U232#(tt(),V2) -> isNzNat#(V2) U232#(tt(),V2) -> U233#(isNzNat(V2)) U241#(tt(),V1,V2) -> isNzNat#(V1) U241#(tt(),V1,V2) -> U242#(isNzNat(V1),V2) U242#(tt(),V2) -> isNzNat#(V2) U242#(tt(),V2) -> U243#(isNzNat(V2)) U251#(tt(),V1) -> isNat#(V1) U251#(tt(),V1) -> U252#(isNat(V1)) U281#(tt(),M',N) -> _>_#(M',N) U281#(tt(),M',N) -> equal#(_>_(M',N),true()) U281#(tt(),M',N) -> U282#(equal(_>_(M',N),true())) U291#(tt(),M',N) -> _>_#(N,M') U291#(tt(),M',N) -> equal#(_>_(N,M'),true()) U291#(tt(),M',N) -> U292#(equal(_>_(N,M'),true()),M',N) U292#(tt(),M',N) -> d{C,#}(N,M') U292#(tt(),M',N) -> quot#(dC(N,M'),M') U41#(tt(),M,N) -> _+_{C,#}(N,M) U51#(tt(),M,N) -> _>_#(M,N) U81#(tt(),M,N) -> _>_#(N,M) _*_{C,#}(N,0()) -> isNatKind#(N) _*_{C,#}(N,0()) -> isNat#(N) _*_{C,#}(N,0()) -> and#(isNat(N),isNatKind(N)) _*_{C,#}(N,0()) -> U11#(and(isNat(N),isNatKind(N))) _*_{C,#}(s_(N),s_(M)) -> isNatKind#(N) _*_{C,#}(s_(N),s_(M)) -> isNat#(N) _*_{C,#}(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) _*_{C,#}(s_(N),s_(M)) -> isNatKind#(M) _*_{C,#}(s_(N),s_(M)) -> isNat#(M) _*_{C,#}(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) _*_{C,#}(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _*_{C,#}(s_(N),s_(M)) -> U21#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _+_{C,#}(N,0()) -> isNatKind#(N) _+_{C,#}(N,0()) -> isNat#(N) _+_{C,#}(N,0()) -> and#(isNat(N),isNatKind(N)) _+_{C,#}(N,0()) -> U31#(and(isNat(N),isNatKind(N)),N) _+_{C,#}(s_(N),s_(M)) -> isNatKind#(N) _+_{C,#}(s_(N),s_(M)) -> isNat#(N) _+_{C,#}(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) _+_{C,#}(s_(N),s_(M)) -> isNatKind#(M) _+_{C,#}(s_(N),s_(M)) -> isNat#(M) _+_{C,#}(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) _+_{C,#}(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _+_{C,#}(s_(N),s_(M)) -> U41#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _<_#(N,M) -> isNatKind#(N) _<_#(N,M) -> isNat#(N) _<_#(N,M) -> and#(isNat(N),isNatKind(N)) _<_#(N,M) -> isNatKind#(M) _<_#(N,M) -> isNat#(M) _<_#(N,M) -> and#(isNat(M),isNatKind(M)) _<_#(N,M) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _<_#(N,M) -> U51#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _>_#(0(),M) -> isNatKind#(M) _>_#(0(),M) -> isNat#(M) _>_#(0(),M) -> and#(isNat(M),isNatKind(M)) _>_#(0(),M) -> U61#(and(isNat(M),isNatKind(M))) _>_#(N',0()) -> isNatKind#(N') _>_#(N',0()) -> isNzNat#(N') _>_#(N',0()) -> and#(isNzNat(N'),isNatKind(N')) _>_#(N',0()) -> U71#(and(isNzNat(N'),isNatKind(N'))) _>_#(s_(N),s_(M)) -> isNatKind#(N) _>_#(s_(N),s_(M)) -> isNat#(N) _>_#(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) _>_#(s_(N),s_(M)) -> isNatKind#(M) _>_#(s_(N),s_(M)) -> isNat#(M) _>_#(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) _>_#(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _>_#(s_(N),s_(M)) -> U81#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) d{C,#}(0(),N) -> isNatKind#(N) d{C,#}(0(),N) -> isNat#(N) d{C,#}(0(),N) -> and#(isNat(N),isNatKind(N)) d{C,#}(0(),N) -> U91#(and(isNat(N),isNatKind(N)),N) d{C,#}(s_(N),s_(M)) -> isNatKind#(N) d{C,#}(s_(N),s_(M)) -> isNat#(N) d{C,#}(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) d{C,#}(s_(N),s_(M)) -> isNatKind#(M) d{C,#}(s_(N),s_(M)) -> isNat#(M) d{C,#}(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) d{C,#}(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) d{C,#}(s_(N),s_(M)) -> U101#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) gcd{C,#}(0(),N) -> isNatKind#(N) gcd{C,#}(0(),N) -> isNat#(N) gcd{C,#}(0(),N) -> and#(isNat(N),isNatKind(N)) gcd{C,#}(0(),N) -> U111#(and(isNat(N),isNatKind(N))) gcd{C,#}(N',M') -> isNatKind#(N') gcd{C,#}(N',M') -> isNzNat#(N') gcd{C,#}(N',M') -> and#(isNzNat(N'),isNatKind(N')) gcd{C,#}(N',M') -> isNatKind#(M') gcd{C,#}(N',M') -> isNzNat#(M') gcd{C,#}(N',M') -> and#(isNzNat(M'),isNatKind(M')) gcd{C,#}(N',M') -> and#(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'),isNatKind(N'))) gcd{C,#}(N',M') -> U121#(and(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'),isNatKind(N'))),M',N') gcd{C,#}(N',N') -> isNatKind#(N') gcd{C,#}(N',N') -> isNzNat#(N') gcd{C,#}(N',N') -> and#(isNzNat(N'),isNatKind(N')) gcd{C,#}(N',N') -> U131#(and(isNzNat(N'),isNatKind(N')),N') isBoolean#(_<_(V1,V2)) -> isNatKind#(V2) isBoolean#(_<_(V1,V2)) -> isNatKind#(V1) isBoolean#(_<_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isBoolean#(_<_(V1,V2)) -> U141#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBoolean#(_>_(V1,V2)) -> isNatKind#(V2) isBoolean#(_>_(V1,V2)) -> isNatKind#(V1) isBoolean#(_>_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isBoolean#(_>_(V1,V2)) -> U151#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBooleanKind#(_<_(V1,V2)) -> isNatKind#(V2) isBooleanKind#(_<_(V1,V2)) -> isNatKind#(V1) isBooleanKind#(_<_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isBooleanKind#(_>_(V1,V2)) -> isNatKind#(V2) isBooleanKind#(_>_(V1,V2)) -> isNatKind#(V1) isBooleanKind#(_>_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(V) -> isNatKind#(V) isNat#(V) -> U161#(isNatKind(V),V) isNat#(_*_C(V1,V2)) -> isNatKind#(V2) isNat#(_*_C(V1,V2)) -> isNatKind#(V1) isNat#(_*_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(_*_C(V1,V2)) -> U171#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(_+_C(V1,V2)) -> isNatKind#(V2) isNat#(_+_C(V1,V2)) -> isNatKind#(V1) isNat#(_+_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(_+_C(V1,V2)) -> U181#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(dC(V1,V2)) -> isNatKind#(V2) isNat#(dC(V1,V2)) -> isNatKind#(V1) isNat#(dC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(dC(V1,V2)) -> U191#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(gcdC(V1,V2)) -> isNatKind#(V2) isNat#(gcdC(V1,V2)) -> isNatKind#(V1) isNat#(gcdC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(gcdC(V1,V2)) -> U201#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(p_(V1)) -> isNatKind#(V1) isNat#(p_(V1)) -> U211#(isNatKind(V1),V1) isNat#(quot(V1,V2)) -> isNatKind#(V2) isNat#(quot(V1,V2)) -> isNatKind#(V1) isNat#(quot(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(quot(V1,V2)) -> U221#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNatKind#(_*_C(V1,V2)) -> isNatKind#(V2) isNatKind#(_*_C(V1,V2)) -> isNatKind#(V1) isNatKind#(_*_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(_+_C(V1,V2)) -> isNatKind#(V2) isNatKind#(_+_C(V1,V2)) -> isNatKind#(V1) isNatKind#(_+_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(dC(V1,V2)) -> isNatKind#(V2) isNatKind#(dC(V1,V2)) -> isNatKind#(V1) isNatKind#(dC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(gcdC(V1,V2)) -> isNatKind#(V2) isNatKind#(gcdC(V1,V2)) -> isNatKind#(V1) isNatKind#(gcdC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(p_(V1)) -> isNatKind#(V1) isNatKind#(quot(V1,V2)) -> isNatKind#(V2) isNatKind#(quot(V1,V2)) -> isNatKind#(V1) isNatKind#(quot(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(s_(V1)) -> isNatKind#(V1) isNzNat#(_*_C(V1,V2)) -> isNatKind#(V2) isNzNat#(_*_C(V1,V2)) -> isNatKind#(V1) isNzNat#(_*_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNzNat#(_*_C(V1,V2)) -> U231#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat#(gcdC(V1,V2)) -> isNatKind#(V2) isNzNat#(gcdC(V1,V2)) -> isNatKind#(V1) isNzNat#(gcdC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNzNat#(gcdC(V1,V2)) -> U241#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat#(s_(V1)) -> isNatKind#(V1) isNzNat#(s_(V1)) -> U251#(isNatKind(V1),V1) p_#(s_(N)) -> isNatKind#(N) p_#(s_(N)) -> isNat#(N) p_#(s_(N)) -> and#(isNat(N),isNatKind(N)) p_#(s_(N)) -> U261#(and(isNat(N),isNatKind(N)),N) quot#(M',M') -> isNatKind#(M') quot#(M',M') -> isNzNat#(M') quot#(M',M') -> and#(isNzNat(M'),isNatKind(M')) quot#(M',M') -> U271#(and(isNzNat(M'),isNatKind(M'))) quot#(N,M') -> isNatKind#(N) quot#(N,M') -> isNat#(N) quot#(N,M') -> and#(isNat(N),isNatKind(N)) quot#(N,M') -> isNatKind#(M') quot#(N,M') -> isNzNat#(M') quot#(N,M') -> and#(isNzNat(M'),isNatKind(M')) quot#(N,M') -> and#(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))) quot#(N,M') -> U281#(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) quot#(N,M') -> U291#(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) Equations: TRS: 1() -> s_(0()) 2() -> s_(s_(0())) 3() -> s_(s_(s_(0()))) 4() -> s_(s_(s_(s_(0())))) 5() -> s_(s_(s_(s_(s_(0()))))) 6() -> s_(s_(s_(s_(s_(s_(0())))))) 7() -> s_(s_(s_(s_(s_(s_(s_(0()))))))) U101(tt(),M,N) -> dC(N,M) U11(tt()) -> 0() U111(tt()) -> 0() U121(tt(),M',N') -> U122(equal(_>_(N',M'),true()),M',N') U122(tt(),M',N') -> gcdC(dC(N',M'),M') U131(tt(),N') -> N' U141(tt(),V1,V2) -> U142(isNat(V1),V2) U142(tt(),V2) -> U143(isNat(V2)) U143(tt()) -> tt() U151(tt(),V1,V2) -> U152(isNat(V1),V2) U152(tt(),V2) -> U153(isNat(V2)) U153(tt()) -> tt() U161(tt(),V) -> U162(isNzNat(V)) U162(tt()) -> tt() U171(tt(),V1,V2) -> U172(isNat(V1),V2) U172(tt(),V2) -> U173(isNat(V2)) U173(tt()) -> tt() U181(tt(),V1,V2) -> U182(isNat(V1),V2) U182(tt(),V2) -> U183(isNat(V2)) U183(tt()) -> tt() U191(tt(),V1,V2) -> U192(isNat(V1),V2) U192(tt(),V2) -> U193(isNat(V2)) U193(tt()) -> tt() U201(tt(),V1,V2) -> U202(isNat(V1),V2) U202(tt(),V2) -> U203(isNat(V2)) U203(tt()) -> tt() U21(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M)))) U211(tt(),V1) -> U212(isNzNat(V1)) U212(tt()) -> tt() U221(tt(),V1,V2) -> U222(isNat(V1),V2) U222(tt(),V2) -> U223(isNzNat(V2)) U223(tt()) -> tt() U231(tt(),V1,V2) -> U232(isNzNat(V1),V2) U232(tt(),V2) -> U233(isNzNat(V2)) U233(tt()) -> tt() U241(tt(),V1,V2) -> U242(isNzNat(V1),V2) U242(tt(),V2) -> U243(isNzNat(V2)) U243(tt()) -> tt() U251(tt(),V1) -> U252(isNat(V1)) U252(tt()) -> tt() U261(tt(),N) -> N U271(tt()) -> s_(0()) U281(tt(),M',N) -> U282(equal(_>_(M',N),true())) U282(tt()) -> 0() U291(tt(),M',N) -> U292(equal(_>_(N,M'),true()),M',N) U292(tt(),M',N) -> s_(quot(dC(N,M'),M')) U31(tt(),N) -> N U41(tt(),M,N) -> s_(s_(_+_C(N,M))) U51(tt(),M,N) -> _>_(M,N) U61(tt()) -> false() U71(tt()) -> true() U81(tt(),M,N) -> _>_(N,M) U91(tt(),N) -> N _*_C(N,0()) -> U11(and(isNat(N),isNatKind(N))) _*_C(s_(N),s_(M)) -> U21(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _+_C(N,0()) -> U31(and(isNat(N),isNatKind(N)),N) _+_C(s_(N),s_(M)) -> U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _<_(N,M) -> U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _>_(0(),M) -> U61(and(isNat(M),isNatKind(M))) _>_(N',0()) -> U71(and(isNzNat(N'),isNatKind(N'))) _>_(s_(N),s_(M)) -> U81(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) and(tt(),X) -> X dC(0(),N) -> U91(and(isNat(N),isNatKind(N)),N) dC(s_(N),s_(M)) -> U101(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) equal(X,X) -> tt() gcdC(0(),N) -> U111(and(isNat(N),isNatKind(N))) gcdC(N',M') -> U121(and(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'),isNatKind(N'))),M',N') gcdC(N',N') -> U131(and(isNzNat(N'),isNatKind(N')),N') isBoolean(false()) -> tt() isBoolean(true()) -> tt() isBoolean(_<_(V1,V2)) -> U141(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBoolean(_>_(V1,V2)) -> U151(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBooleanKind(false()) -> tt() isBooleanKind(true()) -> tt() isBooleanKind(_<_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isBooleanKind(_>_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNat(0()) -> tt() isNat(V) -> U161(isNatKind(V),V) isNat(_*_C(V1,V2)) -> U171(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(_+_C(V1,V2)) -> U181(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(dC(V1,V2)) -> U191(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(gcdC(V1,V2)) -> U201(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(p_(V1)) -> U211(isNatKind(V1),V1) isNat(quot(V1,V2)) -> U221(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNatKind(0()) -> tt() isNatKind(1()) -> tt() isNatKind(2()) -> tt() isNatKind(3()) -> tt() isNatKind(4()) -> tt() isNatKind(5()) -> tt() isNatKind(6()) -> tt() isNatKind(7()) -> tt() isNatKind(_*_C(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(_+_C(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(dC(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(gcdC(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(p_(V1)) -> isNatKind(V1) isNatKind(quot(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(s_(V1)) -> isNatKind(V1) isNzNat(1()) -> tt() isNzNat(2()) -> tt() isNzNat(3()) -> tt() isNzNat(4()) -> tt() isNzNat(5()) -> tt() isNzNat(6()) -> tt() isNzNat(7()) -> tt() isNzNat(_*_C(V1,V2)) -> U231(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat(gcdC(V1,V2)) -> U241(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat(s_(V1)) -> U251(isNatKind(V1),V1) p_(s_(N)) -> U261(and(isNat(N),isNatKind(N)),N) quot(M',M') -> U271(and(isNzNat(M'),isNatKind(M'))) quot(N,M') -> U281(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) quot(N,M') -> U291(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) S: AC-EDG Processor: Equations#: DPs: U101#(tt(),M,N) -> d{C,#}(N,M) U121#(tt(),M',N') -> _>_#(N',M') U121#(tt(),M',N') -> equal#(_>_(N',M'),true()) U121#(tt(),M',N') -> U122#(equal(_>_(N',M'),true()),M',N') U122#(tt(),M',N') -> d{C,#}(N',M') U122#(tt(),M',N') -> gcd{C,#}(dC(N',M'),M') U141#(tt(),V1,V2) -> isNat#(V1) U141#(tt(),V1,V2) -> U142#(isNat(V1),V2) U142#(tt(),V2) -> isNat#(V2) U142#(tt(),V2) -> U143#(isNat(V2)) U151#(tt(),V1,V2) -> isNat#(V1) U151#(tt(),V1,V2) -> U152#(isNat(V1),V2) U152#(tt(),V2) -> isNat#(V2) U152#(tt(),V2) -> U153#(isNat(V2)) U161#(tt(),V) -> isNzNat#(V) U161#(tt(),V) -> U162#(isNzNat(V)) U171#(tt(),V1,V2) -> isNat#(V1) U171#(tt(),V1,V2) -> U172#(isNat(V1),V2) U172#(tt(),V2) -> isNat#(V2) U172#(tt(),V2) -> U173#(isNat(V2)) U181#(tt(),V1,V2) -> isNat#(V1) U181#(tt(),V1,V2) -> U182#(isNat(V1),V2) U182#(tt(),V2) -> isNat#(V2) U182#(tt(),V2) -> U183#(isNat(V2)) U191#(tt(),V1,V2) -> isNat#(V1) U191#(tt(),V1,V2) -> U192#(isNat(V1),V2) U192#(tt(),V2) -> isNat#(V2) U192#(tt(),V2) -> U193#(isNat(V2)) U201#(tt(),V1,V2) -> isNat#(V1) U201#(tt(),V1,V2) -> U202#(isNat(V1),V2) U202#(tt(),V2) -> isNat#(V2) U202#(tt(),V2) -> U203#(isNat(V2)) U21#(tt(),M,N) -> _*_{C,#}(N,M) U21#(tt(),M,N) -> _+_{C,#}(M,_*_C(N,M)) U21#(tt(),M,N) -> _+_{C,#}(N,_+_C(M,_*_C(N,M))) U211#(tt(),V1) -> isNzNat#(V1) U211#(tt(),V1) -> U212#(isNzNat(V1)) U221#(tt(),V1,V2) -> isNat#(V1) U221#(tt(),V1,V2) -> U222#(isNat(V1),V2) U222#(tt(),V2) -> isNzNat#(V2) U222#(tt(),V2) -> U223#(isNzNat(V2)) U231#(tt(),V1,V2) -> isNzNat#(V1) U231#(tt(),V1,V2) -> U232#(isNzNat(V1),V2) U232#(tt(),V2) -> isNzNat#(V2) U232#(tt(),V2) -> U233#(isNzNat(V2)) U241#(tt(),V1,V2) -> isNzNat#(V1) U241#(tt(),V1,V2) -> U242#(isNzNat(V1),V2) U242#(tt(),V2) -> isNzNat#(V2) U242#(tt(),V2) -> U243#(isNzNat(V2)) U251#(tt(),V1) -> isNat#(V1) U251#(tt(),V1) -> U252#(isNat(V1)) U281#(tt(),M',N) -> _>_#(M',N) U281#(tt(),M',N) -> equal#(_>_(M',N),true()) U281#(tt(),M',N) -> U282#(equal(_>_(M',N),true())) U291#(tt(),M',N) -> _>_#(N,M') U291#(tt(),M',N) -> equal#(_>_(N,M'),true()) U291#(tt(),M',N) -> U292#(equal(_>_(N,M'),true()),M',N) U292#(tt(),M',N) -> d{C,#}(N,M') U292#(tt(),M',N) -> quot#(dC(N,M'),M') U41#(tt(),M,N) -> _+_{C,#}(N,M) U51#(tt(),M,N) -> _>_#(M,N) U81#(tt(),M,N) -> _>_#(N,M) _*_{C,#}(N,0()) -> isNatKind#(N) _*_{C,#}(N,0()) -> isNat#(N) _*_{C,#}(N,0()) -> and#(isNat(N),isNatKind(N)) _*_{C,#}(N,0()) -> U11#(and(isNat(N),isNatKind(N))) _*_{C,#}(s_(N),s_(M)) -> isNatKind#(N) _*_{C,#}(s_(N),s_(M)) -> isNat#(N) _*_{C,#}(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) _*_{C,#}(s_(N),s_(M)) -> isNatKind#(M) _*_{C,#}(s_(N),s_(M)) -> isNat#(M) _*_{C,#}(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) _*_{C,#}(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _*_{C,#}(s_(N),s_(M)) -> U21#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _+_{C,#}(N,0()) -> isNatKind#(N) _+_{C,#}(N,0()) -> isNat#(N) _+_{C,#}(N,0()) -> and#(isNat(N),isNatKind(N)) _+_{C,#}(N,0()) -> U31#(and(isNat(N),isNatKind(N)),N) _+_{C,#}(s_(N),s_(M)) -> isNatKind#(N) _+_{C,#}(s_(N),s_(M)) -> isNat#(N) _+_{C,#}(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) _+_{C,#}(s_(N),s_(M)) -> isNatKind#(M) _+_{C,#}(s_(N),s_(M)) -> isNat#(M) _+_{C,#}(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) _+_{C,#}(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _+_{C,#}(s_(N),s_(M)) -> U41#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _<_#(N,M) -> isNatKind#(N) _<_#(N,M) -> isNat#(N) _<_#(N,M) -> and#(isNat(N),isNatKind(N)) _<_#(N,M) -> isNatKind#(M) _<_#(N,M) -> isNat#(M) _<_#(N,M) -> and#(isNat(M),isNatKind(M)) _<_#(N,M) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _<_#(N,M) -> U51#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _>_#(0(),M) -> isNatKind#(M) _>_#(0(),M) -> isNat#(M) _>_#(0(),M) -> and#(isNat(M),isNatKind(M)) _>_#(0(),M) -> U61#(and(isNat(M),isNatKind(M))) _>_#(N',0()) -> isNatKind#(N') _>_#(N',0()) -> isNzNat#(N') _>_#(N',0()) -> and#(isNzNat(N'),isNatKind(N')) _>_#(N',0()) -> U71#(and(isNzNat(N'),isNatKind(N'))) _>_#(s_(N),s_(M)) -> isNatKind#(N) _>_#(s_(N),s_(M)) -> isNat#(N) _>_#(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) _>_#(s_(N),s_(M)) -> isNatKind#(M) _>_#(s_(N),s_(M)) -> isNat#(M) _>_#(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) _>_#(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) _>_#(s_(N),s_(M)) -> U81#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) d{C,#}(0(),N) -> isNatKind#(N) d{C,#}(0(),N) -> isNat#(N) d{C,#}(0(),N) -> and#(isNat(N),isNatKind(N)) d{C,#}(0(),N) -> U91#(and(isNat(N),isNatKind(N)),N) d{C,#}(s_(N),s_(M)) -> isNatKind#(N) d{C,#}(s_(N),s_(M)) -> isNat#(N) d{C,#}(s_(N),s_(M)) -> and#(isNat(N),isNatKind(N)) d{C,#}(s_(N),s_(M)) -> isNatKind#(M) d{C,#}(s_(N),s_(M)) -> isNat#(M) d{C,#}(s_(N),s_(M)) -> and#(isNat(M),isNatKind(M)) d{C,#}(s_(N),s_(M)) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))) d{C,#}(s_(N),s_(M)) -> U101#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) gcd{C,#}(0(),N) -> isNatKind#(N) gcd{C,#}(0(),N) -> isNat#(N) gcd{C,#}(0(),N) -> and#(isNat(N),isNatKind(N)) gcd{C,#}(0(),N) -> U111#(and(isNat(N),isNatKind(N))) gcd{C,#}(N',M') -> isNatKind#(N') gcd{C,#}(N',M') -> isNzNat#(N') gcd{C,#}(N',M') -> and#(isNzNat(N'),isNatKind(N')) gcd{C,#}(N',M') -> isNatKind#(M') gcd{C,#}(N',M') -> isNzNat#(M') gcd{C,#}(N',M') -> and#(isNzNat(M'),isNatKind(M')) gcd{C,#}(N',M') -> and#(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'),isNatKind(N'))) gcd{C,#}(N',M') -> U121#(and(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'),isNatKind(N'))),M',N') gcd{C,#}(N',N') -> isNatKind#(N') gcd{C,#}(N',N') -> isNzNat#(N') gcd{C,#}(N',N') -> and#(isNzNat(N'),isNatKind(N')) gcd{C,#}(N',N') -> U131#(and(isNzNat(N'),isNatKind(N')),N') isBoolean#(_<_(V1,V2)) -> isNatKind#(V2) isBoolean#(_<_(V1,V2)) -> isNatKind#(V1) isBoolean#(_<_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isBoolean#(_<_(V1,V2)) -> U141#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBoolean#(_>_(V1,V2)) -> isNatKind#(V2) isBoolean#(_>_(V1,V2)) -> isNatKind#(V1) isBoolean#(_>_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isBoolean#(_>_(V1,V2)) -> U151#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBooleanKind#(_<_(V1,V2)) -> isNatKind#(V2) isBooleanKind#(_<_(V1,V2)) -> isNatKind#(V1) isBooleanKind#(_<_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isBooleanKind#(_>_(V1,V2)) -> isNatKind#(V2) isBooleanKind#(_>_(V1,V2)) -> isNatKind#(V1) isBooleanKind#(_>_(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(V) -> isNatKind#(V) isNat#(V) -> U161#(isNatKind(V),V) isNat#(_*_C(V1,V2)) -> isNatKind#(V2) isNat#(_*_C(V1,V2)) -> isNatKind#(V1) isNat#(_*_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(_*_C(V1,V2)) -> U171#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(_+_C(V1,V2)) -> isNatKind#(V2) isNat#(_+_C(V1,V2)) -> isNatKind#(V1) isNat#(_+_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(_+_C(V1,V2)) -> U181#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(dC(V1,V2)) -> isNatKind#(V2) isNat#(dC(V1,V2)) -> isNatKind#(V1) isNat#(dC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(dC(V1,V2)) -> U191#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(gcdC(V1,V2)) -> isNatKind#(V2) isNat#(gcdC(V1,V2)) -> isNatKind#(V1) isNat#(gcdC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(gcdC(V1,V2)) -> U201#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat#(p_(V1)) -> isNatKind#(V1) isNat#(p_(V1)) -> U211#(isNatKind(V1),V1) isNat#(quot(V1,V2)) -> isNatKind#(V2) isNat#(quot(V1,V2)) -> isNatKind#(V1) isNat#(quot(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNat#(quot(V1,V2)) -> U221#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNatKind#(_*_C(V1,V2)) -> isNatKind#(V2) isNatKind#(_*_C(V1,V2)) -> isNatKind#(V1) isNatKind#(_*_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(_+_C(V1,V2)) -> isNatKind#(V2) isNatKind#(_+_C(V1,V2)) -> isNatKind#(V1) isNatKind#(_+_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(dC(V1,V2)) -> isNatKind#(V2) isNatKind#(dC(V1,V2)) -> isNatKind#(V1) isNatKind#(dC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(gcdC(V1,V2)) -> isNatKind#(V2) isNatKind#(gcdC(V1,V2)) -> isNatKind#(V1) isNatKind#(gcdC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(p_(V1)) -> isNatKind#(V1) isNatKind#(quot(V1,V2)) -> isNatKind#(V2) isNatKind#(quot(V1,V2)) -> isNatKind#(V1) isNatKind#(quot(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNatKind#(s_(V1)) -> isNatKind#(V1) isNzNat#(_*_C(V1,V2)) -> isNatKind#(V2) isNzNat#(_*_C(V1,V2)) -> isNatKind#(V1) isNzNat#(_*_C(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNzNat#(_*_C(V1,V2)) -> U231#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat#(gcdC(V1,V2)) -> isNatKind#(V2) isNzNat#(gcdC(V1,V2)) -> isNatKind#(V1) isNzNat#(gcdC(V1,V2)) -> and#(isNatKind(V1),isNatKind(V2)) isNzNat#(gcdC(V1,V2)) -> U241#(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat#(s_(V1)) -> isNatKind#(V1) isNzNat#(s_(V1)) -> U251#(isNatKind(V1),V1) p_#(s_(N)) -> isNatKind#(N) p_#(s_(N)) -> isNat#(N) p_#(s_(N)) -> and#(isNat(N),isNatKind(N)) p_#(s_(N)) -> U261#(and(isNat(N),isNatKind(N)),N) quot#(M',M') -> isNatKind#(M') quot#(M',M') -> isNzNat#(M') quot#(M',M') -> and#(isNzNat(M'),isNatKind(M')) quot#(M',M') -> U271#(and(isNzNat(M'),isNatKind(M'))) quot#(N,M') -> isNatKind#(N) quot#(N,M') -> isNat#(N) quot#(N,M') -> and#(isNat(N),isNatKind(N)) quot#(N,M') -> isNatKind#(M') quot#(N,M') -> isNzNat#(M') quot#(N,M') -> and#(isNzNat(M'),isNatKind(M')) quot#(N,M') -> and#(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))) quot#(N,M') -> U281#(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) quot#(N,M') -> U291#(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) Equations: TRS: 1() -> s_(0()) 2() -> s_(s_(0())) 3() -> s_(s_(s_(0()))) 4() -> s_(s_(s_(s_(0())))) 5() -> s_(s_(s_(s_(s_(0()))))) 6() -> s_(s_(s_(s_(s_(s_(0())))))) 7() -> s_(s_(s_(s_(s_(s_(s_(0()))))))) U101(tt(),M,N) -> dC(N,M) U11(tt()) -> 0() U111(tt()) -> 0() U121(tt(),M',N') -> U122(equal(_>_(N',M'),true()),M',N') U122(tt(),M',N') -> gcdC(dC(N',M'),M') U131(tt(),N') -> N' U141(tt(),V1,V2) -> U142(isNat(V1),V2) U142(tt(),V2) -> U143(isNat(V2)) U143(tt()) -> tt() U151(tt(),V1,V2) -> U152(isNat(V1),V2) U152(tt(),V2) -> U153(isNat(V2)) U153(tt()) -> tt() U161(tt(),V) -> U162(isNzNat(V)) U162(tt()) -> tt() U171(tt(),V1,V2) -> U172(isNat(V1),V2) U172(tt(),V2) -> U173(isNat(V2)) U173(tt()) -> tt() U181(tt(),V1,V2) -> U182(isNat(V1),V2) U182(tt(),V2) -> U183(isNat(V2)) U183(tt()) -> tt() U191(tt(),V1,V2) -> U192(isNat(V1),V2) U192(tt(),V2) -> U193(isNat(V2)) U193(tt()) -> tt() U201(tt(),V1,V2) -> U202(isNat(V1),V2) U202(tt(),V2) -> U203(isNat(V2)) U203(tt()) -> tt() U21(tt(),M,N) -> s_(_+_C(N,_+_C(M,_*_C(N,M)))) U211(tt(),V1) -> U212(isNzNat(V1)) U212(tt()) -> tt() U221(tt(),V1,V2) -> U222(isNat(V1),V2) U222(tt(),V2) -> U223(isNzNat(V2)) U223(tt()) -> tt() U231(tt(),V1,V2) -> U232(isNzNat(V1),V2) U232(tt(),V2) -> U233(isNzNat(V2)) U233(tt()) -> tt() U241(tt(),V1,V2) -> U242(isNzNat(V1),V2) U242(tt(),V2) -> U243(isNzNat(V2)) U243(tt()) -> tt() U251(tt(),V1) -> U252(isNat(V1)) U252(tt()) -> tt() U261(tt(),N) -> N U271(tt()) -> s_(0()) U281(tt(),M',N) -> U282(equal(_>_(M',N),true())) U282(tt()) -> 0() U291(tt(),M',N) -> U292(equal(_>_(N,M'),true()),M',N) U292(tt(),M',N) -> s_(quot(dC(N,M'),M')) U31(tt(),N) -> N U41(tt(),M,N) -> s_(s_(_+_C(N,M))) U51(tt(),M,N) -> _>_(M,N) U61(tt()) -> false() U71(tt()) -> true() U81(tt(),M,N) -> _>_(N,M) U91(tt(),N) -> N _*_C(N,0()) -> U11(and(isNat(N),isNatKind(N))) _*_C(s_(N),s_(M)) -> U21(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _+_C(N,0()) -> U31(and(isNat(N),isNatKind(N)),N) _+_C(s_(N),s_(M)) -> U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _<_(N,M) -> U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) _>_(0(),M) -> U61(and(isNat(M),isNatKind(M))) _>_(N',0()) -> U71(and(isNzNat(N'),isNatKind(N'))) _>_(s_(N),s_(M)) -> U81(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) and(tt(),X) -> X dC(0(),N) -> U91(and(isNat(N),isNatKind(N)),N) dC(s_(N),s_(M)) -> U101(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) equal(X,X) -> tt() gcdC(0(),N) -> U111(and(isNat(N),isNatKind(N))) gcdC(N',M') -> U121(and(and(isNzNat(M'),isNatKind(M')),and(isNzNat(N'),isNatKind(N'))),M',N') gcdC(N',N') -> U131(and(isNzNat(N'),isNatKind(N')),N') isBoolean(false()) -> tt() isBoolean(true()) -> tt() isBoolean(_<_(V1,V2)) -> U141(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBoolean(_>_(V1,V2)) -> U151(and(isNatKind(V1),isNatKind(V2)),V1,V2) isBooleanKind(false()) -> tt() isBooleanKind(true()) -> tt() isBooleanKind(_<_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isBooleanKind(_>_(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNat(0()) -> tt() isNat(V) -> U161(isNatKind(V),V) isNat(_*_C(V1,V2)) -> U171(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(_+_C(V1,V2)) -> U181(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(dC(V1,V2)) -> U191(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(gcdC(V1,V2)) -> U201(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNat(p_(V1)) -> U211(isNatKind(V1),V1) isNat(quot(V1,V2)) -> U221(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNatKind(0()) -> tt() isNatKind(1()) -> tt() isNatKind(2()) -> tt() isNatKind(3()) -> tt() isNatKind(4()) -> tt() isNatKind(5()) -> tt() isNatKind(6()) -> tt() isNatKind(7()) -> tt() isNatKind(_*_C(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(_+_C(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(dC(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(gcdC(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(p_(V1)) -> isNatKind(V1) isNatKind(quot(V1,V2)) -> and(isNatKind(V1),isNatKind(V2)) isNatKind(s_(V1)) -> isNatKind(V1) isNzNat(1()) -> tt() isNzNat(2()) -> tt() isNzNat(3()) -> tt() isNzNat(4()) -> tt() isNzNat(5()) -> tt() isNzNat(6()) -> tt() isNzNat(7()) -> tt() isNzNat(_*_C(V1,V2)) -> U231(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat(gcdC(V1,V2)) -> U241(and(isNatKind(V1),isNatKind(V2)),V1,V2) isNzNat(s_(V1)) -> U251(isNatKind(V1),V1) p_(s_(N)) -> U261(and(isNat(N),isNatKind(N)),N) quot(M',M') -> U271(and(isNzNat(M'),isNatKind(M'))) quot(N,M') -> U281(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) quot(N,M') -> U291(and(and(isNzNat(M'),isNatKind(M')),and(isNat(N),isNatKind(N))),M',N) S: Open