MAYBE
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN"
"http:/www.w3.org/TR/html4/frameset.dtd">
<html>
<head>
<title>Left Termination proof of ../tpdb/LP/lpexamples/kay4.pl</title>
</head>
<body>
<BR><B>Left Termination</B> of the query pattern
kay4_in_1(g)
w.r.t. the given <I>Prolog program</I> could not be shown:<BR><BR><BR><BR><pre>&#8627 <B>Prolog</B></pre><pre>  &#8627 UndefinedPredicateHandlerProof</pre><BR>Clauses:<BR><BR>kay4(I)&#160;:-&#160;','(length(.(_, .(_, L)), I), ','(top(L), ','(mid([], L), bot(L)))).<BR>top(L)&#160;:-&#160;','(write(a), ','(mwrite('-', L), ','(write(b), nl))).<BR>bot(L)&#160;:-&#160;','(write(c), ','(mwrite('-', L), ','(write(d), nl))).<BR>mid(X, []).<BR>mid(X, .(_, []))&#160;:-&#160;','(write('|'), ','(mwrite(' ', X), ','(write('X'), ','(mwrite(' ', X), ','(write('|'), nl))))).<BR>mid(X, .(_, .(_, Y)))&#160;:-&#160;','(write('|'), ','(mwrite(' ', X), ','(write('\\'), ','(mwrite(' ', Y), ','(write('/'), ','(mwrite(' ', X), ','(write('|'), ','(nl, ','(mid(.(_, X), Y), ','(write('|'), ','(mwrite(' ', X), ','(write('/'), ','(mwrite(' ', Y), ','(write('\\'), ','(mwrite(' ', X), ','(write('|'), nl)))))))))))))))).<BR>mwrite(Char, L)&#160;:-&#160;findall(_, ','(member(_, L), write(Char)), _).<BR>member(X, .(X, _)).<BR>member(X, .(_, Xs))&#160;:-&#160;member(X, Xs).<BR><BR>Queries:<BR><BR>kay4(g).<BR><BR>Added facts for all undefined predicates.<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 UndefinedPredicateHandlerProof</pre><pre>    &#8627 <B>Prolog</B></pre><BR>Clauses:<BR><BR>kay4(I)&#160;:-&#160;','(length(.(_, .(_, L)), I), ','(top(L), ','(mid([], L), bot(L)))).<BR>top(L)&#160;:-&#160;','(write(a), ','(mwrite('-', L), ','(write(b), nl))).<BR>bot(L)&#160;:-&#160;','(write(c), ','(mwrite('-', L), ','(write(d), nl))).<BR>mid(X, []).<BR>mid(X, .(_, []))&#160;:-&#160;','(write('|'), ','(mwrite(' ', X), ','(write('X'), ','(mwrite(' ', X), ','(write('|'), nl))))).<BR>mid(X, .(_, .(_, Y)))&#160;:-&#160;','(write('|'), ','(mwrite(' ', X), ','(write('\\'), ','(mwrite(' ', Y), ','(write('/'), ','(mwrite(' ', X), ','(write('|'), ','(nl, ','(mid(.(_, X), Y), ','(write('|'), ','(mwrite(' ', X), ','(write('/'), ','(mwrite(' ', Y), ','(write('\\'), ','(mwrite(' ', X), ','(write('|'), nl)))))))))))))))).<BR>mwrite(Char, L)&#160;:-&#160;findall(_, ','(member(_, L), write(Char)), _).<BR>member(X, .(X, _)).<BR>member(X, .(_, Xs))&#160;:-&#160;member(X, Xs).<BR>length(X0, X1).<BR>write(X0).<BR>nl.<BR>findall(X0, X1, X2).<BR><BR>Queries:<BR><BR>kay4(g).<BR><BR><BR></body>

