% ================================================================= %
% THF0 TPTP Code                                                    %
%                                                                   %
% This input file includes an encoding of quantales in THF0 syntax  %
% and shows 0 is the least element of arbitrary sums.               %
%                                                                   %
%                                                                   %
%                                              (c) 2009 H.-H. Dang  %
% ================================================================= %

% ============================== %
% Usual Definition of Set Theory %
% ============================== %

thf(emptyset,type,(
    emptyset: $i > $o )).

thf(emptyset_def,definition,
    ( emptyset
    = ( ^ [X: $i] : $false ) )).

thf(union,type,(
    union: ( $i > $o ) > ( $i > $o ) > $i > $o )).

thf(union_def,definition,
    ( union
    = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
          ( ( X @ U )
          | ( Y @ U ) ) ) )).

thf(union_comm,axiom,(
    ! [X: $i > $o, Y: $i > $o] :
      ( ( union @ X @ Y ) = ( union @ Y @ X ) 
      ) )).

thf(union_asso,axiom,(
    ! [X: $i > $o, Y: $i > $o, Z: $i > $o] : (
      ( union @ ( union @ X @ Y ) @ Z ) = ( union @ X @ ( union @ Y @ Z ) ) 
      ) )).

thf(union_idem,axiom,(
    ! [X: $i > $o] :
      ( ( union @ X @ X ) = X 
      ) )).

thf(union_empty,axiom,(
    ! [X: $i > $o] :
      ( ( union @ X @ emptyset ) = X 
      ) )).

thf(singleton,type,(
    singleton: ( $i > $i > $o ) )).

thf(singleton_def,definition,
    ( singleton
    = ( ^ [X: $i,U: $i] : ( U = X ) ) )).

% ======================== %
%   Supremum Definition    %
% ======================== %

thf(zero,type,(
    zero: $i )).

thf(sup,type,(
    sup: ( ( $i > $o ) > $i ) )).

thf(sup_es,axiom,(
    (sup @ emptyset) = zero
    )).

thf(sup_singleset,axiom,(
    ! [X: $i] : ( ( sup @ ( singleton @ X ) ) = X ) )).

thf(supset,type,(
    supset: ( ( ( $i > $o ) > $o ) > $i > $o ) )).

thf(supset,definition,
    ( supset
    = ( ^ [F: ( $i > $o ) > $o, X: $i ] :
      ? [Y: $i > $o] : ( ( F @ Y ) & ( ( sup @ Y ) = X ) ) ) )).

thf(unionset,type,(
    unionset: ( ( ( $i > $o ) > $o ) > $i > $o ) )).

thf(unionset,definition,
    ( unionset
    = ( ^ [F: ( $i > $o ) > $o, X: $i ] :
      ( ? [Y: $i > $o] : ( ( F @ Y ) & ( Y @ X ) ) ) ) )).

thf(sup_set,axiom,(
    ! [X: ( $i > $o ) > $o] : ( ( sup @ ( supset @ X ) ) = ( sup @ ( unionset @ X ) ) ) )).

% =========================================== %
% Definition of binary sums and lattice order %
% =========================================== %

thf(addition,type,(
    addition: $i > $i > $i )).

thf(addition_def, definition,
   ( addition
    = ( ^ [X: $i, Y: $i ] :
      ( sup @ ( union @ ( singleton @ X ) @ ( singleton @ Y ) ) )
      ) )).

thf(order,type,(
    leq: $i > $i > $o )).

thf(order_def, axiom,(
   ! [X1: $i,X2: $i] :
     ( ( leq @ X1 @ X2 ) <=> ( ( addition @ X1 @ X2 ) = X2 ) ) )).

% ================================ %
%   Definition of multiplication   %
% ================================ %

thf(multiplication,type,(
    multiplication: $i > $i > $i )).

thf(crossmult,type,(
    crossmult: ( $i > $o ) > ( $i > $o ) > $i > $o )).

thf(crossmult_def,definition,(
    crossmult = (
    ^ [X: $i > $o,Y: $i > $o, A: $i] : (
      ? [X1: $i, Y1: $i] : ( ( X @ X1 ) & ( Y @ Y1 ) & ( A = ( multiplication @ X1 @ Y1 ) ) )
    ) ) )).

thf(multiplication_def,axiom,(
      ! [X: $i > $o, Y: $i > $o] : ( ( multiplication @ ( sup @ X ) @ ( sup @ Y ) ) = ( sup @ ( crossmult @ X @ Y ) ) )
    )).

thf(one,type,(
    one: $i )).

thf(multiplication_neutral_right,axiom,(
      ! [X: $i] : ( ( multiplication @ X @ one ) = X )
    )).

thf(multiplication_neutral_left,axiom,(
      ! [X: $i] : ( ( multiplication @ one @ X ) = X )
    )).

% ================================= %
%    Additional Theorem (proved)    %
% ================================= %

thf(sup_binary,theorem,(
    ! [X: $i > $o, Y: $i > $o] : (
      ( sup @ ( union @ ( singleton @ ( sup @ X ) ) @ ( singleton @ (sup @ Y ) ) ) ) =
      ( sup @ ( union @ X @ Y ) )
      ) )).

% ======================================== %
% Goal : 0 is least element in the lattice %
% ======================================== %

thf(zero_least,conjecture,(
    ! [X: $i > $o] : ( ( sup @ ( union @ X @ ( singleton @ zero ) ) ) = ( sup @ X ) ) )).