YES

We show the termination of the TRS R:

  NUMERAL(|0|()) -> |0|()
  BIT0(|0|()) -> |0|()
  SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
  SUC(|0|()) -> BIT1(|0|())
  SUC(BIT0(n)) -> BIT1(n)
  SUC(BIT1(n)) -> BIT0(SUC(n))
  PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
  PRE(|0|()) -> |0|()
  PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
  PRE(BIT1(n)) -> BIT0(n)
  plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
  plus(|0|(),|0|()) -> |0|()
  plus(|0|(),BIT0(n)) -> BIT0(n)
  plus(|0|(),BIT1(n)) -> BIT1(n)
  plus(BIT0(n),|0|()) -> BIT0(n)
  plus(BIT1(n),|0|()) -> BIT1(n)
  plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
  plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
  plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
  plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
  mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
  mult(|0|(),|0|()) -> |0|()
  mult(|0|(),BIT0(n)) -> |0|()
  mult(|0|(),BIT1(n)) -> |0|()
  mult(BIT0(n),|0|()) -> |0|()
  mult(BIT1(n),|0|()) -> |0|()
  mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
  mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
  mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
  mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
  exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
  exp(|0|(),|0|()) -> BIT1(|0|())
  exp(BIT0(m),|0|()) -> BIT1(|0|())
  exp(BIT1(m),|0|()) -> BIT1(|0|())
  exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
  exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
  exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
  exp(|0|(),BIT1(n)) -> |0|()
  exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
  exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
  EVEN(NUMERAL(n)) -> EVEN(n)
  EVEN(|0|()) -> T()
  EVEN(BIT0(n)) -> T()
  EVEN(BIT1(n)) -> F()
  ODD(NUMERAL(n)) -> ODD(n)
  ODD(|0|()) -> F()
  ODD(BIT0(n)) -> F()
  ODD(BIT1(n)) -> T()
  eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
  eq(|0|(),|0|()) -> T()
  eq(BIT0(n),|0|()) -> eq(n,|0|())
  eq(BIT1(n),|0|()) -> F()
  eq(|0|(),BIT0(n)) -> eq(|0|(),n)
  eq(|0|(),BIT1(n)) -> F()
  eq(BIT0(m),BIT0(n)) -> eq(m,n)
  eq(BIT0(m),BIT1(n)) -> F()
  eq(BIT1(m),BIT0(n)) -> F()
  eq(BIT1(m),BIT1(n)) -> eq(m,n)
  le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
  le(|0|(),|0|()) -> T()
  le(BIT0(n),|0|()) -> le(n,|0|())
  le(BIT1(n),|0|()) -> F()
  le(|0|(),BIT0(n)) -> T()
  le(|0|(),BIT1(n)) -> T()
  le(BIT0(m),BIT0(n)) -> le(m,n)
  le(BIT0(m),BIT1(n)) -> le(m,n)
  le(BIT1(m),BIT0(n)) -> lt(m,n)
  le(BIT1(m),BIT1(n)) -> le(m,n)
  lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
  lt(|0|(),|0|()) -> F()
  lt(BIT0(n),|0|()) -> F()
  lt(BIT1(n),|0|()) -> F()
  lt(|0|(),BIT0(n)) -> lt(|0|(),n)
  lt(|0|(),BIT1(n)) -> T()
  lt(BIT0(m),BIT0(n)) -> lt(m,n)
  lt(BIT0(m),BIT1(n)) -> le(m,n)
  lt(BIT1(m),BIT0(n)) -> lt(m,n)
  lt(BIT1(m),BIT1(n)) -> lt(m,n)
  ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
  ge(|0|(),|0|()) -> T()
  ge(|0|(),BIT0(n)) -> ge(|0|(),n)
  ge(|0|(),BIT1(n)) -> F()
  ge(BIT0(n),|0|()) -> T()
  ge(BIT1(n),|0|()) -> T()
  ge(BIT0(n),BIT0(m)) -> ge(n,m)
  ge(BIT1(n),BIT0(m)) -> ge(n,m)
  ge(BIT0(n),BIT1(m)) -> gt(n,m)
  ge(BIT1(n),BIT1(m)) -> ge(n,m)
  gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
  gt(|0|(),|0|()) -> F()
  gt(|0|(),BIT0(n)) -> F()
  gt(|0|(),BIT1(n)) -> F()
  gt(BIT0(n),|0|()) -> gt(n,|0|())
  gt(BIT1(n),|0|()) -> T()
  gt(BIT0(n),BIT0(m)) -> gt(n,m)
  gt(BIT1(n),BIT0(m)) -> ge(n,m)
  gt(BIT0(n),BIT1(m)) -> gt(n,m)
  gt(BIT1(n),BIT1(m)) -> gt(n,m)
  minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
  minus(|0|(),|0|()) -> |0|()
  minus(|0|(),BIT0(n)) -> |0|()
  minus(|0|(),BIT1(n)) -> |0|()
  minus(BIT0(n),|0|()) -> BIT0(n)
  minus(BIT1(n),|0|()) -> BIT1(n)
  minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
  minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
  minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
  minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

