MAYBE
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CpxRelTRS
    (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) typed CpxTrs
    (5) OrderProof [LOWER BOUND(ID), 0 ms]
    (6) typed CpxTrs
(7) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(8) CpxTRS
(9) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(10) TRS for Loop Detection
(11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CpxWeightedTrs
    (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxTypedWeightedTrs
    (15) CompletionProof [UPPER BOUND(ID), 0 ms]
    (16) CpxTypedWeightedCompleteTrs
        (17) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (18) CpxTypedWeightedCompleteTrs
        (19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (20) CpxRNTS
        (21) InliningProof [UPPER BOUND(ID), 328 ms]
        (22) CpxRNTS
        (23) SimplificationProof [BOTH BOUNDS(ID, ID), 3 ms]
        (24) CpxRNTS
        (25) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
        (26) CpxRNTS
        (27) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (28) CpxRNTS
        (29) IntTrsBoundProof [UPPER BOUND(ID), 182 ms]
        (30) CpxRNTS
        (31) IntTrsBoundProof [UPPER BOUND(ID), 45 ms]
        (32) CpxRNTS
        (33) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (34) CpxRNTS
        (35) IntTrsBoundProof [UPPER BOUND(ID), 85 ms]
        (36) CpxRNTS
        (37) IntTrsBoundProof [UPPER BOUND(ID), 43 ms]
        (38) CpxRNTS
        (39) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (40) CpxRNTS
        (41) IntTrsBoundProof [UPPER BOUND(ID), 98 ms]
        (42) CpxRNTS
        (43) IntTrsBoundProof [UPPER BOUND(ID), 42 ms]
        (44) CpxRNTS
        (45) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (46) CpxRNTS
        (47) IntTrsBoundProof [UPPER BOUND(ID), 149 ms]
        (48) CpxRNTS
        (49) IntTrsBoundProof [UPPER BOUND(ID), 33 ms]
        (50) CpxRNTS
        (51) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (52) CpxRNTS
        (53) IntTrsBoundProof [UPPER BOUND(ID), 108 ms]
        (54) CpxRNTS
        (55) IntTrsBoundProof [UPPER BOUND(ID), 53 ms]
        (56) CpxRNTS
        (57) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (58) CpxRNTS
        (59) IntTrsBoundProof [UPPER BOUND(ID), 119 ms]
        (60) CpxRNTS
        (61) IntTrsBoundProof [UPPER BOUND(ID), 13 ms]
        (62) CpxRNTS
        (63) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (64) CpxRNTS
        (65) IntTrsBoundProof [UPPER BOUND(ID), 3423 ms]
        (66) CpxRNTS
        (67) IntTrsBoundProof [UPPER BOUND(ID), 730 ms]
        (68) CpxRNTS
    (69) CompletionProof [UPPER BOUND(ID), 0 ms]
    (70) CpxTypedWeightedCompleteTrs
        (71) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (72) CpxRNTS
(73) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(74) CdtProblem
    (75) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (76) CdtProblem
    (77) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (78) CdtProblem
    (79) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (80) CdtProblem
    (81) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (82) CdtProblem
    (83) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (84) CdtProblem
    (85) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (86) CdtProblem
    (87) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (88) CdtProblem
    (89) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (90) CdtProblem
    (91) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (92) CdtProblem
    (93) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (94) CdtProblem
    (95) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (96) CdtProblem


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

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


The TRS R consists of the following rules:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

The (relative) TRS S consists of the following rules:

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> cons(z0, z1)
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))

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

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

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


The TRS R consists of the following rules:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

The (relative) TRS S consists of the following rules:

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> cons(z0, z1)
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))

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

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

(4)
Obligation:
Innermost TRS:
Rules:
IS_EMPTY(nil) -> c
IS_EMPTY(cons(z0, z1)) -> c1
HD(cons(z0, z1)) -> c2
TL(cons(z0, z1)) -> c3
APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
IFAPPEND(z0, z1, true) -> c5
IFAPPEND(z0, z1, false) -> c6(HD(z0))
IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))
is_empty(nil) -> true
is_empty(cons(z0, z1)) -> false
hd(cons(z0, z1)) -> z0
tl(cons(z0, z1)) -> cons(z0, z1)
append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
ifappend(z0, z1, true) -> z1
ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))

