%------------------------------------------------------------------------------
% File     : LAT006-0 : TPTP v7.2.0. Released v3.2.0.
% Domain   : Lattice Theory
% Axioms   : Tarski's fixed point theorem (equality) axioms
% Version  : [Pau06] (equality) axioms.
% English  :

% Refs     : [Pau06] Paulson (2006), Email to G. Sutcliffe
% Source   : [Pau06]
% Names    : Tarski.ax [Pau06]

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

% Comments :
%------------------------------------------------------------------------------
cnf(cls_Tarski_Opotype_Oext__inject_0,axiom,
    ( c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_more,T_a,T_z) != c_Tarski_Opotype_Opotype__ext(V_pset_H,V_order_H,V_more_H,T_a,T_z)
    | V_pset = V_pset_H )).

cnf(cls_Tarski_Opotype_Oext__inject_1,axiom,
    ( c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_more,T_a,T_z) != c_Tarski_Opotype_Opotype__ext(V_pset_H,V_order_H,V_more_H,T_a,T_z)
    | V_order = V_order_H )).

cnf(cls_Tarski_Opotype_Oext__inject_2,axiom,
    ( c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_more,T_a,T_z) != c_Tarski_Opotype_Opotype__ext(V_pset_H,V_order_H,V_more_H,T_a,T_z)
    | V_more = V_more_H )).

cnf(cls_Tarski_Opotype_Oselect__convs__1_0,axiom,
    ( c_Tarski_Opotype_Opset(c_Tarski_Opotype_Opotype__ext(V_y,V_order,V_more,T_a,T_z),T_a,T_z) = V_y )).

cnf(cls_Tarski_Opotype_Oselect__convs__2_0,axiom,
    ( c_Tarski_Opotype_Oorder(c_Tarski_Opotype_Opotype__ext(V_pset,V_y,V_more,T_a,T_z),T_a,T_z) = V_y )).

cnf(cls_Tarski_Opotype_Oselect__convs__3_0,axiom,
    ( c_Tarski_Opotype_Omore(c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_y,T_a,T_a),T_a,T_a) = V_y )).

cnf(cls_Tarski_Opotype_Oupdate__convs__1_0,axiom,
    ( c_Tarski_Opotype_Opset__update(V_pset_H,c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_more,T_a,T_z),T_a,T_z) = c_Tarski_Opotype_Opotype__ext(V_pset_H,V_order,V_more,T_a,T_z) )).

cnf(cls_Tarski_Opotype_Oupdate__convs__2_0,axiom,
    ( c_Tarski_Opotype_Oorder__update(V_order_H,c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_more,T_a,T_z),T_a,T_z) = c_Tarski_Opotype_Opotype__ext(V_pset,V_order_H,V_more,T_a,T_z) )).

cnf(cls_Tarski_Opotype_Oupdate__convs__3_0,axiom,
    ( c_Tarski_Opotype_Omore__update(V_more_H,c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_more,T_a,T_z),T_z,T_a) = c_Tarski_Opotype_Opotype__ext(V_pset,V_order,V_more_H,T_a,T_z) )).

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