a__g(X) → a__h(X)
a__c → d
a__h(d) → a__g(c)
mark(g(X)) → a__g(X)
mark(h(X)) → a__h(X)
mark(c) → a__c
mark(d) → d
a__g(X) → g(X)
a__h(X) → h(X)
a__c → c
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__g'(X) → a__h'(X)
a__c' → d'
a__h'(d') → a__g'(c')
mark'(g'(X)) → a__g'(X)
mark'(h'(X)) → a__h'(X)
mark'(c') → a__c'
mark'(d') → d'
a__g'(X) → g'(X)
a__h'(X) → h'(X)
a__c' → c'
Infered types.
Rules:
a__g'(X) → a__h'(X)
a__c' → d'
a__h'(d') → a__g'(c')
mark'(g'(X)) → a__g'(X)
mark'(h'(X)) → a__h'(X)
mark'(c') → a__c'
mark'(d') → d'
a__g'(X) → g'(X)
a__h'(X) → h'(X)
a__c' → c'
Types:
a__g' :: d':c':g':h' → d':c':g':h'
a__h' :: d':c':g':h' → d':c':g':h'
a__c' :: d':c':g':h'
d' :: d':c':g':h'
c' :: d':c':g':h'
mark' :: d':c':g':h' → d':c':g':h'
g' :: d':c':g':h' → d':c':g':h'
h' :: d':c':g':h' → d':c':g':h'
_hole_d':c':g':h'1 :: d':c':g':h'
_gen_d':c':g':h'2 :: Nat → d':c':g':h'
Heuristically decided to analyse the following defined symbols:
a__g', a__h'
They will be analysed ascendingly in the following order:
a__g' = a__h'
Rules:
a__g'(X) → a__h'(X)
a__c' → d'
a__h'(d') → a__g'(c')
mark'(g'(X)) → a__g'(X)
mark'(h'(X)) → a__h'(X)
mark'(c') → a__c'
mark'(d') → d'
a__g'(X) → g'(X)
a__h'(X) → h'(X)
a__c' → c'
Types:
a__g' :: d':c':g':h' → d':c':g':h'
a__h' :: d':c':g':h' → d':c':g':h'
a__c' :: d':c':g':h'
d' :: d':c':g':h'
c' :: d':c':g':h'
mark' :: d':c':g':h' → d':c':g':h'
g' :: d':c':g':h' → d':c':g':h'
h' :: d':c':g':h' → d':c':g':h'
_hole_d':c':g':h'1 :: d':c':g':h'
_gen_d':c':g':h'2 :: Nat → d':c':g':h'
Generator Equations:
_gen_d':c':g':h'2(0) ⇔ d'
_gen_d':c':g':h'2(+(x, 1)) ⇔ h'(_gen_d':c':g':h'2(x))
The following defined symbols remain to be analysed:
a__h', a__g'
They will be analysed ascendingly in the following order:
a__g' = a__h'
Could not prove a rewrite lemma for the defined symbol a__h'.
Rules:
a__g'(X) → a__h'(X)
a__c' → d'
a__h'(d') → a__g'(c')
mark'(g'(X)) → a__g'(X)
mark'(h'(X)) → a__h'(X)
mark'(c') → a__c'
mark'(d') → d'
a__g'(X) → g'(X)
a__h'(X) → h'(X)
a__c' → c'
Types:
a__g' :: d':c':g':h' → d':c':g':h'
a__h' :: d':c':g':h' → d':c':g':h'
a__c' :: d':c':g':h'
d' :: d':c':g':h'
c' :: d':c':g':h'
mark' :: d':c':g':h' → d':c':g':h'
g' :: d':c':g':h' → d':c':g':h'
h' :: d':c':g':h' → d':c':g':h'
_hole_d':c':g':h'1 :: d':c':g':h'
_gen_d':c':g':h'2 :: Nat → d':c':g':h'
Generator Equations:
_gen_d':c':g':h'2(0) ⇔ d'
_gen_d':c':g':h'2(+(x, 1)) ⇔ h'(_gen_d':c':g':h'2(x))
The following defined symbols remain to be analysed:
a__g'
They will be analysed ascendingly in the following order:
a__g' = a__h'
Could not prove a rewrite lemma for the defined symbol a__g'.
Rules:
a__g'(X) → a__h'(X)
a__c' → d'
a__h'(d') → a__g'(c')
mark'(g'(X)) → a__g'(X)
mark'(h'(X)) → a__h'(X)
mark'(c') → a__c'
mark'(d') → d'
a__g'(X) → g'(X)
a__h'(X) → h'(X)
a__c' → c'
Types:
a__g' :: d':c':g':h' → d':c':g':h'
a__h' :: d':c':g':h' → d':c':g':h'
a__c' :: d':c':g':h'
d' :: d':c':g':h'
c' :: d':c':g':h'
mark' :: d':c':g':h' → d':c':g':h'
g' :: d':c':g':h' → d':c':g':h'
h' :: d':c':g':h' → d':c':g':h'
_hole_d':c':g':h'1 :: d':c':g':h'
_gen_d':c':g':h'2 :: Nat → d':c':g':h'
Generator Equations:
_gen_d':c':g':h'2(0) ⇔ d'
_gen_d':c':g':h'2(+(x, 1)) ⇔ h'(_gen_d':c':g':h'2(x))
No more defined symbols left to analyse.