YES
We show the termination of the TRS R:

  not(true()) -> false()
  not(false()) -> true()
  evenodd(x,|0|()) -> not(evenodd(x,s(|0|())))
  evenodd(|0|(),s(|0|())) -> false()
  evenodd(s(x),s(|0|())) -> evenodd(x,|0|())


-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: evenodd#(x,|0|()) -> not#(evenodd(x,s(|0|())))
p2: evenodd#(x,|0|()) -> evenodd#(x,s(|0|()))
p3: evenodd#(s(x),s(|0|())) -> evenodd#(x,|0|())

and R consists of:

r1: not(true()) -> false()
r2: not(false()) -> true()
r3: evenodd(x,|0|()) -> not(evenodd(x,s(|0|())))
r4: evenodd(|0|(),s(|0|())) -> false()
r5: evenodd(s(x),s(|0|())) -> evenodd(x,|0|())

The estimated dependency graph contains the following SCCs:

  {p2, p3}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: evenodd#(x,|0|()) -> evenodd#(x,s(|0|()))
p2: evenodd#(s(x),s(|0|())) -> evenodd#(x,|0|())

and R consists of:

r1: not(true()) -> false()
r2: not(false()) -> true()
r3: evenodd(x,|0|()) -> not(evenodd(x,s(|0|())))
r4: evenodd(|0|(),s(|0|())) -> false()
r5: evenodd(s(x),s(|0|())) -> evenodd(x,|0|())

The set of usable rules consists of

  r1, r2, r3, r4, r5

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      model-based reduction triple (=A, >=A!, >A!):
      
        finite algebra:
        
          carrier: {0,1}
          interpretations:
            evenodd#_A(0,0) = 0
            evenodd#_A(0,1) = 0
            evenodd#_A(1,0) = 0
            evenodd#_A(1,1) = 0
            |0|_A = 1
            s_A(0) = 1
            s_A(1) = 0
            not_A(0) = 1
            not_A(1) = 0
            true_A = 0
            false_A = 1
            evenodd_A(0,0) = 0
            evenodd_A(0,1) = 1
            evenodd_A(1,0) = 1
            evenodd_A(1,1) = 0
            evenodd#!_A(0,0) = 1
            evenodd#!_A(0,1) = 1
            evenodd#!_A(1,0) = 1
            evenodd#!_A(1,1) = 1
            |0|!_A = 1
            s!_A(0) = 1
            s!_A(1) = 1
            not!_A(0) = 0
            not!_A(1) = 0
            true!_A = 0
            false!_A = 0
            evenodd!_A(0,0) = 0
            evenodd!_A(0,1) = 0
            evenodd!_A(1,0) = 0
            evenodd!_A(1,1) = 0
  
    partial status:
  
      pi(evenodd#) = [1]
      pi(|0|) = []
      pi(s) = [1]
      pi(not) = []
      pi(true) = []
      pi(false) = []
      pi(evenodd) = []

The following rules are removed:

  p2



-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: evenodd#(x,|0|()) -> evenodd#(x,s(|0|()))

and R consists of:

r1: not(true()) -> false()
r2: not(false()) -> true()
r3: evenodd(x,|0|()) -> not(evenodd(x,s(|0|())))
r4: evenodd(|0|(),s(|0|())) -> false()
r5: evenodd(s(x),s(|0|())) -> evenodd(x,|0|())

The estimated dependency graph contains the following SCCs:

  (no SCCs)