YES Left Termination proof of ../tpdb/LP/lpexamples/factorial.pl
Left Termination of the query pattern factorial_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PredefinedPredicateTransformerProof

Clauses:

factorial1(N, F) :- ','(>(N, 0), ','(is(N1, -(N, 1)), ','(factorial1(N1, F1), is(F, *(N, F1))))).
factorial1(0, 1).
factorial2(N, F) :- factorial2(0, N, 1, F).
factorial2(I, N, T, F) :- ','(<(I, N), ','(is(I1, +(I, 1)), ','(is(T1, *(T, I1)), factorial2(I1, N, T1, F)))).
factorial2(N, N, F, F).
factorial3(N, F) :- factorial3(N, 1, F).
factorial3(N, T, F) :- ','(>(N, 0), ','(is(T1, *(T, N)), ','(is(N1, -(N, 1)), factorial3(N1, T1, F)))).
factorial3(0, F, F).

Queries:

factorial(g,a).

Added definitions of predefined predicates.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ PrologToPiTRSProof

Clauses:

factorial1(N, F) :- ','(=(X, N), ','(=(X1, zero), ','(isGreater(X, X1), ','(isMinus(N, succ(zero), U), ','(=(N1, U), ','(factorial1(N1, F1), ','(isTimes(N, F1, U), =(F, U)))))))).
factorial1(zero, succ(zero)).
factorial2(N, F) :- factorial2(zero, N, succ(zero), F).
factorial2(I, N, T, F) :- ','(=(X, I), ','(=(X1, N), ','(isLess(X, X1), ','(isPlus(I, succ(zero), U), ','(=(I1, U), ','(isTimes(T, I1, U), ','(=(T1, U), factorial2(I1, N, T1, F)))))))).
factorial2(N, N, F, F).
factorial3(N, F) :- factorial3(N, succ(zero), F).
factorial3(N, T, F) :- ','(=(X, N), ','(=(X1, zero), ','(isGreater(X, X1), ','(isTimes(T, N, U), ','(=(T1, U), ','(isMinus(N, succ(zero), U), ','(=(N1, U), factorial3(N1, T1, F)))))))).
factorial3(zero, F, F).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
isGreater(succ(X), zero).
isGreater(succ(X), pred(Y)).
isGreater(succ(X), succ(Y)) :- isGreater(X, Y).
isGreater(zero, pred(Y)).
isGreater(pred(X), pred(Y)) :- isGreater(X, Y).
isLess(pred(X), zero).
isLess(pred(X), succ(Y)).
isLess(pred(X), pred(Y)) :- isLess(X, Y).
isLess(zero, succ(Y)).
isLess(succ(X), succ(Y)) :- isLess(X, Y).

Queries:

factorial(g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
R is empty.
Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ RisEmptyProof

Pi-finite rewrite system:
R is empty.
Pi is empty.

The TRS R is empty. Hence, termination is trivially proven.