Online Otter-λ

Examples

Examples -> Algebra -> homomorphism.prf

1 [] Ap(G,x)!=$T|Ap(H,Ap(Phi,x))=$T.
2 [] Ap(H,x)!=$T|Ap(K,Ap(Psi,x))=$T.
3 [] Ap(G,x)!=$T|Ap(G,y)!=$T|Ap(Phi,x*y)=Ap(Phi,x)*Ap(Phi,y).
4 [] Ap(G,x)!=$T|Ap(Phi,i(x))=i(Ap(Phi,x)).
5 [] Ap(H,x)!=$T|Ap(H,y)!=$T|Ap(Psi,x*y)=Ap(Psi,x)*Ap(Psi,y).
6 [] Ap(H,x)!=$T|Ap(Psi,i(x))=i(Ap(Psi,x)).
8 [] Ap(G,b)=$T.
9 [] Ap(G,a)=$T.
10 [] Ap(G,b)=$T.
11 [] Chi=lambda(x,Ap(Psi,Ap(Phi,x))).
12 [] (x=x)=$T.
13 [] Ap(Chi,a*b)!=Ap(Chi,a)*Ap(Chi,b)|Ap(Chi,i(a))!=i(Ap(Chi,a))|Ap(K,Ap(Chi,a))!=$T.
14 [para_into,13.3.2,8.1.2,demod,11,beta,11,beta,11,beta,11,beta,11,beta,11,beta,10] Ap(Psi,Ap(Phi,a*b))!=Ap(Psi,Ap(Phi,a))*Ap(Psi,Ap(Phi,b))|Ap(Psi,Ap(Phi,i(a)))!=i(Ap(Psi,Ap(Phi,a)))|Ap(K,Ap(Psi,Ap(Phi,a)))!=$T.
19 [para_into,14.3.1,2.2.1,demod,12,propositional] Ap(Psi,Ap(Phi,a*b))!=Ap(Psi,Ap(Phi,a))*Ap(Psi,Ap(Phi,b))|Ap(Psi,Ap(Phi,i(a)))!=i(Ap(Psi,Ap(Phi,a)))|Ap(H,Ap(Phi,a))!=$T.
24 [para_into,19.3.1,1.2.1,demod,12,9,12,propositional] Ap(Psi,Ap(Phi,a*b))!=Ap(Psi,Ap(Phi,a))*Ap(Psi,Ap(Phi,b))|Ap(Psi,Ap(Phi,i(a)))!=i(Ap(Psi,Ap(Phi,a))).
26 [para_into,24.2.1.2,4.2.1,demod,9,12,propositional] Ap(Psi,Ap(Phi,a*b))!=Ap(Psi,Ap(Phi,a))*Ap(Psi,Ap(Phi,b))|Ap(Psi,i(Ap(Phi,a)))!=i(Ap(Psi,Ap(Phi,a))).
29 [para_into,26.2.1,6.2.1,demod,12,propositional] Ap(Psi,Ap(Phi,a*b))!=Ap(Psi,Ap(Phi,a))*Ap(Psi,Ap(Phi,b))|Ap(H,Ap(Phi,a))!=$T.
32 [para_into,29.2.1,1.2.1,demod,12,9,12,propositional] Ap(Psi,Ap(Phi,a*b))!=Ap(Psi,Ap(Phi,a))*Ap(Psi,Ap(Phi,b)).
33 [para_into,32.1.1.2,3.3.1,demod,9,12,10,12,propositional] Ap(Psi,Ap(Phi,a)*Ap(Phi,b))!=Ap(Psi,Ap(Phi,a))*Ap(Psi,Ap(Phi,b)).
34 [para_into,33.1.1,5.3.1,demod,12,propositional] Ap(H,Ap(Phi,a))!=$T|Ap(H,Ap(Phi,b))!=$T.
35 [para_into,34.1.1,1.2.1,demod,12,9,12,propositional] Ap(H,Ap(Phi,b))!=$T.
37 [para_into,35.1.1,1.2.1,demod,12,10,12,propositional] $F.