Types:
IS_EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: hd -> nil:cons -> nil:cons
c1 :: c:c1
HD :: nil:cons -> c2
c2 :: c2
TL :: nil:cons -> c3
c3 :: c3
APPEND :: nil:cons -> a -> c4
c4 :: c5:c6:c7 -> c:c1 -> c4
IFAPPEND :: nil:cons -> a -> true:false -> c5:c6:c7
is_empty :: nil:cons -> true:false
true :: true:false
c5 :: c5:c6:c7
false :: true:false
c6 :: c2 -> c5:c6:c7
c7 :: c4 -> c3 -> c5:c6:c7
tl :: nil:cons -> nil:cons
hd :: nil:cons -> hd
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> true:false -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_hd3_8 :: hd
hole_c24_8 :: c2
hole_c35_8 :: c3
hole_c46_8 :: c4
hole_a7_8 :: a
hole_c5:c6:c78_8 :: c5:c6:c7
hole_true:false9_8 :: true:false
gen_nil:cons10_8 :: Nat -> nil:cons

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

(5) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
APPEND, append
----------------------------------------

(6)
Obligation:
Innermost TRS:
Rules:
IS_EMPTY(nil) -> c
IS_EMPTY(cons(z0, z1)) -> c1
HD(cons(z0, z1)) -> c2
TL(cons(z0, z1)) -> c3
APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
IFAPPEND(z0, z1, true) -> c5
IFAPPEND(z0, z1, false) -> c6(HD(z0))
IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))
is_empty(nil) -> true
is_empty(cons(z0, z1)) -> false
hd(cons(z0, z1)) -> z0
tl(cons(z0, z1)) -> cons(z0, z1)
append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
ifappend(z0, z1, true) -> z1
ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))

Types:
IS_EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: hd -> nil:cons -> nil:cons
c1 :: c:c1
HD :: nil:cons -> c2
c2 :: c2
TL :: nil:cons -> c3
c3 :: c3
APPEND :: nil:cons -> a -> c4
c4 :: c5:c6:c7 -> c:c1 -> c4
IFAPPEND :: nil:cons -> a -> true:false -> c5:c6:c7
is_empty :: nil:cons -> true:false
true :: true:false
c5 :: c5:c6:c7
false :: true:false
c6 :: c2 -> c5:c6:c7
c7 :: c4 -> c3 -> c5:c6:c7
tl :: nil:cons -> nil:cons
hd :: nil:cons -> hd
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> true:false -> nil:cons
hole_c:c11_8 :: c:c1
hole_nil:cons2_8 :: nil:cons
hole_hd3_8 :: hd
hole_c24_8 :: c2
hole_c35_8 :: c3
hole_c46_8 :: c4
hole_a7_8 :: a
hole_c5:c6:c78_8 :: c5:c6:c7
hole_true:false9_8 :: true:false
gen_nil:cons10_8 :: Nat -> nil:cons


Generator Equations:
gen_nil:cons10_8(0) <=> nil
gen_nil:cons10_8(+(x, 1)) <=> cons(hole_hd3_8, gen_nil:cons10_8(x))


The following defined symbols remain to be analysed:
APPEND, append
----------------------------------------

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

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


The TRS R consists of the following rules:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> cons(z0, z1)
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))

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

(9) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(10)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

The (relative) TRS S consists of the following rules:

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> cons(z0, z1)
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))

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

(11) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(12)
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:

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> cons(z0, z1) [0]
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0)) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1)) [0]

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

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

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

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> cons(z0, z1) [0]
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0)) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1)) [0]

The TRS has the following type information:
IS_EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: hd -> nil:cons -> nil:cons
c1 :: c:c1
HD :: nil:cons -> c2
c2 :: c2
TL :: nil:cons -> c3
c3 :: c3
APPEND :: nil:cons -> a -> c4
c4 :: c5:c6:c7 -> c:c1 -> c4
IFAPPEND :: nil:cons -> a -> true:false -> c5:c6:c7
is_empty :: nil:cons -> true:false
true :: true:false
c5 :: c5:c6:c7
false :: true:false
c6 :: c2 -> c5:c6:c7
c7 :: c4 -> c3 -> c5:c6:c7
tl :: nil:cons -> nil:cons
hd :: nil:cons -> hd
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> true:false -> nil:cons

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

(15) 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:

   IS_EMPTY_1
   HD_1
   TL_1
   APPEND_2
   IFAPPEND_3

(c) The following functions are completely defined:

   is_empty_1
   hd_1
   tl_1
   append_2
   ifappend_3

