%
% lists (binary trees) with strict subterm ordering
% 


use(to,[< = @<, =< = @=<]).
use(simple_lists).

% subterm ordering

X @< cons(X,Y).
Y @< cons(X,Y).

% discreteness of the ordering
X @< Y -> X @=< car(Y), X @=< cdr(Y).



/*
Here's a proof that the subterm ordering is not dense (clause 13):

Proof:
======

   7 : car(cons(A,B))=A                                                 [input]
   8 : cdr(cons(A,B))=B                                                 [input]
   9 : cons(car(A),cdr(A))=A                                            [input]
  10 : A@<cons(A,B)                                                     [input]
  12 : A@<B -> A@=<car(B),A@=<cdr(B)                                    [input]
  13 + ~!A,B.(?C.(B@<A=>B@<C and C@<A)) ->                              [input]
  14 : A@=<B,B@=<car(A),B@=<cdr(A)                [totality resolution from 12]
  15 + !A,B.(?C.(B@<A=>B@<C and C@<A))                 [reduction of 13 by [L]]
  16 + ?C.(A@<B=>A@<C and C@<B)                            [condensement of 15]
  17 : car(A)@<cdr(A),B@=<car(A),A@=<B                        [factoring on 14]
  22 + A@<B -> A@<s$3(A,B)and s$3(A,B)@<B                   [expansion from 16]
  23 : car(A)@<A                                        [chaining of 9 from 10]
  26 + A@=<B,B@<s$3(B,A)and s$3(B,A)@<A           [totality resolution from 22]
  27 + A@=<B,B@<s$3(B,A)                                    [expansion from 26]
  28 + A@=<B,s$3(B,A)@<A                                    [expansion from 26]
  99 + A@<car(B),car(B)@<cdr(B),B@=<s$3(A,C),C@=<A     [chaining of 17 from 27]
 332 + A@<B,B@=<C,C@<car(A),car(A)@<cdr(A),B@=<C       [chaining of 28 from 99]
 345 + A@<B,C@<car(A),car(A)@<cdr(A),B@=<C                [condensement of 332]
 346 + A@<car(B),B@=<A,car(B)@<cdr(B)           [variable elimination from 345]
 347 + A@=<car(A),car(A)@<cdr(A)                [variable elimination from 346]
 348 + car(A)@<cdr(A)                              [reduction of 347 by [23,L]]
 387 + car(cons(A,B))@<B                               [chaining of 8 from 348]
 391 + A@<B                                           [reduction of 387 by [7]]

Length = 23, Depth = 14, Search Depth = 3

*/