-- SCC decomposition.

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

p1: SUC#(NUMERAL(n)) -> NUMERAL#(SUC(n))
p2: SUC#(NUMERAL(n)) -> SUC#(n)
p3: SUC#(BIT1(n)) -> BIT0#(SUC(n))
p4: SUC#(BIT1(n)) -> SUC#(n)
p5: PRE#(NUMERAL(n)) -> NUMERAL#(PRE(n))
p6: PRE#(NUMERAL(n)) -> PRE#(n)
p7: PRE#(BIT0(n)) -> eq#(n,|0|())
p8: PRE#(BIT0(n)) -> PRE#(n)
p9: PRE#(BIT1(n)) -> BIT0#(n)
p10: plus#(NUMERAL(m),NUMERAL(n)) -> NUMERAL#(plus(m,n))
p11: plus#(NUMERAL(m),NUMERAL(n)) -> plus#(m,n)
p12: plus#(BIT0(m),BIT0(n)) -> BIT0#(plus(m,n))
p13: plus#(BIT0(m),BIT0(n)) -> plus#(m,n)
p14: plus#(BIT0(m),BIT1(n)) -> plus#(m,n)
p15: plus#(BIT1(m),BIT0(n)) -> plus#(m,n)
p16: plus#(BIT1(m),BIT1(n)) -> BIT0#(SUC(plus(m,n)))
p17: plus#(BIT1(m),BIT1(n)) -> SUC#(plus(m,n))
p18: plus#(BIT1(m),BIT1(n)) -> plus#(m,n)
p19: mult#(NUMERAL(m),NUMERAL(n)) -> NUMERAL#(mult(m,n))
p20: mult#(NUMERAL(m),NUMERAL(n)) -> mult#(m,n)
p21: mult#(BIT0(m),BIT0(n)) -> BIT0#(BIT0(mult(m,n)))
p22: mult#(BIT0(m),BIT0(n)) -> BIT0#(mult(m,n))
p23: mult#(BIT0(m),BIT0(n)) -> mult#(m,n)
p24: mult#(BIT0(m),BIT1(n)) -> plus#(BIT0(m),BIT0(BIT0(mult(m,n))))
p25: mult#(BIT0(m),BIT1(n)) -> BIT0#(BIT0(mult(m,n)))
p26: mult#(BIT0(m),BIT1(n)) -> BIT0#(mult(m,n))
p27: mult#(BIT0(m),BIT1(n)) -> mult#(m,n)
p28: mult#(BIT1(m),BIT0(n)) -> plus#(BIT0(n),BIT0(BIT0(mult(m,n))))
p29: mult#(BIT1(m),BIT0(n)) -> BIT0#(BIT0(mult(m,n)))
p30: mult#(BIT1(m),BIT0(n)) -> BIT0#(mult(m,n))
p31: mult#(BIT1(m),BIT0(n)) -> mult#(m,n)
p32: mult#(BIT1(m),BIT1(n)) -> plus#(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
p33: mult#(BIT1(m),BIT1(n)) -> plus#(BIT1(m),BIT0(n))
p34: mult#(BIT1(m),BIT1(n)) -> BIT0#(n)
p35: mult#(BIT1(m),BIT1(n)) -> BIT0#(BIT0(mult(m,n)))
p36: mult#(BIT1(m),BIT1(n)) -> BIT0#(mult(m,n))
p37: mult#(BIT1(m),BIT1(n)) -> mult#(m,n)
p38: exp#(NUMERAL(m),NUMERAL(n)) -> NUMERAL#(exp(m,n))
p39: exp#(NUMERAL(m),NUMERAL(n)) -> exp#(m,n)
p40: exp#(|0|(),BIT0(n)) -> mult#(exp(|0|(),n),exp(|0|(),n))
p41: exp#(|0|(),BIT0(n)) -> exp#(|0|(),n)
p42: exp#(BIT0(m),BIT0(n)) -> mult#(exp(BIT0(m),n),exp(BIT0(m),n))
p43: exp#(BIT0(m),BIT0(n)) -> exp#(BIT0(m),n)
p44: exp#(BIT1(m),BIT0(n)) -> mult#(exp(BIT1(m),n),exp(BIT1(m),n))
p45: exp#(BIT1(m),BIT0(n)) -> exp#(BIT1(m),n)
p46: exp#(BIT0(m),BIT1(n)) -> mult#(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
p47: exp#(BIT0(m),BIT1(n)) -> mult#(BIT0(m),exp(BIT0(m),n))
p48: exp#(BIT0(m),BIT1(n)) -> exp#(BIT0(m),n)
p49: exp#(BIT1(m),BIT1(n)) -> mult#(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
p50: exp#(BIT1(m),BIT1(n)) -> mult#(BIT1(m),exp(BIT1(m),n))
p51: exp#(BIT1(m),BIT1(n)) -> exp#(BIT1(m),n)
p52: EVEN#(NUMERAL(n)) -> EVEN#(n)
p53: ODD#(NUMERAL(n)) -> ODD#(n)
p54: eq#(NUMERAL(m),NUMERAL(n)) -> eq#(m,n)
p55: eq#(BIT0(n),|0|()) -> eq#(n,|0|())
p56: eq#(|0|(),BIT0(n)) -> eq#(|0|(),n)
p57: eq#(BIT0(m),BIT0(n)) -> eq#(m,n)
p58: eq#(BIT1(m),BIT1(n)) -> eq#(m,n)
p59: le#(NUMERAL(m),NUMERAL(n)) -> le#(m,n)
p60: le#(BIT0(n),|0|()) -> le#(n,|0|())
p61: le#(BIT0(m),BIT0(n)) -> le#(m,n)
p62: le#(BIT0(m),BIT1(n)) -> le#(m,n)
p63: le#(BIT1(m),BIT0(n)) -> lt#(m,n)
p64: le#(BIT1(m),BIT1(n)) -> le#(m,n)
p65: lt#(NUMERAL(m),NUMERAL(n)) -> lt#(m,n)
p66: lt#(|0|(),BIT0(n)) -> lt#(|0|(),n)
p67: lt#(BIT0(m),BIT0(n)) -> lt#(m,n)
p68: lt#(BIT0(m),BIT1(n)) -> le#(m,n)
p69: lt#(BIT1(m),BIT0(n)) -> lt#(m,n)
p70: lt#(BIT1(m),BIT1(n)) -> lt#(m,n)
p71: ge#(NUMERAL(n),NUMERAL(m)) -> ge#(n,m)
p72: ge#(|0|(),BIT0(n)) -> ge#(|0|(),n)
p73: ge#(BIT0(n),BIT0(m)) -> ge#(n,m)
p74: ge#(BIT1(n),BIT0(m)) -> ge#(n,m)
p75: ge#(BIT0(n),BIT1(m)) -> gt#(n,m)
p76: ge#(BIT1(n),BIT1(m)) -> ge#(n,m)
p77: gt#(NUMERAL(n),NUMERAL(m)) -> gt#(n,m)
p78: gt#(BIT0(n),|0|()) -> gt#(n,|0|())
p79: gt#(BIT0(n),BIT0(m)) -> gt#(n,m)
p80: gt#(BIT1(n),BIT0(m)) -> ge#(n,m)
p81: gt#(BIT0(n),BIT1(m)) -> gt#(n,m)
p82: gt#(BIT1(n),BIT1(m)) -> gt#(n,m)
p83: minus#(NUMERAL(m),NUMERAL(n)) -> NUMERAL#(minus(m,n))
p84: minus#(NUMERAL(m),NUMERAL(n)) -> minus#(m,n)
p85: minus#(BIT0(m),BIT0(n)) -> BIT0#(minus(m,n))
p86: minus#(BIT0(m),BIT0(n)) -> minus#(m,n)
p87: minus#(BIT0(m),BIT1(n)) -> PRE#(BIT0(minus(m,n)))
p88: minus#(BIT0(m),BIT1(n)) -> BIT0#(minus(m,n))
p89: minus#(BIT0(m),BIT1(n)) -> minus#(m,n)
p90: minus#(BIT1(m),BIT0(n)) -> le#(n,m)
p91: minus#(BIT1(m),BIT0(n)) -> minus#(m,n)
p92: minus#(BIT1(m),BIT1(n)) -> BIT0#(minus(m,n))
p93: minus#(BIT1(m),BIT1(n)) -> minus#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The estimated dependency graph contains the following SCCs:

  {p39, p43, p48}
  {p45, p51}
  {p41}
  {p20, p23, p27, p31, p37}
  {p11, p13, p14, p15, p18}
  {p2, p4}
  {p84, p86, p89, p91, p93}
  {p6, p8}
  {p54, p57, p58}
  {p55}
  {p52}
  {p53}
  {p56}
  {p59, p61, p62, p63, p64, p65, p67, p68, p69, p70}
  {p60}
  {p66}
  {p71, p73, p74, p75, p76, p77, p79, p80, p81, p82}
  {p72}
  {p78}