Due to the following rules being added:

   is_empty(v0) -> null_is_empty [0]
   hd(v0) -> const [0]
   tl(v0) -> nil [0]
   append(v0, v1) -> nil [0]
   ifappend(v0, v1, v2) -> nil [0]

And the following fresh constants:    null_is_empty, const, const1, const2

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

(16)
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:

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> cons(z0, z1) [0]
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0)) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1)) [0]
   is_empty(v0) -> null_is_empty [0]
   hd(v0) -> const [0]
   tl(v0) -> nil [0]
   append(v0, v1) -> nil [0]
   ifappend(v0, v1, v2) -> nil [0]

The TRS has the following type information:
IS_EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: const -> nil:cons -> nil:cons
c1 :: c:c1
HD :: nil:cons -> c2
c2 :: c2
TL :: nil:cons -> c3
c3 :: c3
APPEND :: nil:cons -> a -> c4
c4 :: c5:c6:c7 -> c:c1 -> c4
IFAPPEND :: nil:cons -> a -> true:false:null_is_empty -> c5:c6:c7
is_empty :: nil:cons -> true:false:null_is_empty
true :: true:false:null_is_empty
c5 :: c5:c6:c7
false :: true:false:null_is_empty
c6 :: c2 -> c5:c6:c7
c7 :: c4 -> c3 -> c5:c6:c7
tl :: nil:cons -> nil:cons
hd :: nil:cons -> const
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> true:false:null_is_empty -> nil:cons
null_is_empty :: true:false:null_is_empty
const :: const
const1 :: c4
const2 :: a

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

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

