0 QTRS
↳1 DirectTerminationProof (⇔)
↳2 TRUE
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
d > mark1 > g1 > ah1 > h1 > ag1 > c > ac
a__c=3 d=2 c=1 a__g_1=3 a__h_1=2 mark_1=3 g_1=1 h_1=1