Problem: f(X) -> if(X,c(),f(true())) if(true(),X,Y) -> X if(false(),X,Y) -> Y Proof: Containment Processor: loop length: 1 terms: f(X) context: if(X,c(),[]) substitution: X -> true() Qed