11.02/3.42 YES
11.02/3.42
11.02/3.42 Problem:
11.02/3.42 even(0()) -> true()
11.02/3.42 even(s(x)) -> false() <= odd(x) = false()
11.02/3.42 even(s(x)) -> true() <= odd(x) = true()
11.02/3.42 odd(0()) -> false()
11.02/3.42 odd(s(x)) -> false() <= even(x) = false()
11.02/3.42 odd(s(x)) -> true() <= even(x) = true()
11.02/3.42
11.02/3.42 Proof:
11.02/3.42 This system is confluent.
11.02/3.42 By \cite{SMI95}, Corollary 4.7 or 5.3.
11.02/3.42 This system is oriented.
11.02/3.42 This system is of type 3 or smaller.
11.02/3.42 This system is right-stable.
11.02/3.42 This system is properly oriented.
11.02/3.42 This is an overlay system.
11.02/3.42 This system is left-linear.
11.02/3.42 All 4 critical pairs are trivial or infeasible.
11.02/3.42 CP: false() = true() <= odd(x) = true(), odd(x) = false():
11.02/3.42 This critical pair is infeasible.
11.02/3.42 This critical pair is conditional.
11.02/3.42 This critical pair has some non-trivial conditions.
11.02/3.42 This system is of type 3 or smaller.
11.02/3.42 This system is deterministic.
11.02/3.42 This system is quasi-decreasing.
11.02/3.42 By \cite{O02}, p. 214, Proposition 7.2.50.
11.02/3.42 This system is of type 3 or smaller.
11.02/3.42 This system is deterministic.
11.02/3.42 System R transformed to optimized U(R).
11.02/3.42 This system is terminating.
11.02/3.42 Call external tool:
11.02/3.42 ./ttt2.sh
11.02/3.42 Input:
11.02/3.42 even(0()) -> true()
11.02/3.42 ?1(false(), x) -> false()
11.02/3.42 even(s(x)) -> ?1(odd(x), x)
11.02/3.42 ?1(true(), x) -> true()
11.02/3.42 odd(0()) -> false()
11.02/3.42 ?2(false(), x) -> false()
11.02/3.42 odd(s(x)) -> ?2(even(x), x)
11.02/3.42 ?2(true(), x) -> true()
11.02/3.42
11.02/3.42 Matrix Interpretation Processor: dim=3
11.02/3.42
11.02/3.42 interpretation:
11.02/3.42 [1 1 0] [1 1 0]
11.02/3.42 [?2](x0, x1) = [1 1 0]x0 + [0 0 0]x1
11.02/3.42 [0 1 0] [0 1 0] ,
11.02/3.42
11.02/3.42 [1 0 1] [1]
11.02/3.42 [odd](x0) = [0 1 1]x0 + [0]
11.02/3.42 [0 0 1] [0],
11.02/3.42
11.02/3.42 [1 1 1] [0]
11.02/3.42 [s](x0) = [0 0 1]x0 + [1]
11.02/3.42 [1 1 1] [0],
11.02/3.42
11.02/3.42 [1 1 0] [1 0 0] [0]
11.02/3.42 [?1](x0, x1) = [0 1 0]x0 + [0 0 0]x1 + [0]
11.02/3.42 [0 1 1] [1 0 0] [1],
11.02/3.42
11.02/3.42 [1]
11.02/3.42 [false] = [1]
11.02/3.42 [1],
11.02/3.42
11.02/3.42 [0]
11.02/3.42 [true] = [1]
11.02/3.42 [0],
11.02/3.42
11.02/3.42 [1 0 1] [1]
11.02/3.42 [even](x0) = [0 0 1]x0 + [0]
11.02/3.42 [1 1 0] [0],
11.02/3.42
11.02/3.42 [0]
11.02/3.42 [0] = [0]
11.02/3.42 [1]
11.02/3.42 orientation:
11.02/3.42 [2] [0]
11.02/3.42 even(0()) = [1] >= [1] = true()
11.02/3.42 [0] [0]
11.02/3.42
11.02/3.42 [1 0 0] [2] [1]
11.02/3.42 ?1(false(),x) = [0 0 0]x + [1] >= [1] = false()
11.02/3.42 [1 0 0] [3] [1]
11.02/3.42
11.02/3.42 [2 2 2] [1] [2 1 2] [1]
11.02/3.42 even(s(x)) = [1 1 1]x + [0] >= [0 1 1]x + [0] = ?1(odd(x),x)
11.02/3.42 [1 1 2] [1] [1 1 2] [1]
11.02/3.42
11.02/3.42 [1 0 0] [1] [0]
11.02/3.42 ?1(true(),x) = [0 0 0]x + [1] >= [1] = true()
11.02/3.42 [1 0 0] [2] [0]
11.02/3.42
11.02/3.42 [2] [1]
11.02/3.42 odd(0()) = [1] >= [1] = false()
11.02/3.42 [1] [1]
11.02/3.42
11.02/3.42 [1 1 0] [2] [1]
11.02/3.42 ?2(false(),x) = [0 0 0]x + [2] >= [1] = false()
11.02/3.42 [0 1 0] [1] [1]
11.02/3.42
11.02/3.42 [2 2 2] [1] [2 1 2] [1]
11.02/3.42 odd(s(x)) = [1 1 2]x + [1] >= [1 0 2]x + [1] = ?2(even(x),x)
11.02/3.42 [1 1 1] [0] [0 1 1] [0]
11.02/3.42
11.02/3.42 [1 1 0] [1] [0]
11.02/3.42 ?2(true(),x) = [0 0 0]x + [1] >= [1] = true()
11.02/3.42 [0 1 0] [1] [0]
11.02/3.42 problem:
11.02/3.42 even(s(x)) -> ?1(odd(x),x)
11.02/3.42 odd(s(x)) -> ?2(even(x),x)
11.02/3.42 Matrix Interpretation Processor: dim=1
11.02/3.42
11.02/3.42 interpretation:
11.02/3.42 [?2](x0, x1) = 2x0 + 4x1,
11.02/3.42
11.02/3.42 [odd](x0) = x0 + 4,
11.02/3.42
11.02/3.42 [s](x0) = 6x0 + 7,
11.02/3.42
11.02/3.42 [?1](x0, x1) = 3x0 + 3x1,
11.02/3.42
11.02/3.42 [even](x0) = x0 + 5
11.02/3.42 orientation:
11.02/3.42 even(s(x)) = 6x + 12 >= 6x + 12 = ?1(odd(x),x)
11.02/3.42
11.02/3.42 odd(s(x)) = 6x + 11 >= 6x + 10 = ?2(even(x),x)
11.02/3.42 problem:
11.02/3.42 even(s(x)) -> ?1(odd(x),x)
11.02/3.42 Matrix Interpretation Processor: dim=3
11.02/3.42
11.02/3.42 interpretation:
11.02/3.42 [1 0 0]
11.02/3.42 [odd](x0) = [1 0 0]x0
11.02/3.42 [0 0 0] ,
11.02/3.42
11.02/3.42 [1 0 0]
11.02/3.42 [s](x0) = [1 0 0]x0
11.02/3.42 [1 0 0] ,
11.02/3.42
11.02/3.42 [1 1 0] [1 0 0]
11.02/3.42 [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1
11.02/3.42 [0 0 0] [0 0 0] ,
11.02/3.42
11.02/3.42 [1 1 1] [1]
11.02/3.42 [even](x0) = [0 0 0]x0 + [0]
11.02/3.42 [0 0 0] [0]
11.02/3.42 orientation:
11.02/3.43 [3 0 0] [1] [3 0 0]
11.02/3.43 even(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?1(odd(x),x)
11.02/3.43 [0 0 0] [0] [0 0 0]
11.02/3.43 problem:
11.02/3.43
11.02/3.43 Qed
11.02/3.43 This critical pair is unfeasible.
11.02/3.43 CP: true() = false() <= odd(x) = false(), odd(x) = true():
11.02/3.43 This critical pair is infeasible.
11.02/3.43 This critical pair is conditional.
11.02/3.43 This critical pair has some non-trivial conditions.
11.02/3.43 This system is of type 3 or smaller.
11.02/3.43 This system is deterministic.
11.02/3.43 This system is quasi-decreasing.
11.02/3.43 By \cite{A14}, Theorem 11.5.9.
11.02/3.43 This system is of type 3 or smaller.
11.02/3.43 This system is deterministic.
11.02/3.43 System R transformed to V(R) + Emb.
11.02/3.43 This system is terminating.
11.02/3.43 Call external tool:
11.02/3.43 ./ttt2.sh
11.02/3.43 Input:
11.02/3.43 even(0()) -> true()
11.02/3.43 even(s(x)) -> false()
11.02/3.43 even(s(x)) -> odd(x)
11.02/3.43 even(s(x)) -> true()
11.02/3.43 odd(0()) -> false()
11.02/3.43 odd(s(x)) -> false()
11.02/3.43 odd(s(x)) -> even(x)
11.02/3.43 odd(s(x)) -> true()
11.02/3.43 even(x) -> x
11.02/3.43 s(x) -> x
11.02/3.43 odd(x) -> x
11.02/3.43
11.02/3.43 Matrix Interpretation Processor: dim=3
11.02/3.43
11.02/3.43 interpretation:
11.02/3.43
11.02/3.43 [odd](x0) = x0
11.02/3.43 ,
11.02/3.43
11.02/3.43 [0]
11.02/3.43 [false] = [0]
11.02/3.43 [0],
11.02/3.43
11.02/3.43 [1]
11.02/3.43 [s](x0) = x0 + [0]
11.02/3.43 [0],
11.02/3.43
11.02/3.43 [0]
11.02/3.43 [true] = [0]
11.02/3.43 [0],
11.02/3.43
11.02/3.43
11.02/3.43 [even](x0) = x0
11.02/3.43 ,
11.02/3.43
11.02/3.43 [1]
11.02/3.43 [0] = [0]
11.02/3.43 [0]
11.02/3.43 orientation:
11.02/3.43 [1] [0]
11.02/3.43 even(0()) = [0] >= [0] = true()
11.02/3.43 [0] [0]
11.02/3.43
11.02/3.43 [1] [0]
11.02/3.43 even(s(x)) = x + [0] >= [0] = false()
11.02/3.43 [0] [0]
11.02/3.43
11.02/3.43 [1]
11.02/3.43 even(s(x)) = x + [0] >= x = odd(x)
11.02/3.43 [0]
11.02/3.43
11.02/3.43 [1] [0]
11.02/3.43 even(s(x)) = x + [0] >= [0] = true()
11.02/3.43 [0] [0]
11.02/3.43
11.02/3.43 [1] [0]
11.02/3.43 odd(0()) = [0] >= [0] = false()
11.02/3.43 [0] [0]
11.02/3.43
11.02/3.43 [1] [0]
11.02/3.43 odd(s(x)) = x + [0] >= [0] = false()
11.02/3.43 [0] [0]
11.02/3.43
11.02/3.43 [1]
11.02/3.43 odd(s(x)) = x + [0] >= x = even(x)
11.02/3.43 [0]
11.02/3.43
11.02/3.43 [1] [0]
11.02/3.43 odd(s(x)) = x + [0] >= [0] = true()
11.02/3.43 [0] [0]
11.02/3.43
11.02/3.43
11.02/3.43 even(x) = x >= x = x
11.02/3.43
11.02/3.43
11.02/3.43 [1]
11.02/3.43 s(x) = x + [0] >= x = x
11.02/3.43 [0]
11.02/3.43
11.02/3.43
11.02/3.43 odd(x) = x >= x = x
11.02/3.43
11.02/3.43 problem:
11.02/3.43 even(x) -> x
11.02/3.43 odd(x) -> x
11.02/3.43 Matrix Interpretation Processor: dim=3
11.02/3.43
11.02/3.43 interpretation:
11.02/3.43 [1]
11.02/3.43 [odd](x0) = x0 + [0]
11.02/3.43 [0],
11.02/3.43
11.02/3.43
11.02/3.43 [even](x0) = x0
11.02/3.43
11.02/3.43 orientation:
11.02/3.44
11.02/3.44 even(x) = x >= x = x
11.02/3.44
11.02/3.44
11.02/3.44 [1]
11.02/3.44 odd(x) = x + [0] >= x = x
11.02/3.44 [0]
11.02/3.44 problem:
11.02/3.44 even(x) -> x
11.02/3.44 Matrix Interpretation Processor: dim=3
11.02/3.44
11.02/3.44 interpretation:
11.02/3.44 [1]
11.02/3.44 [even](x0) = x0 + [0]
11.02/3.44 [0]
11.02/3.44 orientation:
11.02/3.44 [1]
11.02/3.44 even(x) = x + [0] >= x = x
11.02/3.44 [0]
11.02/3.44 problem:
11.02/3.44
11.02/3.44 Qed
11.02/3.44 This critical pair is unfeasible.
11.02/3.44 CP: false() = true() <= even(x) = true(), even(x) = false():
11.02/3.44 This critical pair is infeasible.
11.02/3.44 This critical pair is conditional.
11.02/3.44 This critical pair has some non-trivial conditions.
11.02/3.44 This system is of type 3 or smaller.
11.02/3.44 This system is deterministic.
11.02/3.44 This system is quasi-decreasing.
11.02/3.44 By \cite{O02}, p. 214, Proposition 7.2.50.
11.02/3.44 This system is of type 3 or smaller.
11.02/3.44 This system is deterministic.
11.02/3.44 System R transformed to U(R).
11.02/3.44 This system is terminating.
11.02/3.44 Call external tool:
11.02/3.44 ./ttt2.sh
11.02/3.44 Input:
11.02/3.44 even(0()) -> true()
11.02/3.44 ?1(false(), x) -> false()
11.02/3.44 even(s(x)) -> ?1(odd(x), x)
11.02/3.44 ?2(true(), x) -> true()
11.02/3.44 even(s(x)) -> ?2(odd(x), x)
11.02/3.44 odd(0()) -> false()
11.02/3.44 ?3(false(), x) -> false()
11.02/3.44 odd(s(x)) -> ?3(even(x), x)
11.02/3.44 ?4(true(), x) -> true()
11.02/3.44 odd(s(x)) -> ?4(even(x), x)
11.02/3.44
11.02/3.44 Matrix Interpretation Processor: dim=1
11.02/3.44
11.02/3.44 interpretation:
11.02/3.44 [?4](x0, x1) = 4x0 + 2x1 + 7,
11.02/3.44
11.02/3.44 [?3](x0, x1) = x0 + 2x1 + 1,
11.02/3.44
11.02/3.44 [?2](x0, x1) = 2x0 + 2x1 + 2,
11.02/3.44
11.02/3.44 [odd](x0) = 5x0 + 3,
11.02/3.44
11.02/3.44 [s](x0) = 4x0 + 4,
11.02/3.44
11.02/3.44 [?1](x0, x1) = x0 + x1 + 6,
11.02/3.44
11.02/3.44 [false] = 2,
11.02/3.44
11.02/3.44 [true] = 2,
11.02/3.44
11.02/3.44 [even](x0) = 4x0 + 4,
11.02/3.44
11.02/3.44 [0] = 2
11.02/3.44 orientation:
11.02/3.44 even(0()) = 12 >= 2 = true()
11.02/3.44
11.02/3.44 ?1(false(),x) = x + 8 >= 2 = false()
11.02/3.44
11.02/3.44 even(s(x)) = 16x + 20 >= 6x + 9 = ?1(odd(x),x)
11.02/3.44
11.02/3.44 ?2(true(),x) = 2x + 6 >= 2 = true()
11.02/3.44
11.02/3.44 even(s(x)) = 16x + 20 >= 12x + 8 = ?2(odd(x),x)
11.02/3.44
11.02/3.44 odd(0()) = 13 >= 2 = false()
11.02/3.44
11.02/3.44 ?3(false(),x) = 2x + 3 >= 2 = false()
11.02/3.44
11.02/3.44 odd(s(x)) = 20x + 23 >= 6x + 5 = ?3(even(x),x)
11.02/3.44
11.02/3.44 ?4(true(),x) = 2x + 15 >= 2 = true()
11.02/3.44
11.02/3.44 odd(s(x)) = 20x + 23 >= 18x + 23 = ?4(even(x),x)
11.02/3.44 problem:
11.02/3.44 odd(s(x)) -> ?4(even(x),x)
11.02/3.44 Matrix Interpretation Processor: dim=3
11.02/3.44
11.02/3.44 interpretation:
11.02/3.44 [1 1 0] [1 0 0]
11.02/3.44 [?4](x0, x1) = [0 0 0]x0 + [0 0 0]x1
11.02/3.44 [0 0 0] [0 0 0] ,
11.02/3.44
11.02/3.44 [1 1 1] [1]
11.02/3.44 [odd](x0) = [0 0 0]x0 + [0]
11.02/3.44 [0 0 0] [0],
11.02/3.44
11.02/3.44 [1 0 0]
11.02/3.44 [s](x0) = [1 0 0]x0
11.02/3.44 [1 0 0] ,
11.02/3.44
11.02/3.44 [1 0 0]
11.02/3.44 [even](x0) = [1 0 0]x0
11.02/3.44 [0 0 0]
11.02/3.44 orientation:
11.02/3.44 [3 0 0] [1] [3 0 0]
11.02/3.44 odd(s(x)) = [0 0 0]x + [0] >= [0 0 0]x = ?4(even(x),x)
11.02/3.44 [0 0 0] [0] [0 0 0]
11.02/3.44 problem:
11.02/3.44
11.02/3.44 Qed
11.02/3.44 This critical pair is unfeasible.
11.02/3.44 CP: true() = false() <= even(x) = false(), even(x) = true():
11.02/3.45 This critical pair is infeasible.
11.02/3.45 This critical pair is conditional.
11.02/3.45 This critical pair has some non-trivial conditions.
11.02/3.45 This system is of type 3 or smaller.
11.02/3.45 This system is deterministic.
11.02/3.45 This system is quasi-decreasing.
11.02/3.45 By \cite{O02}, p. 214, Proposition 7.2.50.
11.02/3.45 This system is of type 3 or smaller.
11.02/3.45 This system is deterministic.
11.02/3.45 System R transformed to U(R).
11.02/3.45 This system is terminating.
11.02/3.45 Call external tool:
11.02/3.45 ./ttt2.sh
11.02/3.45 Input:
11.02/3.45 even(0()) -> true()
11.02/3.45 ?1(false(), x) -> false()
11.02/3.45 even(s(x)) -> ?1(odd(x), x)
11.02/3.45 ?2(true(), x) -> true()
11.02/3.45 even(s(x)) -> ?2(odd(x), x)
11.02/3.45 odd(0()) -> false()
11.02/3.45 ?3(false(), x) -> false()
11.02/3.45 odd(s(x)) -> ?3(even(x), x)
11.02/3.45 ?4(true(), x) -> true()
11.02/3.45 odd(s(x)) -> ?4(even(x), x)
11.02/3.45
11.02/3.45 Matrix Interpretation Processor: dim=1
11.02/3.45
11.02/3.45 interpretation:
11.02/3.45 [?4](x0, x1) = 4x0 + 2x1 + 7,
11.02/3.45
11.02/3.45 [?3](x0, x1) = x0 + 2x1 + 1,
11.02/3.45
11.02/3.45 [?2](x0, x1) = 2x0 + 2x1 + 2,
11.02/3.45
11.02/3.45 [odd](x0) = 5x0 + 3,
11.02/3.45
11.02/3.45 [s](x0) = 4x0 + 4,
11.02/3.45
11.02/3.45 [?1](x0, x1) = x0 + x1 + 6,
11.02/3.45
11.02/3.45 [false] = 2,
11.02/3.45
11.02/3.45 [true] = 2,
11.02/3.45
11.02/3.45 [even](x0) = 4x0 + 4,
11.02/3.45
11.02/3.45 [0] = 2
11.02/3.45 orientation:
11.02/3.45 even(0()) = 12 >= 2 = true()
11.02/3.45
11.02/3.45 ?1(false(),x) = x + 8 >= 2 = false()
11.02/3.45
11.02/3.45 even(s(x)) = 16x + 20 >= 6x + 9 = ?1(odd(x),x)
11.02/3.45
11.02/3.45 ?2(true(),x) = 2x + 6 >= 2 = true()
11.02/3.45
11.02/3.45 even(s(x)) = 16x + 20 >= 12x + 8 = ?2(odd(x),x)
11.02/3.45
11.02/3.45 odd(0()) = 13 >= 2 = false()
11.02/3.45
11.02/3.45 ?3(false(),x) = 2x + 3 >= 2 = false()
11.02/3.45
11.02/3.45 odd(s(x)) = 20x + 23 >= 6x + 5 = ?3(even(x),x)
11.02/3.45
11.02/3.45 ?4(true(),x) = 2x + 15 >= 2 = true()
11.02/3.45
11.02/3.45 odd(s(x)) = 20x + 23 >= 18x + 23 = ?4(even(x),x)
11.02/3.45 problem:
11.02/3.45 odd(s(x)) -> ?4(even(x),x)
11.02/3.45 Matrix Interpretation Processor: dim=1
11.02/3.45
11.02/3.45 interpretation:
11.02/3.45 [?4](x0, x1) = 4x0 + 5x1,
11.02/3.45
11.02/3.45 [odd](x0) = 5x0 + 7,
11.02/3.45
11.02/3.45 [s](x0) = 6x0 + 4,
11.02/3.45
11.02/3.45 [even](x0) = 6x0 + 4
11.02/3.45 orientation:
11.02/3.45 odd(s(x)) = 30x + 27 >= 29x + 16 = ?4(even(x),x)
11.02/3.45 problem:
11.02/3.45
11.02/3.45 Qed
11.02/3.45 This critical pair is unfeasible.
11.02/3.45
11.02/3.47 EOF