(18)
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:

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(nil, z1) -> c4(IFAPPEND(nil, z1, true), IS_EMPTY(nil)) [1]
   APPEND(cons(z0', z1'), z1) -> c4(IFAPPEND(cons(z0', z1'), z1, false), IS_EMPTY(cons(z0', z1'))) [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, null_is_empty), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(cons(z0'', z1''), z1, false) -> c7(APPEND(cons(z0'', z1''), z1), TL(cons(z0'', z1''))) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(nil, z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> cons(z0, z1) [0]
   append(nil, z1) -> ifappend(nil, z1, true) [0]
   append(cons(z01, z11), z1) -> ifappend(cons(z01, z11), z1, false) [0]
   append(z0, z1) -> ifappend(z0, z1, null_is_empty) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(cons(z02, z12), z1, false) -> cons(hd(cons(z02, z12)), append(cons(z02, z12), z1)) [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(nil, z1)) [0]
   is_empty(v0) -> null_is_empty [0]
   hd(v0) -> const [0]
   tl(v0) -> nil [0]
   append(v0, v1) -> nil [0]
   ifappend(v0, v1, v2) -> nil [0]

The TRS has the following type information:
IS_EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: const -> nil:cons -> nil:cons
c1 :: c:c1
HD :: nil:cons -> c2
c2 :: c2
TL :: nil:cons -> c3
c3 :: c3
APPEND :: nil:cons -> a -> c4
c4 :: c5:c6:c7 -> c:c1 -> c4
IFAPPEND :: nil:cons -> a -> true:false:null_is_empty -> c5:c6:c7
is_empty :: nil:cons -> true:false:null_is_empty
true :: true:false:null_is_empty
c5 :: c5:c6:c7
false :: true:false:null_is_empty
c6 :: c2 -> c5:c6:c7
c7 :: c4 -> c3 -> c5:c6:c7
tl :: nil:cons -> nil:cons
hd :: nil:cons -> const
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> true:false:null_is_empty -> nil:cons
null_is_empty :: true:false:null_is_empty
const :: const
const1 :: c4
const2 :: a

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

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

   nil => 0
   c => 0
   c1 => 1
   c2 => 0
   c3 => 0
   true => 2
   c5 => 0
   false => 1
   null_is_empty => 0
   const => 0
   const1 => 0
   const2 => 0

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

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

   APPEND(z, z') -{ 1 }-> 1 + IFAPPEND(z0, z1, 0) + IS_EMPTY(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   APPEND(z, z') -{ 1 }-> 1 + IFAPPEND(0, z1, 2) + IS_EMPTY(0) :|: z1 >= 0, z' = z1, z = 0
   APPEND(z, z') -{ 1 }-> 1 + IFAPPEND(1 + z0' + z1', z1, 1) + IS_EMPTY(1 + z0' + z1') :|: z1 >= 0, z0' >= 0, z1' >= 0, z' = z1, z = 1 + z0' + z1'
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + HD(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + APPEND(0, z1) + TL(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + APPEND(1 + z0'' + z1'', z1) + TL(1 + z0'' + z1'') :|: z = 1 + z0'' + z1'', z1 >= 0, z' = z1, z0'' >= 0, z'' = 1, z1'' >= 0
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z0, z1, 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   append(z, z') -{ 0 }-> ifappend(0, z1, 2) :|: z1 >= 0, z' = z1, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z1, 1) :|: z11 >= 0, z1 >= 0, z01 >= 0, z = 1 + z01 + z11, z' = z1
   append(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   ifappend(z, z', z'') -{ 0 }-> z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + hd(z0) + append(0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + hd(1 + z02 + z12) + append(1 + z02 + z12, z1) :|: z = 1 + z02 + z12, z1 >= 0, z02 >= 0, z' = z1, z12 >= 0, z'' = 1
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   tl(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1


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

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

   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z0, z1, 0) + 1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z1' >= 0, z0' >= 0, z0 = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z0, z1, 0) + 0 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z1, 2) + 0 :|: z1 >= 0, z' = z1, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z1, 1) + 1 :|: z1 >= 0, z0' >= 0, z1' >= 0, z' = z1, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1, z1' >= 0, z0' >= 0, z0 = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z1) + 0 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1, z1' >= 0, z0' >= 0, z0 = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z1) + 0 :|: z = 1 + z0'' + z1'', z1 >= 0, z' = z1, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z0, z1, 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   append(z, z') -{ 0 }-> ifappend(0, z1, 2) :|: z1 >= 0, z' = z1, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z1, 1) :|: z11 >= 0, z1 >= 0, z01 >= 0, z = 1 + z01 + z11, z' = z1
   append(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   ifappend(z, z', z'') -{ 0 }-> z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z1) :|: z = 1 + z02 + z12, z1 >= 0, z02 >= 0, z' = z1, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1, z1' >= 0, z0' >= 0, z0 = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1, v0 >= 0, z0 = v0
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z1) :|: z = 1 + z02 + z12, z1 >= 0, z02 >= 0, z' = z1, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   tl(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1


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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1


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

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

   { is_empty }
   { HD }
   { TL }
   { tl }
   { IS_EMPTY }
   { hd }
   { IFAPPEND, APPEND }
   { ifappend, append }

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {is_empty}, {HD}, {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}

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

(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:

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {is_empty}, {HD}, {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}

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

(29) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {is_empty}, {HD}, {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: ?, size: O(1) [2]

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

(31) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {HD}, {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]

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

(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:

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {HD}, {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]

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

(35) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {HD}, {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: ?, size: O(1) [0]

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

(37) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: HD
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:

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]

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

(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:

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]

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

(41) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {TL}, {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: ?, size: O(1) [0]

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

(43) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: TL
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:

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]

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

(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:

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]

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

(47) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {tl}, {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: ?, size: O(n^1) [z]

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

(49) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [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:

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]

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

(53) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {IS_EMPTY}, {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: ?, size: O(1) [1]

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

(55) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: O(1) [1], size: O(1) [1]

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: O(1) [1], size: O(1) [1]

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

(59) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {hd}, {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: O(1) [1], size: O(1) [1]
  hd: runtime: ?, size: O(n^1) [z]

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

(61) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: O(1) [1], size: O(1) [1]
  hd: runtime: O(1) [0], size: O(n^1) [z]

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: O(1) [1], size: O(1) [1]
  hd: runtime: O(1) [0], size: O(n^1) [z]

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

(65) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: O(1) [1], size: O(1) [1]
  hd: runtime: O(1) [0], size: O(n^1) [z]
  IFAPPEND: runtime: ?, size: INF
  APPEND: runtime: ?, size: INF

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

(67) IntTrsBoundProof (UPPER BOUND(ID))

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

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

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

   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 1 :|: z' >= 0, z >= 0, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(z, z', 0) + 0 :|: z' >= 0, z >= 0, z = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(0, z', 2) + 0 :|: z' >= 0, z = 0, 0 = 0
   APPEND(z, z') -{ 2 }-> 1 + IFAPPEND(1 + z0' + z1', z', 1) + 1 :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + z0' + z1', z1'' >= 0, z0 >= 0, 1 + z0' + z1' = 1 + z0 + z1''
   HD(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z' >= 0, z >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(0, z') + 0 :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   IFAPPEND(z, z', z'') -{ 2 }-> 1 + APPEND(1 + z0'' + z1'', z') + 0 :|: z = 1 + z0'' + z1'', z' >= 0, z0'' >= 0, z'' = 1, z1'' >= 0, z1' >= 0, z0 >= 0, 1 + z0'' + z1'' = 1 + z0 + z1'
   IS_EMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 0 :|: z = 0
   TL(z) -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> ifappend(z, z', 0) :|: z' >= 0, z >= 0
   append(z, z') -{ 0 }-> ifappend(0, z', 2) :|: z' >= 0, z = 0
   append(z, z') -{ 0 }-> ifappend(1 + z01 + z11, z', 1) :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + z01 + z11
   append(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: z >= 0
   ifappend(z, z', z'') -{ 0 }-> z' :|: z' >= 0, z >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + z0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, z1' >= 0, z0 >= 0, 1 + z02 + z12 = 1 + z0 + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + z0' + append(0, z') :|: z' >= 0, z >= 0, z'' = 1, z1' >= 0, z0' >= 0, z = 1 + z0' + z1'
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(0, z') :|: z' >= 0, z >= 0, z'' = 1
   ifappend(z, z', z'') -{ 0 }-> 1 + 0 + append(1 + z02 + z12, z') :|: z = 1 + z02 + z12, z' >= 0, z02 >= 0, z12 >= 0, z'' = 1, v0 >= 0, 1 + z02 + z12 = v0
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 0 :|: z >= 0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Function symbols to be analyzed: {IFAPPEND,APPEND}, {ifappend,append}
Previous analysis results are:
  is_empty: runtime: O(1) [0], size: O(1) [2]
  HD: runtime: O(1) [1], size: O(1) [0]
  TL: runtime: O(1) [1], size: O(1) [0]
  tl: runtime: O(1) [0], size: O(n^1) [z]
  IS_EMPTY: runtime: O(1) [1], size: O(1) [1]
  hd: runtime: O(1) [0], size: O(n^1) [z]
  IFAPPEND: runtime: INF, size: INF
  APPEND: runtime: ?, size: INF

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

(69) 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:

   is_empty(v0) -> null_is_empty [0]
   hd(v0) -> null_hd [0]
   tl(v0) -> null_tl [0]
   append(v0, v1) -> null_append [0]
   ifappend(v0, v1, v2) -> null_ifappend [0]
   IS_EMPTY(v0) -> null_IS_EMPTY [0]
   HD(v0) -> null_HD [0]
   TL(v0) -> null_TL [0]
   IFAPPEND(v0, v1, v2) -> null_IFAPPEND [0]

And the following fresh constants:    null_is_empty, null_hd, null_tl, null_append, null_ifappend, null_IS_EMPTY, null_HD, null_TL, null_IFAPPEND, const, const1

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

(70)
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:

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> cons(z0, z1) [0]
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0)) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1)) [0]
   is_empty(v0) -> null_is_empty [0]
   hd(v0) -> null_hd [0]
   tl(v0) -> null_tl [0]
   append(v0, v1) -> null_append [0]
   ifappend(v0, v1, v2) -> null_ifappend [0]
   IS_EMPTY(v0) -> null_IS_EMPTY [0]
   HD(v0) -> null_HD [0]
   TL(v0) -> null_TL [0]
   IFAPPEND(v0, v1, v2) -> null_IFAPPEND [0]

The TRS has the following type information:
IS_EMPTY :: nil:cons:null_tl:null_append:null_ifappend -> c:c1:null_IS_EMPTY
nil :: nil:cons:null_tl:null_append:null_ifappend
c :: c:c1:null_IS_EMPTY
cons :: null_hd -> nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend
c1 :: c:c1:null_IS_EMPTY
HD :: nil:cons:null_tl:null_append:null_ifappend -> c2:null_HD
c2 :: c2:null_HD
TL :: nil:cons:null_tl:null_append:null_ifappend -> c3:null_TL
c3 :: c3:null_TL
APPEND :: nil:cons:null_tl:null_append:null_ifappend -> a -> c4
c4 :: c5:c6:c7:null_IFAPPEND -> c:c1:null_IS_EMPTY -> c4
IFAPPEND :: nil:cons:null_tl:null_append:null_ifappend -> a -> true:false:null_is_empty -> c5:c6:c7:null_IFAPPEND
is_empty :: nil:cons:null_tl:null_append:null_ifappend -> true:false:null_is_empty
true :: true:false:null_is_empty
c5 :: c5:c6:c7:null_IFAPPEND
false :: true:false:null_is_empty
c6 :: c2:null_HD -> c5:c6:c7:null_IFAPPEND
c7 :: c4 -> c3:null_TL -> c5:c6:c7:null_IFAPPEND
tl :: nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend
hd :: nil:cons:null_tl:null_append:null_ifappend -> null_hd
append :: nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend
ifappend :: nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend -> true:false:null_is_empty -> nil:cons:null_tl:null_append:null_ifappend
null_is_empty :: true:false:null_is_empty
null_hd :: null_hd
null_tl :: nil:cons:null_tl:null_append:null_ifappend
null_append :: nil:cons:null_tl:null_append:null_ifappend
null_ifappend :: nil:cons:null_tl:null_append:null_ifappend
null_IS_EMPTY :: c:c1:null_IS_EMPTY
null_HD :: c2:null_HD
null_TL :: c3:null_TL
null_IFAPPEND :: c5:c6:c7:null_IFAPPEND
const :: c4
const1 :: a

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

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

   nil => 0
   c => 1
   c1 => 2
   c2 => 1
   c3 => 1
   true => 2
   c5 => 0
   false => 1
   null_is_empty => 0
   null_hd => 0
   null_tl => 0
   null_append => 0
   null_ifappend => 0
   null_IS_EMPTY => 0
   null_HD => 0
   null_TL => 0
   null_IFAPPEND => 0
   const => 0
   const1 => 0

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

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

   APPEND(z, z') -{ 1 }-> 1 + IFAPPEND(z0, z1, is_empty(z0)) + IS_EMPTY(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   HD(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   HD(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + HD(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + APPEND(tl(z0), z1) + TL(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   IS_EMPTY(z) -{ 1 }-> 2 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 1 :|: z = 0
   IS_EMPTY(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   TL(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   TL(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   append(z, z') -{ 0 }-> ifappend(z0, z1, is_empty(z0)) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   append(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   ifappend(z, z', z'') -{ 0 }-> z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + hd(z0) + append(tl(z0), z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   tl(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   tl(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

Only complete derivations are relevant for the runtime complexity.

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

(73) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(74)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> cons(z0, z1)
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))
   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))
Tuples:
   IS_EMPTY'(nil) -> c8
   IS_EMPTY'(cons(z0, z1)) -> c9
   HD'(cons(z0, z1)) -> c10
   TL'(cons(z0, z1)) -> c11
   APPEND'(z0, z1) -> c12(IFAPPEND'(z0, z1, is_empty(z0)), IS_EMPTY'(z0))
   IFAPPEND'(z0, z1, true) -> c13
   IFAPPEND'(z0, z1, false) -> c14(HD'(z0), APPEND'(tl(z0), z1), TL'(z0))
   IS_EMPTY''(nil) -> c15
   IS_EMPTY''(cons(z0, z1)) -> c16
   HD''(cons(z0, z1)) -> c17
   TL''(cons(z0, z1)) -> c18
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)), IS_EMPTY'(z0), IS_EMPTY''(z0))
   IFAPPEND''(z0, z1, true) -> c20
   IFAPPEND''(z0, z1, false) -> c21(HD''(z0))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1), TL'(z0), TL''(z0))
S tuples:
   IS_EMPTY''(nil) -> c15
   IS_EMPTY''(cons(z0, z1)) -> c16
   HD''(cons(z0, z1)) -> c17
   TL''(cons(z0, z1)) -> c18
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)), IS_EMPTY'(z0), IS_EMPTY''(z0))
   IFAPPEND''(z0, z1, true) -> c20
   IFAPPEND''(z0, z1, false) -> c21(HD''(z0))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1), TL'(z0), TL''(z0))
K tuples:none
Defined Rule Symbols:   IS_EMPTY_1, HD_1, TL_1, APPEND_2, IFAPPEND_3, is_empty_1, hd_1, tl_1, append_2, ifappend_3

Defined Pair Symbols:   IS_EMPTY'_1, HD'_1, TL'_1, APPEND'_2, IFAPPEND'_3, IS_EMPTY''_1, HD''_1, TL''_1, APPEND''_2, IFAPPEND''_3

Compound Symbols:   c8, c9, c10, c11, c12_2, c13, c14_3, c15, c16, c17, c18, c19_3, c20, c21_1, c22_3


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

(75) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 11 trailing nodes:
   TL''(cons(z0, z1)) -> c18
   IS_EMPTY'(cons(z0, z1)) -> c9
   IFAPPEND''(z0, z1, true) -> c20
   IS_EMPTY''(cons(z0, z1)) -> c16
   IS_EMPTY'(nil) -> c8
   HD''(cons(z0, z1)) -> c17
   IFAPPEND''(z0, z1, false) -> c21(HD''(z0))
   IFAPPEND'(z0, z1, true) -> c13
   HD'(cons(z0, z1)) -> c10
   TL'(cons(z0, z1)) -> c11
   IS_EMPTY''(nil) -> c15

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

(76)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> cons(z0, z1)
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))
   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))
