YES
We show the termination of the TRS R:
active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
active(U13(tt())) -> mark(tt())
active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
active(U22(tt())) -> mark(tt())
active(U31(tt(),N)) -> mark(N)
active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
active(and(tt(),X)) -> mark(X)
active(isNat(|0|())) -> mark(tt())
active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
active(isNatKind(|0|())) -> mark(tt())
active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
active(isNatKind(s(V1))) -> mark(isNatKind(V1))
active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
mark(tt()) -> active(tt())
mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
mark(isNat(X)) -> active(isNat(X))
mark(U13(X)) -> active(U13(mark(X)))
mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
mark(U22(X)) -> active(U22(mark(X)))
mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
mark(s(X)) -> active(s(mark(X)))
mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
mark(and(X1,X2)) -> active(and(mark(X1),X2))
mark(|0|()) -> active(|0|())
mark(isNatKind(X)) -> active(isNatKind(X))
U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
U11(active(X1),X2,X3) -> U11(X1,X2,X3)
U11(X1,active(X2),X3) -> U11(X1,X2,X3)
U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
U12(mark(X1),X2) -> U12(X1,X2)
U12(X1,mark(X2)) -> U12(X1,X2)
U12(active(X1),X2) -> U12(X1,X2)
U12(X1,active(X2)) -> U12(X1,X2)
isNat(mark(X)) -> isNat(X)
isNat(active(X)) -> isNat(X)
U13(mark(X)) -> U13(X)
U13(active(X)) -> U13(X)
U21(mark(X1),X2) -> U21(X1,X2)
U21(X1,mark(X2)) -> U21(X1,X2)
U21(active(X1),X2) -> U21(X1,X2)
U21(X1,active(X2)) -> U21(X1,X2)
U22(mark(X)) -> U22(X)
U22(active(X)) -> U22(X)
U31(mark(X1),X2) -> U31(X1,X2)
U31(X1,mark(X2)) -> U31(X1,X2)
U31(active(X1),X2) -> U31(X1,X2)
U31(X1,active(X2)) -> U31(X1,X2)
U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
U41(active(X1),X2,X3) -> U41(X1,X2,X3)
U41(X1,active(X2),X3) -> U41(X1,X2,X3)
U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
plus(mark(X1),X2) -> plus(X1,X2)
plus(X1,mark(X2)) -> plus(X1,X2)
plus(active(X1),X2) -> plus(X1,X2)
plus(X1,active(X2)) -> plus(X1,X2)
and(mark(X1),X2) -> and(X1,X2)
and(X1,mark(X2)) -> and(X1,X2)
and(active(X1),X2) -> and(X1,X2)
and(X1,active(X2)) -> and(X1,X2)
isNatKind(mark(X)) -> isNatKind(X)
isNatKind(active(X)) -> isNatKind(X)
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: active#(U11(tt(),V1,V2)) -> U12#(isNat(V1),V2)
p3: active#(U11(tt(),V1,V2)) -> isNat#(V1)
p4: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p5: active#(U12(tt(),V2)) -> U13#(isNat(V2))
p6: active#(U12(tt(),V2)) -> isNat#(V2)
p7: active#(U13(tt())) -> mark#(tt())
p8: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p9: active#(U21(tt(),V1)) -> U22#(isNat(V1))
p10: active#(U21(tt(),V1)) -> isNat#(V1)
p11: active#(U22(tt())) -> mark#(tt())
p12: active#(U31(tt(),N)) -> mark#(N)
p13: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p14: active#(U41(tt(),M,N)) -> s#(plus(N,M))
p15: active#(U41(tt(),M,N)) -> plus#(N,M)
p16: active#(and(tt(),X)) -> mark#(X)
p17: active#(isNat(|0|())) -> mark#(tt())
p18: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p19: active#(isNat(plus(V1,V2))) -> U11#(and(isNatKind(V1),isNatKind(V2)),V1,V2)
p20: active#(isNat(plus(V1,V2))) -> and#(isNatKind(V1),isNatKind(V2))
p21: active#(isNat(plus(V1,V2))) -> isNatKind#(V1)
p22: active#(isNat(plus(V1,V2))) -> isNatKind#(V2)
p23: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p24: active#(isNat(s(V1))) -> U21#(isNatKind(V1),V1)
p25: active#(isNat(s(V1))) -> isNatKind#(V1)
p26: active#(isNatKind(|0|())) -> mark#(tt())
p27: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p28: active#(isNatKind(plus(V1,V2))) -> and#(isNatKind(V1),isNatKind(V2))
p29: active#(isNatKind(plus(V1,V2))) -> isNatKind#(V1)
p30: active#(isNatKind(plus(V1,V2))) -> isNatKind#(V2)
p31: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p32: active#(isNatKind(s(V1))) -> isNatKind#(V1)
p33: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p34: active#(plus(N,|0|())) -> U31#(and(isNat(N),isNatKind(N)),N)
p35: active#(plus(N,|0|())) -> and#(isNat(N),isNatKind(N))
p36: active#(plus(N,|0|())) -> isNat#(N)
p37: active#(plus(N,|0|())) -> isNatKind#(N)
p38: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p39: active#(plus(N,s(M))) -> U41#(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
p40: active#(plus(N,s(M))) -> and#(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
p41: active#(plus(N,s(M))) -> and#(isNat(M),isNatKind(M))
p42: active#(plus(N,s(M))) -> isNat#(M)
p43: active#(plus(N,s(M))) -> isNatKind#(M)
p44: active#(plus(N,s(M))) -> and#(isNat(N),isNatKind(N))
p45: active#(plus(N,s(M))) -> isNat#(N)
p46: active#(plus(N,s(M))) -> isNatKind#(N)
p47: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p48: mark#(U11(X1,X2,X3)) -> U11#(mark(X1),X2,X3)
p49: mark#(U11(X1,X2,X3)) -> mark#(X1)
p50: mark#(tt()) -> active#(tt())
p51: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p52: mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
p53: mark#(U12(X1,X2)) -> mark#(X1)
p54: mark#(isNat(X)) -> active#(isNat(X))
p55: mark#(U13(X)) -> active#(U13(mark(X)))
p56: mark#(U13(X)) -> U13#(mark(X))
p57: mark#(U13(X)) -> mark#(X)
p58: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p59: mark#(U21(X1,X2)) -> U21#(mark(X1),X2)
p60: mark#(U21(X1,X2)) -> mark#(X1)
p61: mark#(U22(X)) -> active#(U22(mark(X)))
p62: mark#(U22(X)) -> U22#(mark(X))
p63: mark#(U22(X)) -> mark#(X)
p64: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p65: mark#(U31(X1,X2)) -> U31#(mark(X1),X2)
p66: mark#(U31(X1,X2)) -> mark#(X1)
p67: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p68: mark#(U41(X1,X2,X3)) -> U41#(mark(X1),X2,X3)
p69: mark#(U41(X1,X2,X3)) -> mark#(X1)
p70: mark#(s(X)) -> active#(s(mark(X)))
p71: mark#(s(X)) -> s#(mark(X))
p72: mark#(s(X)) -> mark#(X)
p73: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p74: mark#(plus(X1,X2)) -> plus#(mark(X1),mark(X2))
p75: mark#(plus(X1,X2)) -> mark#(X1)
p76: mark#(plus(X1,X2)) -> mark#(X2)
p77: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p78: mark#(and(X1,X2)) -> and#(mark(X1),X2)
p79: mark#(and(X1,X2)) -> mark#(X1)
p80: mark#(|0|()) -> active#(|0|())
p81: mark#(isNatKind(X)) -> active#(isNatKind(X))
p82: U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
p83: U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
p84: U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
p85: U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
p86: U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
p87: U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
p88: U12#(mark(X1),X2) -> U12#(X1,X2)
p89: U12#(X1,mark(X2)) -> U12#(X1,X2)
p90: U12#(active(X1),X2) -> U12#(X1,X2)
p91: U12#(X1,active(X2)) -> U12#(X1,X2)
p92: isNat#(mark(X)) -> isNat#(X)
p93: isNat#(active(X)) -> isNat#(X)
p94: U13#(mark(X)) -> U13#(X)
p95: U13#(active(X)) -> U13#(X)
p96: U21#(mark(X1),X2) -> U21#(X1,X2)
p97: U21#(X1,mark(X2)) -> U21#(X1,X2)
p98: U21#(active(X1),X2) -> U21#(X1,X2)
p99: U21#(X1,active(X2)) -> U21#(X1,X2)
p100: U22#(mark(X)) -> U22#(X)
p101: U22#(active(X)) -> U22#(X)
p102: U31#(mark(X1),X2) -> U31#(X1,X2)
p103: U31#(X1,mark(X2)) -> U31#(X1,X2)
p104: U31#(active(X1),X2) -> U31#(X1,X2)
p105: U31#(X1,active(X2)) -> U31#(X1,X2)
p106: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
p107: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
p108: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
p109: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
p110: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
p111: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
p112: s#(mark(X)) -> s#(X)
p113: s#(active(X)) -> s#(X)
p114: plus#(mark(X1),X2) -> plus#(X1,X2)
p115: plus#(X1,mark(X2)) -> plus#(X1,X2)
p116: plus#(active(X1),X2) -> plus#(X1,X2)
p117: plus#(X1,active(X2)) -> plus#(X1,X2)
p118: and#(mark(X1),X2) -> and#(X1,X2)
p119: and#(X1,mark(X2)) -> and#(X1,X2)
p120: and#(active(X1),X2) -> and#(X1,X2)
p121: and#(X1,active(X2)) -> and#(X1,X2)
p122: isNatKind#(mark(X)) -> isNatKind#(X)
p123: isNatKind#(active(X)) -> isNatKind#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p4, p8, p12, p13, p16, p18, p23, p27, p31, p33, p38, p47, p49, p51, p53, p54, p55, p57, p58, p60, p61, p63, p64, p66, p67, p69, p70, p72, p73, p75, p76, p77, p79, p81}
{p88, p89, p90, p91}
{p92, p93}
{p94, p95}
{p100, p101}
{p112, p113}
{p114, p115, p116, p117}
{p82, p83, p84, p85, p86, p87}
{p118, p119, p120, p121}
{p122, p123}
{p96, p97, p98, p99}
{p102, p103, p104, p105}
{p106, p107, p108, p109, p110, p111}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p7: mark#(plus(X1,X2)) -> mark#(X2)
p8: mark#(plus(X1,X2)) -> mark#(X1)
p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p10: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(s(X)) -> active#(s(mark(X)))
p13: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p14: mark#(U41(X1,X2,X3)) -> mark#(X1)
p15: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p16: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p17: mark#(U31(X1,X2)) -> mark#(X1)
p18: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p19: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p20: mark#(U22(X)) -> mark#(X)
p21: mark#(U22(X)) -> active#(U22(mark(X)))
p22: active#(and(tt(),X)) -> mark#(X)
p23: mark#(U21(X1,X2)) -> mark#(X1)
p24: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p25: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p26: mark#(U13(X)) -> mark#(X)
p27: mark#(U13(X)) -> active#(U13(mark(X)))
p28: active#(U31(tt(),N)) -> mark#(N)
p29: mark#(isNat(X)) -> active#(isNat(X))
p30: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p31: mark#(U12(X1,X2)) -> mark#(X1)
p32: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p33: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p34: mark#(U11(X1,X2,X3)) -> mark#(X1)
p35: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = x1
U11_A(x1,x2,x3) = (2,0)
tt_A() = (1,0)
mark#_A(x1) = (2,0)
U12_A(x1,x2) = (2,0)
isNat_A(x1) = (2,1)
isNatKind_A(x1) = (2,1)
plus_A(x1,x2) = (2,0)
s_A(x1) = (2,0)
U41_A(x1,x2,x3) = (2,0)
and_A(x1,x2) = (2,1)
mark_A(x1) = (0,0)
|0|_A() = (1,0)
U31_A(x1,x2) = (2,1)
U21_A(x1,x2) = (2,0)
U22_A(x1) = (1,1)
U13_A(x1) = (1,0)
active_A(x1) = (0,0)
The next rules are strictly ordered:
p21, p27
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p7: mark#(plus(X1,X2)) -> mark#(X2)
p8: mark#(plus(X1,X2)) -> mark#(X1)
p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p10: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(s(X)) -> active#(s(mark(X)))
p13: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p14: mark#(U41(X1,X2,X3)) -> mark#(X1)
p15: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p16: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p17: mark#(U31(X1,X2)) -> mark#(X1)
p18: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p19: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p20: mark#(U22(X)) -> mark#(X)
p21: active#(and(tt(),X)) -> mark#(X)
p22: mark#(U21(X1,X2)) -> mark#(X1)
p23: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p24: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p25: mark#(U13(X)) -> mark#(X)
p26: active#(U31(tt(),N)) -> mark#(N)
p27: mark#(isNat(X)) -> active#(isNat(X))
p28: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p29: mark#(U12(X1,X2)) -> mark#(X1)
p30: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p31: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p32: mark#(U11(X1,X2,X3)) -> mark#(X1)
p33: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(U31(tt(),N)) -> mark#(N)
p10: mark#(U13(X)) -> mark#(X)
p11: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p12: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U22(X)) -> mark#(X)
p15: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p16: active#(and(tt(),X)) -> mark#(X)
p17: mark#(U31(X1,X2)) -> mark#(X1)
p18: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p19: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p20: mark#(U41(X1,X2,X3)) -> mark#(X1)
p21: mark#(s(X)) -> active#(s(mark(X)))
p22: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p23: mark#(s(X)) -> mark#(X)
p24: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p25: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p26: mark#(plus(X1,X2)) -> mark#(X1)
p27: mark#(plus(X1,X2)) -> mark#(X2)
p28: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p29: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p30: mark#(and(X1,X2)) -> mark#(X1)
p31: mark#(isNatKind(X)) -> active#(isNatKind(X))
p32: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p33: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = x1
U11_A(x1,x2,x3) = (2,1)
tt_A() = (1,1)
mark#_A(x1) = (2,0)
U12_A(x1,x2) = (2,1)
isNat_A(x1) = (2,1)
mark_A(x1) = (1,1)
U13_A(x1) = (1,1)
U21_A(x1,x2) = (2,1)
U22_A(x1) = (1,1)
U31_A(x1,x2) = (2,1)
U41_A(x1,x2,x3) = (2,1)
s_A(x1) = (1,1)
plus_A(x1,x2) = (2,1)
and_A(x1,x2) = (2,1)
isNatKind_A(x1) = (2,1)
|0|_A() = (1,1)
active_A(x1) = (1,1)
The next rules are strictly ordered:
p21
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(U31(tt(),N)) -> mark#(N)
p10: mark#(U13(X)) -> mark#(X)
p11: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p12: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U22(X)) -> mark#(X)
p15: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p16: active#(and(tt(),X)) -> mark#(X)
p17: mark#(U31(X1,X2)) -> mark#(X1)
p18: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p19: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p20: mark#(U41(X1,X2,X3)) -> mark#(X1)
p21: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p22: mark#(s(X)) -> mark#(X)
p23: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p24: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p25: mark#(plus(X1,X2)) -> mark#(X1)
p26: mark#(plus(X1,X2)) -> mark#(X2)
p27: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p28: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p29: mark#(and(X1,X2)) -> mark#(X1)
p30: mark#(isNatKind(X)) -> active#(isNatKind(X))
p31: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p32: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(plus(N,|0|())) -> mark#(U31(and(isNat(N),isNatKind(N)),N))
p7: mark#(plus(X1,X2)) -> mark#(X2)
p8: mark#(plus(X1,X2)) -> mark#(X1)
p9: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p10: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p11: mark#(s(X)) -> mark#(X)
p12: mark#(U41(X1,X2,X3)) -> mark#(X1)
p13: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p14: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p15: mark#(U31(X1,X2)) -> mark#(X1)
p16: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p17: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p18: mark#(U22(X)) -> mark#(X)
p19: mark#(U21(X1,X2)) -> mark#(X1)
p20: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p21: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p22: mark#(U13(X)) -> mark#(X)
p23: mark#(isNat(X)) -> active#(isNat(X))
p24: active#(and(tt(),X)) -> mark#(X)
p25: mark#(U12(X1,X2)) -> mark#(X1)
p26: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p27: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p28: mark#(U11(X1,X2,X3)) -> mark#(X1)
p29: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p30: active#(U31(tt(),N)) -> mark#(N)
p31: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p32: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = ((1,0),(1,0)) x1
U11_A(x1,x2,x3) = x1 + ((0,0),(1,0)) x2 + (0,1)
tt_A() = (0,0)
mark#_A(x1) = ((1,0),(1,0)) x1
U12_A(x1,x2) = x1 + (0,1)
isNat_A(x1) = (0,1)
isNatKind_A(x1) = (0,1)
plus_A(x1,x2) = x1 + x2 + (2,1)
s_A(x1) = ((1,0),(1,0)) x1 + (1,1)
U41_A(x1,x2,x3) = x1 + ((1,0),(1,0)) x2 + x3 + (3,1)
and_A(x1,x2) = x1 + x2 + (0,1)
mark_A(x1) = ((1,0),(1,0)) x1 + (0,1)
|0|_A() = (0,1)
U31_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (1,1)
U21_A(x1,x2) = x1 + (0,1)
U22_A(x1) = x1 + (0,1)
U13_A(x1) = x1 + (0,1)
active_A(x1) = ((1,0),(1,0)) x1 + (0,1)
The next rules are strictly ordered:
p6, p7, p8, p11, p12, p15, p30
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p7: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p8: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p9: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p10: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p11: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p12: mark#(U22(X)) -> mark#(X)
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p15: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p16: mark#(U13(X)) -> mark#(X)
p17: mark#(isNat(X)) -> active#(isNat(X))
p18: active#(and(tt(),X)) -> mark#(X)
p19: mark#(U12(X1,X2)) -> mark#(X1)
p20: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p21: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p22: mark#(U11(X1,X2,X3)) -> mark#(X1)
p23: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p24: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p25: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p10: mark#(U13(X)) -> mark#(X)
p11: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p12: active#(and(tt(),X)) -> mark#(X)
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U22(X)) -> mark#(X)
p15: mark#(U31(X1,X2)) -> active#(U31(mark(X1),X2))
p16: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p17: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p18: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p19: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p20: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p21: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p22: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p23: mark#(and(X1,X2)) -> mark#(X1)
p24: mark#(isNatKind(X)) -> active#(isNatKind(X))
p25: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = ((0,1),(0,0)) x1
U11_A(x1,x2,x3) = x2 + x3 + (2,2)
tt_A() = (1,1)
mark#_A(x1) = (2,0)
U12_A(x1,x2) = x2 + (2,2)
isNat_A(x1) = x1 + (1,2)
mark_A(x1) = x1 + (0,1)
U13_A(x1) = ((1,0),(1,0)) x1 + (1,1)
U21_A(x1,x2) = x2 + (1,2)
U22_A(x1) = (1,1)
U41_A(x1,x2,x3) = x1 + x2 + x3 + (1,2)
s_A(x1) = x1 + (0,1)
plus_A(x1,x2) = x1 + x2 + (2,2)
and_A(x1,x2) = x2 + (0,2)
U31_A(x1,x2) = x2 + (1,1)
isNatKind_A(x1) = (1,2)
active_A(x1) = x1 + (0,1)
|0|_A() = (1,1)
The next rules are strictly ordered:
p15
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p10: mark#(U13(X)) -> mark#(X)
p11: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p12: active#(and(tt(),X)) -> mark#(X)
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U22(X)) -> mark#(X)
p15: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p16: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p17: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p18: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p19: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p20: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p21: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p22: mark#(and(X1,X2)) -> mark#(X1)
p23: mark#(isNatKind(X)) -> active#(isNatKind(X))
p24: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p10: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p11: mark#(U22(X)) -> mark#(X)
p12: mark#(U21(X1,X2)) -> mark#(X1)
p13: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p14: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p15: mark#(U13(X)) -> mark#(X)
p16: mark#(isNat(X)) -> active#(isNat(X))
p17: active#(and(tt(),X)) -> mark#(X)
p18: mark#(U12(X1,X2)) -> mark#(X1)
p19: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p20: active#(U41(tt(),M,N)) -> mark#(s(plus(N,M)))
p21: mark#(U11(X1,X2,X3)) -> mark#(X1)
p22: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p23: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p24: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = ((0,1),(0,0)) x1
U11_A(x1,x2,x3) = ((0,1),(0,1)) x1 + (1,0)
tt_A() = (1,0)
mark#_A(x1) = ((0,1),(0,0)) x1
U12_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(0,0)) x2 + (1,0)
isNat_A(x1) = ((0,1),(0,0)) x1 + (1,0)
isNatKind_A(x1) = (1,0)
plus_A(x1,x2) = ((0,1),(0,1)) x1 + (1,2)
s_A(x1) = ((0,1),(0,0)) x1 + (1,1)
U41_A(x1,x2,x3) = x1 + ((0,1),(0,0)) x2 + ((0,1),(0,1)) x3 + (1,2)
and_A(x1,x2) = x1 + x2 + (1,0)
mark_A(x1) = x1 + (1,0)
U21_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (1,0)
U22_A(x1) = ((0,1),(0,1)) x1 + (1,0)
U13_A(x1) = x1 + (1,0)
active_A(x1) = x1 + (1,0)
U31_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(0,1)) x2 + (1,1)
|0|_A() = (1,1)
The next rules are strictly ordered:
p20
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p9: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p10: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p11: mark#(U22(X)) -> mark#(X)
p12: mark#(U21(X1,X2)) -> mark#(X1)
p13: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p14: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p15: mark#(U13(X)) -> mark#(X)
p16: mark#(isNat(X)) -> active#(isNat(X))
p17: active#(and(tt(),X)) -> mark#(X)
p18: mark#(U12(X1,X2)) -> mark#(X1)
p19: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p20: mark#(U11(X1,X2,X3)) -> mark#(X1)
p21: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p22: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p23: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(and(tt(),X)) -> mark#(X)
p10: mark#(U13(X)) -> mark#(X)
p11: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p12: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U22(X)) -> mark#(X)
p15: mark#(U41(X1,X2,X3)) -> active#(U41(mark(X1),X2,X3))
p16: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p17: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p18: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p19: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p20: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p21: mark#(and(X1,X2)) -> mark#(X1)
p22: mark#(isNatKind(X)) -> active#(isNatKind(X))
p23: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = x1
U11_A(x1,x2,x3) = (2,1)
tt_A() = (0,1)
mark#_A(x1) = (2,0)
U12_A(x1,x2) = x1 + (2,0)
isNat_A(x1) = (2,1)
mark_A(x1) = x1 + (1,0)
U13_A(x1) = ((0,1),(0,0)) x1 + (0,1)
U21_A(x1,x2) = (2,1)
U22_A(x1) = (1,1)
and_A(x1,x2) = x2 + (2,0)
plus_A(x1,x2) = x1 + x2 + (2,0)
isNatKind_A(x1) = (2,1)
U41_A(x1,x2,x3) = x3 + (1,0)
s_A(x1) = (1,0)
active_A(x1) = x1 + (1,0)
U31_A(x1,x2) = x2 + (1,1)
|0|_A() = (1,1)
The next rules are strictly ordered:
p15
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
p4: mark#(U11(X1,X2,X3)) -> mark#(X1)
p5: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p6: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p7: mark#(U12(X1,X2)) -> mark#(X1)
p8: mark#(isNat(X)) -> active#(isNat(X))
p9: active#(and(tt(),X)) -> mark#(X)
p10: mark#(U13(X)) -> mark#(X)
p11: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p12: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U22(X)) -> mark#(X)
p15: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p16: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p17: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p18: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p19: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p20: mark#(and(X1,X2)) -> mark#(X1)
p21: mark#(isNatKind(X)) -> active#(isNatKind(X))
p22: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: active#(plus(N,s(M))) -> mark#(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p7: mark#(plus(X1,X2)) -> active#(plus(mark(X1),mark(X2)))
p8: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p9: mark#(U22(X)) -> mark#(X)
p10: mark#(U21(X1,X2)) -> mark#(X1)
p11: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p12: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p13: mark#(U13(X)) -> mark#(X)
p14: mark#(isNat(X)) -> active#(isNat(X))
p15: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p16: mark#(U12(X1,X2)) -> mark#(X1)
p17: mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
p18: active#(and(tt(),X)) -> mark#(X)
p19: mark#(U11(X1,X2,X3)) -> mark#(X1)
p20: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p21: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p22: active#(U12(tt(),V2)) -> mark#(U13(isNat(V2)))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = x1
U11_A(x1,x2,x3) = x1 + ((1,1),(1,1)) x2 + ((1,0),(1,0)) x3 + (4,4)
tt_A() = (0,0)
mark#_A(x1) = ((0,1),(0,0)) x1
U12_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (2,3)
isNat_A(x1) = ((1,0),(1,0)) x1 + (1,1)
isNatKind_A(x1) = (0,0)
plus_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,0),(1,1)) x2 + (3,4)
s_A(x1) = x1 + (1,1)
U41_A(x1,x2,x3) = x2 + ((1,1),(0,0)) x3 + (4,1)
and_A(x1,x2) = x1 + ((1,1),(1,1)) x2
mark_A(x1) = x1
U22_A(x1) = ((0,1),(0,1)) x1 + (1,1)
U21_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (2,2)
U13_A(x1) = x1 + (1,0)
active_A(x1) = x1
U31_A(x1,x2) = ((1,1),(1,1)) x2 + (1,1)
|0|_A() = (1,1)
The next rules are strictly ordered:
p3, p7, p9, p10, p16, p17, p19, p22
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(isNatKind(X)) -> active#(isNatKind(X))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p5: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
p6: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p7: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p8: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p9: mark#(U13(X)) -> mark#(X)
p10: mark#(isNat(X)) -> active#(isNat(X))
p11: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p12: active#(and(tt(),X)) -> mark#(X)
p13: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p14: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(U11(tt(),V1,V2)) -> mark#(U12(isNat(V1),V2))
p2: mark#(U11(X1,X2,X3)) -> active#(U11(mark(X1),X2,X3))
p3: active#(U21(tt(),V1)) -> mark#(U22(isNat(V1)))
p4: mark#(isNat(X)) -> active#(isNat(X))
p5: active#(and(tt(),X)) -> mark#(X)
p6: mark#(U13(X)) -> mark#(X)
p7: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p8: active#(isNat(plus(V1,V2))) -> mark#(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
p9: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p10: active#(isNat(s(V1))) -> mark#(U21(isNatKind(V1),V1))
p11: mark#(and(X1,X2)) -> mark#(X1)
p12: mark#(isNatKind(X)) -> active#(isNatKind(X))
p13: active#(isNatKind(plus(V1,V2))) -> mark#(and(isNatKind(V1),isNatKind(V2)))
p14: active#(isNatKind(s(V1))) -> mark#(isNatKind(V1))
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
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
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = ((1,1),(0,0)) x1
U11_A(x1,x2,x3) = ((0,0),(1,1)) x3 + (3,1)
tt_A() = (0,1)
mark#_A(x1) = ((1,1),(0,0)) x1 + (1,0)
U12_A(x1,x2) = ((0,0),(1,1)) x2 + (1,1)
isNat_A(x1) = ((0,0),(1,1)) x1 + (1,1)
mark_A(x1) = ((0,0),(1,1)) x1
U21_A(x1,x2) = (1,2)
U22_A(x1) = (1,0)
and_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(0,1)) x2 + (1,1)
U13_A(x1) = ((0,0),(1,1)) x1
plus_A(x1,x2) = ((0,0),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,3)
isNatKind_A(x1) = ((1,1),(1,1)) x1 + (1,1)
s_A(x1) = ((1,1),(0,0)) x1 + (2,1)
active_A(x1) = ((0,0),(1,1)) x1
U31_A(x1,x2) = ((1,1),(0,0)) x2 + (1,1)
U41_A(x1,x2,x3) = ((1,1),(1,1)) x2 + ((0,0),(1,1)) x3 + (7,0)
|0|_A() = (1,0)
The next rules are strictly ordered:
p1, p2, p3, p4, p5, p7, p8, p9, p10, p11, p12, p13, p14
We remove them from the problem.
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: mark#(U13(X)) -> mark#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The estimated dependency graph contains the following SCCs:
{p1}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: mark#(U13(X)) -> mark#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
mark#_A(x1) = ((1,0),(1,0)) x1
U13_A(x1) = ((1,1),(1,1)) x1 + (1,0)
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
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: U12#(mark(X1),X2) -> U12#(X1,X2)
p2: U12#(X1,active(X2)) -> U12#(X1,X2)
p3: U12#(active(X1),X2) -> U12#(X1,X2)
p4: U12#(X1,mark(X2)) -> U12#(X1,X2)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
U12#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
The next rules are strictly ordered:
p1, p2, p3, p4
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: isNat#(mark(X)) -> isNat#(X)
p2: isNat#(active(X)) -> isNat#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
isNat#_A(x1) = ((1,0),(1,1)) x1
mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,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
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: U13#(mark(X)) -> U13#(X)
p2: U13#(active(X)) -> U13#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
U13#_A(x1) = ((1,0),(1,1)) x1
mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,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
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: U22#(mark(X)) -> U22#(X)
p2: U22#(active(X)) -> U22#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
U22#_A(x1) = ((1,0),(1,1)) x1
mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,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
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: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
s#_A(x1) = ((1,0),(1,1)) x1
mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,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
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#(mark(X1),X2) -> plus#(X1,X2)
p2: plus#(X1,active(X2)) -> plus#(X1,X2)
p3: plus#(active(X1),X2) -> plus#(X1,X2)
p4: plus#(X1,mark(X2)) -> plus#(X1,X2)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
plus#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
The next rules are strictly ordered:
p1, p2, p3, p4
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: U11#(mark(X1),X2,X3) -> U11#(X1,X2,X3)
p2: U11#(X1,X2,active(X3)) -> U11#(X1,X2,X3)
p3: U11#(X1,active(X2),X3) -> U11#(X1,X2,X3)
p4: U11#(active(X1),X2,X3) -> U11#(X1,X2,X3)
p5: U11#(X1,X2,mark(X3)) -> U11#(X1,X2,X3)
p6: U11#(X1,mark(X2),X3) -> U11#(X1,X2,X3)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
U11#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3
mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
The next rules are strictly ordered:
p1, p2, p3, p4, p5, p6
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
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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(X1,active(X2)) -> and#(X1,X2)
p3: and#(active(X1),X2) -> and#(X1,X2)
p4: and#(X1,mark(X2)) -> and#(X1,X2)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
and#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
The next rules are strictly ordered:
p1, p2, p3, p4
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: isNatKind#(mark(X)) -> isNatKind#(X)
p2: isNatKind#(active(X)) -> isNatKind#(X)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
isNatKind#_A(x1) = ((1,0),(1,1)) x1
mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,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
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: U21#(mark(X1),X2) -> U21#(X1,X2)
p2: U21#(X1,active(X2)) -> U21#(X1,X2)
p3: U21#(active(X1),X2) -> U21#(X1,X2)
p4: U21#(X1,mark(X2)) -> U21#(X1,X2)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
U21#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
The next rules are strictly ordered:
p1, p2, p3, p4
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: U31#(mark(X1),X2) -> U31#(X1,X2)
p2: U31#(X1,active(X2)) -> U31#(X1,X2)
p3: U31#(active(X1),X2) -> U31#(X1,X2)
p4: U31#(X1,mark(X2)) -> U31#(X1,X2)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
U31#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2
mark_A(x1) = ((0,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
The next rules are strictly ordered:
p1, p2, p3, p4
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: U41#(mark(X1),X2,X3) -> U41#(X1,X2,X3)
p2: U41#(X1,X2,active(X3)) -> U41#(X1,X2,X3)
p3: U41#(X1,active(X2),X3) -> U41#(X1,X2,X3)
p4: U41#(active(X1),X2,X3) -> U41#(X1,X2,X3)
p5: U41#(X1,X2,mark(X3)) -> U41#(X1,X2,X3)
p6: U41#(X1,mark(X2),X3) -> U41#(X1,X2,X3)
and R consists of:
r1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
r2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
r3: active(U13(tt())) -> mark(tt())
r4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
r5: active(U22(tt())) -> mark(tt())
r6: active(U31(tt(),N)) -> mark(N)
r7: active(U41(tt(),M,N)) -> mark(s(plus(N,M)))
r8: active(and(tt(),X)) -> mark(X)
r9: active(isNat(|0|())) -> mark(tt())
r10: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
r11: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
r12: active(isNatKind(|0|())) -> mark(tt())
r13: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
r14: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
r15: active(plus(N,|0|())) -> mark(U31(and(isNat(N),isNatKind(N)),N))
r16: active(plus(N,s(M))) -> mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
r17: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
r18: mark(tt()) -> active(tt())
r19: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
r20: mark(isNat(X)) -> active(isNat(X))
r21: mark(U13(X)) -> active(U13(mark(X)))
r22: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r23: mark(U22(X)) -> active(U22(mark(X)))
r24: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
r25: mark(U41(X1,X2,X3)) -> active(U41(mark(X1),X2,X3))
r26: mark(s(X)) -> active(s(mark(X)))
r27: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
r28: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r29: mark(|0|()) -> active(|0|())
r30: mark(isNatKind(X)) -> active(isNatKind(X))
r31: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
r32: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
r33: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
r34: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
r35: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
r36: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
r37: U12(mark(X1),X2) -> U12(X1,X2)
r38: U12(X1,mark(X2)) -> U12(X1,X2)
r39: U12(active(X1),X2) -> U12(X1,X2)
r40: U12(X1,active(X2)) -> U12(X1,X2)
r41: isNat(mark(X)) -> isNat(X)
r42: isNat(active(X)) -> isNat(X)
r43: U13(mark(X)) -> U13(X)
r44: U13(active(X)) -> U13(X)
r45: U21(mark(X1),X2) -> U21(X1,X2)
r46: U21(X1,mark(X2)) -> U21(X1,X2)
r47: U21(active(X1),X2) -> U21(X1,X2)
r48: U21(X1,active(X2)) -> U21(X1,X2)
r49: U22(mark(X)) -> U22(X)
r50: U22(active(X)) -> U22(X)
r51: U31(mark(X1),X2) -> U31(X1,X2)
r52: U31(X1,mark(X2)) -> U31(X1,X2)
r53: U31(active(X1),X2) -> U31(X1,X2)
r54: U31(X1,active(X2)) -> U31(X1,X2)
r55: U41(mark(X1),X2,X3) -> U41(X1,X2,X3)
r56: U41(X1,mark(X2),X3) -> U41(X1,X2,X3)
r57: U41(X1,X2,mark(X3)) -> U41(X1,X2,X3)
r58: U41(active(X1),X2,X3) -> U41(X1,X2,X3)
r59: U41(X1,active(X2),X3) -> U41(X1,X2,X3)
r60: U41(X1,X2,active(X3)) -> U41(X1,X2,X3)
r61: s(mark(X)) -> s(X)
r62: s(active(X)) -> s(X)
r63: plus(mark(X1),X2) -> plus(X1,X2)
r64: plus(X1,mark(X2)) -> plus(X1,X2)
r65: plus(active(X1),X2) -> plus(X1,X2)
r66: plus(X1,active(X2)) -> plus(X1,X2)
r67: and(mark(X1),X2) -> and(X1,X2)
r68: and(X1,mark(X2)) -> and(X1,X2)
r69: and(active(X1),X2) -> and(X1,X2)
r70: and(X1,active(X2)) -> and(X1,X2)
r71: isNatKind(mark(X)) -> isNatKind(X)
r72: isNatKind(active(X)) -> isNatKind(X)
The set of usable rules consists of
(no rules)
Take the monotone reduction pair:
matrix interpretations:
carrier: N^2
order: standard order
interpretations:
U41#_A(x1,x2,x3) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + ((1,1),(1,1)) x3
mark_A(x1) = ((1,1),(1,1)) x1 + (1,1)
active_A(x1) = ((1,1),(1,1)) x1 + (1,1)
The next rules are strictly ordered:
p1, p2, p3, p4, p5, p6
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
We remove them from the problem. Then no dependency pair remains.