%len(L,N) iff natural number N is the length of the list L.

Predicate declaration?
len(L:list(term),N:nat)
[dc,dg]
Schema? {dc} dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1} divide_and_conquer_strategy1
Induction parameter? {L} L
Result parameter? {N} N
Decomposition Operator? {decompose(L,HL,TL)<--L=[HL|TL]}
decompose(L,HL,TL)<--L=[HL|TL]

When does len([],A) hold?
A=0.
When does len([A],B) hold?
B=s(0).
When does len([A,B],C) hold?
C=s(s(0)).
When does len([A,B,C],D) hold?
D=s(s(s(0))).
When does len([A,B,C,D],E) hold?
stop_it.

Do you want another logic program? {yes} yes

Decomposition Operator? {decompose(L,HL1,HL2,TL)<--L=[HL1,HL2|TL]}
decompose(L,HL1,HL2,TL)<--L=[HL1,HL2|TL]

When does len([A,B,C,D],E) hold?
E=s(s(s(s(0)))).
When does len([A,B,C,D,E],F) hold?
stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no


%count(A,B,C) iff natural number C is the number of elements that unifies
%with the term A in list B.

Predicate declaration?
count(A:term,B:list(term),C:nat)
[dc,dg]
Schema? {dc} dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1} divide_and_conquer_strategy1
Induction parameter? {B} B
Result parameter? {C} C
Passive parameter(s)? {[A]} [A]
Decomposition Operator? {decompose(B,HB,TB)<--B=[HB|TB]}
decompose(B,HB,TB)<--B=[HB|TB]

When does count(A,[],B) hold?
B=0.
When does count(A,[B],C) hold?
C=s(0),A=B.
When does count(A,[B,A],C) hold?
C=s(0),A\==B;C=s(s(0)),A=B.
When does count(A,[B,A,A],C) hold?
C=s(s(0)),A\==B;C=s(s(s(0))),A=B.
When does count(A,[B,A,A,A],C) hold?
stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no


%addlast(A,B,C) iff list C is list B with the term A is added in the
%end.

Predicate declaration?
addlast(A:term,B:list(term),C:list(term))
[dc,dg]
Schema? {dc} dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1}
divide_and_conquer_strategy1
Induction parameter? {B} B
Result parameter? {C} C
Passive parameter(s)? {[A]} [A]
Decomposition Operator? {decompose(B,HB,TB)<--B=[HB|TB]}
decompose(B,HB,TB)<--B=[HB|TB]

When does addlast(A,[],B) hold?
B=[A].
When does addlast(A,[B],C) hold?
C=[B|[A]].
When does addlast(A,[B,C],D) hold?
D=[B,C|[A]].
When does addlast(A,[B,C,D],E) hold?
E=[B,C,D|[A]].
When does addlast(A,[B,C,D,E],F) hold?
stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no

%multiply(A,B,C) iff natural number C is the product of natural
%numbers A and B. 

Predicate declaration?
multiply(A:nat,B:nat,C:nat)
[dc,dg]
Schema? {dc} dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1} divide_and_conquer_strategy1
Induction parameter? {A} A
Result parameter? {B} B
Passive parameter(s)? {[C]} [C]
Decomposition Operator? {decompose(A,HA,TA)<--and(A=s(TA),HA=A)}
decompose(A,HA,TA)<--and(A=s(TA),HA=A)

When does multiply(0,A,B) hold?
 A=0.
When does multiply(s(0),A,B) hold?
 A=B+0.
When does multiply(s(s(0)),A,B) hold?
 A=B+(B+0).
When does multiply(s(s(s(0))),A,B) hold?
 A=B+(B+(B+0)).
When does multiply(s(s(s(s(0)))),A,B) hold?
 stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no


%delOdds(A,B) iff list B is list A without its odd elements.

Predicate declaration?
delOdds(L:list(int),R:list(int))
[dc,dg]
Schema? {dc} 
dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1}
divide_and_conquer_strategy1
Induction parameter? {L} L
Result parameter? {R} R
Decomposition Operator? {decompose(L,HL,TL)<--L=[HL|TL]}
decompose(L,HL,TL)<--L=[HL|TL]

When does delOdds([],A) hold?
A=[].
When does delOdds([A],B) hold?
B=[],odd(A);B=[A],even(A).
When does delOdds([A,B],C) hold, assuming even(B)?
C=[B],odd(A);C=[A,B],even(A).
When does delOdds([A,B,C],D) hold, assuming even(B),even(C)?
stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no


%compress(L,R) iff list R is the compressed form of list L.
%e.g. compress([a,a,b,c,c,c,d],[a,s(s(0)),b,s(0),c,s(s(s(0))),d,s(0)])

Predicate declaration?
compress(L:list(atom),R:list(atom))
[dc,dg]
Schema? {dc} dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1} divide_and_conquer_strategy1
Induction parameter? {L} L
Result parameter? {R} R
Decomposition Operator? {decompose(L,HL,TL)<--L=[HL|TL]}
decompose(L,HL,TL)<--L=[HL|TL]

