KILLED
proof of input_fIqo96VtF1.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).

(0) CpxTRS
(1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CpxTRS
(3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(4) CpxTRS
(5) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(6) CpxWeightedTrs
    (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxTypedWeightedTrs
    (9) CompletionProof [UPPER BOUND(ID), 0 ms]
    (10) CpxTypedWeightedCompleteTrs
        (11) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (12) CpxTypedWeightedCompleteTrs
        (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (14) CpxRNTS
        (15) InliningProof [UPPER BOUND(ID), 0 ms]
        (16) CpxRNTS
        (17) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (18) CpxRNTS
        (19) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
        (20) CpxRNTS
        (21) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (22) CpxRNTS
        (23) IntTrsBoundProof [UPPER BOUND(ID), 299 ms]
        (24) CpxRNTS
        (25) IntTrsBoundProof [UPPER BOUND(ID), 86 ms]
        (26) CpxRNTS
        (27) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (28) CpxRNTS
        (29) IntTrsBoundProof [UPPER BOUND(ID), 246 ms]
        (30) CpxRNTS
        (31) IntTrsBoundProof [UPPER BOUND(ID), 6 ms]
        (32) CpxRNTS
        (33) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (34) CpxRNTS
        (35) IntTrsBoundProof [UPPER BOUND(ID), 89 ms]
        (36) CpxRNTS
        (37) IntTrsBoundProof [UPPER BOUND(ID), 2 ms]
        (38) CpxRNTS
        (39) ResultPropagationProof [UPPER BOUND(ID), 1 ms]
        (40) CpxRNTS
        (41) IntTrsBoundProof [UPPER BOUND(ID), 119 ms]
        (42) CpxRNTS
        (43) IntTrsBoundProof [UPPER BOUND(ID), 52 ms]
        (44) CpxRNTS
        (45) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (46) CpxRNTS
        (47) IntTrsBoundProof [UPPER BOUND(ID), 454 ms]
        (48) CpxRNTS
        (49) IntTrsBoundProof [UPPER BOUND(ID), 107 ms]
        (50) CpxRNTS
        (51) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (52) CpxRNTS
        (53) IntTrsBoundProof [UPPER BOUND(ID), 884 ms]
        (54) CpxRNTS
        (55) IntTrsBoundProof [UPPER BOUND(ID), 177 ms]
        (56) CpxRNTS
    (57) CompletionProof [UPPER BOUND(ID), 0 ms]
    (58) CpxTypedWeightedCompleteTrs
        (59) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (60) CpxRNTS
(61) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(62) CdtProblem
    (63) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (64) CdtProblem
    (65) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (66) CdtProblem
    (67) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (68) CdtProblem
    (69) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 4 ms]
    (70) CdtProblem
    (71) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (72) CdtProblem
    (73) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (74) CdtProblem
    (75) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (76) CdtProblem
    (77) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (78) CdtProblem
    (79) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 33 ms]
    (80) CdtProblem
    (81) CdtRewritingProof [BOTH BOUNDS(ID, ID), 1 ms]
    (82) CdtProblem
    (83) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 33 ms]
    (84) CdtProblem
    (85) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (86) CdtProblem
    (87) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 29 ms]
    (88) CdtProblem
    (89) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (90) CdtProblem
    (91) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 27 ms]
    (92) CdtProblem
    (93) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (94) CdtProblem
    (95) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 26 ms]
    (96) CdtProblem
    (97) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (98) CdtProblem
    (99) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (100) CdtProblem
    (101) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (102) CdtProblem
    (103) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (104) CdtProblem
    (105) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (106) CdtProblem
    (107) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (108) CdtProblem


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   fact(X) -> if(zero(X), s(0), prod(X, fact(p(X))))
   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   prod(0, X) -> 0
   prod(s(X), Y) -> add(Y, prod(X, Y))
   if(true, X, Y) -> X
   if(false, X, Y) -> Y
   zero(0) -> true
   zero(s(X)) -> false
   p(s(X)) -> X

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   fact(X) -> if(zero(X), s(0'), prod(X, fact(p(X))))
   add(0', X) -> X
   add(s(X), Y) -> s(add(X, Y))
   prod(0', X) -> 0'
   prod(s(X), Y) -> add(Y, prod(X, Y))
   if(true, X, Y) -> X
   if(false, X, Y) -> Y
   zero(0') -> true
   zero(s(X)) -> false
   p(s(X)) -> X

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(4)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   fact(X) -> if(zero(X), s(0), prod(X, fact(p(X))))
   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   prod(0, X) -> 0
   prod(s(X), Y) -> add(Y, prod(X, Y))
   if(true, X, Y) -> X
   if(false, X, Y) -> Y
   zero(0) -> true
   zero(s(X)) -> false
   p(s(X)) -> X

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(5) RelTrsToWeightedTrsProof (UPPER BOUND(ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   fact(X) -> if(zero(X), s(0), prod(X, fact(p(X)))) [1]
   add(0, X) -> X [1]
   add(s(X), Y) -> s(add(X, Y)) [1]
   prod(0, X) -> 0 [1]
   prod(s(X), Y) -> add(Y, prod(X, Y)) [1]
   if(true, X, Y) -> X [1]
   if(false, X, Y) -> Y [1]
   zero(0) -> true [1]
   zero(s(X)) -> false [1]
   p(s(X)) -> X [1]

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(8)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   fact(X) -> if(zero(X), s(0), prod(X, fact(p(X)))) [1]
   add(0, X) -> X [1]
   add(s(X), Y) -> s(add(X, Y)) [1]
   prod(0, X) -> 0 [1]
   prod(s(X), Y) -> add(Y, prod(X, Y)) [1]
   if(true, X, Y) -> X [1]
   if(false, X, Y) -> Y [1]
   zero(0) -> true [1]
   zero(s(X)) -> false [1]
   p(s(X)) -> X [1]

The TRS has the following type information:
fact :: 0:s -> 0:s
if :: true:false -> 0:s -> 0:s -> 0:s
zero :: 0:s -> true:false
s :: 0:s -> 0:s
0 :: 0:s
prod :: 0:s -> 0:s -> 0:s
p :: 0:s -> 0:s
add :: 0:s -> 0:s -> 0:s
true :: true:false
false :: true:false

Rewrite Strategy: INNERMOST
----------------------------------------

(9) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
none

(c) The following functions are completely defined:

   prod_2
   zero_1
   fact_1
   p_1
   add_2
   if_3

Due to the following rules being added:

   p(v0) -> 0 [0]

And the following fresh constants: none

----------------------------------------

(10)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   fact(X) -> if(zero(X), s(0), prod(X, fact(p(X)))) [1]
   add(0, X) -> X [1]
   add(s(X), Y) -> s(add(X, Y)) [1]
   prod(0, X) -> 0 [1]
   prod(s(X), Y) -> add(Y, prod(X, Y)) [1]
   if(true, X, Y) -> X [1]
   if(false, X, Y) -> Y [1]
   zero(0) -> true [1]
   zero(s(X)) -> false [1]
   p(s(X)) -> X [1]
   p(v0) -> 0 [0]

The TRS has the following type information:
fact :: 0:s -> 0:s
if :: true:false -> 0:s -> 0:s -> 0:s
zero :: 0:s -> true:false
s :: 0:s -> 0:s
0 :: 0:s
prod :: 0:s -> 0:s -> 0:s
p :: 0:s -> 0:s
add :: 0:s -> 0:s -> 0:s
true :: true:false
false :: true:false

Rewrite Strategy: INNERMOST
----------------------------------------

(11) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(12)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   fact(0) -> if(true, s(0), prod(0, fact(0))) [2]
   fact(s(X')) -> if(false, s(0), prod(s(X'), fact(X'))) [3]
   fact(s(X')) -> if(false, s(0), prod(s(X'), fact(0))) [2]
   add(0, X) -> X [1]
   add(s(X), Y) -> s(add(X, Y)) [1]
   prod(0, X) -> 0 [1]
   prod(s(0), Y) -> add(Y, 0) [2]
   prod(s(s(X'')), Y) -> add(Y, add(Y, prod(X'', Y))) [2]
   if(true, X, Y) -> X [1]
   if(false, X, Y) -> Y [1]
   zero(0) -> true [1]
   zero(s(X)) -> false [1]
   p(s(X)) -> X [1]
   p(v0) -> 0 [0]

The TRS has the following type information:
fact :: 0:s -> 0:s
if :: true:false -> 0:s -> 0:s -> 0:s
zero :: 0:s -> true:false
s :: 0:s -> 0:s
0 :: 0:s
prod :: 0:s -> 0:s -> 0:s
p :: 0:s -> 0:s
add :: 0:s -> 0:s -> 0:s
true :: true:false
false :: true:false

Rewrite Strategy: INNERMOST
----------------------------------------

(13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   0 => 0
   true => 1
   false => 0

----------------------------------------

(14)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> X :|: z' = X, X >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + X', fact(X'))) :|: X' >= 0, z = 1 + X'
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + X', fact(0))) :|: X' >= 0, z = 1 + X'
   if(z, z', z'') -{ 1 }-> X :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
   if(z, z', z'') -{ 1 }-> Y :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0
   p(z) -{ 1 }-> X :|: z = 1 + X, X >= 0
   p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   prod(z, z') -{ 2 }-> add(Y, add(Y, prod(X'', Y))) :|: z' = Y, Y >= 0, z = 1 + (1 + X''), X'' >= 0
   prod(z, z') -{ 2 }-> add(Y, 0) :|: z' = Y, Y >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' = X, X >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z = 1 + X, X >= 0


----------------------------------------

(15) InliningProof (UPPER BOUND(ID))
Inlined the following terminating rules on right-hand sides where appropriate:

   if(z, z', z'') -{ 1 }-> X :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
   if(z, z', z'') -{ 1 }-> Y :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0

----------------------------------------

(16)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> X :|: z' = X, X >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + X', fact(X'))) :|: X' >= 0, z = 1 + X'
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + X', fact(0))) :|: X' >= 0, z = 1 + X'
   if(z, z', z'') -{ 1 }-> X :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
   if(z, z', z'') -{ 1 }-> Y :|: z' = X, Y >= 0, z'' = Y, X >= 0, z = 0
   p(z) -{ 1 }-> X :|: z = 1 + X, X >= 0
   p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   prod(z, z') -{ 2 }-> add(Y, add(Y, prod(X'', Y))) :|: z' = Y, Y >= 0, z = 1 + (1 + X''), X'' >= 0
   prod(z, z') -{ 2 }-> add(Y, 0) :|: z' = Y, Y >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' = X, X >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z = 1 + X, X >= 0


----------------------------------------

(17) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(18)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0


----------------------------------------

(19) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { if }
   { add }
   { zero }
   { p }
   { prod }
   { fact }

----------------------------------------

(20)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {if}, {add}, {zero}, {p}, {prod}, {fact}

----------------------------------------

(21) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(22)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {if}, {add}, {zero}, {p}, {prod}, {fact}

----------------------------------------

(23) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z' + z''

----------------------------------------

(24)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {if}, {add}, {zero}, {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: ?, size: O(n^1) [z' + z'']

----------------------------------------

(25) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

----------------------------------------

(26)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {add}, {zero}, {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']

----------------------------------------

(27) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(28)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {add}, {zero}, {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']

----------------------------------------

(29) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z + z'

----------------------------------------

(30)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {add}, {zero}, {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: ?, size: O(n^1) [z + z']

----------------------------------------

(31) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z

----------------------------------------

(32)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 }-> 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 2 }-> add(z', 0) :|: z' >= 0, z = 1 + 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {zero}, {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']

----------------------------------------

(33) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(34)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {zero}, {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']

----------------------------------------

(35) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: zero
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

----------------------------------------

(36)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {zero}, {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: ?, size: O(1) [1]

----------------------------------------

(37) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: zero
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

----------------------------------------

(38)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]

----------------------------------------

(39) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(40)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]

----------------------------------------

(41) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: p
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(42)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {p}, {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: ?, size: O(n^1) [z]

----------------------------------------

(43) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: p
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

----------------------------------------

(44)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: O(1) [1], size: O(n^1) [z]

----------------------------------------

(45) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(46)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: O(1) [1], size: O(n^1) [z]

----------------------------------------

(47) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: prod
after applying outer abstraction to obtain an ITS,
resulting in: O(n^2) with polynomial bound: 2*z*z' + z'

----------------------------------------

(48)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {prod}, {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: O(1) [1], size: O(n^1) [z]
  prod: runtime: ?, size: O(n^2) [2*z*z' + z']

----------------------------------------

(49) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: prod
after applying outer abstraction to obtain an ITS,
resulting in: O(n^2) with polynomial bound: 4 + 4*z + 2*z*z' + z'

----------------------------------------

(50)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 2 }-> add(z', add(z', prod(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: O(1) [1], size: O(n^1) [z]
  prod: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z']

----------------------------------------

(51) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(52)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s2 :|: s'' >= 0, s'' <= z' + 2 * (z' * (z - 2)), s1 >= 0, s1 <= z' + s'', s2 >= 0, s2 <= z' + s1, z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: O(1) [1], size: O(n^1) [z]
  prod: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z']

----------------------------------------

(53) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: fact
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

----------------------------------------

(54)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s2 :|: s'' >= 0, s'' <= z' + 2 * (z' * (z - 2)), s1 >= 0, s1 <= z' + s'', s2 >= 0, s2 <= z' + s1, z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: O(1) [1], size: O(n^1) [z]
  prod: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z']
  fact: runtime: ?, size: O(1) [0]

----------------------------------------

(55) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: fact
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

----------------------------------------

(56)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0
   add(z, z') -{ 1 + z }-> 1 + s :|: s >= 0, s <= z - 1 + z', z' >= 0, z - 1 >= 0
   fact(z) -{ 2 }-> if(1, 1 + 0, prod(0, fact(0))) :|: z = 0
   fact(z) -{ 2 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(0))) :|: z - 1 >= 0
   fact(z) -{ 3 }-> if(0, 1 + 0, prod(1 + (z - 1), fact(z - 1))) :|: z - 1 >= 0
   if(z, z', z'') -{ 1 }-> z' :|: z'' >= 0, z = 1, z' >= 0
   if(z, z', z'') -{ 1 }-> z'' :|: z'' >= 0, z' >= 0, z = 0
   p(z) -{ 0 }-> 0 :|: z >= 0
   p(z) -{ 1 }-> z - 1 :|: z - 1 >= 0
   prod(z, z') -{ 3 + z' }-> s' :|: s' >= 0, s' <= z' + 0, z' >= 0, z = 1 + 0
   prod(z, z') -{ 4*z + 2*z*z' + -1*z' }-> s2 :|: s'' >= 0, s'' <= z' + 2 * (z' * (z - 2)), s1 >= 0, s1 <= z' + s'', s2 >= 0, s2 <= z' + s1, z' >= 0, z - 2 >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0
   zero(z) -{ 1 }-> 1 :|: z = 0
   zero(z) -{ 1 }-> 0 :|: z - 1 >= 0

Function symbols to be analyzed: {fact}
Previous analysis results are:
  if: runtime: O(1) [1], size: O(n^1) [z' + z'']
  add: runtime: O(n^1) [1 + z], size: O(n^1) [z + z']
  zero: runtime: O(1) [1], size: O(1) [1]
  p: runtime: O(1) [1], size: O(n^1) [z]
  prod: runtime: O(n^2) [4 + 4*z + 2*z*z' + z'], size: O(n^2) [2*z*z' + z']
  fact: runtime: INF, size: O(1) [0]

----------------------------------------

(57) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   p(v0) -> null_p [0]
   add(v0, v1) -> null_add [0]
   prod(v0, v1) -> null_prod [0]
   zero(v0) -> null_zero [0]
   if(v0, v1, v2) -> null_if [0]

And the following fresh constants:    null_p, null_add, null_prod, null_zero, null_if

----------------------------------------

(58)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   fact(X) -> if(zero(X), s(0), prod(X, fact(p(X)))) [1]
   add(0, X) -> X [1]
   add(s(X), Y) -> s(add(X, Y)) [1]
   prod(0, X) -> 0 [1]
   prod(s(X), Y) -> add(Y, prod(X, Y)) [1]
   if(true, X, Y) -> X [1]
   if(false, X, Y) -> Y [1]
   zero(0) -> true [1]
   zero(s(X)) -> false [1]
   p(s(X)) -> X [1]
   p(v0) -> null_p [0]
   add(v0, v1) -> null_add [0]
   prod(v0, v1) -> null_prod [0]
   zero(v0) -> null_zero [0]
   if(v0, v1, v2) -> null_if [0]

The TRS has the following type information:
fact :: 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if
if :: true:false:null_zero -> 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if
zero :: 0:s:null_p:null_add:null_prod:null_if -> true:false:null_zero
s :: 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if
0 :: 0:s:null_p:null_add:null_prod:null_if
prod :: 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if
p :: 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if
add :: 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if -> 0:s:null_p:null_add:null_prod:null_if
true :: true:false:null_zero
false :: true:false:null_zero
null_p :: 0:s:null_p:null_add:null_prod:null_if
null_add :: 0:s:null_p:null_add:null_prod:null_if
null_prod :: 0:s:null_p:null_add:null_prod:null_if
null_zero :: true:false:null_zero
null_if :: 0:s:null_p:null_add:null_prod:null_if

Rewrite Strategy: INNERMOST
----------------------------------------

(59) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   0 => 0
   true => 2
   false => 1
   null_p => 0
   null_add => 0
   null_prod => 0
   null_zero => 0
   null_if => 0

----------------------------------------

(60)
Obligation:
Complexity RNTS consisting of the following rules:

   add(z, z') -{ 1 }-> X :|: z' = X, X >= 0, z = 0
   add(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   add(z, z') -{ 1 }-> 1 + add(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
   fact(z) -{ 1 }-> if(zero(X), 1 + 0, prod(X, fact(p(X)))) :|: X >= 0, z = X
   if(z, z', z'') -{ 1 }-> X :|: z = 2, z' = X, Y >= 0, z'' = Y, X >= 0
   if(z, z', z'') -{ 1 }-> Y :|: z' = X, Y >= 0, z = 1, z'' = Y, X >= 0
   if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   p(z) -{ 1 }-> X :|: z = 1 + X, X >= 0
   p(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   prod(z, z') -{ 1 }-> add(Y, prod(X, Y)) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
   prod(z, z') -{ 1 }-> 0 :|: z' = X, X >= 0, z = 0
   prod(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   zero(z) -{ 1 }-> 2 :|: z = 0
   zero(z) -{ 1 }-> 1 :|: z = 1 + X, X >= 0
   zero(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

----------------------------------------

(61) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(62)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   FACT(z0) -> c(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), ZERO(z0))
   FACT(z0) -> c1(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
   ADD(0, z0) -> c2
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(0, z0) -> c4
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ZERO(0) -> c8
   ZERO(s(z0)) -> c9
   P(s(z0)) -> c10
S tuples:
   FACT(z0) -> c(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), ZERO(z0))
   FACT(z0) -> c1(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
   ADD(0, z0) -> c2
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(0, z0) -> c4
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ZERO(0) -> c8
   ZERO(s(z0)) -> c9
   P(s(z0)) -> c10
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   FACT_1, ADD_2, PROD_2, IF_3, ZERO_1, P_1

Compound Symbols:   c_2, c1_4, c2, c3_1, c4, c5_2, c6, c7, c8, c9, c10


----------------------------------------

(63) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing nodes:
   ZERO(0) -> c8
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ADD(0, z0) -> c2
   FACT(z0) -> c(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), ZERO(z0))
   PROD(0, z0) -> c4
   P(s(z0)) -> c10
   ZERO(s(z0)) -> c9

----------------------------------------

(64)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   FACT(z0) -> c1(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
S tuples:
   FACT(z0) -> c1(IF(zero(z0), s(0), prod(z0, fact(p(z0)))), PROD(z0, fact(p(z0))), FACT(p(z0)), P(z0))
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   FACT_1, ADD_2, PROD_2

Compound Symbols:   c1_4, c3_1, c5_2


----------------------------------------

(65) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing tuple parts
----------------------------------------

(66)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(z0) -> c1(PROD(z0, fact(p(z0))), FACT(p(z0)))
S tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(z0) -> c1(PROD(z0, fact(p(z0))), FACT(p(z0)))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   ADD_2, PROD_2, FACT_1

Compound Symbols:   c3_1, c5_2, c1_2


----------------------------------------

(67) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace FACT(z0) -> c1(PROD(z0, fact(p(z0))), FACT(p(z0))) by 
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), fact(p(p(x0)))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), fact(z0)), FACT(p(s(z0))))

----------------------------------------

(68)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), fact(p(p(x0)))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), fact(z0)), FACT(p(s(z0))))
S tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), fact(p(p(x0)))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), fact(z0)), FACT(p(s(z0))))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   ADD_2, PROD_2, FACT_1

Compound Symbols:   c3_1, c5_2, c1_2


----------------------------------------

(69) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), fact(p(p(x0)))))), FACT(p(x0))) by 
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))

----------------------------------------

(70)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), fact(z0)), FACT(p(s(z0))))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
S tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), fact(z0)), FACT(p(s(z0))))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   ADD_2, PROD_2, FACT_1

Compound Symbols:   c3_1, c5_2, c1_2, c1_1


----------------------------------------

(71) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace FACT(s(z0)) -> c1(PROD(s(z0), fact(z0)), FACT(p(s(z0)))) by 
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))

----------------------------------------

(72)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
S tuples:
   ADD(s(z0), z1) -> c3(ADD(z0, z1))
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   ADD_2, PROD_2, FACT_1

Compound Symbols:   c3_1, c5_2, c1_2, c1_1


----------------------------------------

(73) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ADD(s(z0), z1) -> c3(ADD(z0, z1)) by 
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))

----------------------------------------

(74)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_2, c1_1, c3_1


----------------------------------------

(75) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(x0) -> c1(PROD(x0, if(zero(p(x0)), s(0), prod(p(x0), if(zero(p(p(x0))), s(0), prod(p(p(x0)), fact(p(p(p(x0))))))))), FACT(p(x0))) by FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
----------------------------------------

(76)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_2, c1_1, c3_1


----------------------------------------

(77) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(p(s(z0)))) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
----------------------------------------

(78)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
K tuples:none
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_2, c1_1, c3_1


----------------------------------------

(79) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
We considered the (Usable) Rules:
   p(s(z0)) -> z0
And the Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [1]
   POL(ADD(x_1, x_2)) = 0
   POL(FACT(x_1)) = x_1
   POL(PROD(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_1 + x_2
   POL(c1(x_1)) = x_1
   POL(c1(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c5(x_1, x_2)) = x_1 + x_2
   POL(fact(x_1)) = [1]
   POL(false) = [1]
   POL(if(x_1, x_2, x_3)) = [1] + x_2
   POL(p(x_1)) = x_1
   POL(prod(x_1, x_2)) = [1]
   POL(s(x_1)) = [1] + x_1
   POL(true) = [1]
   POL(zero(x_1)) = [1]

----------------------------------------

(80)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_2, c1_1, c3_1


----------------------------------------

(81) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(p(s(z0)))) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
----------------------------------------

(82)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_2, c1_1, c3_1


----------------------------------------

(83) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
We considered the (Usable) Rules:
   p(s(z0)) -> z0
And the Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [1]
   POL(ADD(x_1, x_2)) = 0
   POL(FACT(x_1)) = x_1
   POL(PROD(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_1 + x_2
   POL(c1(x_1)) = x_1
   POL(c1(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c5(x_1, x_2)) = x_1 + x_2
   POL(fact(x_1)) = [1] + x_1
   POL(false) = 0
   POL(if(x_1, x_2, x_3)) = x_1 + x_3
   POL(p(x_1)) = x_1
   POL(prod(x_1, x_2)) = x_2
   POL(s(x_1)) = [1] + x_1
   POL(true) = 0
   POL(zero(x_1)) = 0

----------------------------------------

(84)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0))))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_2, c1_1, c3_1


----------------------------------------

(85) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(p(s(z0)))) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
----------------------------------------

(86)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c1_2, c3_1


----------------------------------------

(87) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
We considered the (Usable) Rules:
   p(s(z0)) -> z0
And the Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [1]
   POL(ADD(x_1, x_2)) = 0
   POL(FACT(x_1)) = x_1
   POL(PROD(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_1 + x_2
   POL(c1(x_1)) = x_1
   POL(c1(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c5(x_1, x_2)) = x_1 + x_2
   POL(fact(x_1)) = [1] + x_1
   POL(false) = 0
   POL(if(x_1, x_2, x_3)) = x_1 + x_3
   POL(p(x_1)) = x_1
   POL(prod(x_1, x_2)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1
   POL(true) = 0
   POL(zero(x_1)) = 0

----------------------------------------

(88)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0))))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c1_2, c3_1


----------------------------------------

(89) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(p(s(z0)))) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
----------------------------------------

(90)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(91) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
We considered the (Usable) Rules:
   p(s(z0)) -> z0
And the Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(ADD(x_1, x_2)) = 0
   POL(FACT(x_1)) = x_1
   POL(PROD(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_1 + x_2
   POL(c1(x_1)) = x_1
   POL(c1(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c5(x_1, x_2)) = x_1 + x_2
   POL(fact(x_1)) = [1] + x_1
   POL(false) = [1]
   POL(if(x_1, x_2, x_3)) = x_1 + x_2
   POL(p(x_1)) = x_1
   POL(prod(x_1, x_2)) = [1] + x_1 + x_2
   POL(s(x_1)) = [1] + x_1
   POL(true) = 0
   POL(zero(x_1)) = x_1

----------------------------------------

(92)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(x0)) -> c1(FACT(p(s(x0))))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(93) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(x0)) -> c1(FACT(p(s(x0)))) by FACT(s(z0)) -> c1(FACT(z0))
----------------------------------------

(94)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(FACT(z0))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(95) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   FACT(s(z0)) -> c1(FACT(z0))
We considered the (Usable) Rules:
   p(s(z0)) -> z0
And the Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [1]
   POL(ADD(x_1, x_2)) = 0
   POL(FACT(x_1)) = x_1
   POL(PROD(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_1 + x_2
   POL(c1(x_1)) = x_1
   POL(c1(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c5(x_1, x_2)) = x_1 + x_2
   POL(fact(x_1)) = [1] + x_1
   POL(false) = 0
   POL(if(x_1, x_2, x_3)) = x_1 + x_3
   POL(p(x_1)) = x_1
   POL(prod(x_1, x_2)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1
   POL(true) = 0
   POL(zero(x_1)) = 0

----------------------------------------

(96)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(97) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), fact(p(p(p(p(z0)))))))))))), FACT(p(z0))) by FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
----------------------------------------

(98)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(99) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0)) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
----------------------------------------

(100)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(101) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0)) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
----------------------------------------

(102)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(103) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0)) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
----------------------------------------

(104)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(105) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0)) by FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
----------------------------------------

(106)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(s(z0)) -> c1(FACT(z0))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c3_1, c1_2


----------------------------------------

(107) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ADD(s(s(y0)), z1) -> c3(ADD(s(y0), z1)) by 
   ADD(s(s(s(y0))), z1) -> c3(ADD(s(s(y0)), z1))

----------------------------------------

(108)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   fact(z0) -> if(zero(z0), s(0), prod(z0, fact(p(z0))))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   prod(0, z0) -> 0
   prod(s(z0), z1) -> add(z1, prod(z0, z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   zero(0) -> true
   zero(s(z0)) -> false
   p(s(z0)) -> z0
Tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(s(z0)) -> c1(FACT(z0))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), if(zero(p(p(s(z0)))), s(0), prod(p(p(s(z0))), fact(p(p(p(s(z0)))))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, if(zero(p(z0)), s(0), prod(p(z0), fact(p(p(z0)))))))), FACT(z0))
   ADD(s(s(s(y0))), z1) -> c3(ADD(s(s(y0)), z1))
