0 Prolog
↳1 PrologToTRSTransformerProof (⇒, 80 ms)
↳2 QTRS
↳3 Overlay + Local Confluence (⇔, 64 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 38 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 QDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 QDP
↳12 QReductionProof (⇔, 9 ms)
↳13 QDP
↳14 QDPOrderProof (⇔, 112 ms)
↳15 QDP
↳16 DependencyGraphProof (⇔, 0 ms)
↳17 TRUE
↳18 QDP
↳19 UsableRulesProof (⇔, 0 ms)
↳20 QDP
↳21 QReductionProof (⇔, 0 ms)
↳22 QDP
↳23 MRRProof (⇔, 0 ms)
↳24 QDP
↳25 PisEmptyProof (⇔, 0 ms)
↳26 YES
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
f2_in(d(d(T57))) → U3(f81_in(T57), d(d(T57)))
U3(f81_out1(X53, T59), d(d(T57))) → f2_out1(T59)
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
f81_in(T57) → U6(f2_in(d(T57)), T57)
U6(f2_out1(T60), T57) → U7(f2_in(d(e(T60))), T57, T60)
U7(f2_out1(T59), T57, T60) → f81_out1(T60, T59)
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
f2_in(d(d(T57))) → U3(f81_in(T57), d(d(T57)))
U3(f81_out1(X53, T59), d(d(T57))) → f2_out1(T59)
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
f81_in(T57) → U6(f2_in(d(T57)), T57)
U6(f2_out1(T60), T57) → U7(f2_in(d(e(T60))), T57, T60)
U7(f2_out1(T59), T57, T60) → f81_out1(T60, T59)
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
U3(f81_out1(x0, x1), d(d(x2)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
F2_IN(d(e(+(T24, T25)))) → U11(f44_in(T24, T25), d(e(+(T24, T25))))
F2_IN(d(e(+(T24, T25)))) → F44_IN(T24, T25)
F2_IN(d(e(*(T47, T48)))) → U21(f44_in(T47, T48), d(e(*(T47, T48))))
F2_IN(d(e(*(T47, T48)))) → F44_IN(T47, T48)
F2_IN(d(d(T57))) → U31(f81_in(T57), d(d(T57)))
F2_IN(d(d(T57))) → F81_IN(T57)
F44_IN(T24, T25) → U41(f2_in(d(e(T24))), T24, T25)
F44_IN(T24, T25) → F2_IN(d(e(T24)))
U41(f2_out1(T28), T24, T25) → U51(f2_in(d(e(T25))), T24, T25, T28)
U41(f2_out1(T28), T24, T25) → F2_IN(d(e(T25)))
F81_IN(T57) → U61(f2_in(d(T57)), T57)
F81_IN(T57) → F2_IN(d(T57))
U61(f2_out1(T60), T57) → U71(f2_in(d(e(T60))), T57, T60)
U61(f2_out1(T60), T57) → F2_IN(d(e(T60)))
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
f2_in(d(d(T57))) → U3(f81_in(T57), d(d(T57)))
U3(f81_out1(X53, T59), d(d(T57))) → f2_out1(T59)
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
f81_in(T57) → U6(f2_in(d(T57)), T57)
U6(f2_out1(T60), T57) → U7(f2_in(d(e(T60))), T57, T60)
U7(f2_out1(T59), T57, T60) → f81_out1(T60, T59)
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
U3(f81_out1(x0, x1), d(d(x2)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
F2_IN(d(e(+(T24, T25)))) → F44_IN(T24, T25)
F44_IN(T24, T25) → U41(f2_in(d(e(T24))), T24, T25)
U41(f2_out1(T28), T24, T25) → F2_IN(d(e(T25)))
F2_IN(d(e(*(T47, T48)))) → F44_IN(T47, T48)
F44_IN(T24, T25) → F2_IN(d(e(T24)))
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
f2_in(d(d(T57))) → U3(f81_in(T57), d(d(T57)))
U3(f81_out1(X53, T59), d(d(T57))) → f2_out1(T59)
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
f81_in(T57) → U6(f2_in(d(T57)), T57)
U6(f2_out1(T60), T57) → U7(f2_in(d(e(T60))), T57, T60)
U7(f2_out1(T59), T57, T60) → f81_out1(T60, T59)
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
U3(f81_out1(x0, x1), d(d(x2)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
F2_IN(d(e(+(T24, T25)))) → F44_IN(T24, T25)
F44_IN(T24, T25) → U41(f2_in(d(e(T24))), T24, T25)
U41(f2_out1(T28), T24, T25) → F2_IN(d(e(T25)))
F2_IN(d(e(*(T47, T48)))) → F44_IN(T47, T48)
F44_IN(T24, T25) → F2_IN(d(e(T24)))
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
U3(f81_out1(x0, x1), d(d(x2)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
U3(f81_out1(x0, x1), d(d(x2)))
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
F2_IN(d(e(+(T24, T25)))) → F44_IN(T24, T25)
F44_IN(T24, T25) → U41(f2_in(d(e(T24))), T24, T25)
U41(f2_out1(T28), T24, T25) → F2_IN(d(e(T25)))
F2_IN(d(e(*(T47, T48)))) → F44_IN(T47, T48)
F44_IN(T24, T25) → F2_IN(d(e(T24)))
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F44_IN(T24, T25) → U41(f2_in(d(e(T24))), T24, T25)
F44_IN(T24, T25) → F2_IN(d(e(T24)))
POL(*(x1, x2)) = 1 + x1 + x2
POL(+(x1, x2)) = 1 + x1 + x2
POL(0) = 0
POL(1) = 0
POL(F2_IN(x1)) = x1
POL(F44_IN(x1, x2)) = 1 + x1 + x2
POL(U1(x1, x2)) = 0
POL(U2(x1, x2)) = 0
POL(U4(x1, x2, x3)) = 0
POL(U41(x1, x2, x3)) = x3
POL(U5(x1, x2, x3, x4)) = 0
POL(const(x1)) = 0
POL(d(x1)) = x1
POL(e(x1)) = x1
POL(f2_in(x1)) = 0
POL(f2_out1(x1)) = 0
POL(f44_in(x1, x2)) = 0
POL(f44_out1(x1, x2)) = 0
POL(t) = 0
F2_IN(d(e(+(T24, T25)))) → F44_IN(T24, T25)
U41(f2_out1(T28), T24, T25) → F2_IN(d(e(T25)))
F2_IN(d(e(*(T47, T48)))) → F44_IN(T47, T48)
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
F2_IN(d(d(T57))) → F81_IN(T57)
F81_IN(T57) → F2_IN(d(T57))
f2_in(d(e(t))) → f2_out1(const(1))
f2_in(d(e(const(T7)))) → f2_out1(const(0))
f2_in(d(e(+(T24, T25)))) → U1(f44_in(T24, T25), d(e(+(T24, T25))))
U1(f44_out1(T28, T29), d(e(+(T24, T25)))) → f2_out1(+(T28, T29))
f2_in(d(e(*(T47, T48)))) → U2(f44_in(T47, T48), d(e(*(T47, T48))))
U2(f44_out1(T51, T52), d(e(*(T47, T48)))) → f2_out1(+(*(T47, T52), *(T48, T51)))
f2_in(d(d(T57))) → U3(f81_in(T57), d(d(T57)))
U3(f81_out1(X53, T59), d(d(T57))) → f2_out1(T59)
f44_in(T24, T25) → U4(f2_in(d(e(T24))), T24, T25)
U4(f2_out1(T28), T24, T25) → U5(f2_in(d(e(T25))), T24, T25, T28)
U5(f2_out1(T30), T24, T25, T28) → f44_out1(T28, T30)
f81_in(T57) → U6(f2_in(d(T57)), T57)
U6(f2_out1(T60), T57) → U7(f2_in(d(e(T60))), T57, T60)
U7(f2_out1(T59), T57, T60) → f81_out1(T60, T59)
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
U3(f81_out1(x0, x1), d(d(x2)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
F2_IN(d(d(T57))) → F81_IN(T57)
F81_IN(T57) → F2_IN(d(T57))
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
U3(f81_out1(x0, x1), d(d(x2)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
f2_in(d(e(t)))
f2_in(d(e(const(x0))))
f2_in(d(e(+(x0, x1))))
U1(f44_out1(x0, x1), d(e(+(x2, x3))))
f2_in(d(e(*(x0, x1))))
U2(f44_out1(x0, x1), d(e(*(x2, x3))))
f2_in(d(d(x0)))
U3(f81_out1(x0, x1), d(d(x2)))
f44_in(x0, x1)
U4(f2_out1(x0), x1, x2)
U5(f2_out1(x0), x1, x2, x3)
f81_in(x0)
U6(f2_out1(x0), x1)
U7(f2_out1(x0), x1, x2)
F2_IN(d(d(T57))) → F81_IN(T57)
F81_IN(T57) → F2_IN(d(T57))
F2_IN(d(d(T57))) → F81_IN(T57)
F81_IN(T57) → F2_IN(d(T57))
F81IN1 > d1 > F2IN1
F2_IN_1=1
d_1=1
F81_IN_1=2