# Generated with Euler on Tue Apr 24 22:27:03 GMT+02:00 2001
#
# {:x :list {:y :list :nil}} :append {<data:,a> :list {<data:,b> :list {<data:,c> :list :nil}}}.

@prefix log: <http://www.w3.org/2000/10/swap/log.n3#>.
@prefix : <file:/euler/lists.axiom.n3#>.

{:nil :list {{<data:,a> :list {<data:,b> :list {<data:,c> :list :nil}}} :list :nil}} :append {<data:,a> :list {<data:,b> :list {<data:,c> :list :nil}}}.

 {{:nil :list {{<data:,b> :list {<data:,c> :list :nil}} :list :nil}} :append {<data:,b> :list {<data:,c> :list :nil}}} log:implies
{{{<data:,a> :list :nil} :list {{<data:,b> :list {<data:,c> :list :nil}} :list :nil}} :append {<data:,a> :list {<data:,b> :list {<data:,c> :list :nil}}}}.

 {{{:nil :list {{<data:,c> :list :nil} :list :nil}} :append {<data:,c> :list :nil}} log:implies
  {{{<data:,b> :list :nil} :list {{<data:,c> :list :nil} :list :nil}} :append {<data:,b> :list {<data:,c> :list :nil}}}} log:implies
{{{<data:,a> :list {<data:,b> :list :nil}} :list {{<data:,c> :list :nil} :list :nil}} :append {<data:,a> :list {<data:,b> :list {<data:,c> :list :nil}}}}.

 {{{{:nil :list {:nil :list :nil}} :append :nil} log:implies
    {{{<data:,c> :list :nil} :list {:nil :list :nil}} :append {<data:,c> :list :nil}}} log:implies
  {{{<data:,b> :list {<data:,c> :list :nil}} :list {:nil :list :nil}} :append {<data:,b> :list {<data:,c> :list :nil}}}} log:implies
{{{<data:,a> :list {<data:,b> :list {<data:,c> :list :nil}}} :list {:nil :list :nil}} :append {<data:,a> :list {<data:,b> :list {<data:,c> :list :nil}}}}.

# Proof found in 14 steps (2847 steps/sec)