; @origtpdbfilename TRS//AProVE_10/double.trs ; @xtcfilename "./TRS_Standard/AProVE_10/double.xml" (format TRS) (fun f 2) (fun tt 0) (fun isDouble 1) (fun s 1) (fun |0| 0) (rule (f tt x) (f (isDouble x) (s (s x)))) (rule (isDouble (s (s x))) (isDouble x)) (rule (isDouble |0|) tt)