Tuples:
   APPEND'(z0, z1) -> c12(IFAPPEND'(z0, z1, is_empty(z0)), IS_EMPTY'(z0))
   IFAPPEND'(z0, z1, false) -> c14(HD'(z0), APPEND'(tl(z0), z1), TL'(z0))
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)), IS_EMPTY'(z0), IS_EMPTY''(z0))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1), TL'(z0), TL''(z0))
S tuples:
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)), IS_EMPTY'(z0), IS_EMPTY''(z0))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1), TL'(z0), TL''(z0))
K tuples:none
Defined Rule Symbols:   IS_EMPTY_1, HD_1, TL_1, APPEND_2, IFAPPEND_3, is_empty_1, hd_1, tl_1, append_2, ifappend_3

Defined Pair Symbols:   APPEND'_2, IFAPPEND'_3, APPEND''_2, IFAPPEND''_3

Compound Symbols:   c12_2, c14_3, c19_3, c22_3


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

(77) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 7 trailing tuple parts
----------------------------------------

(78)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> cons(z0, z1)
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))
   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))
Tuples:
   APPEND'(z0, z1) -> c12(IFAPPEND'(z0, z1, is_empty(z0)))
   IFAPPEND'(z0, z1, false) -> c14(APPEND'(tl(z0), z1))
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
S tuples:
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
K tuples:none
Defined Rule Symbols:   IS_EMPTY_1, HD_1, TL_1, APPEND_2, IFAPPEND_3, is_empty_1, hd_1, tl_1, append_2, ifappend_3

