domains
avl=avl(bt,integer)
bt=bt(avl,char,avl);nil

predicates
nondeterm run(avl)
nondeterm insertA(char,avl,avl)
nondeterm unionA(avl,char,avl,char,avl,avl)
max(integer,integer,integer)

clauses
run(A):-readchar(C),C<>'.',insertA(C,A,An),write(An),nl,run(An);write("\nThat's it\n").

insertA(New,avl(nil,0),avl(bt(avl(nil,0),New,avl(nil,0)),1)).
insertA(E,avl(bt(Left,E,Right),H),avl(bt(Left,E,Right),H)).

insertA(New,avl(bt(Left,E,Right),_),NewA):-
    New < E,
    insertA(New,Left,avl(bt(LT,X,RT),_)),
    unionA(LT,X,RT,E,Right,NewA).

insertA(New,avl(bt(Left,E,Right),_),NewA):-
    New > E,
    insertA(New,Right,avl(bt(LT,X,RT),_)),
    unionA(Left,E,LT,X,RT,NewA).

unionA(avl(T1,H1),A,avl(bt(L2,C,R2),H2),B,avl(T3,H3),avl(bt(avl(bt(avl(T1,H1),A,L2),HA),C,avl(bt(R2,B,avl(T3,H3)),HB)),HC)):-
    H2>H1,H2>H3,
    HA=H1+1,HB=H3+1,HC=HA+1.

unionA(avl(T1,H1),A,avl(T2,H2),B,avl(T3,H3),avl(bt(avl(T1,H1),A,avl(bt(avl(T2,H2),B,avl(T3,H3)),HB)),HA)):-
    H1>=H2,H1>=H3,
    max(H2,H3,Hb), max(H1,HB,HA).

unionA(avl(T1,H1),A,avl(T2,H2),B,avl(T3,H3),avl(bt(avl(bt(avl(T1,H1),A,avl(T2,H2)),HA),B,avl(T3,H3)),HB)):-
    H3>=H2,H3>=H1,
    max(H1,H2,HA),max(HA,H3,HB).

max(X,Y,Z) :- X>Y, !, Z=X+1.
max(X,Y,Z) :- X<=Y,!, Z=Y+1.


goal
run(avl(nil,0)).