# $Id: list.n3 1295 2007-05-11 16:52:51Z josd $
# PxButton | test  | python euler.py list.n3
# PxButton | proof | python euler.py --why list.n3

@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix list: <http://www.w3.org/2000/10/swap/list#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix : <http://eulersharp.sourceforge.net/2005/11swap/list#>.

{?L rdf:first ?I} => {?I list:in ?L}.
{?L rdf:rest ?R. ?I list:in ?R} => {?I list:in ?L}.

{?L rdf:rest (). ?L rdf:first ?I} => {?I list:last ?L}.
{?L rdf:rest ?R. ?I list:last ?R} => {?I list:last ?L}.

() :length 0.
{?L rdf:rest ?T. ?T :length ?M. (?M 1) math:sum ?N} => {?L :length ?N}.

(() ?L) :sum ?L.
{(?L1 ?L2) :sum ?L} => {((?A/?L1) ?L2) :sum (?A/?L)}.

(() ?A) :remove ().
{(?L1 ?A) :remove ?L} => {((?A/?L1) ?A) :remove ?L}.
{?A log:notEqualTo ?B. (?L1 ?A) :remove ?L} => {((?B/?L1) ?A) :remove (?B/?L)}.

(?L ()) :difference ?L.
{(?L1 ?A) :remove ?R. (?R ?L2) :difference ?L} => {(?L1 (?A/?L2)) :difference ?L}.

{?X list:in (:a :b :c :d :e :f :g)} => [].
{?X list:last (:a :b :c :d :e :f :g)} => [].
{(:a :b :c :d :e :f :g) :length ?X} => [].
{((:a :b :c) (:d :e :f :g)) :sum ?X} => [].
{((:a :b :c :d :e :f :g) (:g :f :b :e)) :difference ?X} => [].