Defined Pair Symbols:   APPEND'_2, IFAPPEND'_3, APPEND''_2, IFAPPEND''_3

Compound Symbols:   c12_1, c14_1, c19_1, c22_1


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

(79) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   hd(cons(z0, z1)) -> z0
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))
   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

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

(80)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   APPEND'(z0, z1) -> c12(IFAPPEND'(z0, z1, is_empty(z0)))
   IFAPPEND'(z0, z1, false) -> c14(APPEND'(tl(z0), z1))
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
S tuples:
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
K tuples:none
Defined Rule Symbols:   is_empty_1, tl_1

Defined Pair Symbols:   APPEND'_2, IFAPPEND'_3, APPEND''_2, IFAPPEND''_3

Compound Symbols:   c12_1, c14_1, c19_1, c22_1


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

(81) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace APPEND'(z0, z1) -> c12(IFAPPEND'(z0, z1, is_empty(z0))) by 
   APPEND'(nil, x1) -> c12(IFAPPEND'(nil, x1, true))
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))

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

(82)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   IFAPPEND'(z0, z1, false) -> c14(APPEND'(tl(z0), z1))
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND'(nil, x1) -> c12(IFAPPEND'(nil, x1, true))
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
S tuples:
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
K tuples:none
Defined Rule Symbols:   is_empty_1, tl_1

