:- pred ff.
:- pred append(list(int),list(int),list(int)).
:- pred zip(list(int),list(int),list(pair(int,int))).
:- pred len(list(int),int).
:- pred take(int,list(int),list(int)).
:- pred drop(int,list(int),list(int)).
:- pred zappend(list(pair(int,int)),list(pair(int,int)),list(pair(int,int))).
:- pred leq(int,int,bool).

:- mode append(in,in,out).
:- mode zip(in,in,out).
:- mode len(in,out).
:- mode take(in,in,out).
:- mode drop(in,in,out).
:- mode zappend(in,in,out).
:- mode leq(in,in,out).

:- pred adt_eqlistpairs(list(pair(int,int)),list(pair(int,int)),bool).
:- mode adt_eqlistpairs(in,in,out).

adt_eqlistpairs([],[],R) :- R=:=1.
adt_eqlistpairs([],[_|_],R) :- R=:=0.
adt_eqlistpairs([_|_],[],R) :- R=:=0.
adt_eqlistpairs([(A,B)|L],[(A1,B1)|L1],R) :- R=:=0, A>=A1+1.
adt_eqlistpairs([(A,B)|L],[(A1,B1)|L1],R) :- R=:=0, A=<A1-1.
adt_eqlistpairs([(A,B)|L],[(A1,B1)|L1],R) :- R=:=0, B>=B1+1.
adt_eqlistpairs([(A,B)|L],[(A1,B1)|L1],R) :- R=:=0, B=<B1-1.
adt_eqlistpairs([(A,B)|L],[(A1,B1)|L1],R1) :- R1=:=R2, A=A1, B=B1, adt_eqlistpairs(L,L1,R2).


zappend([],A,A).
zappend([A|B],C,[A|D]) :- zappend(B,C,D).
drop(A,[],[]).
drop(A,B,B) :- A=0.
drop(A,[B|C],D) :- A=1+E, E>=0, drop(E,C,D).
take(A,[],[]).
take(A,B,[]) :- A=0.
take(A,[B|C],[B|D]) :- A=1+E, E>=0, take(E,C,D).
len([],A) :- A=0.
len([A|B],C) :- C=1+D, len(B,D).
zip([],A,[]).
zip(A,[],[]).
zip([A|B],[C|D],[(A,C)|E]) :- zip(B,D,E).
append([],A,A).
append([A|B],C,[A|D]) :- append(B,C,D).

% (forall ((xs Lst) (ys Lst) (zs Lst)) (= (zip (append xs ys) zs)
                    % (zappend (zip xs (take (len xs) zs)) (zip ys (drop (len xs) zs))))) ; G85


ff :-append(X,Y,XY), zip(XY,Z, Zip),
    len(X,LX),
    take(LX,Z,TZ),  zip(X,TZ,ZipX),
    drop(LX,Z,DZ),  zip(Y,DZ,ZipY),
    zappend(ZipX,ZipY,ZipXY),
    A=:=0, adt_eqlistpairs(Zip,ZipXY,A).