(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](cs, ncs, node, colorednodes, Cons(x, xs), colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
colorof(S(y91_3), Cons(CN(cl, N(0, adjs)), xs)) →+ colorof(S(y91_3), xs)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(CN(cl, N(0, adjs)), xs)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](cs, ncs, node, colorednodes, Cons(x, xs), colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)
Rewrite Strategy: INNERMOST
(5) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
colorednoderest[Ite][True][Ite][True][Let]/0
colorednoderest[Ite][True][Ite][True][Let]/1
colorednoderest[Ite][True][Ite][True][Let]/2
colorednoderest[Ite][True][Ite][True][Let]/3
colorednoderest[Ite][True][Ite][True][Let]/4
(6) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)
Rewrite Strategy: INNERMOST
(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(8) Obligation:
Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
(9) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
colorof,
!EQ,
eqColorList,
revapp,
possible,
colorrest,
colorednoderest,
colornodeThey will be analysed ascendingly in the following order:
!EQ < colorof
colorof < possible
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
(10) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
!EQ, colorof, eqColorList, revapp, possible, colorrest, colorednoderest, colornode
They will be analysed ascendingly in the following order:
!EQ < colorof
colorof < possible
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol !EQ.
(12) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
colorof, eqColorList, revapp, possible, colorrest, colorednoderest, colornode
They will be analysed ascendingly in the following order:
colorof < possible
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol colorof.
(14) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
eqColorList, revapp, possible, colorrest, colorednoderest, colornode
They will be analysed ascendingly in the following order:
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
eqColorList(
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(
+(
1,
n41_0)),
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(
n41_0)) →
False, rt ∈ Ω(1 + n41
0)
Induction Base:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, 0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →RΩ(1)
False
Induction Step:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, +(n41_0, 1))), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n41_0, 1))) →RΩ(1)
and(True, eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0))) →IH
and(True, False) →RΩ(0)
False
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(16) Complex Obligation (BEST)
(17) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
revapp, possible, colorrest, colorednoderest, colornode
They will be analysed ascendingly in the following order:
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
revapp(
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(
n4056430_0),
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(
b)) →
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(
+(
n4056430_0,
b)), rt ∈ Ω(1 + n4056430
0)
Induction Base:
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) →RΩ(1)
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)
Induction Step:
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, 1)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) →RΩ(1)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b))) →IH
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(+(b, 1), c4056431_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(19) Complex Obligation (BEST)
(20) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, b)), rt ∈ Ω(1 + n40564300)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
possible, colorrest, colorednoderest, colornode
They will be analysed ascendingly in the following order:
possible < colorednoderest
possible < colornode
colorrest = colorednoderest
(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
possible(
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(
0),
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(
n4058308_0),
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(
0)) →
True, rt ∈ Ω(1 + n4058308
0)
Induction Base:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →RΩ(1)
True
Induction Step:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4058308_0, 1)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →RΩ(1)
possible[Ite][True][Ite](eqColor(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), colorof(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0))), gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →RΩ(1)
possible[Ite][True][Ite](eqColor(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), NoColor), gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →RΩ(1)
possible[Ite][True][Ite](False, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →RΩ(0)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) →IH
True
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(22) Complex Obligation (BEST)
(23) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, b)), rt ∈ Ω(1 + n40564300)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n40583080)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
colornode, colorrest, colorednoderest
They will be analysed ascendingly in the following order:
colorrest = colorednoderest
(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol colornode.
(25) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, b)), rt ∈ Ω(1 + n40564300)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n40583080)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
colorednoderest, colorrest
They will be analysed ascendingly in the following order:
colorrest = colorednoderest
(26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol colorednoderest.
(27) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, b)), rt ∈ Ω(1 + n40564300)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n40583080)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
The following defined symbols remain to be analysed:
colorrest
They will be analysed ascendingly in the following order:
colorrest = colorednoderest
(28) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol colorrest.
(29) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, b)), rt ∈ Ω(1 + n40564300)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n40583080)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
No more defined symbols left to analyse.
(30) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
(31) BOUNDS(n^1, INF)
(32) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, b)), rt ∈ Ω(1 + n40564300)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4058308_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0)) → True, rt ∈ Ω(1 + n40583080)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
No more defined symbols left to analyse.
(33) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
(34) BOUNDS(n^1, INF)
(35) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
revapp(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n4056430_0), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(b)) → gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(n4056430_0, b)), rt ∈ Ω(1 + n40564300)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
No more defined symbols left to analyse.
(36) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
(37) BOUNDS(n^1, INF)
(38) Obligation:
Innermost TRS:
Rules:
colorof(
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs)) →
colorof[Ite][True][Ite](
!EQ(
name,
node),
node,
Cons(
CN(
cl,
N(
name,
adjs)),
xs))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Yellow,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Yellow,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Blue,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Blue,
cs1),
Cons(
Red,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
NoColor,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Yellow,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Blue,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
Red,
cs1),
Cons(
Red,
cs2)) →
and(
True,
eqColorList(
cs1,
cs2))
eqColorList(
Cons(
NoColor,
cs1),
Cons(
b,
cs2)) →
and(
False,
eqColorList(
cs1,
cs2))
revapp(
Cons(
x,
xs),
rest) →
revapp(
xs,
Cons(
x,
rest))
revapp(
Nil,
rest) →
restpossible(
color,
Cons(
x,
xs),
colorednodes) →
possible[Ite][True][Ite](
eqColor(
color,
colorof(
x,
colorednodes)),
color,
Cons(
x,
xs),
colorednodes)
possible(
color,
Nil,
colorednodes) →
Truecolorrest(
cs,
ncs,
colorednodes,
Cons(
x,
xs)) →
colorednoderest(
cs,
ncs,
x,
colorednodes,
Cons(
x,
xs))
colorrest(
cs,
ncs,
colorednodes,
Nil) →
colorednodescolorof(
node,
Nil) →
NoColorcolornode(
Cons(
x,
xs),
N(
n,
ns),
colorednodes) →
colornode[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
Cons(
x,
xs),
N(
n,
ns),
colorednodes)
colornode(
Nil,
node,
colorednodes) →
NotPossiblecolorednoderest(
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest) →
colorednoderest[Ite][True][Ite](
possible(
x,
ns,
colorednodes),
cs,
Cons(
x,
xs),
N(
n,
ns),
colorednodes,
rest)
colorednoderest(
cs,
Nil,
node,
colorednodes,
rest) →
Nilgraphcolour(
Cons(
x,
xs),
cs) →
reverse(
colorrest(
cs,
cs,
Cons(
colornode(
cs,
x,
Nil),
Nil),
xs))
eqColorList(
Cons(
c1,
cs1),
Nil) →
FalseeqColorList(
Nil,
Cons(
c2,
cs2)) →
FalseeqColorList(
Nil,
Nil) →
TrueeqColor(
Yellow,
NoColor) →
FalseeqColor(
Yellow,
Yellow) →
TrueeqColor(
Yellow,
Blue) →
FalseeqColor(
Yellow,
Red) →
FalseeqColor(
Blue,
NoColor) →
FalseeqColor(
Blue,
Yellow) →
FalseeqColor(
Blue,
Blue) →
TrueeqColor(
Blue,
Red) →
FalseeqColor(
Red,
NoColor) →
FalseeqColor(
Red,
Yellow) →
FalseeqColor(
Red,
Blue) →
FalseeqColor(
Red,
Red) →
TruenotEmpty(
Cons(
x,
xs)) →
TruenotEmpty(
Nil) →
FalsegetNodeName(
N(
name,
adjs)) →
namegetNodeFromCN(
CN(
cl,
n)) →
ngetColorListFromCN(
CN(
cl,
n)) →
clgetAdjs(
N(
n,
ns)) →
nseqColor(
NoColor,
b) →
Falsereverse(
xs) →
revapp(
xs,
Nil)
and(
False,
False) →
Falseand(
True,
False) →
Falseand(
False,
True) →
Falseand(
True,
True) →
True!EQ(
S(
x),
S(
y)) →
!EQ(
x,
y)
!EQ(
0',
S(
y)) →
False!EQ(
S(
x),
0') →
False!EQ(
0',
0') →
Truecolorof[Ite][True][Ite](
True,
node,
Cons(
CN(
Cons(
x,
xs),
n),
xs')) →
xpossible[Ite][True][Ite](
False,
color,
Cons(
x,
xs),
colorednodes) →
possible(
color,
xs,
colorednodes)
colorof[Ite][True][Ite](
False,
node,
Cons(
x,
xs)) →
colorof(
node,
xs)
colornode[Ite][True][Ite](
False,
Cons(
x,
xs),
node,
colorednodes) →
colornode(
xs,
node,
colorednodes)
colorednoderest[Ite][True][Ite](
False,
cs,
Cons(
x,
xs),
node,
colorednodes,
rest) →
colorednoderest(
cs,
xs,
node,
colorednodes,
rest)
colorednoderest[Ite][True][Ite](
True,
cs,
ncs,
node,
colorednodes,
Cons(
x,
xs)) →
colorednoderest[Ite][True][Ite][True][Let](
colorrest(
cs,
cs,
Cons(
CN(
ncs,
node),
colorednodes),
xs))
possible[Ite][True][Ite](
True,
color,
adjs,
colorednodes) →
Falsecolornode[Ite][True][Ite](
True,
cs,
node,
colorednodes) →
CN(
cs,
node)
Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
CN :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Nil :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colorednoderest :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
colornode :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite] :: False:True → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
graphcolour :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
reverse :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
notEmpty :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorednoderest[Ite][True][Ite][True][Let] :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let] → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]2_0 :: Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0 :: Nat → Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]
Lemmas:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(0) ⇔ Nil
gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(x))
No more defined symbols left to analyse.
(39) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(+(1, n41_0)), gen_Cons:Nil:colorednoderest[Ite][True][Ite][True][Let]5_0(n41_0)) → False, rt ∈ Ω(1 + n410)
(40) BOUNDS(n^1, INF)