% Input data:

% (1) obligatory:
%     ===========

pred_def( void/0, [], [], [] ).
 
init_clause(( void :- true )).
 
ex( void, true ).
 

% (2) List Processing: Membership 
%     ===========================
 
pred_def( mmember/2, [ -x, +xl ], [ mmember/2 ], [] ).
 
ex(mmember(a,[a]),true).        % 1
ex(mmember(c,[b,c]),true).      % 2


% The session of WiM
% ==================

Examples of mmember(X,Y)

   mmember(a,[a]), true
   mmember(c,[b,c]), true


Found clause after searching 1 clauses:
    mmember(X,[X|Y]):-true.

Found clause after searching 3 clauses:
    mmember(X,[Y|Z]):-mmember(X,Z).


Found predicate after searching 4 clauses (Total = 4) :
    mmember(X,[Y|Z]):-mmember(X,Z).
    mmember(U,[U|V]):-true.
with no need of assumption.
OK (yes. / no. / continue. / new example) ?  continue.

 
The most preferable example is   mmember(a,[a]) . 

An extended constant set is   [a,new] . 

New assumptions are generated ... 

After a replacement of an individual constant: mmember(new,[a])

Examples of mmember(X,Y)

   mmember(a,[a]), true
   mmember(c,[b,c]), true
   mmember(new,[a]), false


Found clause after searching 1 clauses:
    mmember(X,[X|Y]):-true.

Found clause after searching 3 clauses:
    mmember(X,[Y|Z]):-mmember(X,Z).


After deleting a list element: mmember(a,[])

Examples of mmember(X,Y)

   mmember(a,[a]), true
   mmember(c,[b,c]), true
   mmember(a,[]), false


Found clause after searching 1 clauses:
    mmember(X,[X|Y]):-true.

Found clause after searching 3 clauses:
    mmember(X,[Y|Z]):-mmember(X,Z).


After adding a list element: mmember(a,[a,a])

Examples of mmember(X,Y)

   mmember(a,[a]), true
   mmember(c,[b,c]), true
   mmember(a,[a,a]), false


Found clause after searching 2 clauses:
    mmember(X,[X]):-true.


After adding a list element: mmember(a,[a,a])

Examples of mmember(X,Y)

   mmember(a,[a]), true
   mmember(c,[b,c]), true
   mmember(a,[a,a]), false


Found clause after searching 2 clauses:
    mmember(X,[X]):-true.


After adding a list element: mmember(a,[new,a])

Examples of mmember(X,Y)

   mmember(a,[a]), true
   mmember(c,[b,c]), true
   mmember(a,[new,a]), false


Found clause after searching 1 clauses:
    mmember(X,[X|Y]):-true.


After adding a list element: mmember(a,[a,new])

Examples of mmember(X,Y)

   mmember(a,[a]), true
   mmember(c,[b,c]), true
   mmember(a,[a,new]), false


Found clause after searching 2 clauses:
    mmember(X,[X]):-true.

Found clause after searching 4 clauses:
    mmember(X,[Y|Z]):-mmember(X,Z).


mmember(a,[a,new]) assumed to be false. O.K. ? (yes. /no. / unknown) yes.

Found predicate after searching 4 clauses (Total = 23) :

    mmember(X,[Y|Z]):-mmember(X,Z).
    mmember(U,[U]):-true.

under assumption that 

    mmember(a,[a,new]) = false


OK (yes. / no. / continue. / new example) ?  yes.

The found solutions :

    mmember(X,[Y|Z]):-mmember(X,Z).
    mmember(U,[U|V]):-true.


    mmember(X,[Y|Z]):-mmember(X,Z).
    mmember(U,[U]):-true.
    =  under assumption that  mmember(a,[a,new]) = false