## Examples

Examples -> Algebra -> homomorphism.in% composition of group homomorphisms is a homomorphism

set(lambda).

set(demod_inf).

set(para_into).

set(para_from).

assign(max_distinct_vars,0).

% Hom(xG,xH,xPhi) means Phi is a homomorphism from G to H

% that is, forall x,y in xG, we have Phi(x*y) = Phi(x) * Phi(y) and Phi(i(x)) = i(Phi(y)).

list(usable).

Ap(G,x) != $T | Ap(H,Ap(Phi,x)) = $T. % Phi maps G to H

Ap(H,x) != $T | Ap(K,Ap(Psi,x)) = $T. % Psi maps H to K

Ap(G,x) != $T | Ap(G,y) != $T | Ap(Phi,x*y) = Ap(Phi,x) * Ap(Phi,y). %Phi preserves product on G

Ap(G,x) != $T | Ap(Phi,i(x)) = i(Ap(Phi,x)). %Phi preserves inverse

Ap(H,x) != $T | Ap(H,y) != $T | Ap(Psi,x*y) = Ap(Psi,x) * Ap(Psi,y). %Psi preserves product on H

Ap(H,x) != $T | Ap(Psi,i(x)) = i(Ap(Psi,x)). %Psi preserves inverse

Ap(G,a) = $T.

Ap(G,b) = $T.

end_of_list.

list(demodulators).

Ap(G,a) = $T.

Ap(G,b) = $T.

Chi = lambda(x,Ap(Psi,Ap(Phi,x))). % Chi is the composition of Phi and Psi

(x=x) = $T.

end_of_list.

list(sos).

Ap(Chi,a*b) != Ap(Chi,a) * Ap(Chi,b) | Ap(Chi,i(a)) != i(Ap(Chi,a)) | Ap(K,Ap(Chi,a)) != $T.

end_of_list.