Defined Pair Symbols:   IFAPPEND'_3, APPEND''_2, IFAPPEND''_3, APPEND'_2

Compound Symbols:   c14_1, c19_1, c22_1, c12_1


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

(83) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   APPEND'(nil, x1) -> c12(IFAPPEND'(nil, x1, true))

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

(84)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   IFAPPEND'(z0, z1, false) -> c14(APPEND'(tl(z0), z1))
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
S tuples:
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
K tuples:none
Defined Rule Symbols:   is_empty_1, tl_1

Defined Pair Symbols:   IFAPPEND'_3, APPEND''_2, IFAPPEND''_3, APPEND'_2

Compound Symbols:   c14_1, c19_1, c22_1, c12_1


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

(85) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IFAPPEND'(z0, z1, false) -> c14(APPEND'(tl(z0), z1)) by 
   IFAPPEND'(cons(z0, z1), x1, false) -> c14(APPEND'(cons(z0, z1), x1))

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

(86)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
   IFAPPEND'(cons(z0, z1), x1, false) -> c14(APPEND'(cons(z0, z1), x1))
S tuples:
   APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0)))
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
K tuples:none
Defined Rule Symbols:   is_empty_1, tl_1

Defined Pair Symbols:   APPEND''_2, IFAPPEND''_3, APPEND'_2, IFAPPEND'_3

