#    Axioms for lists using compact lists
# 
@prefix rdf:  <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix s: <http://www.w3.org/2000/01/rdf-schema#> .
# @prefix daml:  <http://www.daml.org/2000/10/daml-ont#> .
# @prefix dpo:  <http://www.daml.org/2001/03/daml+oil#> .
# @prefix ex:   <http://www.daml.org/2000/10/daml-ex#> .
@prefix log:  <http://www.w3.org/2000/10/swap/log#> .

@prefix : <foo.n3#>.  # Local stuff

# @prefix foo: <http://www.w3.org/2000/10/swap/test/includes/foo.n3#>.  # Local stuff
@prefix foo: <foo.n3#>.  # Local stuff



@forAll :d, :e, :l, :m, :n, :o, :p, :s, :S, :s1, :x, :y, :F, :G, :H.

# List generators are things which work as lists and also if you
# use them as a predicate they construct a list one longer.

() a :compactList.

{  :l  ()  :m }  log:implies {  :l a :compactList.
          :l :tail :m }.

{ :k :l :e.  :l a :compactList } log:implies {
        :k a :compactList}.

{ :k :l :e.  :l a :compactList } log:implies { :k daml:first :e; daml:rest :l.}.

#ends