; @origtpdbfilename arith.trs
; @xtcfilename "./TRS_Standard/Kaliszyk_19/arith.xml"
(format TRS)
(fun NUMERAL 1)
(fun |0| 0)
(fun BIT0 1)
(fun SUC 1)
(fun BIT1 1)
(fun PRE 1)
(fun if 3)
(fun eq 2)
(fun plus 2)
(fun mult 2)
(fun exp 2)
(fun EVEN 1)
(fun T 0)
(fun F 0)
(fun ODD 1)
(fun le 2)
(fun lt 2)
(fun ge 2)
(fun gt 2)
(fun minus 2)
(rule (NUMERAL |0|) |0|)
(rule (BIT0 |0|) |0|)
(rule (SUC (NUMERAL n)) (NUMERAL (SUC n)))
(rule (SUC |0|) (BIT1 |0|))
(rule (SUC (BIT0 n)) (BIT1 n))
(rule (SUC (BIT1 n)) (BIT0 (SUC n)))
(rule (PRE (NUMERAL n)) (NUMERAL (PRE n)))
(rule (PRE |0|) |0|)
(rule (PRE (BIT0 n)) (if (eq n |0|) |0| (BIT1 (PRE n))))
(rule (PRE (BIT1 n)) (BIT0 n))
(rule (plus (NUMERAL m) (NUMERAL n)) (NUMERAL (plus m n)))
(rule (plus |0| |0|) |0|)
(rule (plus |0| (BIT0 n)) (BIT0 n))
(rule (plus |0| (BIT1 n)) (BIT1 n))
(rule (plus (BIT0 n) |0|) (BIT0 n))
(rule (plus (BIT1 n) |0|) (BIT1 n))
(rule (plus (BIT0 m) (BIT0 n)) (BIT0 (plus m n)))
(rule (plus (BIT0 m) (BIT1 n)) (BIT1 (plus m n)))
(rule (plus (BIT1 m) (BIT0 n)) (BIT1 (plus m n)))
(rule (plus (BIT1 m) (BIT1 n)) (BIT0 (SUC (plus m n))))
(rule (mult (NUMERAL m) (NUMERAL n)) (NUMERAL (mult m n)))
(rule (mult |0| |0|) |0|)
(rule (mult |0| (BIT0 n)) |0|)
(rule (mult |0| (BIT1 n)) |0|)
(rule (mult (BIT0 n) |0|) |0|)
(rule (mult (BIT1 n) |0|) |0|)
(rule (mult (BIT0 m) (BIT0 n)) (BIT0 (BIT0 (mult m n))))
(rule (mult (BIT0 m) (BIT1 n)) (plus (BIT0 m) (BIT0 (BIT0 (mult m n)))))
(rule (mult (BIT1 m) (BIT0 n)) (plus (BIT0 n) (BIT0 (BIT0 (mult m n)))))
(rule (mult (BIT1 m) (BIT1 n)) (plus (plus (BIT1 m) (BIT0 n)) (BIT0 (BIT0 (mult m n)))))
(rule (exp (NUMERAL m) (NUMERAL n)) (NUMERAL (exp m n)))
(rule (exp |0| |0|) (BIT1 |0|))
(rule (exp (BIT0 m) |0|) (BIT1 |0|))
(rule (exp (BIT1 m) |0|) (BIT1 |0|))
(rule (exp |0| (BIT0 n)) (mult (exp |0| n) (exp |0| n)))
(rule (exp (BIT0 m) (BIT0 n)) (mult (exp (BIT0 m) n) (exp (BIT0 m) n)))
(rule (exp (BIT1 m) (BIT0 n)) (mult (exp (BIT1 m) n) (exp (BIT1 m) n)))
(rule (exp |0| (BIT1 n)) |0|)
(rule (exp (BIT0 m) (BIT1 n)) (mult (mult (BIT0 m) (exp (BIT0 m) n)) (exp (BIT0 m) n)))
(rule (exp (BIT1 m) (BIT1 n)) (mult (mult (BIT1 m) (exp (BIT1 m) n)) (exp (BIT1 m) n)))
(rule (EVEN (NUMERAL n)) (EVEN n))
(rule (EVEN |0|) T)
(rule (EVEN (BIT0 n)) T)
(rule (EVEN (BIT1 n)) F)
(rule (ODD (NUMERAL n)) (ODD n))
(rule (ODD |0|) F)
(rule (ODD (BIT0 n)) F)
(rule (ODD (BIT1 n)) T)
(rule (eq (NUMERAL m) (NUMERAL n)) (eq m n))
(rule (eq |0| |0|) T)
(rule (eq (BIT0 n) |0|) (eq n |0|))
(rule (eq (BIT1 n) |0|) F)
(rule (eq |0| (BIT0 n)) (eq |0| n))
(rule (eq |0| (BIT1 n)) F)
(rule (eq (BIT0 m) (BIT0 n)) (eq m n))
(rule (eq (BIT0 m) (BIT1 n)) F)
(rule (eq (BIT1 m) (BIT0 n)) F)
(rule (eq (BIT1 m) (BIT1 n)) (eq m n))
(rule (le (NUMERAL m) (NUMERAL n)) (le m n))
(rule (le |0| |0|) T)
(rule (le (BIT0 n) |0|) (le n |0|))
(rule (le (BIT1 n) |0|) F)
(rule (le |0| (BIT0 n)) T)
(rule (le |0| (BIT1 n)) T)
(rule (le (BIT0 m) (BIT0 n)) (le m n))
(rule (le (BIT0 m) (BIT1 n)) (le m n))
(rule (le (BIT1 m) (BIT0 n)) (lt m n))
(rule (le (BIT1 m) (BIT1 n)) (le m n))
(rule (lt (NUMERAL m) (NUMERAL n)) (lt m n))
(rule (lt |0| |0|) F)
(rule (lt (BIT0 n) |0|) F)
(rule (lt (BIT1 n) |0|) F)
(rule (lt |0| (BIT0 n)) (lt |0| n))
(rule (lt |0| (BIT1 n)) T)
(rule (lt (BIT0 m) (BIT0 n)) (lt m n))
(rule (lt (BIT0 m) (BIT1 n)) (le m n))
(rule (lt (BIT1 m) (BIT0 n)) (lt m n))
(rule (lt (BIT1 m) (BIT1 n)) (lt m n))
(rule (ge (NUMERAL n) (NUMERAL m)) (ge n m))
(rule (ge |0| |0|) T)
(rule (ge |0| (BIT0 n)) (ge |0| n))
(rule (ge |0| (BIT1 n)) F)
(rule (ge (BIT0 n) |0|) T)
(rule (ge (BIT1 n) |0|) T)
(rule (ge (BIT0 n) (BIT0 m)) (ge n m))
(rule (ge (BIT1 n) (BIT0 m)) (ge n m))
(rule (ge (BIT0 n) (BIT1 m)) (gt n m))
(rule (ge (BIT1 n) (BIT1 m)) (ge n m))
(rule (gt (NUMERAL n) (NUMERAL m)) (gt n m))
(rule (gt |0| |0|) F)
(rule (gt |0| (BIT0 n)) F)
(rule (gt |0| (BIT1 n)) F)
(rule (gt (BIT0 n) |0|) (gt n |0|))
(rule (gt (BIT1 n) |0|) T)
(rule (gt (BIT0 n) (BIT0 m)) (gt n m))
(rule (gt (BIT1 n) (BIT0 m)) (ge n m))
(rule (gt (BIT0 n) (BIT1 m)) (gt n m))
(rule (gt (BIT1 n) (BIT1 m)) (gt n m))
(rule (minus (NUMERAL m) (NUMERAL n)) (NUMERAL (minus m n)))
(rule (minus |0| |0|) |0|)
(rule (minus |0| (BIT0 n)) |0|)
(rule (minus |0| (BIT1 n)) |0|)
(rule (minus (BIT0 n) |0|) (BIT0 n))
(rule (minus (BIT1 n) |0|) (BIT1 n))
(rule (minus (BIT0 m) (BIT0 n)) (BIT0 (minus m n)))
(rule (minus (BIT0 m) (BIT1 n)) (PRE (BIT0 (minus m n))))
(rule (minus (BIT1 m) (BIT0 n)) (if (le n m) (BIT1 (minus m n)) |0|))
(rule (minus (BIT1 m) (BIT1 n)) (BIT0 (minus m n)))