Left Termination proof of /tmp/tmpYgTbtW/lessleaves.pl

Left Termination of the query pattern
lessleaves(g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 114 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 28 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 3 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 27 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPOrderProof (⇔, 80 ms)

        ↳20 QDP

        ↳21 DependencyGraphProof (⇔, 0 ms)

        ↳22 TRUE

(0) Obligation:

Clauses:

append(nil, Y, Y).
append(cons(U, V), Y, cons(U, Z)) :- append(V, Y, Z).
lessleaves(nil, cons(W, Z)).
lessleaves(cons(U, V), cons(W, Z)) :- ','(append(U, V, U1), ','(append(W, Z, W1), lessleaves(U1, W1))).

Query: lessleaves(g,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: lessleaves(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: lessleaves(T1, T2), SCOPE: 1, CLAUSE: 2 | lessleaves(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | lessleaves(nil, cons(T5, T6)), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: lessleaves(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX3 is free\nX4 is free\nlessleaves(T1, T2) !=? lessleaves(nil, cons(X3, X4))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: lessleaves(nil, cons(T5, T6)), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(append(T11, T12, X17), ','(append(T13, T14, X18), lessleaves(X17, X18)))\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(append(T11, T12, X17), ','(append(T13, T14, X18), lessleaves(X17, X18))), SCOPE: 2, CLAUSE: 0 | ','(append(T11, T12, X17), ','(append(T13, T14, X18), lessleaves(X17, X18))), SCOPE: 2, CLAUSE: 1\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(append(T11, T12, X17), ','(append(T13, T14, X18), lessleaves(X17, X18))), SCOPE: 2, CLAUSE: 0\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(append(T11, T12, X17), ','(append(T13, T14, X18), lessleaves(X17, X18))), SCOPE: 2, CLAUSE: 1\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="B: ','(append(T13, T14, X18), lessleaves(T19, X18))\n\nT13 is ground\nT14 is ground\nT19 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="D: append(T13, T14, X18)\n\nT13 is ground\nT14 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: lessleaves(T19, T22)\n\nT19 is ground\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: append(T13, T14, X18), SCOPE: 3, CLAUSE: 0 | append(T13, T14, X18), SCOPE: 3, CLAUSE: 1\n\nT13 is ground\nT14 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: append(T13, T14, X18), SCOPE: 3, CLAUSE: 0\n\nT13 is ground\nT14 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: append(T13, T14, X18), SCOPE: 3, CLAUSE: 1\n\nT13 is ground\nT14 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: append(T37, T38, X47)\n\nT37 is ground\nT38 is ground\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="C: ','(append(T52, T53, X68), ','(append(T13, T14, X18), lessleaves(cons(T51, X68), X18)))\n\nT13 is ground\nT14 is ground\nT51 is ground\nT52 is ground\nT53 is ground\nX18 is free\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: append(T52, T53, X68)\n\nT52 is ground\nT53 is ground\nX68 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(append(T13, T14, X18), lessleaves(cons(T51, T56), X18))\n\nT13 is ground\nT14 is ground\nT51 is ground\nT56 is ground\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 76 [arrowhead = none ];
76 -> 4;

77 [label="EVAL with clause\nlessleaves(nil, cons(X3, X4)).\nand substitutionT1 -> nil,\nX3 -> T5,\nX4 -> T6,\nT2 -> cons(T5, T6)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 77 [arrowhead = none ];
77 -> 9;

78 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 78 [arrowhead = none ];
78 -> 11;

79 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 79 [arrowhead = none ];
79 -> 17;

80 [label="EVAL with clause\nlessleaves(cons(X13, X14), cons(X15, X16)) :- ','(append(X13, X14, X17), ','(append(X15, X16, X18), lessleaves(X17, X18))).\nand substitutionX13 -> T11,\nX14 -> T12,\nT1 -> cons(T11, T12),\nX15 -> T13,\nX16 -> T14,\nT2 -> cons(T13, T14)", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 80 [arrowhead = none ];
80 -> 22;

81 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 81 [arrowhead = none ];
81 -> 24;

82 [label="BACKTRACK\nfor clause: lessleaves(cons(U, V), cons(W, Z)) :- ','(append(U, V, U1), ','(append(W, Z, W1), lessleaves(U1, W1)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 82 [arrowhead = none ];
82 -> 18;

83 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 83 [arrowhead = none ];
83 -> 26;

84 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 84 [arrowhead = none ];
84 -> 28;

85 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 85 [arrowhead = none ];
85 -> 30;

86 [label="EVAL with clause\nappend(nil, X23, X23).\nand substitutionT11 -> nil,\nT12 -> T19,\nX23 -> T19,\nX17 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 86 [arrowhead = none ];
86 -> 32;

87 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 87 [arrowhead = none ];
87 -> 34;

88 [label="EVAL with clause\nappend(cons(X64, X65), X66, cons(X64, X67)) :- append(X65, X66, X67).\nand substitutionX64 -> T51,\nX65 -> T52,\nT11 -> cons(T51, T52),\nT12 -> T53,\nX66 -> T53,\nX67 -> X68,\nX17 -> cons(T51, X68)", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 88 [arrowhead = none ];
88 -> 70;

89 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 89 [arrowhead = none ];
89 -> 71;

90 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
32 -> 90 [arrowhead = none ];
90 -> 40;

91 [label="SPLIT 2\nnew knowledge:\nT13 is ground\nT14 is ground\nT22 is ground\nreplacements:X18 -> T22", fontsize=14, style = filled, fillcolor = violet];
32 -> 91 [arrowhead = none ];
91 -> 41;

92 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 92 [arrowhead = none ];
92 -> 46;

93 [label="INSTANCE with matching:\nT1 -> T19\nT2 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
41 -> 93 [arrowhead = none , style=dashed];
93 -> 2[style=dashed];

94 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 94 [arrowhead = none ];
94 -> 47;

95 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 95 [arrowhead = none ];
95 -> 48;

96 [label="EVAL with clause\nappend(nil, X32, X32).\nand substitutionT13 -> nil,\nT14 -> T29,\nX32 -> T29,\nX18 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 96 [arrowhead = none ];
96 -> 52;

97 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 97 [arrowhead = none ];
97 -> 53;

98 [label="EVAL with clause\nappend(cons(X43, X44), X45, cons(X43, X46)) :- append(X44, X45, X46).\nand substitutionX43 -> T36,\nX44 -> T37,\nT13 -> cons(T36, T37),\nT14 -> T38,\nX45 -> T38,\nX46 -> X47,\nX18 -> cons(T36, X47)", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 98 [arrowhead = none ];
98 -> 62;

99 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 99 [arrowhead = none ];
99 -> 63;

100 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 100 [arrowhead = none ];
100 -> 54;

101 [label="INSTANCE with matching:\nT13 -> T37\nT14 -> T38\nX18 -> X47", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 101 [arrowhead = none , style=dashed];
101 -> 40[style=dashed];

102 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
70 -> 102 [arrowhead = none ];
102 -> 74;

103 [label="SPLIT 2\nnew knowledge:\nT52 is ground\nT53 is ground\nT56 is ground\nreplacements:X68 -> T56", fontsize=14, style = filled, fillcolor = violet];
70 -> 103 [arrowhead = none ];
103 -> 75;

104 [label="INSTANCE with matching:\nT13 -> T52\nT14 -> T53\nX18 -> X68", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 104 [arrowhead = none , style=dashed];
104 -> 40[style=dashed];

105 [label="INSTANCE with matching:\nT19 -> cons(T51, T56)", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 105 [arrowhead = none , style=dashed];
105 -> 32[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

lessleavesA_in_gg(nil, cons(T5, T6)) → lessleavesA_out_gg(nil, cons(T5, T6))
lessleavesA_in_gg(cons(nil, T19), cons(T13, T14)) → U1_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, T22, T19) → U4_ggag(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
appendD_in_gga(nil, T29, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U3_gga(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
U3_gga(T36, T37, T38, X47, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))
U4_ggag(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → U5_ggag(T13, T14, T22, T19, lessleavesA_in_gg(T19, T22))
lessleavesA_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U2_gg(T51, T52, T53, T13, T14, pC_in_ggaggag(T52, T53, X68, T13, T14, X18, T51))
pC_in_ggaggag(T52, T53, T56, T13, T14, X18, T51) → U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → pC_out_ggaggag(T52, T53, T56, T13, T14, X18, T51)
U2_gg(T51, T52, T53, T13, T14, pC_out_ggaggag(T52, T53, X68, T13, T14, X18, T51)) → lessleavesA_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U5_ggag(T13, T14, T22, T19, lessleavesA_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U1_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesA_out_gg(cons(nil, T19), cons(T13, T14))

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → U1_GG(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, T22, T19) → U4_GGAG(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
PB_IN_GGAG(T13, T14, T22, T19) → APPENDD_IN_GGA(T13, T14, T22)
APPENDD_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → U3_GGA(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
APPENDD_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDD_IN_GGA(T37, T38, X47)
U4_GGAG(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → U5_GGAG(T13, T14, T22, T19, lessleavesA_in_gg(T19, T22))
U4_GGAG(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → LESSLEAVESA_IN_GG(T19, T22)
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U2_GG(T51, T52, T53, T13, T14, pC_in_ggaggag(T52, T53, X68, T13, T14, X18, T51))
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → PC_IN_GGAGGAG(T52, T53, X68, T13, T14, X18, T51)
PC_IN_GGAGGAG(T52, T53, T56, T13, T14, X18, T51) → U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
PC_IN_GGAGGAG(T52, T53, T56, T13, T14, X18, T51) → APPENDD_IN_GGA(T52, T53, T56)
U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → U7_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))

The TRS R consists of the following rules:

lessleavesA_in_gg(nil, cons(T5, T6)) → lessleavesA_out_gg(nil, cons(T5, T6))
lessleavesA_in_gg(cons(nil, T19), cons(T13, T14)) → U1_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, T22, T19) → U4_ggag(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
appendD_in_gga(nil, T29, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U3_gga(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
U3_gga(T36, T37, T38, X47, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))
U4_ggag(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → U5_ggag(T13, T14, T22, T19, lessleavesA_in_gg(T19, T22))
lessleavesA_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U2_gg(T51, T52, T53, T13, T14, pC_in_ggaggag(T52, T53, X68, T13, T14, X18, T51))
pC_in_ggaggag(T52, T53, T56, T13, T14, X18, T51) → U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → pC_out_ggaggag(T52, T53, T56, T13, T14, X18, T51)
U2_gg(T51, T52, T53, T13, T14, pC_out_ggaggag(T52, T53, X68, T13, T14, X18, T51)) → lessleavesA_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U5_ggag(T13, T14, T22, T19, lessleavesA_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U1_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesA_out_gg(cons(nil, T19), cons(T13, T14))

The argument filtering Pi contains the following mapping:
lessleavesA_in_gg(x1, x2) = lessleavesA_in_gg(x1, x2)
nil = nil
cons(x1, x2) = cons(x1, x2)
lessleavesA_out_gg(x1, x2) = lessleavesA_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4) = U1_gg(x1, x2, x3, x4)
pB_in_ggag(x1, x2, x3, x4) = pB_in_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5) = U4_ggag(x1, x2, x4, x5)
appendD_in_gga(x1, x2, x3) = appendD_in_gga(x1, x2)
appendD_out_gga(x1, x2, x3) = appendD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
U5_ggag(x1, x2, x3, x4, x5) = U5_ggag(x1, x2, x3, x4, x5)
U2_gg(x1, x2, x3, x4, x5, x6) = U2_gg(x1, x2, x3, x4, x5, x6)
pC_in_ggaggag(x1, x2, x3, x4, x5, x6, x7) = pC_in_ggaggag(x1, x2, x4, x5, x7)
U6_ggaggag(x1, x2, x3, x4, x5, x6, x7, x8) = U6_ggaggag(x1, x2, x4, x5, x7, x8)
U7_ggaggag(x1, x2, x3, x4, x5, x6, x7, x8) = U7_ggaggag(x1, x2, x3, x4, x5, x7, x8)
pB_out_ggag(x1, x2, x3, x4) = pB_out_ggag(x1, x2, x3, x4)
pC_out_ggaggag(x1, x2, x3, x4, x5, x6, x7) = pC_out_ggaggag(x1, x2, x3, x4, x5, x6, x7)
LESSLEAVESA_IN_GG(x1, x2) = LESSLEAVESA_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4) = U1_GG(x1, x2, x3, x4)
PB_IN_GGAG(x1, x2, x3, x4) = PB_IN_GGAG(x1, x2, x4)
U4_GGAG(x1, x2, x3, x4, x5) = U4_GGAG(x1, x2, x4, x5)
APPENDD_IN_GGA(x1, x2, x3) = APPENDD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U5_GGAG(x1, x2, x3, x4, x5) = U5_GGAG(x1, x2, x3, x4, x5)
U2_GG(x1, x2, x3, x4, x5, x6) = U2_GG(x1, x2, x3, x4, x5, x6)
PC_IN_GGAGGAG(x1, x2, x3, x4, x5, x6, x7) = PC_IN_GGAGGAG(x1, x2, x4, x5, x7)
U6_GGAGGAG(x1, x2, x3, x4, x5, x6, x7, x8) = U6_GGAGGAG(x1, x2, x4, x5, x7, x8)
U7_GGAGGAG(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GGAGGAG(x1, x2, x3, x4, x5, x7, x8)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → U1_GG(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, T22, T19) → U4_GGAG(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
PB_IN_GGAG(T13, T14, T22, T19) → APPENDD_IN_GGA(T13, T14, T22)
APPENDD_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → U3_GGA(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
APPENDD_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDD_IN_GGA(T37, T38, X47)
U4_GGAG(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → U5_GGAG(T13, T14, T22, T19, lessleavesA_in_gg(T19, T22))
U4_GGAG(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → LESSLEAVESA_IN_GG(T19, T22)
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → U2_GG(T51, T52, T53, T13, T14, pC_in_ggaggag(T52, T53, X68, T13, T14, X18, T51))
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → PC_IN_GGAGGAG(T52, T53, X68, T13, T14, X18, T51)
PC_IN_GGAGGAG(T52, T53, T56, T13, T14, X18, T51) → U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
PC_IN_GGAGGAG(T52, T53, T56, T13, T14, X18, T51) → APPENDD_IN_GGA(T52, T53, T56)
U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → U7_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))

The TRS R consists of the following rules:

lessleavesA_in_gg(nil, cons(T5, T6)) → lessleavesA_out_gg(nil, cons(T5, T6))
lessleavesA_in_gg(cons(nil, T19), cons(T13, T14)) → U1_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, T22, T19) → U4_ggag(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
appendD_in_gga(nil, T29, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U3_gga(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
U3_gga(T36, T37, T38, X47, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))
U4_ggag(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → U5_ggag(T13, T14, T22, T19, lessleavesA_in_gg(T19, T22))
lessleavesA_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U2_gg(T51, T52, T53, T13, T14, pC_in_ggaggag(T52, T53, X68, T13, T14, X18, T51))
pC_in_ggaggag(T52, T53, T56, T13, T14, X18, T51) → U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → pC_out_ggaggag(T52, T53, T56, T13, T14, X18, T51)
U2_gg(T51, T52, T53, T13, T14, pC_out_ggaggag(T52, T53, X68, T13, T14, X18, T51)) → lessleavesA_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U5_ggag(T13, T14, T22, T19, lessleavesA_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U1_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesA_out_gg(cons(nil, T19), cons(T13, T14))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDD_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDD_IN_GGA(T37, T38, X47)

The TRS R consists of the following rules:

lessleavesA_in_gg(nil, cons(T5, T6)) → lessleavesA_out_gg(nil, cons(T5, T6))
lessleavesA_in_gg(cons(nil, T19), cons(T13, T14)) → U1_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, T22, T19) → U4_ggag(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
appendD_in_gga(nil, T29, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U3_gga(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
U3_gga(T36, T37, T38, X47, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))
U4_ggag(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → U5_ggag(T13, T14, T22, T19, lessleavesA_in_gg(T19, T22))
lessleavesA_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U2_gg(T51, T52, T53, T13, T14, pC_in_ggaggag(T52, T53, X68, T13, T14, X18, T51))
pC_in_ggaggag(T52, T53, T56, T13, T14, X18, T51) → U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → pC_out_ggaggag(T52, T53, T56, T13, T14, X18, T51)
U2_gg(T51, T52, T53, T13, T14, pC_out_ggaggag(T52, T53, X68, T13, T14, X18, T51)) → lessleavesA_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U5_ggag(T13, T14, T22, T19, lessleavesA_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U1_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesA_out_gg(cons(nil, T19), cons(T13, T14))

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPENDD_IN_GGA(cons(T36, T37), T38, cons(T36, X47)) → APPENDD_IN_GGA(T37, T38, X47)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
APPENDD_IN_GGA(x1, x2, x3) = APPENDD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPENDD_IN_GGA(cons(T36, T37), T38) → APPENDD_IN_GGA(T37, T38)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APPENDD_IN_GGA(cons(T36, T37), T38) → APPENDD_IN_GGA(T37, T38)
The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, T22, T19) → U4_GGAG(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
U4_GGAG(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → LESSLEAVESA_IN_GG(T19, T22)
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → PC_IN_GGAGGAG(T52, T53, X68, T13, T14, X18, T51)
PC_IN_GGAGGAG(T52, T53, T56, T13, T14, X18, T51) → U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))

The TRS R consists of the following rules:

lessleavesA_in_gg(nil, cons(T5, T6)) → lessleavesA_out_gg(nil, cons(T5, T6))
lessleavesA_in_gg(cons(nil, T19), cons(T13, T14)) → U1_gg(T19, T13, T14, pB_in_ggag(T13, T14, X18, T19))
pB_in_ggag(T13, T14, T22, T19) → U4_ggag(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
appendD_in_gga(nil, T29, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U3_gga(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
U3_gga(T36, T37, T38, X47, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))
U4_ggag(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → U5_ggag(T13, T14, T22, T19, lessleavesA_in_gg(T19, T22))
lessleavesA_in_gg(cons(cons(T51, T52), T53), cons(T13, T14)) → U2_gg(T51, T52, T53, T13, T14, pC_in_ggaggag(T52, T53, X68, T13, T14, X18, T51))
pC_in_ggaggag(T52, T53, T56, T13, T14, X18, T51) → U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
U6_ggaggag(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_in_ggag(T13, T14, X18, cons(T51, T56)))
U7_ggaggag(T52, T53, T56, T13, T14, X18, T51, pB_out_ggag(T13, T14, X18, cons(T51, T56))) → pC_out_ggaggag(T52, T53, T56, T13, T14, X18, T51)
U2_gg(T51, T52, T53, T13, T14, pC_out_ggaggag(T52, T53, X68, T13, T14, X18, T51)) → lessleavesA_out_gg(cons(cons(T51, T52), T53), cons(T13, T14))
U5_ggag(T13, T14, T22, T19, lessleavesA_out_gg(T19, T22)) → pB_out_ggag(T13, T14, T22, T19)
U1_gg(T19, T13, T14, pB_out_ggag(T13, T14, X18, T19)) → lessleavesA_out_gg(cons(nil, T19), cons(T13, T14))

The argument filtering Pi contains the following mapping:
lessleavesA_in_gg(x1, x2) = lessleavesA_in_gg(x1, x2)
nil = nil
cons(x1, x2) = cons(x1, x2)
lessleavesA_out_gg(x1, x2) = lessleavesA_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4) = U1_gg(x1, x2, x3, x4)
pB_in_ggag(x1, x2, x3, x4) = pB_in_ggag(x1, x2, x4)
U4_ggag(x1, x2, x3, x4, x5) = U4_ggag(x1, x2, x4, x5)
appendD_in_gga(x1, x2, x3) = appendD_in_gga(x1, x2)
appendD_out_gga(x1, x2, x3) = appendD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
U5_ggag(x1, x2, x3, x4, x5) = U5_ggag(x1, x2, x3, x4, x5)
U2_gg(x1, x2, x3, x4, x5, x6) = U2_gg(x1, x2, x3, x4, x5, x6)
pC_in_ggaggag(x1, x2, x3, x4, x5, x6, x7) = pC_in_ggaggag(x1, x2, x4, x5, x7)
U6_ggaggag(x1, x2, x3, x4, x5, x6, x7, x8) = U6_ggaggag(x1, x2, x4, x5, x7, x8)
U7_ggaggag(x1, x2, x3, x4, x5, x6, x7, x8) = U7_ggaggag(x1, x2, x3, x4, x5, x7, x8)
pB_out_ggag(x1, x2, x3, x4) = pB_out_ggag(x1, x2, x3, x4)
pC_out_ggaggag(x1, x2, x3, x4, x5, x6, x7) = pC_out_ggaggag(x1, x2, x3, x4, x5, x6, x7)
LESSLEAVESA_IN_GG(x1, x2) = LESSLEAVESA_IN_GG(x1, x2)
PB_IN_GGAG(x1, x2, x3, x4) = PB_IN_GGAG(x1, x2, x4)
U4_GGAG(x1, x2, x3, x4, x5) = U4_GGAG(x1, x2, x4, x5)
PC_IN_GGAGGAG(x1, x2, x3, x4, x5, x6, x7) = PC_IN_GGAGGAG(x1, x2, x4, x5, x7)
U6_GGAGGAG(x1, x2, x3, x4, x5, x6, x7, x8) = U6_GGAGGAG(x1, x2, x4, x5, x7, x8)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, X18, T19)
PB_IN_GGAG(T13, T14, T22, T19) → U4_GGAG(T13, T14, T22, T19, appendD_in_gga(T13, T14, T22))
U4_GGAG(T13, T14, T22, T19, appendD_out_gga(T13, T14, T22)) → LESSLEAVESA_IN_GG(T19, T22)
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → PC_IN_GGAGGAG(T52, T53, X68, T13, T14, X18, T51)
PC_IN_GGAGGAG(T52, T53, T56, T13, T14, X18, T51) → U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_in_gga(T52, T53, T56))
U6_GGAGGAG(T52, T53, T56, T13, T14, X18, T51, appendD_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, X18, cons(T51, T56))

The TRS R consists of the following rules:

appendD_in_gga(nil, T29, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38, cons(T36, X47)) → U3_gga(T36, T37, T38, X47, appendD_in_gga(T37, T38, X47))
U3_gga(T36, T37, T38, X47, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))

The argument filtering Pi contains the following mapping:
nil = nil
cons(x1, x2) = cons(x1, x2)
appendD_in_gga(x1, x2, x3) = appendD_in_gga(x1, x2)
appendD_out_gga(x1, x2, x3) = appendD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
LESSLEAVESA_IN_GG(x1, x2) = LESSLEAVESA_IN_GG(x1, x2)
PB_IN_GGAG(x1, x2, x3, x4) = PB_IN_GGAG(x1, x2, x4)
U4_GGAG(x1, x2, x3, x4, x5) = U4_GGAG(x1, x2, x4, x5)
PC_IN_GGAGGAG(x1, x2, x3, x4, x5, x6, x7) = PC_IN_GGAGGAG(x1, x2, x4, x5, x7)
U6_GGAGGAG(x1, x2, x3, x4, x5, x6, x7, x8) = U6_GGAGGAG(x1, x2, x4, x5, x7, x8)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, T19)
PB_IN_GGAG(T13, T14, T19) → U4_GGAG(T13, T14, T19, appendD_in_gga(T13, T14))
U4_GGAG(T13, T14, T19, appendD_out_gga(T13, T14, T22)) → LESSLEAVESA_IN_GG(T19, T22)
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → PC_IN_GGAGGAG(T52, T53, T13, T14, T51)
PC_IN_GGAGGAG(T52, T53, T13, T14, T51) → U6_GGAGGAG(T52, T53, T13, T14, T51, appendD_in_gga(T52, T53))
U6_GGAGGAG(T52, T53, T13, T14, T51, appendD_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, cons(T51, T56))

The TRS R consists of the following rules:

appendD_in_gga(nil, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38) → U3_gga(T36, T37, T38, appendD_in_gga(T37, T38))
U3_gga(T36, T37, T38, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))

The set Q consists of the following terms:

appendD_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

LESSLEAVESA_IN_GG(cons(nil, T19), cons(T13, T14)) → PB_IN_GGAG(T13, T14, T19)
LESSLEAVESA_IN_GG(cons(cons(T51, T52), T53), cons(T13, T14)) → PC_IN_GGAGGAG(T52, T53, T13, T14, T51)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(LESSLEAVESA_IN_GG(x₁, x₂)) = x₂
POL(PB_IN_GGAG(x₁, x₂, x₃)) = x₁ + x₂
POL(PC_IN_GGAGGAG(x₁, x₂, x₃, x₄, x₅)) = x₃ + x₄
POL(U3_gga(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₄
POL(U4_GGAG(x₁, x₂, x₃, x₄)) = x₄
POL(U6_GGAGGAG(x₁, x₂, x₃, x₄, x₅, x₆)) = x₃ + x₄
POL(appendD_in_gga(x₁, x₂)) = x₁ + x₂
POL(appendD_out_gga(x₁, x₂, x₃)) = x₃
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(nil) = 0

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

appendD_in_gga(nil, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38) → U3_gga(T36, T37, T38, appendD_in_gga(T37, T38))
U3_gga(T36, T37, T38, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PB_IN_GGAG(T13, T14, T19) → U4_GGAG(T13, T14, T19, appendD_in_gga(T13, T14))
U4_GGAG(T13, T14, T19, appendD_out_gga(T13, T14, T22)) → LESSLEAVESA_IN_GG(T19, T22)
PC_IN_GGAGGAG(T52, T53, T13, T14, T51) → U6_GGAGGAG(T52, T53, T13, T14, T51, appendD_in_gga(T52, T53))
U6_GGAGGAG(T52, T53, T13, T14, T51, appendD_out_gga(T52, T53, T56)) → PB_IN_GGAG(T13, T14, cons(T51, T56))

The TRS R consists of the following rules:

appendD_in_gga(nil, T29) → appendD_out_gga(nil, T29, T29)
appendD_in_gga(cons(T36, T37), T38) → U3_gga(T36, T37, T38, appendD_in_gga(T37, T38))
U3_gga(T36, T37, T38, appendD_out_gga(T37, T38, X47)) → appendD_out_gga(cons(T36, T37), T38, cons(T36, X47))

The set Q consists of the following terms:

appendD_in_gga(x0, x1)
U3_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPOrderProof (EQUIVALENT transformation)

(20) Obligation:

(21) DependencyGraphProof (EQUIVALENT transformation)

(22) TRUE