# $Id: lists.n3,v 1.2 2001/10/01 00:12:35 amdus Exp $

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix dpo: <http://www.daml.org/2001/03/daml+oil#>.
@prefix : <lists#>.

this log:forAll :a, :b, :c, :x.
:x :in [ dpo:first :x; dpo:rest :b].
{:x :in :b} log:implies {:x :in [ dpo:first :a; dpo:rest :b]}.

[ :l1 dpo:nil; :l2 :x; :l12 :x].
{[ :l1 :a; :l2 :b; :l12 :c]} log:implies {[:l1 [ dpo:first :x; dpo:rest :a]; :l2 :b; :l12 [ dpo:first :x; dpo:rest :c]]}.