YES proof of Kaliszyk_19_arith.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished Termination w.r.t. Q of the given QTRS could be proven: (0) QTRS (1) QTRSRRRProof [EQUIVALENT, 250 ms] (2) QTRS (3) QTRSRRRProof [EQUIVALENT, 0 ms] (4) QTRS (5) RisEmptyProof [EQUIVALENT, 0 ms] (6) YES ---------------------------------------- (0) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: NUMERAL(0) -> 0 BIT0(0) -> 0 SUC(NUMERAL(n)) -> NUMERAL(SUC(n)) SUC(0) -> BIT1(0) SUC(BIT0(n)) -> BIT1(n) SUC(BIT1(n)) -> BIT0(SUC(n)) PRE(NUMERAL(n)) -> NUMERAL(PRE(n)) PRE(0) -> 0 PRE(BIT0(n)) -> if(eq(n, 0), 0, BIT1(PRE(n))) PRE(BIT1(n)) -> BIT0(n) plus(NUMERAL(m), NUMERAL(n)) -> NUMERAL(plus(m, n)) plus(0, 0) -> 0 plus(0, BIT0(n)) -> BIT0(n) plus(0, BIT1(n)) -> BIT1(n) plus(BIT0(n), 0) -> BIT0(n) plus(BIT1(n), 0) -> BIT1(n) plus(BIT0(m), BIT0(n)) -> BIT0(plus(m, n)) plus(BIT0(m), BIT1(n)) -> BIT1(plus(m, n)) plus(BIT1(m), BIT0(n)) -> BIT1(plus(m, n)) plus(BIT1(m), BIT1(n)) -> BIT0(SUC(plus(m, n))) mult(NUMERAL(m), NUMERAL(n)) -> NUMERAL(mult(m, n)) mult(0, 0) -> 0 mult(0, BIT0(n)) -> 0 mult(0, BIT1(n)) -> 0 mult(BIT0(n), 0) -> 0 mult(BIT1(n), 0) -> 0 mult(BIT0(m), BIT0(n)) -> BIT0(BIT0(mult(m, n))) mult(BIT0(m), BIT1(n)) -> plus(BIT0(m), BIT0(BIT0(mult(m, n)))) mult(BIT1(m), BIT0(n)) -> plus(BIT0(n), BIT0(BIT0(mult(m, n)))) mult(BIT1(m), BIT1(n)) -> plus(plus(BIT1(m), BIT0(n)), BIT0(BIT0(mult(m, n)))) exp(NUMERAL(m), NUMERAL(n)) -> NUMERAL(exp(m, n)) exp(0, 0) -> BIT1(0) exp(BIT0(m), 0) -> BIT1(0) exp(BIT1(m), 0) -> BIT1(0) exp(0, BIT0(n)) -> mult(exp(0, n), exp(0, n)) exp(BIT0(m), BIT0(n)) -> mult(exp(BIT0(m), n), exp(BIT0(m), n)) exp(BIT1(m), BIT0(n)) -> mult(exp(BIT1(m), n), exp(BIT1(m), n)) exp(0, BIT1(n)) -> 0 exp(BIT0(m), BIT1(n)) -> mult(mult(BIT0(m), exp(BIT0(m), n)), exp(BIT0(m), n)) exp(BIT1(m), BIT1(n)) -> mult(mult(BIT1(m), exp(BIT1(m), n)), exp(BIT1(m), n)) EVEN(NUMERAL(n)) -> EVEN(n) EVEN(0) -> T EVEN(BIT0(n)) -> T EVEN(BIT1(n)) -> F ODD(NUMERAL(n)) -> ODD(n) ODD(0) -> F ODD(BIT0(n)) -> F ODD(BIT1(n)) -> T eq(NUMERAL(m), NUMERAL(n)) -> eq(m, n) eq(0, 0) -> T eq(BIT0(n), 0) -> eq(n, 0) eq(BIT1(n), 0) -> F eq(0, BIT0(n)) -> eq(0, n) eq(0, BIT1(n)) -> F eq(BIT0(m), BIT0(n)) -> eq(m, n) eq(BIT0(m), BIT1(n)) -> F eq(BIT1(m), BIT0(n)) -> F eq(BIT1(m), BIT1(n)) -> eq(m, n) le(NUMERAL(m), NUMERAL(n)) -> le(m, n) le(0, 0) -> T le(BIT0(n), 0) -> le(n, 0) le(BIT1(n), 0) -> F le(0, BIT0(n)) -> T le(0, BIT1(n)) -> T le(BIT0(m), BIT0(n)) -> le(m, n) le(BIT0(m), BIT1(n)) -> le(m, n) le(BIT1(m), BIT0(n)) -> lt(m, n) le(BIT1(m), BIT1(n)) -> le(m, n) lt(NUMERAL(m), NUMERAL(n)) -> lt(m, n) lt(0, 0) -> F lt(BIT0(n), 0) -> F lt(BIT1(n), 0) -> F lt(0, BIT0(n)) -> lt(0, n) lt(0, BIT1(n)) -> T lt(BIT0(m), BIT0(n)) -> lt(m, n) lt(BIT0(m), BIT1(n)) -> le(m, n) lt(BIT1(m), BIT0(n)) -> lt(m, n) lt(BIT1(m), BIT1(n)) -> lt(m, n) ge(NUMERAL(n), NUMERAL(m)) -> ge(n, m) ge(0, 0) -> T ge(0, BIT0(n)) -> ge(0, n) ge(0, BIT1(n)) -> F ge(BIT0(n), 0) -> T ge(BIT1(n), 0) -> T ge(BIT0(n), BIT0(m)) -> ge(n, m) ge(BIT1(n), BIT0(m)) -> ge(n, m) ge(BIT0(n), BIT1(m)) -> gt(n, m) ge(BIT1(n), BIT1(m)) -> ge(n, m) gt(NUMERAL(n), NUMERAL(m)) -> gt(n, m) gt(0, 0) -> F gt(0, BIT0(n)) -> F gt(0, BIT1(n)) -> F gt(BIT0(n), 0) -> gt(n, 0) gt(BIT1(n), 0) -> T gt(BIT0(n), BIT0(m)) -> gt(n, m) gt(BIT1(n), BIT0(m)) -> ge(n, m) gt(BIT0(n), BIT1(m)) -> gt(n, m) gt(BIT1(n), BIT1(m)) -> gt(n, m) minus(NUMERAL(m), NUMERAL(n)) -> NUMERAL(minus(m, n)) minus(0, 0) -> 0 minus(0, BIT0(n)) -> 0 minus(0, BIT1(n)) -> 0 minus(BIT0(n), 0) -> BIT0(n) minus(BIT1(n), 0) -> BIT1(n) minus(BIT0(m), BIT0(n)) -> BIT0(minus(m, n)) minus(BIT0(m), BIT1(n)) -> PRE(BIT0(minus(m, n))) minus(BIT1(m), BIT0(n)) -> if(le(n, m), BIT1(minus(m, n)), 0) minus(BIT1(m), BIT1(n)) -> BIT0(minus(m, n)) Q is empty. ---------------------------------------- (1) QTRSRRRProof (EQUIVALENT) Used ordering: Quasi precedence: exp_2 > mult_2 > plus_2 > [0, T] > [NUMERAL_1, BIT0_1, SUC_1, BIT1_1, if_3, F, ge_2, gt_2] EVEN_1 > [0, T] > [NUMERAL_1, BIT0_1, SUC_1, BIT1_1, if_3, F, ge_2, gt_2] ODD_1 > [0, T] > [NUMERAL_1, BIT0_1, SUC_1, BIT1_1, if_3, F, ge_2, gt_2] minus_2 > PRE_1 > eq_2 > [0, T] > [NUMERAL_1, BIT0_1, SUC_1, BIT1_1, if_3, F, ge_2, gt_2] minus_2 > [le_2, lt_2] > [0, T] > [NUMERAL_1, BIT0_1, SUC_1, BIT1_1, if_3, F, ge_2, gt_2] Status: NUMERAL_1: [1] 0: multiset status BIT0_1: [1] SUC_1: [1] BIT1_1: [1] PRE_1: multiset status if_3: [2,1,3] eq_2: [2,1] plus_2: [1,2] mult_2: [1,2] exp_2: [2,1] EVEN_1: multiset status T: multiset status F: multiset status ODD_1: multiset status le_2: [1,2] lt_2: [1,2] ge_2: multiset status gt_2: multiset status minus_2: [1,2] With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: NUMERAL(0) -> 0 BIT0(0) -> 0 SUC(BIT0(n)) -> BIT1(n) PRE(NUMERAL(n)) -> NUMERAL(PRE(n)) PRE(0) -> 0 PRE(BIT0(n)) -> if(eq(n, 0), 0, BIT1(PRE(n))) PRE(BIT1(n)) -> BIT0(n) plus(NUMERAL(m), NUMERAL(n)) -> NUMERAL(plus(m, n)) plus(0, 0) -> 0 plus(0, BIT0(n)) -> BIT0(n) plus(0, BIT1(n)) -> BIT1(n) plus(BIT0(n), 0) -> BIT0(n) plus(BIT1(n), 0) -> BIT1(n) plus(BIT0(m), BIT0(n)) -> BIT0(plus(m, n)) plus(BIT0(m), BIT1(n)) -> BIT1(plus(m, n)) plus(BIT1(m), BIT0(n)) -> BIT1(plus(m, n)) plus(BIT1(m), BIT1(n)) -> BIT0(SUC(plus(m, n))) mult(NUMERAL(m), NUMERAL(n)) -> NUMERAL(mult(m, n)) mult(0, 0) -> 0 mult(0, BIT0(n)) -> 0 mult(0, BIT1(n)) -> 0 mult(BIT0(n), 0) -> 0 mult(BIT1(n), 0) -> 0 mult(BIT0(m), BIT0(n)) -> BIT0(BIT0(mult(m, n))) mult(BIT0(m), BIT1(n)) -> plus(BIT0(m), BIT0(BIT0(mult(m, n)))) mult(BIT1(m), BIT0(n)) -> plus(BIT0(n), BIT0(BIT0(mult(m, n)))) mult(BIT1(m), BIT1(n)) -> plus(plus(BIT1(m), BIT0(n)), BIT0(BIT0(mult(m, n)))) exp(NUMERAL(m), NUMERAL(n)) -> NUMERAL(exp(m, n)) exp(0, 0) -> BIT1(0) exp(BIT0(m), 0) -> BIT1(0) exp(BIT1(m), 0) -> BIT1(0) exp(0, BIT0(n)) -> mult(exp(0, n), exp(0, n)) exp(BIT0(m), BIT0(n)) -> mult(exp(BIT0(m), n), exp(BIT0(m), n)) exp(BIT1(m), BIT0(n)) -> mult(exp(BIT1(m), n), exp(BIT1(m), n)) exp(0, BIT1(n)) -> 0 exp(BIT0(m), BIT1(n)) -> mult(mult(BIT0(m), exp(BIT0(m), n)), exp(BIT0(m), n)) exp(BIT1(m), BIT1(n)) -> mult(mult(BIT1(m), exp(BIT1(m), n)), exp(BIT1(m), n)) EVEN(NUMERAL(n)) -> EVEN(n) EVEN(0) -> T EVEN(BIT0(n)) -> T EVEN(BIT1(n)) -> F ODD(NUMERAL(n)) -> ODD(n) ODD(0) -> F ODD(BIT0(n)) -> F ODD(BIT1(n)) -> T eq(NUMERAL(m), NUMERAL(n)) -> eq(m, n) eq(0, 0) -> T eq(BIT0(n), 0) -> eq(n, 0) eq(BIT1(n), 0) -> F eq(0, BIT0(n)) -> eq(0, n) eq(0, BIT1(n)) -> F eq(BIT0(m), BIT0(n)) -> eq(m, n) eq(BIT0(m), BIT1(n)) -> F eq(BIT1(m), BIT0(n)) -> F eq(BIT1(m), BIT1(n)) -> eq(m, n) le(NUMERAL(m), NUMERAL(n)) -> le(m, n) le(0, 0) -> T le(BIT0(n), 0) -> le(n, 0) le(BIT1(n), 0) -> F le(0, BIT0(n)) -> T le(0, BIT1(n)) -> T le(BIT0(m), BIT0(n)) -> le(m, n) le(BIT0(m), BIT1(n)) -> le(m, n) le(BIT1(m), BIT0(n)) -> lt(m, n) le(BIT1(m), BIT1(n)) -> le(m, n) lt(NUMERAL(m), NUMERAL(n)) -> lt(m, n) lt(0, 0) -> F lt(BIT0(n), 0) -> F lt(BIT1(n), 0) -> F lt(0, BIT0(n)) -> lt(0, n) lt(0, BIT1(n)) -> T lt(BIT0(m), BIT0(n)) -> lt(m, n) lt(BIT0(m), BIT1(n)) -> le(m, n) lt(BIT1(m), BIT0(n)) -> lt(m, n) lt(BIT1(m), BIT1(n)) -> lt(m, n) ge(NUMERAL(n), NUMERAL(m)) -> ge(n, m) ge(0, 0) -> T ge(0, BIT0(n)) -> ge(0, n) ge(0, BIT1(n)) -> F ge(BIT0(n), 0) -> T ge(BIT1(n), 0) -> T ge(BIT0(n), BIT0(m)) -> ge(n, m) ge(BIT1(n), BIT0(m)) -> ge(n, m) ge(BIT0(n), BIT1(m)) -> gt(n, m) ge(BIT1(n), BIT1(m)) -> ge(n, m) gt(NUMERAL(n), NUMERAL(m)) -> gt(n, m) gt(0, 0) -> F gt(0, BIT0(n)) -> F gt(0, BIT1(n)) -> F gt(BIT0(n), 0) -> gt(n, 0) gt(BIT1(n), 0) -> T gt(BIT0(n), BIT0(m)) -> gt(n, m) gt(BIT1(n), BIT0(m)) -> ge(n, m) gt(BIT0(n), BIT1(m)) -> gt(n, m) gt(BIT1(n), BIT1(m)) -> gt(n, m) minus(NUMERAL(m), NUMERAL(n)) -> NUMERAL(minus(m, n)) minus(0, 0) -> 0 minus(0, BIT0(n)) -> 0 minus(0, BIT1(n)) -> 0 minus(BIT0(n), 0) -> BIT0(n) minus(BIT1(n), 0) -> BIT1(n) minus(BIT0(m), BIT0(n)) -> BIT0(minus(m, n)) minus(BIT0(m), BIT1(n)) -> PRE(BIT0(minus(m, n))) minus(BIT1(m), BIT0(n)) -> if(le(n, m), BIT1(minus(m, n)), 0) minus(BIT1(m), BIT1(n)) -> BIT0(minus(m, n)) ---------------------------------------- (2) Obligation: Q restricted rewrite system: The TRS R consists of the following rules: SUC(NUMERAL(n)) -> NUMERAL(SUC(n)) SUC(0) -> BIT1(0) SUC(BIT1(n)) -> BIT0(SUC(n)) Q is empty. ---------------------------------------- (3) QTRSRRRProof (EQUIVALENT) Used ordering: Knuth-Bendix order [KBO] with precedence:SUC_1 > BIT0_1 > BIT1_1 > 0 > NUMERAL_1 and weight map: 0=1 SUC_1=2 NUMERAL_1=1 BIT1_1=2 BIT0_1=2 The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: SUC(NUMERAL(n)) -> NUMERAL(SUC(n)) SUC(0) -> BIT1(0) SUC(BIT1(n)) -> BIT0(SUC(n)) ---------------------------------------- (4) Obligation: Q restricted rewrite system: R is empty. Q is empty. ---------------------------------------- (5) RisEmptyProof (EQUIVALENT) The TRS R is empty. Hence, termination is trivially proven. ---------------------------------------- (6) YES