type([id,nonce,nc,pk,sk,ts]).

typed_subterm(A,A).
  
typed_subterm(T,T1):-
  compound(T),
  type(Types),
  T  =..[F|Arg],
  \+(member(F,Types)),
  member(A,Arg),
  typed_subterm(A,T1).

%%%%
weak_unify(X,X,X):-
 atomic(X),!.

weak_unify(X,Y,Y):-
 var(X),
 unify_with_occurs_check(X,Y),!.

weak_unify(X,Y,Y):-
 nonvar(X),
 var(Y),
 unify_with_occurs_check(X,Y),!.
 
weak_unify(T,T1,T2):-
 compound(T),
 compound(T1),
 T \= sup(_),
 T1 \= sup(_),!,
 T  =..[F|Arg],
 T1 =..[F|Arg1],
 unif_arg(Arg,Arg1,Arg2),
 T2=..[F|Arg2].

weak_unify(T,T1,T2):-
 compound(T),
 T \= sup(_),
 T1  = sup(S),!,
 typed_subterm(T,SubT),
 weak_unify(SubT,S,T2).

weak_unify(T,T1,SubT2):-
 compound(T),
 T1 \= sup(_),
 T  = sup(S),!,
 typed_subterm(T1,SubT1),
 weak_unify(S,SubT1,SubT2).

weak_unify(T,T1,T1):-
 compound(T),
 T = sup(_),
 T1 = sup(_),!.

unif_arg([A|R],[B|S],[B1|S1]):-
 weak_unify(A,B,B1),
 unif_arg(R,S,S1).

unif_arg([],[],[]).

%%%%

subsumes_sup(X,T,T1):-
 subsumes_sup(X,T,[],_,T1).

subsumes_sup(X,T,L,[a(X,T)|L],T):-
 var(X),
 \+ chklist(X,L,_),
 !.

subsumes_sup(X,T,L,L,T):-
 var(X),
 chklist(X,L,Y),
 Y == T,
 !.

chklist(X,L,Y):-
 member(a(X1,Y),L),
 X1==X.

subsumes_sup(A,A,L,L,A):-
  atomic(A),!.

subsumes_sup(T,T1,L,L1,sup(SubT1)):-
 compound(T),
 compound(T1),
 T = sup(S),
 T1 \= sup(_),!,
 typed_subterm(T1,SubT1),
 subsumes_sup(S,SubT1,L,L1,SubT1).

subsumes_sup(T,T1,L,L1,sup(SubS1)):-
 compound(T),
 compound(T1),
 T = sup(S),
 T1 = sup(S1),!,
 typed_subterm(S1,SubS1),
 subsumes_sup(S,SubS1,L,L1,SubT1).

subsumes_sup(T,T1,L,L1,T2):-
 compound(T),
 compound(T1),
 T  \= sup(_),
 T1 \= sup(_),
 !,
 T  =..[F|Arg],
 T1 =..[F|Arg1],
 !,
 subsumes_arg_sup(Arg,Arg1,L,L1,Arg2),
 T2=..[F|Arg2].
 
 
subsumes_arg_sup([A|R],[B|S],L,L2,[B1|S1]):-
 subsumes_sup(A,B,L,L1,B1),
 subsumes_arg_sup(R,S,L1,L2,S1).
 
subsumes_arg_sup([],[],L,L,[]).