; @origtpdbfilename ./TRS/TRCSR/PEANO_complete_GM.trs ; @xtcfilename "./TRS_Standard/Transformed_CSR_04/PEANO_complete_GM.xml" (format TRS) (fun a__U11 3) (fun tt 0) (fun a__U12 2) (fun a__isNat 1) (fun a__U13 1) (fun a__U21 2) (fun a__U22 1) (fun a__U31 2) (fun mark 1) (fun a__U41 3) (fun s 1) (fun a__plus 2) (fun a__and 2) (fun |0| 0) (fun plus 2) (fun a__isNatKind 1) (fun isNatKind 1) (fun and 2) (fun isNat 1) (fun U11 3) (fun U12 2) (fun U13 1) (fun U21 2) (fun U22 1) (fun U31 2) (fun U41 3) (rule (a__U11 tt V1 V2) (a__U12 (a__isNat V1) V2)) (rule (a__U12 tt V2) (a__U13 (a__isNat V2))) (rule (a__U13 tt) tt) (rule (a__U21 tt V1) (a__U22 (a__isNat V1))) (rule (a__U22 tt) tt) (rule (a__U31 tt N) (mark N)) (rule (a__U41 tt M N) (s (a__plus (mark N) (mark M)))) (rule (a__and tt X) (mark X)) (rule (a__isNat |0|) tt) (rule (a__isNat (plus V1 V2)) (a__U11 (a__and (a__isNatKind V1) (isNatKind V2)) V1 V2)) (rule (a__isNat (s V1)) (a__U21 (a__isNatKind V1) V1)) (rule (a__isNatKind |0|) tt) (rule (a__isNatKind (plus V1 V2)) (a__and (a__isNatKind V1) (isNatKind V2))) (rule (a__isNatKind (s V1)) (a__isNatKind V1)) (rule (a__plus N |0|) (a__U31 (a__and (a__isNat N) (isNatKind N)) N)) (rule (a__plus N (s M)) (a__U41 (a__and (a__and (a__isNat M) (isNatKind M)) (and (isNat N) (isNatKind N))) M N)) (rule (mark (U11 X1 X2 X3)) (a__U11 (mark X1) X2 X3)) (rule (mark (U12 X1 X2)) (a__U12 (mark X1) X2)) (rule (mark (isNat X)) (a__isNat X)) (rule (mark (U13 X)) (a__U13 (mark X))) (rule (mark (U21 X1 X2)) (a__U21 (mark X1) X2)) (rule (mark (U22 X)) (a__U22 (mark X))) (rule (mark (U31 X1 X2)) (a__U31 (mark X1) X2)) (rule (mark (U41 X1 X2 X3)) (a__U41 (mark X1) X2 X3)) (rule (mark (plus X1 X2)) (a__plus (mark X1) (mark X2))) (rule (mark (and X1 X2)) (a__and (mark X1) X2)) (rule (mark (isNatKind X)) (a__isNatKind X)) (rule (mark tt) tt) (rule (mark (s X)) (s (mark X))) (rule (mark |0|) |0|) (rule (a__U11 X1 X2 X3) (U11 X1 X2 X3)) (rule (a__U12 X1 X2) (U12 X1 X2)) (rule (a__isNat X) (isNat X)) (rule (a__U13 X) (U13 X)) (rule (a__U21 X1 X2) (U21 X1 X2)) (rule (a__U22 X) (U22 X)) (rule (a__U31 X1 X2) (U31 X1 X2)) (rule (a__U41 X1 X2 X3) (U41 X1 X2 X3)) (rule (a__plus X1 X2) (plus X1 X2)) (rule (a__and X1 X2) (and X1 X2)) (rule (a__isNatKind X) (isNatKind X))