Left Termination proof of /tmp/tmp0

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 140 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 114 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 MRRProof (⇔, 4 ms)

        ↳27 QDP

        ↳28 PisEmptyProof (⇔, 0 ms)

        ↳29 YES

    ↳30 PiDP

        ↳31 UsableRulesProof (⇔, 7 ms)

        ↳32 PiDP

        ↳33 PiDPToQDPProof (⇒, 0 ms)

        ↳34 QDP

        ↳35 QDPOrderProof (⇔, 129 ms)

        ↳36 QDP

        ↳37 DependencyGraphProof (⇔, 0 ms)

        ↳38 TRUE

(0) Obligation:

Clauses:

factor(cons(X, nil), X).
factor(cons(X, cons(Y, Xs)), T) :- ','(times(X, Y, Z), factor(cons(Z, Xs), T)).
times(0, X_, 0).
times(s(X), Y, Z) :- ','(times(X, Y, XY), plus(XY, Y, Z)).
plus(0, X, X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).

Query: factor(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: factor(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: factor(T1, T2), SCOPE: 1, CLAUSE: 0 | factor(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | factor(cons(T4, nil), T2), SCOPE: 1, CLAUSE: 1\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: factor(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX2 is free\nfactor(T1, T2) !=? factor(cons(X2, nil), X2)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: factor(cons(T4, nil), T2), SCOPE: 1, CLAUSE: 1\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(times(T10, T11, X15), factor(cons(X15, T12), T14))\n\nT10 is ground\nT11 is ground\nT12 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(times(T10, T11, X15), factor(cons(X15, T12), T14)), SCOPE: 2, CLAUSE: 2 | ','(times(T10, T11, X15), factor(cons(X15, T12), T14)), SCOPE: 2, CLAUSE: 3\n\nT10 is ground\nT11 is ground\nT12 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(times(T10, T11, X15), factor(cons(X15, T12), T14)), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nT11 is ground\nT12 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(times(T10, T11, X15), factor(cons(X15, T12), T14)), SCOPE: 2, CLAUSE: 3\n\nT10 is ground\nT11 is ground\nT12 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: factor(cons(0, T12), T14)\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="B: ','(','(times(T24, T25, X35), plus(X35, T25, X36)), factor(cons(X36, T12), T14))\n\nT12 is ground\nT24 is ground\nT25 is ground\nX36 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="C: times(T24, T25, X35)\n\nT24 is ground\nT25 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="F: ','(plus(T28, T25, X36), factor(cons(X36, T12), T14))\n\nT12 is ground\nT25 is ground\nT28 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: times(T24, T25, X35), SCOPE: 3, CLAUSE: 2 | times(T24, T25, X35), SCOPE: 3, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: times(T24, T25, X35), SCOPE: 3, CLAUSE: 2\n\nT24 is ground\nT25 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: times(T24, T25, X35), SCOPE: 3, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="D: ','(times(T40, T41, X58), plus(X58, T41, X59))\n\nT40 is ground\nT41 is ground\nX59 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: times(T40, T41, X58)\n\nT40 is ground\nT41 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="E: plus(T44, T41, X59)\n\nT41 is ground\nT44 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: plus(T44, T41, X59), SCOPE: 4, CLAUSE: 4 | plus(T44, T41, X59), SCOPE: 4, CLAUSE: 5\n\nT41 is ground\nT44 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: plus(T44, T41, X59), SCOPE: 4, CLAUSE: 4\n\nT41 is ground\nT44 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: plus(T44, T41, X59), SCOPE: 4, CLAUSE: 5\n\nT41 is ground\nT44 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: plus(T58, T59, X82)\n\nT58 is ground\nT59 is ground\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: plus(T28, T25, X36)\n\nT25 is ground\nT28 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: factor(cons(T64, T12), T14)\n\nT12 is ground\nT64 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 94 [arrowhead = none ];
94 -> 5;

95 [label="EVAL with clause\nfactor(cons(X2, nil), X2).\nand substitutionX2 -> T4,\nT1 -> cons(T4, nil),\nT2 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 95 [arrowhead = none ];
95 -> 10;

96 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 96 [arrowhead = none ];
96 -> 13;

97 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 97 [arrowhead = none ];
97 -> 16;

98 [label="EVAL with clause\nfactor(cons(X11, cons(X12, X13)), X14) :- ','(times(X11, X12, X15), factor(cons(X15, X13), X14)).\nand substitutionX11 -> T10,\nX12 -> T11,\nX13 -> T12,\nT1 -> cons(T10, cons(T11, T12)),\nT2 -> T14,\nX14 -> T14,\nT13 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 98 [arrowhead = none ];
98 -> 22;

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

100 [label="BACKTRACK\nfor clause: factor(cons(X, cons(Y, Xs)), T) :- ','(times(X, Y, Z), factor(cons(Z, Xs), T))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 100 [arrowhead = none ];
100 -> 18;

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

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

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

104 [label="EVAL with clause\ntimes(0, X20, 0).\nand substitutionT10 -> 0,\nT11 -> T19,\nX20 -> T19,\nX15 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 104 [arrowhead = none ];
104 -> 32;

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

106 [label="EVAL with clause\ntimes(s(X32), X33, X34) :- ','(times(X32, X33, X35), plus(X35, X33, X34)).\nand substitutionX32 -> T24,\nT10 -> s(T24),\nT11 -> T25,\nX33 -> T25,\nX15 -> X36,\nX34 -> X36", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 106 [arrowhead = none ];
106 -> 39;

107 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 107 [arrowhead = none ];
107 -> 40;

108 [label="INSTANCE with matching:\nT1 -> cons(0, T12)\nT2 -> T14", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 108 [arrowhead = none , style=dashed];
108 -> 3[style=dashed];

109 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
39 -> 109 [arrowhead = none ];
109 -> 46;

110 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT25 is ground\nT28 is ground\nreplacements:X35 -> T28", fontsize=14, style = filled, fillcolor = violet];
39 -> 110 [arrowhead = none ];
110 -> 47;

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

112 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
47 -> 112 [arrowhead = none ];
112 -> 92;

113 [label="SPLIT 2\nnew knowledge:\nT28 is ground\nT25 is ground\nT64 is ground\nreplacements:X36 -> T64", fontsize=14, style = filled, fillcolor = violet];
47 -> 113 [arrowhead = none ];
113 -> 93;

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

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

116 [label="EVAL with clause\ntimes(0, X45, 0).\nand substitutionT24 -> 0,\nT25 -> T35,\nX45 -> T35,\nX35 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 116 [arrowhead = none ];
116 -> 55;

117 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 117 [arrowhead = none ];
117 -> 56;

118 [label="EVAL with clause\ntimes(s(X55), X56, X57) :- ','(times(X55, X56, X58), plus(X58, X56, X57)).\nand substitutionX55 -> T40,\nT24 -> s(T40),\nT25 -> T41,\nX56 -> T41,\nX35 -> X59,\nX57 -> X59", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 118 [arrowhead = none ];
118 -> 64;

119 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 119 [arrowhead = none ];
119 -> 66;

120 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 120 [arrowhead = none ];
120 -> 57;

121 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
64 -> 121 [arrowhead = none ];
121 -> 76;

122 [label="SPLIT 2\nnew knowledge:\nT40 is ground\nT41 is ground\nT44 is ground\nreplacements:X58 -> T44", fontsize=14, style = filled, fillcolor = violet];
64 -> 122 [arrowhead = none ];
122 -> 77;

123 [label="INSTANCE with matching:\nT24 -> T40\nT25 -> T41\nX35 -> X58", fontsize=14, style = filled, fillcolor = lightgrey];
76 -> 123 [arrowhead = none , style=dashed];
123 -> 46[style=dashed];

124 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
77 -> 124 [arrowhead = none ];
124 -> 78;

125 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
78 -> 125 [arrowhead = none ];
125 -> 80;

126 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
78 -> 126 [arrowhead = none ];
126 -> 81;

127 [label="EVAL with clause\nplus(0, X70, X70).\nand substitutionT44 -> 0,\nT41 -> T53,\nX70 -> T53,\nX59 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 127 [arrowhead = none ];
127 -> 83;

128 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 128 [arrowhead = none ];
128 -> 84;

129 [label="EVAL with clause\nplus(s(X79), X80, s(X81)) :- plus(X79, X80, X81).\nand substitutionX79 -> T58,\nT44 -> s(T58),\nT41 -> T59,\nX80 -> T59,\nX81 -> X82,\nX59 -> s(X82)", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 129 [arrowhead = none ];
129 -> 88;

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

131 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 131 [arrowhead = none ];
131 -> 85;

132 [label="INSTANCE with matching:\nT44 -> T58\nT41 -> T59\nX59 -> X82", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 132 [arrowhead = none , style=dashed];
132 -> 77[style=dashed];

133 [label="INSTANCE with matching:\nT44 -> T28\nT41 -> T25\nX59 -> X36", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 133 [arrowhead = none , style=dashed];
133 -> 77[style=dashed];

134 [label="INSTANCE with matching:\nT1 -> cons(T64, T12)\nT2 -> T14", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 134 [arrowhead = none , style=dashed];
134 -> 3[style=dashed];

}

(2) Obligation:

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

factorA_in_ga(cons(T4, nil), T4) → factorA_out_ga(cons(T4, nil), T4)
factorA_in_ga(cons(0, cons(T19, T12)), T14) → U1_ga(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
factorA_in_ga(cons(s(T24), cons(T25, T12)), T14) → U2_ga(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
pB_in_ggaaga(T24, T25, T28, X36, T12, T14) → U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
pF_in_ggaga(T28, T25, T64, T12, T14) → U7_ggaga(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_ggaga(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_ggaga(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U8_ggaga(T28, T25, T64, T12, T14, factorA_out_ga(cons(T64, T12), T14)) → pF_out_ggaga(T28, T25, T64, T12, T14)
U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_out_ggaga(T28, T25, X36, T12, T14)) → pB_out_ggaaga(T24, T25, T28, X36, T12, T14)
U2_ga(T24, T25, T12, T14, pB_out_ggaaga(T24, T25, X35, X36, T12, T14)) → factorA_out_ga(cons(s(T24), cons(T25, T12)), T14)
U1_ga(T19, T12, T14, factorA_out_ga(cons(0, T12), T14)) → factorA_out_ga(cons(0, cons(T19, T12)), 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:

FACTORA_IN_GA(cons(0, cons(T19, T12)), T14) → U1_GA(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
FACTORA_IN_GA(cons(0, cons(T19, T12)), T14) → FACTORA_IN_GA(cons(0, T12), T14)
FACTORA_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U2_GA(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
FACTORA_IN_GA(cons(s(T24), cons(T25, T12)), T14) → PB_IN_GGAAGA(T24, T25, X35, X36, T12, T14)
PB_IN_GGAAGA(T24, T25, T28, X36, T12, T14) → U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
PB_IN_GGAAGA(T24, T25, T28, X36, T12, T14) → TIMESC_IN_GGA(T24, T25, T28)
TIMESC_IN_GGA(s(T40), T41, X59) → U3_GGA(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
TIMESC_IN_GGA(s(T40), T41, X59) → PD_IN_GGAA(T40, T41, X58, X59)
PD_IN_GGAA(T40, T41, T44, X59) → U9_GGAA(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
PD_IN_GGAA(T40, T41, T44, X59) → TIMESC_IN_GGA(T40, T41, T44)
U9_GGAA(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_GGAA(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
U9_GGAA(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → PLUSE_IN_GGA(T44, T41, X59)
PLUSE_IN_GGA(s(T58), T59, s(X82)) → U4_GGA(T58, T59, X82, plusE_in_gga(T58, T59, X82))
PLUSE_IN_GGA(s(T58), T59, s(X82)) → PLUSE_IN_GGA(T58, T59, X82)
U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_GGAAGA(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → PF_IN_GGAGA(T28, T25, X36, T12, T14)
PF_IN_GGAGA(T28, T25, T64, T12, T14) → U7_GGAGA(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
PF_IN_GGAGA(T28, T25, T64, T12, T14) → PLUSE_IN_GGA(T28, T25, T64)
U7_GGAGA(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_GGAGA(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U7_GGAGA(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → FACTORA_IN_GA(cons(T64, T12), T14)

The TRS R consists of the following rules:

factorA_in_ga(cons(T4, nil), T4) → factorA_out_ga(cons(T4, nil), T4)
factorA_in_ga(cons(0, cons(T19, T12)), T14) → U1_ga(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
factorA_in_ga(cons(s(T24), cons(T25, T12)), T14) → U2_ga(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
pB_in_ggaaga(T24, T25, T28, X36, T12, T14) → U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
pF_in_ggaga(T28, T25, T64, T12, T14) → U7_ggaga(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_ggaga(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_ggaga(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U8_ggaga(T28, T25, T64, T12, T14, factorA_out_ga(cons(T64, T12), T14)) → pF_out_ggaga(T28, T25, T64, T12, T14)
U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_out_ggaga(T28, T25, X36, T12, T14)) → pB_out_ggaaga(T24, T25, T28, X36, T12, T14)
U2_ga(T24, T25, T12, T14, pB_out_ggaaga(T24, T25, X35, X36, T12, T14)) → factorA_out_ga(cons(s(T24), cons(T25, T12)), T14)
U1_ga(T19, T12, T14, factorA_out_ga(cons(0, T12), T14)) → factorA_out_ga(cons(0, cons(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factorA_in_ga(x1, x2) = factorA_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factorA_out_ga(x1, x2) = factorA_out_ga(x1, x2)
0 = 0
U1_ga(x1, x2, x3, x4) = U1_ga(x1, x2, x4)
s(x1) = s(x1)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x3, x5)
pB_in_ggaaga(x1, x2, x3, x4, x5, x6) = pB_in_ggaaga(x1, x2, x5)
U5_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U5_ggaaga(x1, x2, x5, x7)
timesC_in_gga(x1, x2, x3) = timesC_in_gga(x1, x2)
timesC_out_gga(x1, x2, x3) = timesC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4) = pD_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5) = U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5) = U10_ggaa(x1, x2, x3, x5)
plusE_in_gga(x1, x2, x3) = plusE_in_gga(x1, x2)
plusE_out_gga(x1, x2, x3) = plusE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4) = U4_gga(x1, x2, x4)
pD_out_ggaa(x1, x2, x3, x4) = pD_out_ggaa(x1, x2, x3, x4)
U6_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U6_ggaaga(x1, x2, x3, x5, x7)
pF_in_ggaga(x1, x2, x3, x4, x5) = pF_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6) = U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6) = U8_ggaga(x1, x2, x3, x4, x6)
pF_out_ggaga(x1, x2, x3, x4, x5) = pF_out_ggaga(x1, x2, x3, x4, x5)
pB_out_ggaaga(x1, x2, x3, x4, x5, x6) = pB_out_ggaaga(x1, x2, x3, x4, x5, x6)
FACTORA_IN_GA(x1, x2) = FACTORA_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x3, x5)
PB_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PB_IN_GGAAGA(x1, x2, x5)
U5_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U5_GGAAGA(x1, x2, x5, x7)
TIMESC_IN_GGA(x1, x2, x3) = TIMESC_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
PD_IN_GGAA(x1, x2, x3, x4) = PD_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4, x5) = U9_GGAA(x1, x2, x5)
U10_GGAA(x1, x2, x3, x4, x5) = U10_GGAA(x1, x2, x3, x5)
PLUSE_IN_GGA(x1, x2, x3) = PLUSE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4) = U4_GGA(x1, x2, x4)
U6_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U6_GGAAGA(x1, x2, x3, x5, x7)
PF_IN_GGAGA(x1, x2, x3, x4, x5) = PF_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6) = U7_GGAGA(x1, x2, x4, x6)
U8_GGAGA(x1, x2, x3, x4, x5, x6) = U8_GGAGA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

FACTORA_IN_GA(cons(0, cons(T19, T12)), T14) → U1_GA(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
FACTORA_IN_GA(cons(0, cons(T19, T12)), T14) → FACTORA_IN_GA(cons(0, T12), T14)
FACTORA_IN_GA(cons(s(T24), cons(T25, T12)), T14) → U2_GA(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
FACTORA_IN_GA(cons(s(T24), cons(T25, T12)), T14) → PB_IN_GGAAGA(T24, T25, X35, X36, T12, T14)
PB_IN_GGAAGA(T24, T25, T28, X36, T12, T14) → U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
PB_IN_GGAAGA(T24, T25, T28, X36, T12, T14) → TIMESC_IN_GGA(T24, T25, T28)
TIMESC_IN_GGA(s(T40), T41, X59) → U3_GGA(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
TIMESC_IN_GGA(s(T40), T41, X59) → PD_IN_GGAA(T40, T41, X58, X59)
PD_IN_GGAA(T40, T41, T44, X59) → U9_GGAA(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
PD_IN_GGAA(T40, T41, T44, X59) → TIMESC_IN_GGA(T40, T41, T44)
U9_GGAA(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_GGAA(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
U9_GGAA(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → PLUSE_IN_GGA(T44, T41, X59)
PLUSE_IN_GGA(s(T58), T59, s(X82)) → U4_GGA(T58, T59, X82, plusE_in_gga(T58, T59, X82))
PLUSE_IN_GGA(s(T58), T59, s(X82)) → PLUSE_IN_GGA(T58, T59, X82)
U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_GGAAGA(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → PF_IN_GGAGA(T28, T25, X36, T12, T14)
PF_IN_GGAGA(T28, T25, T64, T12, T14) → U7_GGAGA(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
PF_IN_GGAGA(T28, T25, T64, T12, T14) → PLUSE_IN_GGA(T28, T25, T64)
U7_GGAGA(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_GGAGA(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U7_GGAGA(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → FACTORA_IN_GA(cons(T64, T12), T14)

The TRS R consists of the following rules:

factorA_in_ga(cons(T4, nil), T4) → factorA_out_ga(cons(T4, nil), T4)
factorA_in_ga(cons(0, cons(T19, T12)), T14) → U1_ga(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
factorA_in_ga(cons(s(T24), cons(T25, T12)), T14) → U2_ga(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
pB_in_ggaaga(T24, T25, T28, X36, T12, T14) → U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
pF_in_ggaga(T28, T25, T64, T12, T14) → U7_ggaga(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_ggaga(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_ggaga(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U8_ggaga(T28, T25, T64, T12, T14, factorA_out_ga(cons(T64, T12), T14)) → pF_out_ggaga(T28, T25, T64, T12, T14)
U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_out_ggaga(T28, T25, X36, T12, T14)) → pB_out_ggaaga(T24, T25, T28, X36, T12, T14)
U2_ga(T24, T25, T12, T14, pB_out_ggaaga(T24, T25, X35, X36, T12, T14)) → factorA_out_ga(cons(s(T24), cons(T25, T12)), T14)
U1_ga(T19, T12, T14, factorA_out_ga(cons(0, T12), T14)) → factorA_out_ga(cons(0, cons(T19, T12)), T14)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 11 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

PLUSE_IN_GGA(s(T58), T59, s(X82)) → PLUSE_IN_GGA(T58, T59, X82)

The TRS R consists of the following rules:

factorA_in_ga(cons(T4, nil), T4) → factorA_out_ga(cons(T4, nil), T4)
factorA_in_ga(cons(0, cons(T19, T12)), T14) → U1_ga(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
factorA_in_ga(cons(s(T24), cons(T25, T12)), T14) → U2_ga(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
pB_in_ggaaga(T24, T25, T28, X36, T12, T14) → U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
pF_in_ggaga(T28, T25, T64, T12, T14) → U7_ggaga(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_ggaga(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_ggaga(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U8_ggaga(T28, T25, T64, T12, T14, factorA_out_ga(cons(T64, T12), T14)) → pF_out_ggaga(T28, T25, T64, T12, T14)
U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_out_ggaga(T28, T25, X36, T12, T14)) → pB_out_ggaaga(T24, T25, T28, X36, T12, T14)
U2_ga(T24, T25, T12, T14, pB_out_ggaaga(T24, T25, X35, X36, T12, T14)) → factorA_out_ga(cons(s(T24), cons(T25, T12)), T14)
U1_ga(T19, T12, T14, factorA_out_ga(cons(0, T12), T14)) → factorA_out_ga(cons(0, cons(T19, T12)), 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:

PLUSE_IN_GGA(s(T58), T59, s(X82)) → PLUSE_IN_GGA(T58, T59, X82)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
PLUSE_IN_GGA(x1, x2, x3) = PLUSE_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:

PLUSE_IN_GGA(s(T58), T59) → PLUSE_IN_GGA(T58, T59)

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:

PLUSE_IN_GGA(s(T58), T59) → PLUSE_IN_GGA(T58, T59)
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:

TIMESC_IN_GGA(s(T40), T41, X59) → PD_IN_GGAA(T40, T41, X58, X59)
PD_IN_GGAA(T40, T41, T44, X59) → TIMESC_IN_GGA(T40, T41, T44)

The TRS R consists of the following rules:

factorA_in_ga(cons(T4, nil), T4) → factorA_out_ga(cons(T4, nil), T4)
factorA_in_ga(cons(0, cons(T19, T12)), T14) → U1_ga(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
factorA_in_ga(cons(s(T24), cons(T25, T12)), T14) → U2_ga(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
pB_in_ggaaga(T24, T25, T28, X36, T12, T14) → U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
pF_in_ggaga(T28, T25, T64, T12, T14) → U7_ggaga(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_ggaga(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_ggaga(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U8_ggaga(T28, T25, T64, T12, T14, factorA_out_ga(cons(T64, T12), T14)) → pF_out_ggaga(T28, T25, T64, T12, T14)
U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_out_ggaga(T28, T25, X36, T12, T14)) → pB_out_ggaaga(T24, T25, T28, X36, T12, T14)
U2_ga(T24, T25, T12, T14, pB_out_ggaaga(T24, T25, X35, X36, T12, T14)) → factorA_out_ga(cons(s(T24), cons(T25, T12)), T14)
U1_ga(T19, T12, T14, factorA_out_ga(cons(0, T12), T14)) → factorA_out_ga(cons(0, cons(T19, T12)), T14)

(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:

TIMESC_IN_GGA(s(T40), T41, X59) → PD_IN_GGAA(T40, T41, X58, X59)
PD_IN_GGAA(T40, T41, T44, X59) → TIMESC_IN_GGA(T40, T41, T44)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
TIMESC_IN_GGA(x1, x2, x3) = TIMESC_IN_GGA(x1, x2)
PD_IN_GGAA(x1, x2, x3, x4) = PD_IN_GGAA(x1, x2)

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:

TIMESC_IN_GGA(s(T40), T41) → PD_IN_GGAA(T40, T41)
PD_IN_GGAA(T40, T41) → TIMESC_IN_GGA(T40, T41)

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

(19) 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:

PD_IN_GGAA(T40, T41) → TIMESC_IN_GGA(T40, T41)
The graph contains the following edges 1 >= 1, 2 >= 2
TIMESC_IN_GGA(s(T40), T41) → PD_IN_GGAA(T40, T41)
The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

FACTORA_IN_GA(cons(0, cons(T19, T12)), T14) → FACTORA_IN_GA(cons(0, T12), T14)

The TRS R consists of the following rules:

factorA_in_ga(cons(T4, nil), T4) → factorA_out_ga(cons(T4, nil), T4)
factorA_in_ga(cons(0, cons(T19, T12)), T14) → U1_ga(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
factorA_in_ga(cons(s(T24), cons(T25, T12)), T14) → U2_ga(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
pB_in_ggaaga(T24, T25, T28, X36, T12, T14) → U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
pF_in_ggaga(T28, T25, T64, T12, T14) → U7_ggaga(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_ggaga(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_ggaga(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U8_ggaga(T28, T25, T64, T12, T14, factorA_out_ga(cons(T64, T12), T14)) → pF_out_ggaga(T28, T25, T64, T12, T14)
U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_out_ggaga(T28, T25, X36, T12, T14)) → pB_out_ggaaga(T24, T25, T28, X36, T12, T14)
U2_ga(T24, T25, T12, T14, pB_out_ggaaga(T24, T25, X35, X36, T12, T14)) → factorA_out_ga(cons(s(T24), cons(T25, T12)), T14)
U1_ga(T19, T12, T14, factorA_out_ga(cons(0, T12), T14)) → factorA_out_ga(cons(0, cons(T19, T12)), T14)

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

FACTORA_IN_GA(cons(0, cons(T19, T12)), T14) → FACTORA_IN_GA(cons(0, T12), T14)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

FACTORA_IN_GA(cons(0, cons(T19, T12))) → FACTORA_IN_GA(cons(0, T12))

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

(26) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

FACTORA_IN_GA(cons(0, cons(T19, T12))) → FACTORA_IN_GA(cons(0, T12))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(FACTORA_IN_GA(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 1 + x₁ + 2·x₂

(27) Obligation:

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

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(29) YES

(30) Obligation:

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

FACTORA_IN_GA(cons(s(T24), cons(T25, T12)), T14) → PB_IN_GGAAGA(T24, T25, X35, X36, T12, T14)
PB_IN_GGAAGA(T24, T25, T28, X36, T12, T14) → U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → PF_IN_GGAGA(T28, T25, X36, T12, T14)
PF_IN_GGAGA(T28, T25, T64, T12, T14) → U7_GGAGA(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_GGAGA(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → FACTORA_IN_GA(cons(T64, T12), T14)

The TRS R consists of the following rules:

factorA_in_ga(cons(T4, nil), T4) → factorA_out_ga(cons(T4, nil), T4)
factorA_in_ga(cons(0, cons(T19, T12)), T14) → U1_ga(T19, T12, T14, factorA_in_ga(cons(0, T12), T14))
factorA_in_ga(cons(s(T24), cons(T25, T12)), T14) → U2_ga(T24, T25, T12, T14, pB_in_ggaaga(T24, T25, X35, X36, T12, T14))
pB_in_ggaaga(T24, T25, T28, X36, T12, T14) → U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U5_ggaaga(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_in_ggaga(T28, T25, X36, T12, T14))
pF_in_ggaga(T28, T25, T64, T12, T14) → U7_ggaga(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_ggaga(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → U8_ggaga(T28, T25, T64, T12, T14, factorA_in_ga(cons(T64, T12), T14))
U8_ggaga(T28, T25, T64, T12, T14, factorA_out_ga(cons(T64, T12), T14)) → pF_out_ggaga(T28, T25, T64, T12, T14)
U6_ggaaga(T24, T25, T28, X36, T12, T14, pF_out_ggaga(T28, T25, X36, T12, T14)) → pB_out_ggaaga(T24, T25, T28, X36, T12, T14)
U2_ga(T24, T25, T12, T14, pB_out_ggaaga(T24, T25, X35, X36, T12, T14)) → factorA_out_ga(cons(s(T24), cons(T25, T12)), T14)
U1_ga(T19, T12, T14, factorA_out_ga(cons(0, T12), T14)) → factorA_out_ga(cons(0, cons(T19, T12)), T14)

The argument filtering Pi contains the following mapping:
factorA_in_ga(x1, x2) = factorA_in_ga(x1)
cons(x1, x2) = cons(x1, x2)
nil = nil
factorA_out_ga(x1, x2) = factorA_out_ga(x1, x2)
0 = 0
U1_ga(x1, x2, x3, x4) = U1_ga(x1, x2, x4)
s(x1) = s(x1)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x3, x5)
pB_in_ggaaga(x1, x2, x3, x4, x5, x6) = pB_in_ggaaga(x1, x2, x5)
U5_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U5_ggaaga(x1, x2, x5, x7)
timesC_in_gga(x1, x2, x3) = timesC_in_gga(x1, x2)
timesC_out_gga(x1, x2, x3) = timesC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4) = pD_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5) = U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5) = U10_ggaa(x1, x2, x3, x5)
plusE_in_gga(x1, x2, x3) = plusE_in_gga(x1, x2)
plusE_out_gga(x1, x2, x3) = plusE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4) = U4_gga(x1, x2, x4)
pD_out_ggaa(x1, x2, x3, x4) = pD_out_ggaa(x1, x2, x3, x4)
U6_ggaaga(x1, x2, x3, x4, x5, x6, x7) = U6_ggaaga(x1, x2, x3, x5, x7)
pF_in_ggaga(x1, x2, x3, x4, x5) = pF_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6) = U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6) = U8_ggaga(x1, x2, x3, x4, x6)
pF_out_ggaga(x1, x2, x3, x4, x5) = pF_out_ggaga(x1, x2, x3, x4, x5)
pB_out_ggaaga(x1, x2, x3, x4, x5, x6) = pB_out_ggaaga(x1, x2, x3, x4, x5, x6)
FACTORA_IN_GA(x1, x2) = FACTORA_IN_GA(x1)
PB_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PB_IN_GGAAGA(x1, x2, x5)
U5_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U5_GGAAGA(x1, x2, x5, x7)
PF_IN_GGAGA(x1, x2, x3, x4, x5) = PF_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6) = U7_GGAGA(x1, x2, x4, x6)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

FACTORA_IN_GA(cons(s(T24), cons(T25, T12)), T14) → PB_IN_GGAAGA(T24, T25, X35, X36, T12, T14)
PB_IN_GGAAGA(T24, T25, T28, X36, T12, T14) → U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_in_gga(T24, T25, T28))
U5_GGAAGA(T24, T25, T28, X36, T12, T14, timesC_out_gga(T24, T25, T28)) → PF_IN_GGAGA(T28, T25, X36, T12, T14)
PF_IN_GGAGA(T28, T25, T64, T12, T14) → U7_GGAGA(T28, T25, T64, T12, T14, plusE_in_gga(T28, T25, T64))
U7_GGAGA(T28, T25, T64, T12, T14, plusE_out_gga(T28, T25, T64)) → FACTORA_IN_GA(cons(T64, T12), T14)

The TRS R consists of the following rules:

timesC_in_gga(0, T35, 0) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41, X59) → U3_gga(T40, T41, X59, pD_in_ggaa(T40, T41, X58, X59))
plusE_in_gga(0, T53, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59, s(X82)) → U4_gga(T58, T59, X82, plusE_in_gga(T58, T59, X82))
U3_gga(T40, T41, X59, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U4_gga(T58, T59, X82, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
pD_in_ggaa(T40, T41, T44, X59) → U9_ggaa(T40, T41, T44, X59, timesC_in_gga(T40, T41, T44))
U9_ggaa(T40, T41, T44, X59, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, X59, plusE_in_gga(T44, T41, X59))
U10_ggaa(T40, T41, T44, X59, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
0 = 0
s(x1) = s(x1)
timesC_in_gga(x1, x2, x3) = timesC_in_gga(x1, x2)
timesC_out_gga(x1, x2, x3) = timesC_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4) = pD_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5) = U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5) = U10_ggaa(x1, x2, x3, x5)
plusE_in_gga(x1, x2, x3) = plusE_in_gga(x1, x2)
plusE_out_gga(x1, x2, x3) = plusE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4) = U4_gga(x1, x2, x4)
pD_out_ggaa(x1, x2, x3, x4) = pD_out_ggaa(x1, x2, x3, x4)
FACTORA_IN_GA(x1, x2) = FACTORA_IN_GA(x1)
PB_IN_GGAAGA(x1, x2, x3, x4, x5, x6) = PB_IN_GGAAGA(x1, x2, x5)
U5_GGAAGA(x1, x2, x3, x4, x5, x6, x7) = U5_GGAAGA(x1, x2, x5, x7)
PF_IN_GGAGA(x1, x2, x3, x4, x5) = PF_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6) = U7_GGAGA(x1, x2, x4, x6)

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

FACTORA_IN_GA(cons(s(T24), cons(T25, T12))) → PB_IN_GGAAGA(T24, T25, T12)
PB_IN_GGAAGA(T24, T25, T12) → U5_GGAAGA(T24, T25, T12, timesC_in_gga(T24, T25))
U5_GGAAGA(T24, T25, T12, timesC_out_gga(T24, T25, T28)) → PF_IN_GGAGA(T28, T25, T12)
PF_IN_GGAGA(T28, T25, T12) → U7_GGAGA(T28, T25, T12, plusE_in_gga(T28, T25))
U7_GGAGA(T28, T25, T12, plusE_out_gga(T28, T25, T64)) → FACTORA_IN_GA(cons(T64, T12))

The TRS R consists of the following rules:

timesC_in_gga(0, T35) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41) → U3_gga(T40, T41, pD_in_ggaa(T40, T41))
plusE_in_gga(0, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59) → U4_gga(T58, T59, plusE_in_gga(T58, T59))
U3_gga(T40, T41, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U4_gga(T58, T59, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
pD_in_ggaa(T40, T41) → U9_ggaa(T40, T41, timesC_in_gga(T40, T41))
U9_ggaa(T40, T41, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, plusE_in_gga(T44, T41))
U10_ggaa(T40, T41, T44, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)

The set Q consists of the following terms:

timesC_in_gga(x0, x1)
plusE_in_gga(x0, x1)
U3_gga(x0, x1, x2)
U4_gga(x0, x1, x2)
pD_in_ggaa(x0, x1)
U9_ggaa(x0, x1, x2)
U10_ggaa(x0, x1, x2, x3)

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

(35) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

FACTORA_IN_GA(cons(s(T24), cons(T25, T12))) → PB_IN_GGAAGA(T24, T25, T12)

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

POL(0) = 0
POL(FACTORA_IN_GA(x₁)) = x₁
POL(PB_IN_GGAAGA(x₁, x₂, x₃)) = 1 + x₃
POL(PF_IN_GGAGA(x₁, x₂, x₃)) = 1 + x₃
POL(U10_ggaa(x₁, x₂, x₃, x₄)) = 0
POL(U3_gga(x₁, x₂, x₃)) = 0
POL(U4_gga(x₁, x₂, x₃)) = 1
POL(U5_GGAAGA(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(U7_GGAGA(x₁, x₂, x₃, x₄)) = x₃ + x₄
POL(U9_ggaa(x₁, x₂, x₃)) = 0
POL(cons(x₁, x₂)) = 1 + x₂
POL(pD_in_ggaa(x₁, x₂)) = 0
POL(pD_out_ggaa(x₁, x₂, x₃, x₄)) = 0
POL(plusE_in_gga(x₁, x₂)) = 1
POL(plusE_out_gga(x₁, x₂, x₃)) = 1
POL(s(x₁)) = 0
POL(timesC_in_gga(x₁, x₂)) = 0
POL(timesC_out_gga(x₁, x₂, x₃)) = 0

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

plusE_in_gga(0, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59) → U4_gga(T58, T59, plusE_in_gga(T58, T59))
U4_gga(T58, T59, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))

(36) Obligation:

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

PB_IN_GGAAGA(T24, T25, T12) → U5_GGAAGA(T24, T25, T12, timesC_in_gga(T24, T25))
U5_GGAAGA(T24, T25, T12, timesC_out_gga(T24, T25, T28)) → PF_IN_GGAGA(T28, T25, T12)
PF_IN_GGAGA(T28, T25, T12) → U7_GGAGA(T28, T25, T12, plusE_in_gga(T28, T25))
U7_GGAGA(T28, T25, T12, plusE_out_gga(T28, T25, T64)) → FACTORA_IN_GA(cons(T64, T12))

The TRS R consists of the following rules:

timesC_in_gga(0, T35) → timesC_out_gga(0, T35, 0)
timesC_in_gga(s(T40), T41) → U3_gga(T40, T41, pD_in_ggaa(T40, T41))
plusE_in_gga(0, T53) → plusE_out_gga(0, T53, T53)
plusE_in_gga(s(T58), T59) → U4_gga(T58, T59, plusE_in_gga(T58, T59))
U3_gga(T40, T41, pD_out_ggaa(T40, T41, X58, X59)) → timesC_out_gga(s(T40), T41, X59)
U4_gga(T58, T59, plusE_out_gga(T58, T59, X82)) → plusE_out_gga(s(T58), T59, s(X82))
pD_in_ggaa(T40, T41) → U9_ggaa(T40, T41, timesC_in_gga(T40, T41))
U9_ggaa(T40, T41, timesC_out_gga(T40, T41, T44)) → U10_ggaa(T40, T41, T44, plusE_in_gga(T44, T41))
U10_ggaa(T40, T41, T44, plusE_out_gga(T44, T41, X59)) → pD_out_ggaa(T40, T41, T44, X59)

The set Q consists of the following terms:

timesC_in_gga(x0, x1)
plusE_in_gga(x0, x1)
U3_gga(x0, x1, x2)
U4_gga(x0, x1, x2)
pD_in_ggaa(x0, x1)
U9_ggaa(x0, x1, x2)
U10_ggaa(x0, x1, x2, x3)

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

(37) 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) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) MRRProof (EQUIVALENT transformation)

(27) Obligation:

(28) PisEmptyProof (EQUIVALENT transformation)

(29) YES

(30) Obligation:

(31) UsableRulesProof (EQUIVALENT transformation)

(32) Obligation:

(33) PiDPToQDPProof (SOUND transformation)

(34) Obligation:

(35) QDPOrderProof (EQUIVALENT transformation)

(36) Obligation:

(37) DependencyGraphProof (EQUIVALENT transformation)

(38) TRUE