%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%     Exercise 4: Proof of Fermat's Last Theorem 
%         (Lite version, with quantifiers)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% Major results:
%
%   1) Solution to Fermat's equation implies the Frey curve is
%      semistable but not modular (due to Kenneth Ribet).
%
%   2) All semistable elliptic curves with rational coefficients
%      are modular (semistable case of Taniyama-Shimura Conjecture)
%      (due to Andrew Wiles).




% Predicate logic version

FLT_lite_pred: THEORY

BEGIN

  IMPORTING FLT_lite


% Assume the following lemmas.

  Frey_is_elliptic: LEMMA
     FORALL (s: solution):
        FLT_cond(s) IMPLIES elliptic_curve?(Frey_eqn(s))


  semistable_TSC: LEMMA
     FORALL (E: equation):
        elliptic_curve?(E) AND semistable(E) IMPLIES modular(E)

  Frey_not_modular: LEMMA
     FORALL (s: solution):
        FLT_cond(s) AND solves(s, Fermat_eqn) IMPLIES
           semistable(Frey_eqn(s)) AND NOT modular(Frey_eqn(s))


% Prove following theorem using only SPLIT, FLATTEN, LEMMA, and
% quantifier rules.

  FLT_very_lite: THEOREM 
          NOT EXISTS (s: solution):
                 FLT_cond(s) AND solves(s, Fermat_eqn)


END FLT_lite_pred