%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Short course on
% Interactively Proving Mathematical Theorems
% Summer Workshop in Mathematics UnB, 2020
%
% Exercise set on Propositional deduction
%
% Thaynara Arielly de Lima UFG
% Mauricio Ayala-Rincon UnB
% Last modified: March 2 2020
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
prop_algebra: THEORY
BEGIN
% Cyclic : Exists x : For all y : x + ... + x = y
% Abelian : For all x, y : x + y = y + x
% Symmetric_n : ({ f :{1,...,n} -> {1,...,n} | f bijective}, o)
% nGT2 : n is greater than 2 in Symmetric_n
% FiniteDegree : For all y: Exists n: y^n = one
Finite, Infinite, Cyclic, Abelian, Symmetric_n, nGT2, FiniteDegree, Torsion, AbelTorsion: bool
Ax01 : Axiom Cyclic => Abelian
Ax02 : Axiom Symmetric_n AND nGT2 => NOT Abelian
Ax03 : AXIOM FiniteDegree <=> Torsion
Ax04 : AXIOM Finite => FiniteDegree
Ax05 : AXIOM NOT Finite <=> Infinite
AX06 : AXIOM Abelian AND Torsion <=> AbelTorsion
Pr01 : CONJECTURE Symmetric_n AND Cyclic => NOT nGT2
Pr02 : CONJECTURE Finite => Torsion
Pr03 : CONJECTURE Cyclic AND Finite => AbelTorsion
Pr04 : CONJECTURE NOT Torsion => Infinite
END prop_algebra