-- Reduction pair.

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

p1: exp#(BIT0(m),BIT1(n)) -> exp#(BIT0(m),n)
p2: exp#(BIT0(m),BIT0(n)) -> exp#(BIT0(m),n)
p3: exp#(NUMERAL(m),NUMERAL(n)) -> exp#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  r2

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > exp# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(exp#) = [1, 2]
        pi(BIT0) = [1]
        pi(BIT1) = 1
        pi(NUMERAL) = [1]
        pi(|0|) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > exp# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(exp#) = 2
        pi(BIT0) = 1
        pi(BIT1) = 1
        pi(NUMERAL) = [1]
        pi(|0|) = []
    

The next rules are strictly ordered:

  p2, p3

We remove them from the problem.

-- SCC decomposition.

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

p1: exp#(BIT0(m),BIT1(n)) -> exp#(BIT0(m),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: exp#(BIT0(m),BIT1(n)) -> exp#(BIT0(m),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  r2

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > exp# > BIT1
      
      argument filter:
    
        pi(exp#) = 2
        pi(BIT0) = [1]
        pi(BIT1) = 1
        pi(|0|) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > exp# > BIT1
      
      argument filter:
    
        pi(exp#) = 2
        pi(BIT0) = [1]
        pi(BIT1) = [1]
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: exp#(BIT1(m),BIT1(n)) -> exp#(BIT1(m),n)
p2: exp#(BIT1(m),BIT0(n)) -> exp#(BIT1(m),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        BIT0 > BIT1 > exp#
      
      argument filter:
    
        pi(exp#) = 2
        pi(BIT1) = [1]
        pi(BIT0) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        BIT0 > exp# > BIT1
      
      argument filter:
    
        pi(exp#) = []
        pi(BIT1) = []
        pi(BIT0) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: exp#(BIT1(m),BIT0(n)) -> exp#(BIT1(m),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: exp#(BIT1(m),BIT0(n)) -> exp#(BIT1(m),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        BIT1 > BIT0 > exp#
      
      argument filter:
    
        pi(exp#) = 2
        pi(BIT1) = 1
        pi(BIT0) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        BIT1 > exp# > BIT0
      
      argument filter:
    
        pi(exp#) = 2
        pi(BIT1) = 1
        pi(BIT0) = 1
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: exp#(|0|(),BIT0(n)) -> exp#(|0|(),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > exp# > BIT0
      
      argument filter:
    
        pi(exp#) = [2]
        pi(|0|) = []
        pi(BIT0) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > exp# > BIT0
      
      argument filter:
    
        pi(exp#) = 2
        pi(|0|) = []
        pi(BIT0) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: mult#(BIT1(m),BIT1(n)) -> mult#(m,n)
p2: mult#(BIT1(m),BIT0(n)) -> mult#(m,n)
p3: mult#(BIT0(m),BIT1(n)) -> mult#(m,n)
p4: mult#(BIT0(m),BIT0(n)) -> mult#(m,n)
p5: mult#(NUMERAL(m),NUMERAL(n)) -> mult#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        mult# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(mult#) = [1, 2]
        pi(BIT1) = 1
        pi(BIT0) = 1
        pi(NUMERAL) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        mult# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(mult#) = 1
        pi(BIT1) = [1]
        pi(BIT0) = [1]
        pi(NUMERAL) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4

We remove them from the problem.

-- SCC decomposition.

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

p1: mult#(NUMERAL(m),NUMERAL(n)) -> mult#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: mult#(NUMERAL(m),NUMERAL(n)) -> mult#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > mult#
      
      argument filter:
    
        pi(mult#) = [2]
        pi(NUMERAL) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > mult#
      
      argument filter:
    
        pi(mult#) = [2]
        pi(NUMERAL) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: plus#(BIT1(m),BIT1(n)) -> plus#(m,n)
p2: plus#(BIT1(m),BIT0(n)) -> plus#(m,n)
p3: plus#(BIT0(m),BIT1(n)) -> plus#(m,n)
p4: plus#(BIT0(m),BIT0(n)) -> plus#(m,n)
p5: plus#(NUMERAL(m),NUMERAL(n)) -> plus#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        plus# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(plus#) = [1, 2]
        pi(BIT1) = 1
        pi(BIT0) = 1
        pi(NUMERAL) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        plus# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(plus#) = 1
        pi(BIT1) = [1]
        pi(BIT0) = [1]
        pi(NUMERAL) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4

We remove them from the problem.

-- SCC decomposition.

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

p1: plus#(NUMERAL(m),NUMERAL(n)) -> plus#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: plus#(NUMERAL(m),NUMERAL(n)) -> plus#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > plus#
      
      argument filter:
    
        pi(plus#) = [2]
        pi(NUMERAL) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > plus#
      
      argument filter:
    
        pi(plus#) = [2]
        pi(NUMERAL) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: SUC#(NUMERAL(n)) -> SUC#(n)
p2: SUC#(BIT1(n)) -> SUC#(n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        SUC# > BIT1 > NUMERAL
      
      argument filter:
    
        pi(SUC#) = 1
        pi(NUMERAL) = 1
        pi(BIT1) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        SUC# > BIT1 > NUMERAL
      
      argument filter:
    
        pi(SUC#) = 1
        pi(NUMERAL) = [1]
        pi(BIT1) = [1]
    

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: minus#(BIT1(m),BIT1(n)) -> minus#(m,n)
p2: minus#(BIT1(m),BIT0(n)) -> minus#(m,n)
p3: minus#(BIT0(m),BIT1(n)) -> minus#(m,n)
p4: minus#(BIT0(m),BIT0(n)) -> minus#(m,n)
p5: minus#(NUMERAL(m),NUMERAL(n)) -> minus#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        minus# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(minus#) = [1, 2]
        pi(BIT1) = 1
        pi(BIT0) = 1
        pi(NUMERAL) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        minus# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(minus#) = 1
        pi(BIT1) = [1]
        pi(BIT0) = [1]
        pi(NUMERAL) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4

We remove them from the problem.

-- SCC decomposition.

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

p1: minus#(NUMERAL(m),NUMERAL(n)) -> minus#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: minus#(NUMERAL(m),NUMERAL(n)) -> minus#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > minus#
      
      argument filter:
    
        pi(minus#) = [2]
        pi(NUMERAL) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > minus#
      
      argument filter:
    
        pi(minus#) = [2]
        pi(NUMERAL) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: PRE#(NUMERAL(n)) -> PRE#(n)
p2: PRE#(BIT0(n)) -> PRE#(n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        PRE# > BIT0 > NUMERAL
      
      argument filter:
    
        pi(PRE#) = 1
        pi(NUMERAL) = 1
        pi(BIT0) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        PRE# > BIT0 > NUMERAL
      
      argument filter:
    
        pi(PRE#) = 1
        pi(NUMERAL) = [1]
        pi(BIT0) = [1]
    

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: eq#(BIT1(m),BIT1(n)) -> eq#(m,n)
p2: eq#(BIT0(m),BIT0(n)) -> eq#(m,n)
p3: eq#(NUMERAL(m),NUMERAL(n)) -> eq#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        eq# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(eq#) = [1, 2]
        pi(BIT1) = 1
        pi(BIT0) = 1
        pi(NUMERAL) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        eq# > NUMERAL > BIT0 > BIT1
      
      argument filter:
    
        pi(eq#) = 2
        pi(BIT1) = [1]
        pi(BIT0) = [1]
        pi(NUMERAL) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: eq#(BIT0(n),|0|()) -> eq#(n,|0|())

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > eq#
      
      argument filter:
    
        pi(eq#) = [1]
        pi(BIT0) = [1]
        pi(|0|) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > eq#
      
      argument filter:
    
        pi(eq#) = 1
        pi(BIT0) = [1]
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: EVEN#(NUMERAL(n)) -> EVEN#(n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > EVEN#
      
      argument filter:
    
        pi(EVEN#) = [1]
        pi(NUMERAL) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > EVEN#
      
      argument filter:
    
        pi(EVEN#) = [1]
        pi(NUMERAL) = [1]
    

The next rules are strictly ordered:

  p1
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: ODD#(NUMERAL(n)) -> ODD#(n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > ODD#
      
      argument filter:
    
        pi(ODD#) = [1]
        pi(NUMERAL) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        NUMERAL > ODD#
      
      argument filter:
    
        pi(ODD#) = [1]
        pi(NUMERAL) = [1]
    

The next rules are strictly ordered:

  p1
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: eq#(|0|(),BIT0(n)) -> eq#(|0|(),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > eq# > BIT0
      
      argument filter:
    
        pi(eq#) = [2]
        pi(|0|) = []
        pi(BIT0) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > eq# > BIT0
      
      argument filter:
    
        pi(eq#) = 2
        pi(|0|) = []
        pi(BIT0) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: le#(NUMERAL(m),NUMERAL(n)) -> le#(m,n)
p2: le#(BIT1(m),BIT1(n)) -> le#(m,n)
p3: le#(BIT1(m),BIT0(n)) -> lt#(m,n)
p4: lt#(BIT1(m),BIT1(n)) -> lt#(m,n)
p5: lt#(BIT1(m),BIT0(n)) -> lt#(m,n)
p6: lt#(BIT0(m),BIT1(n)) -> le#(m,n)
p7: le#(BIT0(m),BIT1(n)) -> le#(m,n)
p8: le#(BIT0(m),BIT0(n)) -> le#(m,n)
p9: lt#(BIT0(m),BIT0(n)) -> lt#(m,n)
p10: lt#(NUMERAL(m),NUMERAL(n)) -> lt#(m,n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        lt# > le# > BIT0 > BIT1 > NUMERAL
      
      argument filter:
    
        pi(le#) = 1
        pi(NUMERAL) = 1
        pi(BIT1) = 1
        pi(BIT0) = 1
        pi(lt#) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        lt# > le# > BIT0 > BIT1 > NUMERAL
      
      argument filter:
    
        pi(le#) = 1
        pi(NUMERAL) = [1]
        pi(BIT1) = [1]
        pi(BIT0) = [1]
        pi(lt#) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: le#(BIT0(n),|0|()) -> le#(n,|0|())

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > le#
      
      argument filter:
    
        pi(le#) = [1]
        pi(BIT0) = [1]
        pi(|0|) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > le#
      
      argument filter:
    
        pi(le#) = 1
        pi(BIT0) = [1]
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: lt#(|0|(),BIT0(n)) -> lt#(|0|(),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > lt# > BIT0
      
      argument filter:
    
        pi(lt#) = [2]
        pi(|0|) = []
        pi(BIT0) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > lt# > BIT0
      
      argument filter:
    
        pi(lt#) = 2
        pi(|0|) = []
        pi(BIT0) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: ge#(NUMERAL(n),NUMERAL(m)) -> ge#(n,m)
p2: ge#(BIT1(n),BIT1(m)) -> ge#(n,m)
p3: ge#(BIT0(n),BIT1(m)) -> gt#(n,m)
p4: gt#(BIT1(n),BIT1(m)) -> gt#(n,m)
p5: gt#(BIT0(n),BIT1(m)) -> gt#(n,m)
p6: gt#(BIT1(n),BIT0(m)) -> ge#(n,m)
p7: ge#(BIT1(n),BIT0(m)) -> ge#(n,m)
p8: ge#(BIT0(n),BIT0(m)) -> ge#(n,m)
p9: gt#(BIT0(n),BIT0(m)) -> gt#(n,m)
p10: gt#(NUMERAL(n),NUMERAL(m)) -> gt#(n,m)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        gt# > ge# > BIT0 > BIT1 > NUMERAL
      
      argument filter:
    
        pi(ge#) = 1
        pi(NUMERAL) = 1
        pi(BIT1) = 1
        pi(BIT0) = 1
        pi(gt#) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        ge# > gt# > BIT0 > BIT1 > NUMERAL
      
      argument filter:
    
        pi(ge#) = 1
        pi(NUMERAL) = [1]
        pi(BIT1) = [1]
        pi(BIT0) = [1]
        pi(gt#) = 1
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: ge#(|0|(),BIT0(n)) -> ge#(|0|(),n)

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > ge# > BIT0
      
      argument filter:
    
        pi(ge#) = [2]
        pi(|0|) = []
        pi(BIT0) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > ge# > BIT0
      
      argument filter:
    
        pi(ge#) = 2
        pi(|0|) = []
        pi(BIT0) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: gt#(BIT0(n),|0|()) -> gt#(n,|0|())

and R consists of:

r1: NUMERAL(|0|()) -> |0|()
r2: BIT0(|0|()) -> |0|()
r3: SUC(NUMERAL(n)) -> NUMERAL(SUC(n))
r4: SUC(|0|()) -> BIT1(|0|())
r5: SUC(BIT0(n)) -> BIT1(n)
r6: SUC(BIT1(n)) -> BIT0(SUC(n))
r7: PRE(NUMERAL(n)) -> NUMERAL(PRE(n))
r8: PRE(|0|()) -> |0|()
r9: PRE(BIT0(n)) -> if(eq(n,|0|()),|0|(),BIT1(PRE(n)))
r10: PRE(BIT1(n)) -> BIT0(n)
r11: plus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(plus(m,n))
r12: plus(|0|(),|0|()) -> |0|()
r13: plus(|0|(),BIT0(n)) -> BIT0(n)
r14: plus(|0|(),BIT1(n)) -> BIT1(n)
r15: plus(BIT0(n),|0|()) -> BIT0(n)
r16: plus(BIT1(n),|0|()) -> BIT1(n)
r17: plus(BIT0(m),BIT0(n)) -> BIT0(plus(m,n))
r18: plus(BIT0(m),BIT1(n)) -> BIT1(plus(m,n))
r19: plus(BIT1(m),BIT0(n)) -> BIT1(plus(m,n))
r20: plus(BIT1(m),BIT1(n)) -> BIT0(SUC(plus(m,n)))
r21: mult(NUMERAL(m),NUMERAL(n)) -> NUMERAL(mult(m,n))
r22: mult(|0|(),|0|()) -> |0|()
r23: mult(|0|(),BIT0(n)) -> |0|()
r24: mult(|0|(),BIT1(n)) -> |0|()
r25: mult(BIT0(n),|0|()) -> |0|()
r26: mult(BIT1(n),|0|()) -> |0|()
r27: mult(BIT0(m),BIT0(n)) -> BIT0(BIT0(mult(m,n)))
r28: mult(BIT0(m),BIT1(n)) -> plus(BIT0(m),BIT0(BIT0(mult(m,n))))
r29: mult(BIT1(m),BIT0(n)) -> plus(BIT0(n),BIT0(BIT0(mult(m,n))))
r30: mult(BIT1(m),BIT1(n)) -> plus(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))
r31: exp(NUMERAL(m),NUMERAL(n)) -> NUMERAL(exp(m,n))
r32: exp(|0|(),|0|()) -> BIT1(|0|())
r33: exp(BIT0(m),|0|()) -> BIT1(|0|())
r34: exp(BIT1(m),|0|()) -> BIT1(|0|())
r35: exp(|0|(),BIT0(n)) -> mult(exp(|0|(),n),exp(|0|(),n))
r36: exp(BIT0(m),BIT0(n)) -> mult(exp(BIT0(m),n),exp(BIT0(m),n))
r37: exp(BIT1(m),BIT0(n)) -> mult(exp(BIT1(m),n),exp(BIT1(m),n))
r38: exp(|0|(),BIT1(n)) -> |0|()
r39: exp(BIT0(m),BIT1(n)) -> mult(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))
r40: exp(BIT1(m),BIT1(n)) -> mult(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))
r41: EVEN(NUMERAL(n)) -> EVEN(n)
r42: EVEN(|0|()) -> T()
r43: EVEN(BIT0(n)) -> T()
r44: EVEN(BIT1(n)) -> F()
r45: ODD(NUMERAL(n)) -> ODD(n)
r46: ODD(|0|()) -> F()
r47: ODD(BIT0(n)) -> F()
r48: ODD(BIT1(n)) -> T()
r49: eq(NUMERAL(m),NUMERAL(n)) -> eq(m,n)
r50: eq(|0|(),|0|()) -> T()
r51: eq(BIT0(n),|0|()) -> eq(n,|0|())
r52: eq(BIT1(n),|0|()) -> F()
r53: eq(|0|(),BIT0(n)) -> eq(|0|(),n)
r54: eq(|0|(),BIT1(n)) -> F()
r55: eq(BIT0(m),BIT0(n)) -> eq(m,n)
r56: eq(BIT0(m),BIT1(n)) -> F()
r57: eq(BIT1(m),BIT0(n)) -> F()
r58: eq(BIT1(m),BIT1(n)) -> eq(m,n)
r59: le(NUMERAL(m),NUMERAL(n)) -> le(m,n)
r60: le(|0|(),|0|()) -> T()
r61: le(BIT0(n),|0|()) -> le(n,|0|())
r62: le(BIT1(n),|0|()) -> F()
r63: le(|0|(),BIT0(n)) -> T()
r64: le(|0|(),BIT1(n)) -> T()
r65: le(BIT0(m),BIT0(n)) -> le(m,n)
r66: le(BIT0(m),BIT1(n)) -> le(m,n)
r67: le(BIT1(m),BIT0(n)) -> lt(m,n)
r68: le(BIT1(m),BIT1(n)) -> le(m,n)
r69: lt(NUMERAL(m),NUMERAL(n)) -> lt(m,n)
r70: lt(|0|(),|0|()) -> F()
r71: lt(BIT0(n),|0|()) -> F()
r72: lt(BIT1(n),|0|()) -> F()
r73: lt(|0|(),BIT0(n)) -> lt(|0|(),n)
r74: lt(|0|(),BIT1(n)) -> T()
r75: lt(BIT0(m),BIT0(n)) -> lt(m,n)
r76: lt(BIT0(m),BIT1(n)) -> le(m,n)
r77: lt(BIT1(m),BIT0(n)) -> lt(m,n)
r78: lt(BIT1(m),BIT1(n)) -> lt(m,n)
r79: ge(NUMERAL(n),NUMERAL(m)) -> ge(n,m)
r80: ge(|0|(),|0|()) -> T()
r81: ge(|0|(),BIT0(n)) -> ge(|0|(),n)
r82: ge(|0|(),BIT1(n)) -> F()
r83: ge(BIT0(n),|0|()) -> T()
r84: ge(BIT1(n),|0|()) -> T()
r85: ge(BIT0(n),BIT0(m)) -> ge(n,m)
r86: ge(BIT1(n),BIT0(m)) -> ge(n,m)
r87: ge(BIT0(n),BIT1(m)) -> gt(n,m)
r88: ge(BIT1(n),BIT1(m)) -> ge(n,m)
r89: gt(NUMERAL(n),NUMERAL(m)) -> gt(n,m)
r90: gt(|0|(),|0|()) -> F()
r91: gt(|0|(),BIT0(n)) -> F()
r92: gt(|0|(),BIT1(n)) -> F()
r93: gt(BIT0(n),|0|()) -> gt(n,|0|())
r94: gt(BIT1(n),|0|()) -> T()
r95: gt(BIT0(n),BIT0(m)) -> gt(n,m)
r96: gt(BIT1(n),BIT0(m)) -> ge(n,m)
r97: gt(BIT0(n),BIT1(m)) -> gt(n,m)
r98: gt(BIT1(n),BIT1(m)) -> gt(n,m)
r99: minus(NUMERAL(m),NUMERAL(n)) -> NUMERAL(minus(m,n))
r100: minus(|0|(),|0|()) -> |0|()
r101: minus(|0|(),BIT0(n)) -> |0|()
r102: minus(|0|(),BIT1(n)) -> |0|()
r103: minus(BIT0(n),|0|()) -> BIT0(n)
r104: minus(BIT1(n),|0|()) -> BIT1(n)
r105: minus(BIT0(m),BIT0(n)) -> BIT0(minus(m,n))
r106: minus(BIT0(m),BIT1(n)) -> PRE(BIT0(minus(m,n)))
r107: minus(BIT1(m),BIT0(n)) -> if(le(n,m),BIT1(minus(m,n)),|0|())
r108: minus(BIT1(m),BIT1(n)) -> BIT0(minus(m,n))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > gt#
      
      argument filter:
    
        pi(gt#) = [1]
        pi(BIT0) = [1]
        pi(|0|) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        |0| > BIT0 > gt#
      
      argument filter:
    
        pi(gt#) = 1
        pi(BIT0) = [1]
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.