%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%     Exercise 3: Proof of Fermat's Last Theorem
%         (Lite version, without 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).


% Propositional logic version

FLT_lite_prop: THEORY

BEGIN

  IMPORTING FLT_lite

  a_soln: solution   %% Candidate solution to Fermat equation


  all_semistable_elliptic_curves_are_modular: bool


% Assume the following lemmas (don't try to prove them).

  Frey_is_elliptic: LEMMA
        FLT_cond(a_soln) IMPLIES elliptic_curve?(Frey_eqn(a_soln))


  semistable_TSC: LEMMA
        all_semistable_elliptic_curves_are_modular

  semistable_modular_Frey: LEMMA
        all_semistable_elliptic_curves_are_modular AND
        elliptic_curve?(Frey_eqn(a_soln)) AND
        semistable(Frey_eqn(a_soln))
     IMPLIES
        modular(Frey_eqn(a_soln))

  Frey_not_modular: LEMMA
        FLT_cond(a_soln) AND
        solves(a_soln, Fermat_eqn)
     IMPLIES
        semistable(Frey_eqn(a_soln)) AND
        NOT modular(Frey_eqn(a_soln))


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

  FLT_extra_lite: THEOREM
           NOT (FLT_cond(a_soln) AND solves(a_soln, Fermat_eqn))


END FLT_lite_prop