S tuples:
   PROD(s(z0), z1) -> c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
   FACT(x0) -> c1(FACT(p(x0)))
   FACT(z0) -> c1(PROD(z0, if(zero(p(z0)), s(0), prod(p(z0), if(zero(p(p(z0))), s(0), prod(p(p(z0)), if(zero(p(p(p(z0)))), s(0), prod(p(p(p(z0))), if(zero(p(p(p(p(z0))))), s(0), prod(p(p(p(p(z0)))), fact(p(p(p(p(p(z0))))))))))))))), FACT(p(z0)))
   ADD(s(s(s(y0))), z1) -> c3(ADD(s(s(y0)), z1))
K tuples:
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(p(s(z0)), fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(p(s(z0))), s(0), prod(z0, fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(p(s(z0)), fact(p(p(s(z0))))))), FACT(z0))
   FACT(s(z0)) -> c1(PROD(s(z0), if(zero(z0), s(0), prod(z0, fact(p(z0))))), FACT(z0))
   FACT(s(z0)) -> c1(FACT(z0))
Defined Rule Symbols:   fact_1, add_2, prod_2, if_3, zero_1, p_1

Defined Pair Symbols:   PROD_2, FACT_1, ADD_2

Compound Symbols:   c5_2, c1_1, c1_2, c3_1