Compound Symbols:   c19_1, c22_1, c12_1, c14_1


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

(87) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace APPEND''(z0, z1) -> c19(IFAPPEND''(z0, z1, is_empty(z0))) by 
   APPEND''(nil, x1) -> c19(IFAPPEND''(nil, x1, true))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))

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

(88)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
   IFAPPEND'(cons(z0, z1), x1, false) -> c14(APPEND'(cons(z0, z1), x1))
   APPEND''(nil, x1) -> c19(IFAPPEND''(nil, x1, true))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
S tuples:
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND''(nil, x1) -> c19(IFAPPEND''(nil, x1, true))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
K tuples:none
Defined Rule Symbols:   is_empty_1, tl_1

Defined Pair Symbols:   IFAPPEND''_3, APPEND'_2, IFAPPEND'_3, APPEND''_2

Compound Symbols:   c22_1, c12_1, c14_1, c19_1


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

(89) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   APPEND''(nil, x1) -> c19(IFAPPEND''(nil, x1, true))

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

(90)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
   IFAPPEND'(cons(z0, z1), x1, false) -> c14(APPEND'(cons(z0, z1), x1))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
S tuples:
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
K tuples:none
Defined Rule Symbols:   is_empty_1, tl_1

Defined Pair Symbols:   IFAPPEND''_3, APPEND'_2, IFAPPEND'_3, APPEND''_2

Compound Symbols:   c22_1, c12_1, c14_1, c19_1


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

(91) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false

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

(92)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
   IFAPPEND'(cons(z0, z1), x1, false) -> c14(APPEND'(cons(z0, z1), x1))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
S tuples:
   IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
K tuples:none
Defined Rule Symbols:   tl_1

Defined Pair Symbols:   IFAPPEND''_3, APPEND'_2, IFAPPEND'_3, APPEND''_2

Compound Symbols:   c22_1, c12_1, c14_1, c19_1


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

(93) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace IFAPPEND''(z0, z1, false) -> c22(APPEND''(tl(z0), z1)) by 
   IFAPPEND''(cons(z0, z1), x1, false) -> c22(APPEND''(cons(z0, z1), x1))

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

(94)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   tl(cons(z0, z1)) -> cons(z0, z1)
Tuples:
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
   IFAPPEND'(cons(z0, z1), x1, false) -> c14(APPEND'(cons(z0, z1), x1))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
   IFAPPEND''(cons(z0, z1), x1, false) -> c22(APPEND''(cons(z0, z1), x1))
S tuples:
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
   IFAPPEND''(cons(z0, z1), x1, false) -> c22(APPEND''(cons(z0, z1), x1))
K tuples:none
Defined Rule Symbols:   tl_1

Defined Pair Symbols:   APPEND'_2, IFAPPEND'_3, APPEND''_2, IFAPPEND''_3

Compound Symbols:   c12_1, c14_1, c19_1, c22_1


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

(95) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   tl(cons(z0, z1)) -> cons(z0, z1)

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

(96)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   APPEND'(cons(z0, z1), x1) -> c12(IFAPPEND'(cons(z0, z1), x1, false))
   IFAPPEND'(cons(z0, z1), x1, false) -> c14(APPEND'(cons(z0, z1), x1))
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
   IFAPPEND''(cons(z0, z1), x1, false) -> c22(APPEND''(cons(z0, z1), x1))
S tuples:
   APPEND''(cons(z0, z1), x1) -> c19(IFAPPEND''(cons(z0, z1), x1, false))
   IFAPPEND''(cons(z0, z1), x1, false) -> c22(APPEND''(cons(z0, z1), x1))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   APPEND'_2, IFAPPEND'_3, APPEND''_2, IFAPPEND''_3

Compound Symbols:   c12_1, c14_1, c19_1, c22_1