WORST_CASE(?,O(n^2)) Solution: --------- "Add" :: ["A"(4, 4) x "A"(0, 4)] -(4)-> "A"(0, 4) "Nat" :: ["A"(0, 4)] -(4)-> "A"(0, 4) "Sub" :: ["A"(4, 4) x "A"(0, 4)] -(4)-> "A"(0, 4) "Succ" :: ["A"(0, 1)] -(0)-> "A"(0, 1) "Succ" :: ["A"(1, 1)] -(1)-> "A"(1, 1) "Zero" :: [] -(0)-> "A"(0, 1) "Zero" :: [] -(0)-> "A"(1, 1) "Zero" :: [] -(0)-> "A"(15, 8) "add#2" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1) "eval#1" :: ["A"(0, 4)] -(0)-> "A"(0, 1) "main" :: ["A"(14, 10)] -(16)-> "A"(0, 0) "sub#2" :: ["A"(1, 1) x "A"(0, 1)] -(2)-> "A"(1, 1) Cost Free Signatures: --------------------- "Add" :: ["A"_cf(4, 0) x "A"_cf(4, 0)] -(4)-> "A"_cf(4, 0) "Add" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "Nat" :: ["A"_cf(4, 0)] -(0)-> "A"_cf(4, 0) "Nat" :: ["A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "Sub" :: ["A"_cf(4, 0) x "A"_cf(4, 0)] -(4)-> "A"_cf(4, 0) "Sub" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "Succ" :: ["A"_cf(1, 0)] -(1)-> "A"_cf(1, 0) "Succ" :: ["A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "Succ" :: ["A"_cf(4, 0)] -(4)-> "A"_cf(4, 0) "Zero" :: [] -(0)-> "A"_cf(1, 0) "Zero" :: [] -(0)-> "A"_cf(0, 0) "Zero" :: [] -(0)-> "A"_cf(8, 0) "Zero" :: [] -(0)-> "A"_cf(4, 0) "Zero" :: [] -(0)-> "A"_cf(8, 8) "add#2" :: ["A"_cf(1, 0) x "A"_cf(1, 0)] -(0)-> "A"_cf(1, 0) "add#2" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "add#2" :: ["A"_cf(4, 0) x "A"_cf(4, 0)] -(0)-> "A"_cf(4, 0) "eval#1" :: ["A"_cf(4, 0)] -(0)-> "A"_cf(1, 0) "eval#1" :: ["A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "eval#1" :: ["A"_cf(4, 0)] -(0)-> "A"_cf(4, 0) "sub#2" :: ["A"_cf(1, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(1, 0) "sub#2" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "sub#2" :: ["A"_cf(4, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(4, 0) Base Constructors: ------------------ "\"Add\"_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "\"Add\"_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1) "\"Nat\"_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "\"Nat\"_A" :: ["A"(0, 1)] -(1)-> "A"(0, 1) "\"Sub\"_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "\"Sub\"_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1) "\"Succ\"_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "\"Succ\"_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1) "\"Zero\"_A" :: [] -(0)-> "A"(1, 0) "\"Zero\"_A" :: [] -(0)-> "A"(0, 1)