/usr/share/doc/prover9-doc/examples/ring41.in is in prover9-doc 0.0.200902a-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 | assign(iterate, primes).
% The following fixes [+,-,*] as the ring of integers (mod domain_size).
set(integer_ring).
formulas(assumptions).
% Assume that f and g have a ring structure.
g(x) = M * x.
f(x,y) = (H * x) + (K * y).
% Denial of associativity.
f(f(a,b),c) != f(a,f(b,c)).
end_of_list.
formulas(assumptions).
% Each of these equations was a candidate for being a single axiom
% for group theory.
%
% We can show that each has a nonassociative model (and therefore
% is not a single axiom) by using ring structures.
%
% The sizes required for these examples range from 11 to 41.
% f(f(g(f(y,g(z))),x),f(f(g(f(z,x)),z),y)) = z. % candidate 1
% f(f(x,f(g(x),z)),f(g(f(f(y,x),g(x))),y)) = z. % candidate 64
% f(f(f(x,x),g(x)),g(f(g(f(y,z)),f(y,x)))) = z. % candidate 30
g(f(g(f(y,f(x,z))),f(y,f(f(x,x),g(x))))) = z. % candidate 107
% g(f(g(f(x,f(y,z))),f(f(f(g(x),x),x),y))) = z. % candidate 60
% f(f(y,g(f(z,y))),f(f(z,g(f(x,g(z)))),x)) = z. % candidate 68
% f(f(x,y),f(y,g(f(f(g(f(g(x),z)),y),y)))) = z. % candidate 11
end_of_list.
|