Re: My first lptp proof

Update:

mylist([]).
mylist([_|L]) :- mylist(L).

mymember(X,[X|_]).
mymember(X,[_|L]) :- mymember(X,L).

myappend([],L,L).
myappend([X|L1],L2,[X|L3]) :- myappend(L1,L2,L3).

mysublist([],[]).
mysublist([X|L1],L2) :- mysublist(L1,L2).
mysublist([X|L1],[X|L2]) :- mysublist(L1,L2).

mysublist_rem([],[],[]).
mysublist_rem([X|L1],L2,[X|L3]) :- mysublist_rem(L1,L2,L3).
mysublist_rem([X|L1],[X|L2],L3) :- mysublist_rem(L1,L2,L3).

More theorems (partial listing):

| ?- facts(mysublist_rem).
facts(mysublist_rem).

lemma(mysublist_rem:types:1)
all [l1,l2,l3]: succeeds mysublist_rem(?l1,?l2,?l3) => succeeds mylist(?l1).

lemma(mysublist_rem:types:2)
all [l1,l2,l3]: succeeds mysublist_rem(?l1,?l2,?l3) & succeeds mylist(?l2) =>
succeeds mylist(?l3).

lemma(mysublist_rem:mysublist:1)
all [l1,l2,l3]: succeeds mysublist_rem(?l1,?l2,?l3) =>
  succeeds mysublist(?l1,?l2).

lemma(mysublist_rem:mysublist:2)
all [l1,l2,l3]: succeeds mysublist_rem(?l1,?l2,?l3) =>
  succeeds mysublist(?l1,?l3).

lemma(mysublist_rem:mymember:1)
all [x,l1,l2,l3]: succeeds mysublist_rem(?l1,?l2,?l3) &
 succeeds mymember(?x,?l2) => succeeds mymember(?x,?l1).

lemma(mysublist_rem:mymember:2)
all [x,l1,l2,l3]: succeeds mysublist_rem(?l1,?l2,?l3) &
 succeeds mymember(?x,?l3) => succeeds mymember(?x,?l1).

Currently stuck trying to prove:

 all [l1,l2,l3,x]:
    succeeds mysublist_rem(?l1,?l2,?l3) & succeeds mymember(?x,?l1) =>
      succeeds mymember(?x,?l2) \/ succeeds mymember(?x,?l3).

Apparently, there is something else that needs to be proved first
but I haven't figured out what it is.

--
.