%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%     Exercise 3: Proof of Fermat's Last Theorem (Lite version)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% DISCLAIMER: The following is a highly abstract and abridged 
% formulation intended solely as a theorem proving exercise.  Do
% not take this as a serious rendition of the mathematics involved.


FLT_lite: THEORY

BEGIN

  equation: TYPE+
  solution: TYPE+


  solves: [solution, equation -> bool]

  elliptic_curve?: [equation -> bool]

  elliptic_curve: TYPE = {e: equation | elliptic_curve?(e)}


  semistable(e: elliptic_curve): bool

  modular(e: elliptic_curve): bool


% Following represents the celebrated equation x^n + y^n = z^n
% studied by Pierre de Fermat.

  Fermat_eqn: equation

  FLT_cond(s: solution): bool  %% x,y,z,n nonnegative integers and n > 2


% Following represents the elliptic curve studied by Gerhard Frey,
% Y^2 = X(X - x^n)(X + y^n), whose coefficients come from the terms
% of Fermat's equation.

  Frey_eqn(s: solution): equation


END FLT_lite