0 QTRS
↳1 DirectTerminationProof (⇔)
↳2 TRUE
a__c → a__f(g(c)) a__f(g(X)) → g(X) mark(c) → a__c mark(f(X)) → a__f(X) mark(g(X)) → g(X) a__c → c a__f(X) → f(X)
f1 > af1 > ac > mark1 > c > g1
a__c=5 c=1 a__f_1=2 g_1=1 mark_1=5 f_1=1