Online Otter-λ
-->
Examples
% 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.