When does compress([],A) hold?
A=[].
When does compress([A],B) hold?
B=[A,s(0)].
When does compress([A,B],C) hold?
C=[A,s(s(0))],eq(A,B);C=[A,s(0),B,s(0)],diff(A,B).
When does compress([A,B,C],D) hold, assuming eq(B,C)?
D=[A,s(s(s(0)))],eq(A,B);D=[A,s(0),B,s(s(0))],diff(A,B).
When does compress([A,B,C],D) hold, assuming diff(B,C)?
D=[A,s(s(0)),C,s(0)],eq(A,B);D=[A,s(0),B,s(0),C,s(0)],diff(A,B).
When does compress([A,B,C,D],E) hold, assuming eq(B,C),eq(C,D)?
stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no


%factorial(A,B) iff natural number B is the factorial of natural number A.

Predicate declaration?  factorial(A:nat,B:nat)
[dc,dg]
Schema? {dc}
dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1}
divide_and_conquer_strategy1
Induction parameter? {A} A
Result parameter? {B} B
Decomposition Operator? {decompose(A,HA,TA)<--and(A=s(TA),HA=A)}
decompose(A,HA,TA)<--and(A=s(TA),HA=A)
When does factorial(0,A) hold?
A=s(0).
When does factorial(s(0),A) hold?
A=s(0).
When does factorial(s(s(0)),A) hold?
A=s(s(0)).
When does factorial(s(s(s(0))),A) hold?
A=s(s(s(s(s(s(0)))))).
When does factorial(s(s(s(s(0)))),A) hold?
stop_it.


Say "yes" to the following question at the first two occurences:
Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] yes


When does compose_factorial(0,A,B) hold?
 B=0.
When does compose_factorial(s(0),A,B) hold?
 B=A+0.
When does compose_factorial(s(s(0)),A,B) hold?
 B=A+(A+0).
When does compose_factorial(s(s(s(0))),A,B) hold?
 B=A+(A+(A+0)).
When does factorial(s(s(s(s(0)))),A) hold?
 stop_it.


Say "no", to the third question:
Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no

%reverse(L,R) iff list R is the reverse of list L.

Predicate declaration? reverse(L:list(term),R:list(term))
[dc,dg]
Schema? {dc}
dc
[divide_and_conquer_strategy1]
Strategy? {divide_and_conquer_strategy1}
divide_and_conquer_strategy1
Induction parameter? {L} L
Result parameter? {R} R
Decomposition Operator? {decompose(L,HL,TL)<--L=[HL|TL]}
decompose(L,HL,TL)<--L=[HL|TL]

When does reverse([],A) hold?
A=[].
When does reverse([A],B) hold?
B=[A].
When does reverse([A,B],C) hold?
C=[B,A].
When does reverse([A,B,C],D) hold?
D=[C,B,A].
When does reverse([A,B,C,D],E) hold?
E=[D,C,B,A].
When does reverse([A,B,C,D,E],F) hold?
stop_it.


Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] yes

When does reverse([A,B,C,D,E],F) hold?
stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no



%s(L,S) iff list S is (ascendingly) sorted version of list L.

Predicate declaration?
s(L:list(int),S:list(int))
Schema? {dc} dc
Strategy? {divide_and_conquer_strategy1} divide_and_conquer_strategy1
Induction parameter? {L} L
Result parameter? {S} S
Decomposition Operator? {decompose(L,HL,TL)<--L=[HL|TL]}
decompose(L,HL,TL)<--L=[HL|TL]

When does s([],A) hold?
A=[].
When does s([A],B) hold?
B=[A].
When does s([A,B],C) hold?
C=[A,B],le(A,B);C=[B,A],gt(A,B).
When does s([A,B,C],D) hold, assuming le(B,C)?
D=[A,B,C],le(A,B);D=[B,A,C],gt(A,B),le(A,C);D=[B,C,A],gt(A,B),gt(A,C).
When does s([A,B,C,D],E) hold, assuming le(B,C),le(C,D)?
stop_it.

Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] yes

When does s([A,B,C,D],E) hold, assuming le(B,C),le(C,D)?
 E=[A,B,C,D],le(A,B);E=[B,A,C,D],le(A,C),gt(A,B);E=[B,C,A,D],le(A,D),gt(A,C);E=[B,C,D,A],gt(A,D).
When does s([A,B,C],D) hold, assuming le(B,C),le(A,C)?
 D=[A,B,C],le(A,B);D=[B,A,C],gt(A,B).
When does ...?
 stop_it.


Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no


%reverse(L,R) iff list R is the reverse of list L.
%synthesis with descending generalization.

Predicate declaration?
reverse(A:list(term),R:list(term),L:list(term))
[dc,dg]
Schema? {dc} dg
[descend_gen_strategy1]
Strategy? {descend_gen_strategy1} descend_gen_strategy1
Induction parameter? {A} A
Result parameter? {R} R
Passive parameter(s)? {[L]} []
Accumulation parameter(s)? {[L]} [L]
Decomposition Operator? {decompose(A,HA,TA)<--A=[HA|TA]}
decompose(A,HA,TA)<--A=[HA|TA]

When does reverse([],A,B) hold?
 A=B.
When does reverse([A],B,C) hold?
 B=[A|C].
When does reverse([A,B],[B|C],D) hold?
 [B|C]=[B,A|D].
When does reverse([A,B,C],[C,B|D],E) hold?
 [C,B|D]=[C,B,A|E].
When does reverse([A,B,C,D],[D,C,B|E],F) hold?
 [D,C,B|E]=[D,C,B,A|F].
When does reverse([A,B,C,D,E],[E,D,C,B|F],G) hold?
 stop_it.


Please evaluate the Program Closing Method results: need for recursive synthesis? [yes/no] no









