Online Otter-λ

Examples

Examples -> SetTheory -> setdistrib.prf


1 [] in(x,y)=Ap(y,x).
3 [] j=lambda(u,lambda(v,lambda(x,and(in(x,u),in(x,v))))).
4 [] i=lambda(u,lambda(v,lambda(x,or(in(x,u),in(x,v))))).
5 [] or(x,and(y,z))=and(or(x,y),or(x,z)).
12 [] x=x.
13 [] Ap(Ap(i,p),Ap(Ap(j,q),r))!=Ap(Ap(j,Ap(Ap(i,p),q)),Ap(Ap(i,p),r)).
14 [copy,13,demod,4,1,1,beta,3,1,1,beta,beta,beta,beta,5,3,1,1,4,1,1,beta,beta,beta,beta,4,1,1,beta,beta,beta,beta] lambda(x,and(or(Ap(p,x),Ap(q,x)),or(Ap(p,x),Ap(r,x))))!=lambda(y,and(or(Ap(p,y),Ap(q,y)),or(Ap(p,y),Ap(r,y)))).
15 [binary,14.1,12.1] $F.