%--------------------------------------------------------------------------
% File     : LDA001-0 : TPTP v7.2.0. Bugfixed v2.6.0.
% Domain   : LD-Algebras (Embedding algebras)
% Axioms   : Embedding algebra
% Version  : [Jec93] axioms : Incomplete.
% English  : LD-algebras are related to large cardinals. Under a very
%            strong large cardinal assumption, the free-monogenic
%            LD-algebra can be represented by an algebra of elementary
%            embeddings. Theorems about this algebra can be proved from
%            a small number of properties, suggesting the definition
%            of an embedding algebra.

% Refs     : [Jec93] Jech (1993), LD-Algebras
%          : [Jec02] Jech (2002), Email to Geoff Sutcliffe
% Source   : [Jec93]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :    9 (   2 non-Horn;   4 unit;   3 RR)
%            Number of atoms      :   16 (   5 equality)
%            Maximal clause size  :    3 (   2 average)
%            Number of predicates :    2 (   0 propositional; 2-2 arity)
%            Number of functors   :    3 (   0 constant; 1-2 arity)
%            Number of variables  :   21 (   0 singleton)
%            Maximal term depth   :    3 (   2 average)
% SPC      : 

% Comments : [Jec93] says, "Even though axioms for embedding algebras
%            include additional properties to those listed below, many
%            results can be proved from these axioms."
% Bugfixes : v2.6.0 - Fixed axioms; they were unsatisfiable [Jec02]
%--------------------------------------------------------------------------
%----A1  x(yz)=(xy)(xz)
cnf(a1,axiom,
    ( f(X,f(Y,Z)) = f(f(X,Y),f(X,Z)) )).

%----A1a a(x,a(y,z)) = a(x*y,a(x,z))
cnf(a1a,axiom,
    ( a(X,a(Y,Z)) = a(f(X,Y),a(X,Z)) )).

%----A2  cr(u*v) = a(u,cr(v))
cnf(a2,axiom,
    ( critical_point(f(U,V)) = a(U,critical_point(V)) )).

%----B1  -(x<x)
cnf(b1,axiom,
    ( ~ less(X,X) )).

%----B2  linear
cnf(b2,axiom,
    ( less(X,Y)
    | less(Y,X)
    | X = Y )).

%----B3  transitive
cnf(b3,axiom,
    ( ~ less(X,Y)
    | ~ less(Y,Z)
    | less(X,Z) )).

%----B4  if x<y then ux<uy
cnf(b4,axiom,
    ( ~ less(X,Y)
    | less(a(U,X),a(U,Y)) )).

%----C2  if x<crit(u) then ux=x
cnf(c2,axiom,
    ( ~ less(X,critical_point(U))
    | a(U,X) = X )).

%----C3  x<crit(u) or x<ux
cnf(c3,axiom,
    ( less(X,critical_point(U))
    | less(X,a(U,X)) )).

%--------------------------------------------------------------------------