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/talp/maria/bid.pl</title>
</head>
<body>
<BR><B>Left Termination</B> of the query pattern
bid_in_4(g, a, a, a)
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 PredefinedPredicateTransformerProof</pre><BR>Clauses:<BR><BR>bid(Hand, Attributes, Points, Bid)&#160;:-&#160;','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).<BR>evaluate(Hand, [], P)&#160;:-&#160;','(hcp(Hand, 0, HCP), ','(adjustments(Hand, MP), is(P, +(HCP, MP)))).<BR>adjustments(_, 0).<BR>make_bid(Hand, Attributes, Points, 'punt...').<BR>hcp([], N, N).<BR>hcp(.(=(_X, C), Sn), Ni, No)&#160;:-&#160;','(hcp_suit(C, N), ','(is(Nt, +(N, Ni)), hcp(Sn, Nt, No))).<BR>hcp_suit(S, P)&#160;:-&#160;','(honors(S, 0, HP), ','(dist(S, DP), ','(misc(S, MP), is(P, +(HP, +(DP, MP)))))).<BR>honors([], Pi, Pi).<BR>honors(.(C1, Cn), Pi, Po)&#160;:-&#160;','(honor(C1, P), ','(>(P, 0), ','(is(Pt, +(P, Pi)), honors(Cn, Pt, Po)))).<BR>honors(.(C1, Cn), Pi, Pi)&#160;:-&#160;honor(C1, 0).<BR>honor(C, N)&#160;:-&#160;face_card(C, N).<BR>honor(C, 0)&#160;:-&#160;integer(C).<BR>face_card(ace, 4).<BR>face_card(king, 3).<BR>face_card(queen, 2).<BR>face_card(jack, 1).<BR>dist([], 3).<BR>dist(.(_, []), 2).<BR>dist(.(_, .(_, [])), 1).<BR>dist(.(_, .(_, .(_, _))), 0).<BR>misc(.(ace, []), -1).<BR>misc(.(king, []), -2).<BR>misc(.(queen, .(_, [])), -2).<BR>misc(.(jack, .(_, [])), -1).<BR>misc(.(_X, .(_Y, .(H3, Rem))), P)&#160;:-&#160;','(honor(H3, X), ','(>(X, 0), ','(length(Rem, N), ','(>(N, 2), is(P, -(N, 2)))))).<BR>misc(_, 0).<BR>sort_hand(Hand, SortedHand)&#160;:-&#160;','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).<BR>split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), [])))))&#160;:-&#160;','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).<BR>filter([], _, []).<BR>filter(.(-(Card, Suit), In), Suit, .(Card, Out))&#160;:-&#160;filter(In, Suit, Out).<BR>filter(.(-(_A, X), In), Suit, Out)&#160;:-&#160;','(\==(Suit, X), filter(In, Suit, Out)).<BR>sort_suits([], []).<BR>sort_suits(.(=(S, Ci), In), .(=(S, Co), Out))&#160;:-&#160;','(i_sort(Ci, [], Co), sort_suits(In, Out)).<BR>i_sort([], L, L).<BR>i_sort(.(C1, Cn), Li, Lo)&#160;:-&#160;','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).<BR>insert(X, [], .(X, [])).<BR>insert(X, .(Y, Z), .(X, .(Y, Z)))&#160;:-&#160;higher(X, Y).<BR>insert(X, .(Y, Z), .(Y, L))&#160;:-&#160;','(lower(X, Y), insert(X, Z, L)).<BR>higher(ace, _).<BR>higher(king, X)&#160;:-&#160;\==(X, ace).<BR>higher(queen, X)&#160;:-&#160;','(\==(X, ace), \==(X, king)).<BR>higher(jack, X)&#160;:-&#160;integer(X).<BR>higher(jack, jack).<BR>higher(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), >=(X, Y))).<BR>lower(king, ace).<BR>lower(queen, X)&#160;:-&#160;','(honor(X, N), >(N, 2)).<BR>lower(jack, X)&#160;:-&#160;','(honor(X, N), >(N, 1)).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), honor(Y, _M)).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), <(X, Y))).<BR>goal&#160;:-&#160;bid(.(-(ace, clubs), .(-(3, hearts), .(-(4, spades), .(-(4, diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(10, clubs), .(-(9, clubs), .(-(6, clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).<BR><BR>Queries:<BR><BR>bid(g,a,a,a).<BR><BR>Added definitions of predefined predicates.<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 PredefinedPredicateTransformerProof</pre><pre>    &#8627 <B>Prolog</B></pre><pre>      &#8627 OrTransformerProof</pre><BR>Clauses:<BR><BR>bid(Hand, Attributes, Points, Bid)&#160;:-&#160;','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).<BR>evaluate(Hand, [], P)&#160;:-&#160;','(hcp(Hand, zero, HCP), ','(adjustments(Hand, MP), ','(isPlus(HCP, MP, U), =(P, U)))).<BR>adjustments(_, zero).<BR>make_bid(Hand, Attributes, Points, 'punt...').<BR>hcp([], N, N).<BR>hcp(.(=(_X, C), Sn), Ni, No)&#160;:-&#160;','(hcp_suit(C, N), ','(','(isPlus(N, Ni, U), =(Nt, U)), hcp(Sn, Nt, No))).<BR>hcp_suit(S, P)&#160;:-&#160;','(honors(S, zero, HP), ','(dist(S, DP), ','(misc(S, MP), ','(isPlus(DP, MP, U), ','(isPlus(HP, U, U1), =(P, U1)))))).<BR>honors([], Pi, Pi).<BR>honors(.(C1, Cn), Pi, Po)&#160;:-&#160;','(honor(C1, P), ','(','(=(X, P), ','(=(X1, zero), isGreater(X, X1))), ','(','(isPlus(P, Pi, U), =(Pt, U)), honors(Cn, Pt, Po)))).<BR>honors(.(C1, Cn), Pi, Pi)&#160;:-&#160;honor(C1, zero).<BR>honor(C, N)&#160;:-&#160;face_card(C, N).<BR>honor(C, zero)&#160;:-&#160;integer(C).<BR>face_card(ace, succ(succ(succ(succ(zero))))).<BR>face_card(king, succ(succ(succ(zero)))).<BR>face_card(queen, succ(succ(zero))).<BR>face_card(jack, succ(zero)).<BR>dist([], succ(succ(succ(zero)))).<BR>dist(.(_, []), succ(succ(zero))).<BR>dist(.(_, .(_, [])), succ(zero)).<BR>dist(.(_, .(_, .(_, _))), zero).<BR>misc(.(ace, []), pred(zero)).<BR>misc(.(king, []), pred(pred(zero))).<BR>misc(.(queen, .(_, [])), pred(pred(zero))).<BR>misc(.(jack, .(_, [])), pred(zero)).<BR>misc(.(_X, .(_Y, .(H3, Rem))), P)&#160;:-&#160;','(honor(H3, X), ','(','(=(X1, X), ','(=(X2, zero), isGreater(X1, X2))), ','(length(Rem, N), ','(','(=(X3, N), ','(=(X4, succ(succ(zero))), isGreater(X3, X4))), ','(isMinus(N, succ(succ(zero)), U), =(P, U)))))).<BR>misc(_, zero).<BR>sort_hand(Hand, SortedHand)&#160;:-&#160;','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).<BR>split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), [])))))&#160;:-&#160;','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).<BR>filter([], _, []).<BR>filter(.(-(Card, Suit), In), Suit, .(Card, Out))&#160;:-&#160;filter(In, Suit, Out).<BR>filter(.(-(_A, X), In), Suit, Out)&#160;:-&#160;','(\==(Suit, X), filter(In, Suit, Out)).<BR>sort_suits([], []).<BR>sort_suits(.(=(S, Ci), In), .(=(S, Co), Out))&#160;:-&#160;','(i_sort(Ci, [], Co), sort_suits(In, Out)).<BR>i_sort([], L, L).<BR>i_sort(.(C1, Cn), Li, Lo)&#160;:-&#160;','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).<BR>insert(X, [], .(X, [])).<BR>insert(X, .(Y, Z), .(X, .(Y, Z)))&#160;:-&#160;higher(X, Y).<BR>insert(X, .(Y, Z), .(Y, L))&#160;:-&#160;','(lower(X, Y), insert(X, Z, L)).<BR>higher(ace, _).<BR>higher(king, X)&#160;:-&#160;\==(X, ace).<BR>higher(queen, X)&#160;:-&#160;','(\==(X, ace), \==(X, king)).<BR>higher(jack, X)&#160;:-&#160;integer(X).<BR>higher(jack, jack).<BR>higher(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), ;(=(X1, X2), isGreater(X1, X2)))))).<BR>lower(king, ace).<BR>lower(queen, X)&#160;:-&#160;','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(succ(zero))), isGreater(X1, X2)))).<BR>lower(jack, X)&#160;:-&#160;','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(zero)), isGreater(X1, X2)))).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), honor(Y, _M)).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isLess(X1, X2))))).<BR>goal&#160;:-&#160;bid(.(-(ace, clubs), .(-(succ(succ(succ(zero))), hearts), .(-(succ(succ(succ(succ(zero)))), spades), .(-(succ(succ(succ(succ(zero)))), diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(zero)))))), clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).<BR>isPlus(zero, X, X).<BR>isPlus(succ(X), zero, succ(X)).<BR>isPlus(succ(X), succ(Y), succ(succ(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(succ(X), pred(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), zero, pred(X)).<BR>isPlus(pred(X), succ(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), pred(Y), pred(pred(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isMinus(X, zero, X).<BR>isMinus(zero, succ(Y), pred(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(zero, pred(Y), succ(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(succ(X), succ(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(succ(X), pred(Y), succ(succ(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), succ(Y), pred(pred(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), pred(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isTimes(X, zero, zero).<BR>isTimes(zero, succ(Y), zero).<BR>isTimes(zero, pred(Y), zero).<BR>isTimes(succ(X), succ(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).<BR>isTimes(succ(X), pred(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).<BR>isTimes(pred(X), succ(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).<BR>isTimes(pred(X), pred(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).<BR>isDiv(zero, succ(Y), zero).<BR>isDiv(zero, pred(Y), zero).<BR>isDiv(succ(X), succ(Y), zero)&#160;:-&#160;isMinus(succ(X), succ(Y), pred(Z)).<BR>isDiv(succ(X), succ(Y), succ(Z))&#160;:-&#160;','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).<BR>isDiv(succ(X), pred(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).<BR>isDiv(pred(X), pred(Y), zero)&#160;:-&#160;isMinus(pred(X), pred(Y), succ(Z)).<BR>isDiv(pred(X), pred(Y), succ(Z))&#160;:-&#160;','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).<BR>isDiv(pred(X), succ(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).<BR>isModulo(X, Y, Z)&#160;:-&#160;','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).<BR>=(X, X).<BR>isGreater(succ(X), zero).<BR>isGreater(succ(X), pred(Y)).<BR>isGreater(succ(X), succ(Y))&#160;:-&#160;isGreater(X, Y).<BR>isGreater(zero, pred(Y)).<BR>isGreater(pred(X), pred(Y))&#160;:-&#160;isGreater(X, Y).<BR>isLess(pred(X), zero).<BR>isLess(pred(X), succ(Y)).<BR>isLess(pred(X), pred(Y))&#160;:-&#160;isLess(X, Y).<BR>isLess(zero, succ(Y)).<BR>isLess(succ(X), succ(Y))&#160;:-&#160;isLess(X, Y).<BR><BR>Queries:<BR><BR>bid(g,a,a,a).<BR><BR>Eliminated all or-constructs.<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 PredefinedPredicateTransformerProof</pre><pre>    &#8627 Prolog</pre><pre>      &#8627 OrTransformerProof</pre><pre>        &#8627 <B>Prolog</B></pre><pre>          &#8627 UndefinedPredicateHandlerProof</pre><BR>Clauses:<BR><BR>bid(Hand, Attributes, Points, Bid)&#160;:-&#160;','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).<BR>evaluate(Hand, [], P)&#160;:-&#160;','(hcp(Hand, zero, HCP), ','(adjustments(Hand, MP), ','(isPlus(HCP, MP, U), =(P, U)))).<BR>adjustments(_, zero).<BR>make_bid(Hand, Attributes, Points, 'punt...').<BR>hcp([], N, N).<BR>hcp(.(=(_X, C), Sn), Ni, No)&#160;:-&#160;','(hcp_suit(C, N), ','(','(isPlus(N, Ni, U), =(Nt, U)), hcp(Sn, Nt, No))).<BR>hcp_suit(S, P)&#160;:-&#160;','(honors(S, zero, HP), ','(dist(S, DP), ','(misc(S, MP), ','(isPlus(DP, MP, U), ','(isPlus(HP, U, U1), =(P, U1)))))).<BR>honors([], Pi, Pi).<BR>honors(.(C1, Cn), Pi, Po)&#160;:-&#160;','(honor(C1, P), ','(','(=(X, P), ','(=(X1, zero), isGreater(X, X1))), ','(','(isPlus(P, Pi, U), =(Pt, U)), honors(Cn, Pt, Po)))).<BR>honors(.(C1, Cn), Pi, Pi)&#160;:-&#160;honor(C1, zero).<BR>honor(C, N)&#160;:-&#160;face_card(C, N).<BR>honor(C, zero)&#160;:-&#160;integer(C).<BR>face_card(ace, succ(succ(succ(succ(zero))))).<BR>face_card(king, succ(succ(succ(zero)))).<BR>face_card(queen, succ(succ(zero))).<BR>face_card(jack, succ(zero)).<BR>dist([], succ(succ(succ(zero)))).<BR>dist(.(_, []), succ(succ(zero))).<BR>dist(.(_, .(_, [])), succ(zero)).<BR>dist(.(_, .(_, .(_, _))), zero).<BR>misc(.(ace, []), pred(zero)).<BR>misc(.(king, []), pred(pred(zero))).<BR>misc(.(queen, .(_, [])), pred(pred(zero))).<BR>misc(.(jack, .(_, [])), pred(zero)).<BR>misc(.(_X, .(_Y, .(H3, Rem))), P)&#160;:-&#160;','(honor(H3, X), ','(','(=(X1, X), ','(=(X2, zero), isGreater(X1, X2))), ','(length(Rem, N), ','(','(=(X3, N), ','(=(X4, succ(succ(zero))), isGreater(X3, X4))), ','(isMinus(N, succ(succ(zero)), U), =(P, U)))))).<BR>misc(_, zero).<BR>sort_hand(Hand, SortedHand)&#160;:-&#160;','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).<BR>split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), [])))))&#160;:-&#160;','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).<BR>filter([], _, []).<BR>filter(.(-(Card, Suit), In), Suit, .(Card, Out))&#160;:-&#160;filter(In, Suit, Out).<BR>filter(.(-(_A, X), In), Suit, Out)&#160;:-&#160;','(\==(Suit, X), filter(In, Suit, Out)).<BR>sort_suits([], []).<BR>sort_suits(.(=(S, Ci), In), .(=(S, Co), Out))&#160;:-&#160;','(i_sort(Ci, [], Co), sort_suits(In, Out)).<BR>i_sort([], L, L).<BR>i_sort(.(C1, Cn), Li, Lo)&#160;:-&#160;','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).<BR>insert(X, [], .(X, [])).<BR>insert(X, .(Y, Z), .(X, .(Y, Z)))&#160;:-&#160;higher(X, Y).<BR>insert(X, .(Y, Z), .(Y, L))&#160;:-&#160;','(lower(X, Y), insert(X, Z, L)).<BR>higher(ace, _).<BR>higher(king, X)&#160;:-&#160;\==(X, ace).<BR>higher(queen, X)&#160;:-&#160;','(\==(X, ace), \==(X, king)).<BR>higher(jack, X)&#160;:-&#160;integer(X).<BR>higher(jack, jack).<BR>lower(king, ace).<BR>lower(queen, X)&#160;:-&#160;','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(succ(zero))), isGreater(X1, X2)))).<BR>lower(jack, X)&#160;:-&#160;','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(zero)), isGreater(X1, X2)))).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), honor(Y, _M)).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isLess(X1, X2))))).<BR>goal&#160;:-&#160;bid(.(-(ace, clubs), .(-(succ(succ(succ(zero))), hearts), .(-(succ(succ(succ(succ(zero)))), spades), .(-(succ(succ(succ(succ(zero)))), diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(zero)))))), clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).<BR>isPlus(zero, X, X).<BR>isPlus(succ(X), zero, succ(X)).<BR>isPlus(succ(X), succ(Y), succ(succ(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(succ(X), pred(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), zero, pred(X)).<BR>isPlus(pred(X), succ(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), pred(Y), pred(pred(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isMinus(X, zero, X).<BR>isMinus(zero, succ(Y), pred(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(zero, pred(Y), succ(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(succ(X), succ(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(succ(X), pred(Y), succ(succ(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), succ(Y), pred(pred(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), pred(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isTimes(X, zero, zero).<BR>isTimes(zero, succ(Y), zero).<BR>isTimes(zero, pred(Y), zero).<BR>isTimes(succ(X), succ(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).<BR>isTimes(succ(X), pred(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).<BR>isTimes(pred(X), succ(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).<BR>isTimes(pred(X), pred(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).<BR>isDiv(zero, succ(Y), zero).<BR>isDiv(zero, pred(Y), zero).<BR>isDiv(succ(X), succ(Y), zero)&#160;:-&#160;isMinus(succ(X), succ(Y), pred(Z)).<BR>isDiv(succ(X), succ(Y), succ(Z))&#160;:-&#160;','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).<BR>isDiv(succ(X), pred(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).<BR>isDiv(pred(X), pred(Y), zero)&#160;:-&#160;isMinus(pred(X), pred(Y), succ(Z)).<BR>isDiv(pred(X), pred(Y), succ(Z))&#160;:-&#160;','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).<BR>isDiv(pred(X), succ(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).<BR>isModulo(X, Y, Z)&#160;:-&#160;','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).<BR>=(X, X).<BR>isGreater(succ(X), zero).<BR>isGreater(succ(X), pred(Y)).<BR>isGreater(succ(X), succ(Y))&#160;:-&#160;isGreater(X, Y).<BR>isGreater(zero, pred(Y)).<BR>isGreater(pred(X), pred(Y))&#160;:-&#160;isGreater(X, Y).<BR>isLess(pred(X), zero).<BR>isLess(pred(X), succ(Y)).<BR>isLess(pred(X), pred(Y))&#160;:-&#160;isLess(X, Y).<BR>isLess(zero, succ(Y)).<BR>isLess(succ(X), succ(Y))&#160;:-&#160;isLess(X, Y).<BR>higher(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), =(X1, X2))))).<BR>higher(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isGreater(X1, X2))))).<BR><BR>Queries:<BR><BR>bid(g,a,a,a).<BR><BR>Added facts for all undefined predicates.<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 PredefinedPredicateTransformerProof</pre><pre>    &#8627 Prolog</pre><pre>      &#8627 OrTransformerProof</pre><pre>        &#8627 Prolog</pre><pre>          &#8627 UndefinedPredicateHandlerProof</pre><pre>            &#8627 <B>Prolog</B></pre><BR>Clauses:<BR><BR>bid(Hand, Attributes, Points, Bid)&#160;:-&#160;','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).<BR>evaluate(Hand, [], P)&#160;:-&#160;','(hcp(Hand, zero, HCP), ','(adjustments(Hand, MP), ','(isPlus(HCP, MP, U), =(P, U)))).<BR>adjustments(_, zero).<BR>make_bid(Hand, Attributes, Points, 'punt...').<BR>hcp([], N, N).<BR>hcp(.(=(_X, C), Sn), Ni, No)&#160;:-&#160;','(hcp_suit(C, N), ','(isPlus(N, Ni, U), ','(=(Nt, U), hcp(Sn, Nt, No)))).<BR>hcp_suit(S, P)&#160;:-&#160;','(honors(S, zero, HP), ','(dist(S, DP), ','(misc(S, MP), ','(isPlus(DP, MP, U), ','(isPlus(HP, U, U1), =(P, U1)))))).<BR>honors([], Pi, Pi).<BR>honors(.(C1, Cn), Pi, Po)&#160;:-&#160;','(honor(C1, P), ','(=(X, P), ','(=(X1, zero), ','(isGreater(X, X1), ','(isPlus(P, Pi, U), ','(=(Pt, U), honors(Cn, Pt, Po))))))).<BR>honors(.(C1, Cn), Pi, Pi)&#160;:-&#160;honor(C1, zero).<BR>honor(C, N)&#160;:-&#160;face_card(C, N).<BR>honor(C, zero)&#160;:-&#160;integer(C).<BR>face_card(ace, succ(succ(succ(succ(zero))))).<BR>face_card(king, succ(succ(succ(zero)))).<BR>face_card(queen, succ(succ(zero))).<BR>face_card(jack, succ(zero)).<BR>dist([], succ(succ(succ(zero)))).<BR>dist(.(_, []), succ(succ(zero))).<BR>dist(.(_, .(_, [])), succ(zero)).<BR>dist(.(_, .(_, .(_, _))), zero).<BR>misc(.(ace, []), pred(zero)).<BR>misc(.(king, []), pred(pred(zero))).<BR>misc(.(queen, .(_, [])), pred(pred(zero))).<BR>misc(.(jack, .(_, [])), pred(zero)).<BR>misc(.(_X, .(_Y, .(H3, Rem))), P)&#160;:-&#160;','(honor(H3, X), ','(=(X1, X), ','(=(X2, zero), ','(isGreater(X1, X2), ','(length(Rem, N), ','(=(X3, N), ','(=(X4, succ(succ(zero))), ','(isGreater(X3, X4), ','(isMinus(N, succ(succ(zero)), U), =(P, U)))))))))).<BR>misc(_, zero).<BR>sort_hand(Hand, SortedHand)&#160;:-&#160;','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).<BR>split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), [])))))&#160;:-&#160;','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).<BR>filter([], _, []).<BR>filter(.(-(Card, Suit), In), Suit, .(Card, Out))&#160;:-&#160;filter(In, Suit, Out).<BR>filter(.(-(_A, X), In), Suit, Out)&#160;:-&#160;','(\==(Suit, X), filter(In, Suit, Out)).<BR>sort_suits([], []).<BR>sort_suits(.(=(S, Ci), In), .(=(S, Co), Out))&#160;:-&#160;','(i_sort(Ci, [], Co), sort_suits(In, Out)).<BR>i_sort([], L, L).<BR>i_sort(.(C1, Cn), Li, Lo)&#160;:-&#160;','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).<BR>insert(X, [], .(X, [])).<BR>insert(X, .(Y, Z), .(X, .(Y, Z)))&#160;:-&#160;higher(X, Y).<BR>insert(X, .(Y, Z), .(Y, L))&#160;:-&#160;','(lower(X, Y), insert(X, Z, L)).<BR>higher(ace, _).<BR>higher(king, X)&#160;:-&#160;\==(X, ace).<BR>higher(queen, X)&#160;:-&#160;','(\==(X, ace), \==(X, king)).<BR>higher(jack, X)&#160;:-&#160;integer(X).<BR>higher(jack, jack).<BR>lower(king, ace).<BR>lower(queen, X)&#160;:-&#160;','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(succ(zero))), isGreater(X1, X2)))).<BR>lower(jack, X)&#160;:-&#160;','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(zero)), isGreater(X1, X2)))).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), honor(Y, _M)).<BR>lower(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isLess(X1, X2))))).<BR>goal&#160;:-&#160;bid(.(-(ace, clubs), .(-(succ(succ(succ(zero))), hearts), .(-(succ(succ(succ(succ(zero)))), spades), .(-(succ(succ(succ(succ(zero)))), diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(zero)))))), clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).<BR>isPlus(zero, X, X).<BR>isPlus(succ(X), zero, succ(X)).<BR>isPlus(succ(X), succ(Y), succ(succ(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(succ(X), pred(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), zero, pred(X)).<BR>isPlus(pred(X), succ(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), pred(Y), pred(pred(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isMinus(X, zero, X).<BR>isMinus(zero, succ(Y), pred(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(zero, pred(Y), succ(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(succ(X), succ(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(succ(X), pred(Y), succ(succ(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), succ(Y), pred(pred(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), pred(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isTimes(X, zero, zero).<BR>isTimes(zero, succ(Y), zero).<BR>isTimes(zero, pred(Y), zero).<BR>isTimes(succ(X), succ(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).<BR>isTimes(succ(X), pred(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).<BR>isTimes(pred(X), succ(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).<BR>isTimes(pred(X), pred(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).<BR>isDiv(zero, succ(Y), zero).<BR>isDiv(zero, pred(Y), zero).<BR>isDiv(succ(X), succ(Y), zero)&#160;:-&#160;isMinus(succ(X), succ(Y), pred(Z)).<BR>isDiv(succ(X), succ(Y), succ(Z))&#160;:-&#160;','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).<BR>isDiv(succ(X), pred(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).<BR>isDiv(pred(X), pred(Y), zero)&#160;:-&#160;isMinus(pred(X), pred(Y), succ(Z)).<BR>isDiv(pred(X), pred(Y), succ(Z))&#160;:-&#160;','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).<BR>isDiv(pred(X), succ(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).<BR>isModulo(X, Y, Z)&#160;:-&#160;','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).<BR>=(X, X).<BR>isGreater(succ(X), zero).<BR>isGreater(succ(X), pred(Y)).<BR>isGreater(succ(X), succ(Y))&#160;:-&#160;isGreater(X, Y).<BR>isGreater(zero, pred(Y)).<BR>isGreater(pred(X), pred(Y))&#160;:-&#160;isGreater(X, Y).<BR>isLess(pred(X), zero).<BR>isLess(pred(X), succ(Y)).<BR>isLess(pred(X), pred(Y))&#160;:-&#160;isLess(X, Y).<BR>isLess(zero, succ(Y)).<BR>isLess(succ(X), succ(Y))&#160;:-&#160;isLess(X, Y).<BR>higher(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), =(X1, X2))))).<BR>higher(X, Y)&#160;:-&#160;','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isGreater(X1, X2))))).<BR>integer(X0).<BR>length(X0, X1).<BR>\==(X0, X1).<BR><BR>Queries:<BR><BR>bid(g,a,a,a).<BR><BR><BR></body>

