TPTP Problem File: SWW473^1.p

View Solutions - Solve Problem

%------------------------------------------------------------------------------
% File     : SWW473^1 : TPTP v7.2.0. Released v5.3.0.
% Domain   : Software Verification
% Problem  : Hoare's Logic with Procedures line 383, 100 axioms selected
% Version  : Especial.
% English  :

% Refs     : [BN10]  Boehme & Nipkow (2010), Sledgehammer: Judgement Day
%          : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe
% Source   : [Bla11]
% Names    : hoare_100_thf_l383 [Bla11]

% Status   : Theorem
% Rating   : 0.44 v7.2.0, 0.25 v7.1.0, 0.50 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.60 v6.2.0, 0.43 v6.1.0, 0.57 v6.0.0, 0.43 v5.5.0, 0.67 v5.4.0, 0.80 v5.3.0
% Syntax   : Number of formulae    :  414 (   0 unit; 107 type;   0 defn)
%            Number of atoms       : 2779 ( 137 equality;1504 variable)
%            Maximal formula depth :   15 (   7 average)
%            Number of connectives : 2241 (  43   ~;  14   |;  23   &;1806   @)
%                                         (  42 <=>; 313  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of type conns  : 1252 (1252   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :  113 ( 107   :;   0   =)
%            Number of variables   :  706 (   0 sgn; 658   !;   6   ?;  42   ^)
%                                         ( 706   :;   0  !>;   0  ?*)
%                                         (   0  @-;   0  @+)
% SPC      : TH0_THM_EQU_NAR

% Comments : This file was generated by Isabelle (most likely Sledgehammer)
%            2011-08-09 19:22:04
%------------------------------------------------------------------------------
%----Should-be-implicit typings (3)
thf(ty_ty_t__a,type,(
    x_a: $tType )).

thf(ty_ty_tc__Com__Opname,type,(
    pname: $tType )).

thf(ty_ty_tc__Nat__Onat,type,(
    nat: $tType )).

%----Explicit typings (104)
thf(sy_c_Finite__Set_Ocard_000_062_I_062_It__a_M_Eo_J_M_Eo_J,type,(
    finite_card_a_o_o: ( ( ( x_a > $o ) > $o ) > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    finite221134632me_o_o: ( ( ( pname > $o ) > $o ) > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J,type,(
    finite_card_nat_o_o: ( ( ( nat > $o ) > $o ) > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000_062_It__a_M_Eo_J,type,(
    finite_card_a_o: ( ( x_a > $o ) > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000_062_Itc__Com__Opname_M_Eo_J,type,(
    finite_card_pname_o: ( ( pname > $o ) > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    finite_card_nat_o: ( ( nat > $o ) > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000t__a,type,(
    finite_card_a: ( x_a > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000tc__Com__Opname,type,(
    finite_card_pname: ( pname > $o ) > nat )).

thf(sy_c_Finite__Set_Ocard_000tc__Nat__Onat,type,(
    finite_card_nat: ( nat > $o ) > nat )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_I_062_It__a_M_Eo_J_M_Eo_J_M_Eo_J,type,(
    finite1302365357_o_o_o: ( ( ( ( x_a > $o ) > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_M_Eo,type,(
    finite1648353812_o_o_o: ( ( ( ( pname > $o ) > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J_M_Eo_J,type,(
    finite1237261006_o_o_o: ( ( ( ( nat > $o ) > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_It__a_M_Eo_J_M_Eo_J,type,(
    finite_finite_a_o_o: ( ( ( x_a > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    finite1066544169me_o_o: ( ( ( pname > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J,type,(
    finite1676163439at_o_o: ( ( ( nat > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_It__a_M_Eo_J,type,(
    finite_finite_a_o: ( ( x_a > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_Itc__Com__Opname_M_Eo_J,type,(
    finite297249702name_o: ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    finite_finite_nat_o: ( ( nat > $o ) > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000t__a,type,(
    finite_finite_a: ( x_a > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000tc__Com__Opname,type,(
    finite_finite_pname: ( pname > $o ) > $o )).

thf(sy_c_Finite__Set_Ofinite_000tc__Nat__Onat,type,(
    finite_finite_nat: ( nat > $o ) > $o )).

thf(sy_c_Groups_Ominus__class_Ominus_000tc__Nat__Onat,type,(
    minus_minus_nat: nat > nat > nat )).

thf(sy_c_Nat_OSuc,type,(
    suc: nat > nat )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_I_062_It__a_M_Eo_J_M_Eo_J_M_E,type,(
    ord_less_eq_a_o_o_o: ( ( ( x_a > $o ) > $o ) > $o ) > ( ( ( x_a > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_I_062_Itc__Com__Opname_M_Eo_J,type,(
    ord_le1828183645_o_o_o: ( ( ( pname > $o ) > $o ) > $o ) > ( ( ( pname > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_I_062_Itc__Nat__Onat_M_Eo_J_M,type,(
    ord_le124054423_o_o_o: ( ( ( nat > $o ) > $o ) > $o ) > ( ( ( nat > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_It__a_M_Eo_J_M_Eo_J,type,(
    ord_less_eq_a_o_o: ( ( x_a > $o ) > $o ) > ( ( x_a > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_,type,(
    ord_le1205211808me_o_o: ( ( pname > $o ) > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J,type,(
    ord_less_eq_nat_o_o: ( ( nat > $o ) > $o ) > ( ( nat > $o ) > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_It__a_M_Eo_J,type,(
    ord_less_eq_a_o: ( x_a > $o ) > ( x_a > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_Itc__Com__Opname_M_Eo_J,type,(
    ord_less_eq_pname_o: ( pname > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    ord_less_eq_nat_o: ( nat > $o ) > ( nat > $o ) > $o )).

thf(sy_c_Orderings_Oord__class_Oless__eq_000tc__Nat__Onat,type,(
    ord_less_eq_nat: nat > nat > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_I_062_It__a_M_Eo_J_M_Eo_J_M_Eo_J,type,(
    collect_a_o_o_o: ( ( ( ( x_a > $o ) > $o ) > $o ) > $o ) > ( ( ( x_a > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_M_Eo_J,type,(
    collect_pname_o_o_o: ( ( ( ( pname > $o ) > $o ) > $o ) > $o ) > ( ( ( pname > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J_M_Eo_J,type,(
    collect_nat_o_o_o: ( ( ( ( nat > $o ) > $o ) > $o ) > $o ) > ( ( ( nat > $o ) > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_It__a_M_Eo_J_M_Eo_J,type,(
    collect_a_o_o: ( ( ( x_a > $o ) > $o ) > $o ) > ( ( x_a > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    collect_pname_o_o: ( ( ( pname > $o ) > $o ) > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J,type,(
    collect_nat_o_o: ( ( ( nat > $o ) > $o ) > $o ) > ( ( nat > $o ) > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_It__a_M_Eo_J,type,(
    collect_a_o: ( ( x_a > $o ) > $o ) > ( x_a > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_Itc__Com__Opname_M_Eo_J,type,(
    collect_pname_o: ( ( pname > $o ) > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_OCollect_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    collect_nat_o: ( ( nat > $o ) > $o ) > ( nat > $o ) > $o )).

thf(sy_c_Set_OCollect_000t__a,type,(
    collect_a: ( x_a > $o ) > x_a > $o )).

thf(sy_c_Set_OCollect_000tc__Com__Opname,type,(
    collect_pname: ( pname > $o ) > pname > $o )).

thf(sy_c_Set_OCollect_000tc__Nat__Onat,type,(
    collect_nat: ( nat > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_It__a_M_Eo_J_M_Eo_J_000t__a,type,(
    image_a_o_o_a: ( ( ( x_a > $o ) > $o ) > x_a ) > ( ( ( x_a > $o ) > $o ) > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_It__a_M_Eo_J_M_Eo_J_000tc__Com__Opname,type,(
    image_a_o_o_pname: ( ( ( x_a > $o ) > $o ) > pname ) > ( ( ( x_a > $o ) > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_It__a_M_Eo_J_M_Eo_J_000tc__Nat__Onat,type,(
    image_a_o_o_nat: ( ( ( x_a > $o ) > $o ) > nat ) > ( ( ( x_a > $o ) > $o ) > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_000t__a,type,(
    image_pname_o_o_a: ( ( ( pname > $o ) > $o ) > x_a ) > ( ( ( pname > $o ) > $o ) > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_000tc__Com__Opname,type,(
    image_471733107_pname: ( ( ( pname > $o ) > $o ) > pname ) > ( ( ( pname > $o ) > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J_000tc__Nat__Onat,type,(
    image_pname_o_o_nat: ( ( ( pname > $o ) > $o ) > nat ) > ( ( ( pname > $o ) > $o ) > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J_000t__a,type,(
    image_nat_o_o_a: ( ( ( nat > $o ) > $o ) > x_a ) > ( ( ( nat > $o ) > $o ) > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J_000tc__Com__Opname,type,(
    image_nat_o_o_pname: ( ( ( nat > $o ) > $o ) > pname ) > ( ( ( nat > $o ) > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J_000tc__Nat__Onat,type,(
    image_nat_o_o_nat: ( ( ( nat > $o ) > $o ) > nat ) > ( ( ( nat > $o ) > $o ) > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000_062_It__a_M_Eo_J_000t__a,type,(
    image_a_o_a: ( ( x_a > $o ) > x_a ) > ( ( x_a > $o ) > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000_062_It__a_M_Eo_J_000tc__Com__Opname,type,(
    image_a_o_pname: ( ( x_a > $o ) > pname ) > ( ( x_a > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_It__a_M_Eo_J_000tc__Nat__Onat,type,(
    image_a_o_nat: ( ( x_a > $o ) > nat ) > ( ( x_a > $o ) > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Com__Opname_M_Eo_J_000t__a,type,(
    image_pname_o_a: ( ( pname > $o ) > x_a ) > ( ( pname > $o ) > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Com__Opname_M_Eo_J_000tc__Com__Opname,type,(
    image_pname_o_pname: ( ( pname > $o ) > pname ) > ( ( pname > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Com__Opname_M_Eo_J_000tc__Nat__Onat,type,(
    image_pname_o_nat: ( ( pname > $o ) > nat ) > ( ( pname > $o ) > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Nat__Onat_M_Eo_J_000t__a,type,(
    image_nat_o_a: ( ( nat > $o ) > x_a ) > ( ( nat > $o ) > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Nat__Onat_M_Eo_J_000tc__Com__Opname,type,(
    image_nat_o_pname: ( ( nat > $o ) > pname ) > ( ( nat > $o ) > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000_062_Itc__Nat__Onat_M_Eo_J_000tc__Nat__Onat,type,(
    image_nat_o_nat: ( ( nat > $o ) > nat ) > ( ( nat > $o ) > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000t__a_000t__a,type,(
    image_a_a: ( x_a > x_a ) > ( x_a > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000t__a_000tc__Com__Opname,type,(
    image_a_pname: ( x_a > pname ) > ( x_a > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000t__a_000tc__Nat__Onat,type,(
    image_a_nat: ( x_a > nat ) > ( x_a > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_I_062_It__a_M_Eo_J_M_Eo_J,type,(
    image_pname_a_o_o: ( pname > ( x_a > $o ) > $o ) > ( pname > $o ) > ( ( x_a > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    image_504089495me_o_o: ( pname > ( pname > $o ) > $o ) > ( pname > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J,type,(
    image_pname_nat_o_o: ( pname > ( nat > $o ) > $o ) > ( pname > $o ) > ( ( nat > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_It__a_M_Eo_J,type,(
    image_pname_a_o: ( pname > x_a > $o ) > ( pname > $o ) > ( x_a > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_Itc__Com__Opname_M_Eo_J,type,(
    image_pname_pname_o: ( pname > pname > $o ) > ( pname > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    image_pname_nat_o: ( pname > nat > $o ) > ( pname > $o ) > ( nat > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000t__a,type,(
    image_pname_a: ( pname > x_a ) > ( pname > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000tc__Com__Opname,type,(
    image_pname_pname: ( pname > pname ) > ( pname > $o ) > pname > $o )).

thf(sy_c_Set_Oimage_000tc__Com__Opname_000tc__Nat__Onat,type,(
    image_pname_nat: ( pname > nat ) > ( pname > $o ) > nat > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000_062_I_062_It__a_M_Eo_J_M_Eo_J,type,(
    image_nat_a_o_o: ( nat > ( x_a > $o ) > $o ) > ( nat > $o ) > ( ( x_a > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    image_nat_pname_o_o: ( nat > ( pname > $o ) > $o ) > ( nat > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J,type,(
    image_nat_nat_o_o: ( nat > ( nat > $o ) > $o ) > ( nat > $o ) > ( ( nat > $o ) > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000_062_It__a_M_Eo_J,type,(
    image_nat_a_o: ( nat > x_a > $o ) > ( nat > $o ) > ( x_a > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000_062_Itc__Com__Opname_M_Eo_J,type,(
    image_nat_pname_o: ( nat > pname > $o ) > ( nat > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    image_nat_nat_o: ( nat > nat > $o ) > ( nat > $o ) > ( nat > $o ) > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000t__a,type,(
    image_nat_a: ( nat > x_a ) > ( nat > $o ) > x_a > $o )).

thf(sy_c_Set_Oimage_000tc__Nat__Onat_000tc__Com__Opname,type,(
    image_nat_pname: ( nat > pname ) > ( nat > $o ) > pname > $o )).

thf(sy_c_Set_Oinsert_000_062_I_062_It__a_M_Eo_J_M_Eo_J,type,(
    insert_a_o_o: ( ( x_a > $o ) > $o ) > ( ( ( x_a > $o ) > $o ) > $o ) > ( ( x_a > $o ) > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_I_062_Itc__Com__Opname_M_Eo_J_M_Eo_J,type,(
    insert_pname_o_o: ( ( pname > $o ) > $o ) > ( ( ( pname > $o ) > $o ) > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_I_062_Itc__Nat__Onat_M_Eo_J_M_Eo_J,type,(
    insert_nat_o_o: ( ( nat > $o ) > $o ) > ( ( ( nat > $o ) > $o ) > $o ) > ( ( nat > $o ) > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_It__a_M_Eo_J,type,(
    insert_a_o: ( x_a > $o ) > ( ( x_a > $o ) > $o ) > ( x_a > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_Itc__Com__Opname_M_Eo_J,type,(
    insert_pname_o: ( pname > $o ) > ( ( pname > $o ) > $o ) > ( pname > $o ) > $o )).

thf(sy_c_Set_Oinsert_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    insert_nat_o: ( nat > $o ) > ( ( nat > $o ) > $o ) > ( nat > $o ) > $o )).

thf(sy_c_Set_Oinsert_000t__a,type,(
    insert_a: x_a > ( x_a > $o ) > x_a > $o )).

thf(sy_c_Set_Oinsert_000tc__Com__Opname,type,(
    insert_pname: pname > ( pname > $o ) > pname > $o )).

thf(sy_c_Set_Oinsert_000tc__Nat__Onat,type,(
    insert_nat: nat > ( nat > $o ) > nat > $o )).

thf(sy_c_member_000_062_It__a_M_Eo_J,type,(
    member_a_o: ( x_a > $o ) > ( ( x_a > $o ) > $o ) > $o )).

thf(sy_c_member_000_062_Itc__Com__Opname_M_Eo_J,type,(
    member_pname_o: ( pname > $o ) > ( ( pname > $o ) > $o ) > $o )).

thf(sy_c_member_000_062_Itc__Nat__Onat_M_Eo_J,type,(
    member_nat_o: ( nat > $o ) > ( ( nat > $o ) > $o ) > $o )).

thf(sy_c_member_000t__a,type,(
    member_a: x_a > ( x_a > $o ) > $o )).

thf(sy_c_member_000tc__Com__Opname,type,(
    member_pname: pname > ( pname > $o ) > $o )).

thf(sy_c_member_000tc__Nat__Onat,type,(
    member_nat: nat > ( nat > $o ) > $o )).

thf(sy_v_G,type,(
    g: x_a > $o )).

thf(sy_v_P,type,(
    p: ( x_a > $o ) > ( x_a > $o ) > $o )).

thf(sy_v_U,type,(
    u: pname > $o )).

thf(sy_v_mgt__call,type,(
    mgt_call: pname > x_a )).

thf(sy_v_na,type,(
    na: nat )).

thf(sy_v_pn,type,(
    pn: pname )).

%----Relevant facts (300)
thf(fact_0_assms_I1_J,axiom,(
    ! [Ts: x_a > $o,G: x_a > $o] :
      ( ( ord_less_eq_a_o @ Ts @ G )
     => ( p @ G @ Ts ) ) )).

thf(fact_1_finite__Collect__subsets,axiom,(
    ! [A_59: nat > $o] :
      ( ( finite_finite_nat @ A_59 )
     => ( finite_finite_nat_o
        @ ( collect_nat_o
          @ ^ [B_38: nat > $o] :
              ( ord_less_eq_nat_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_2_finite__Collect__subsets,axiom,(
    ! [A_59: pname > $o] :
      ( ( finite_finite_pname @ A_59 )
     => ( finite297249702name_o
        @ ( collect_pname_o
          @ ^ [B_38: pname > $o] :
              ( ord_less_eq_pname_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_3_finite__Collect__subsets,axiom,(
    ! [A_59: x_a > $o] :
      ( ( finite_finite_a @ A_59 )
     => ( finite_finite_a_o
        @ ( collect_a_o
          @ ^ [B_38: x_a > $o] :
              ( ord_less_eq_a_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_4_finite__Collect__subsets,axiom,(
    ! [A_59: ( ( nat > $o ) > $o ) > $o] :
      ( ( finite1676163439at_o_o @ A_59 )
     => ( finite1237261006_o_o_o
        @ ( collect_nat_o_o_o
          @ ^ [B_38: ( ( nat > $o ) > $o ) > $o] :
              ( ord_le124054423_o_o_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_5_finite__Collect__subsets,axiom,(
    ! [A_59: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ A_59 )
     => ( finite1648353812_o_o_o
        @ ( collect_pname_o_o_o
          @ ^ [B_38: ( ( pname > $o ) > $o ) > $o] :
              ( ord_le1828183645_o_o_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_6_finite__Collect__subsets,axiom,(
    ! [A_59: ( ( x_a > $o ) > $o ) > $o] :
      ( ( finite_finite_a_o_o @ A_59 )
     => ( finite1302365357_o_o_o
        @ ( collect_a_o_o_o
          @ ^ [B_38: ( ( x_a > $o ) > $o ) > $o] :
              ( ord_less_eq_a_o_o_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_7_finite__Collect__subsets,axiom,(
    ! [A_59: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_59 )
     => ( finite_finite_a_o_o
        @ ( collect_a_o_o
          @ ^ [B_38: ( x_a > $o ) > $o] :
              ( ord_less_eq_a_o_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_8_finite__Collect__subsets,axiom,(
    ! [A_59: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_59 )
     => ( finite1066544169me_o_o
        @ ( collect_pname_o_o
          @ ^ [B_38: ( pname > $o ) > $o] :
              ( ord_le1205211808me_o_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_9_finite__Collect__subsets,axiom,(
    ! [A_59: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_59 )
     => ( finite1676163439at_o_o
        @ ( collect_nat_o_o
          @ ^ [B_38: ( nat > $o ) > $o] :
              ( ord_less_eq_nat_o_o @ B_38 @ A_59 ) ) ) ) )).

thf(fact_10_finite__imageI,axiom,(
    ! [H: pname > x_a,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite_finite_a @ ( image_pname_a @ H @ F_15 ) ) ) )).

thf(fact_11_finite__imageI,axiom,(
    ! [H: ( ( nat > $o ) > $o ) > nat,F_15: ( ( nat > $o ) > $o ) > $o] :
      ( ( finite1676163439at_o_o @ F_15 )
     => ( finite_finite_nat @ ( image_nat_o_o_nat @ H @ F_15 ) ) ) )).

thf(fact_12_finite__imageI,axiom,(
    ! [H: ( ( pname > $o ) > $o ) > nat,F_15: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ F_15 )
     => ( finite_finite_nat @ ( image_pname_o_o_nat @ H @ F_15 ) ) ) )).

thf(fact_13_finite__imageI,axiom,(
    ! [H: ( ( x_a > $o ) > $o ) > nat,F_15: ( ( x_a > $o ) > $o ) > $o] :
      ( ( finite_finite_a_o_o @ F_15 )
     => ( finite_finite_nat @ ( image_a_o_o_nat @ H @ F_15 ) ) ) )).

thf(fact_14_finite__imageI,axiom,(
    ! [H: ( x_a > $o ) > nat,F_15: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ F_15 )
     => ( finite_finite_nat @ ( image_a_o_nat @ H @ F_15 ) ) ) )).

thf(fact_15_finite__imageI,axiom,(
    ! [H: ( pname > $o ) > nat,F_15: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ F_15 )
     => ( finite_finite_nat @ ( image_pname_o_nat @ H @ F_15 ) ) ) )).

thf(fact_16_finite__imageI,axiom,(
    ! [H: ( nat > $o ) > nat,F_15: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ F_15 )
     => ( finite_finite_nat @ ( image_nat_o_nat @ H @ F_15 ) ) ) )).

thf(fact_17_finite__imageI,axiom,(
    ! [H: x_a > nat,F_15: x_a > $o] :
      ( ( finite_finite_a @ F_15 )
     => ( finite_finite_nat @ ( image_a_nat @ H @ F_15 ) ) ) )).

thf(fact_18_finite__imageI,axiom,(
    ! [H: ( ( nat > $o ) > $o ) > pname,F_15: ( ( nat > $o ) > $o ) > $o] :
      ( ( finite1676163439at_o_o @ F_15 )
     => ( finite_finite_pname @ ( image_nat_o_o_pname @ H @ F_15 ) ) ) )).

thf(fact_19_finite__imageI,axiom,(
    ! [H: ( ( pname > $o ) > $o ) > pname,F_15: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ F_15 )
     => ( finite_finite_pname @ ( image_471733107_pname @ H @ F_15 ) ) ) )).

thf(fact_20_finite__imageI,axiom,(
    ! [H: ( ( x_a > $o ) > $o ) > pname,F_15: ( ( x_a > $o ) > $o ) > $o] :
      ( ( finite_finite_a_o_o @ F_15 )
     => ( finite_finite_pname @ ( image_a_o_o_pname @ H @ F_15 ) ) ) )).

thf(fact_21_finite__imageI,axiom,(
    ! [H: ( x_a > $o ) > pname,F_15: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ F_15 )
     => ( finite_finite_pname @ ( image_a_o_pname @ H @ F_15 ) ) ) )).

thf(fact_22_finite__imageI,axiom,(
    ! [H: ( pname > $o ) > pname,F_15: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ F_15 )
     => ( finite_finite_pname @ ( image_pname_o_pname @ H @ F_15 ) ) ) )).

thf(fact_23_finite__imageI,axiom,(
    ! [H: ( nat > $o ) > pname,F_15: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ F_15 )
     => ( finite_finite_pname @ ( image_nat_o_pname @ H @ F_15 ) ) ) )).

thf(fact_24_finite__imageI,axiom,(
    ! [H: x_a > pname,F_15: x_a > $o] :
      ( ( finite_finite_a @ F_15 )
     => ( finite_finite_pname @ ( image_a_pname @ H @ F_15 ) ) ) )).

thf(fact_25_finite__imageI,axiom,(
    ! [H: nat > ( nat > $o ) > $o,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite1676163439at_o_o @ ( image_nat_nat_o_o @ H @ F_15 ) ) ) )).

thf(fact_26_finite__imageI,axiom,(
    ! [H: nat > ( pname > $o ) > $o,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite1066544169me_o_o @ ( image_nat_pname_o_o @ H @ F_15 ) ) ) )).

thf(fact_27_finite__imageI,axiom,(
    ! [H: nat > ( x_a > $o ) > $o,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite_finite_a_o_o @ ( image_nat_a_o_o @ H @ F_15 ) ) ) )).

thf(fact_28_finite__imageI,axiom,(
    ! [H: nat > x_a > $o,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite_finite_a_o @ ( image_nat_a_o @ H @ F_15 ) ) ) )).

thf(fact_29_finite__imageI,axiom,(
    ! [H: nat > pname > $o,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite297249702name_o @ ( image_nat_pname_o @ H @ F_15 ) ) ) )).

thf(fact_30_finite__imageI,axiom,(
    ! [H: nat > nat > $o,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite_finite_nat_o @ ( image_nat_nat_o @ H @ F_15 ) ) ) )).

thf(fact_31_finite__imageI,axiom,(
    ! [H: nat > x_a,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite_finite_a @ ( image_nat_a @ H @ F_15 ) ) ) )).

thf(fact_32_finite__imageI,axiom,(
    ! [H: pname > ( nat > $o ) > $o,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite1676163439at_o_o @ ( image_pname_nat_o_o @ H @ F_15 ) ) ) )).

thf(fact_33_finite__imageI,axiom,(
    ! [H: pname > ( pname > $o ) > $o,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite1066544169me_o_o @ ( image_504089495me_o_o @ H @ F_15 ) ) ) )).

thf(fact_34_finite__imageI,axiom,(
    ! [H: pname > ( x_a > $o ) > $o,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite_finite_a_o_o @ ( image_pname_a_o_o @ H @ F_15 ) ) ) )).

thf(fact_35_finite__imageI,axiom,(
    ! [H: pname > x_a > $o,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite_finite_a_o @ ( image_pname_a_o @ H @ F_15 ) ) ) )).

thf(fact_36_finite__imageI,axiom,(
    ! [H: pname > pname > $o,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite297249702name_o @ ( image_pname_pname_o @ H @ F_15 ) ) ) )).

thf(fact_37_finite__imageI,axiom,(
    ! [H: pname > nat > $o,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite_finite_nat_o @ ( image_pname_nat_o @ H @ F_15 ) ) ) )).

thf(fact_38_finite__imageI,axiom,(
    ! [H: pname > pname,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite_finite_pname @ ( image_pname_pname @ H @ F_15 ) ) ) )).

thf(fact_39_finite__imageI,axiom,(
    ! [H: x_a > x_a,F_15: x_a > $o] :
      ( ( finite_finite_a @ F_15 )
     => ( finite_finite_a @ ( image_a_a @ H @ F_15 ) ) ) )).

thf(fact_40_finite__imageI,axiom,(
    ! [H: ( nat > $o ) > x_a,F_15: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ F_15 )
     => ( finite_finite_a @ ( image_nat_o_a @ H @ F_15 ) ) ) )).

thf(fact_41_finite__imageI,axiom,(
    ! [H: ( pname > $o ) > x_a,F_15: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ F_15 )
     => ( finite_finite_a @ ( image_pname_o_a @ H @ F_15 ) ) ) )).

thf(fact_42_finite__imageI,axiom,(
    ! [H: ( x_a > $o ) > x_a,F_15: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ F_15 )
     => ( finite_finite_a @ ( image_a_o_a @ H @ F_15 ) ) ) )).

thf(fact_43_finite__imageI,axiom,(
    ! [H: pname > nat,F_15: pname > $o] :
      ( ( finite_finite_pname @ F_15 )
     => ( finite_finite_nat @ ( image_pname_nat @ H @ F_15 ) ) ) )).

thf(fact_44_finite__imageI,axiom,(
    ! [H: nat > pname,F_15: nat > $o] :
      ( ( finite_finite_nat @ F_15 )
     => ( finite_finite_pname @ ( image_nat_pname @ H @ F_15 ) ) ) )).

thf(fact_45_finite_OinsertI,axiom,(
    ! [A_58: x_a,A_57: x_a > $o] :
      ( ( finite_finite_a @ A_57 )
     => ( finite_finite_a @ ( insert_a @ A_58 @ A_57 ) ) ) )).

thf(fact_46_finite_OinsertI,axiom,(
    ! [A_58: nat,A_57: nat > $o] :
      ( ( finite_finite_nat @ A_57 )
     => ( finite_finite_nat @ ( insert_nat @ A_58 @ A_57 ) ) ) )).

thf(fact_47_finite_OinsertI,axiom,(
    ! [A_58: pname,A_57: pname > $o] :
      ( ( finite_finite_pname @ A_57 )
     => ( finite_finite_pname @ ( insert_pname @ A_58 @ A_57 ) ) ) )).

thf(fact_48_finite_OinsertI,axiom,(
    ! [A_58: ( nat > $o ) > $o,A_57: ( ( nat > $o ) > $o ) > $o] :
      ( ( finite1676163439at_o_o @ A_57 )
     => ( finite1676163439at_o_o @ ( insert_nat_o_o @ A_58 @ A_57 ) ) ) )).

thf(fact_49_finite_OinsertI,axiom,(
    ! [A_58: ( pname > $o ) > $o,A_57: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ A_57 )
     => ( finite1066544169me_o_o @ ( insert_pname_o_o @ A_58 @ A_57 ) ) ) )).

thf(fact_50_finite_OinsertI,axiom,(
    ! [A_58: ( x_a > $o ) > $o,A_57: ( ( x_a > $o ) > $o ) > $o] :
      ( ( finite_finite_a_o_o @ A_57 )
     => ( finite_finite_a_o_o @ ( insert_a_o_o @ A_58 @ A_57 ) ) ) )).

thf(fact_51_finite_OinsertI,axiom,(
    ! [A_58: x_a > $o,A_57: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_57 )
     => ( finite_finite_a_o @ ( insert_a_o @ A_58 @ A_57 ) ) ) )).

thf(fact_52_finite_OinsertI,axiom,(
    ! [A_58: pname > $o,A_57: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_57 )
     => ( finite297249702name_o @ ( insert_pname_o @ A_58 @ A_57 ) ) ) )).

thf(fact_53_finite_OinsertI,axiom,(
    ! [A_58: nat > $o,A_57: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_57 )
     => ( finite_finite_nat_o @ ( insert_nat_o @ A_58 @ A_57 ) ) ) )).

thf(fact_54_card__image__le,axiom,(
    ! [F_14: pname > nat,A_56: pname > $o] :
      ( ( finite_finite_pname @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_nat @ ( image_pname_nat @ F_14 @ A_56 ) ) @ ( finite_card_pname @ A_56 ) ) ) )).

thf(fact_55_card__image__le,axiom,(
    ! [F_14: x_a > nat,A_56: x_a > $o] :
      ( ( finite_finite_a @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_nat @ ( image_a_nat @ F_14 @ A_56 ) ) @ ( finite_card_a @ A_56 ) ) ) )).

thf(fact_56_card__image__le,axiom,(
    ! [F_14: ( nat > $o ) > nat,A_56: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_nat @ ( image_nat_o_nat @ F_14 @ A_56 ) ) @ ( finite_card_nat_o @ A_56 ) ) ) )).

thf(fact_57_card__image__le,axiom,(
    ! [F_14: ( pname > $o ) > nat,A_56: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_nat @ ( image_pname_o_nat @ F_14 @ A_56 ) ) @ ( finite_card_pname_o @ A_56 ) ) ) )).

thf(fact_58_card__image__le,axiom,(
    ! [F_14: ( x_a > $o ) > nat,A_56: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_nat @ ( image_a_o_nat @ F_14 @ A_56 ) ) @ ( finite_card_a_o @ A_56 ) ) ) )).

thf(fact_59_card__image__le,axiom,(
    ! [F_14: x_a > pname,A_56: x_a > $o] :
      ( ( finite_finite_a @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname @ ( image_a_pname @ F_14 @ A_56 ) ) @ ( finite_card_a @ A_56 ) ) ) )).

thf(fact_60_card__image__le,axiom,(
    ! [F_14: nat > pname,A_56: nat > $o] :
      ( ( finite_finite_nat @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname @ ( image_nat_pname @ F_14 @ A_56 ) ) @ ( finite_card_nat @ A_56 ) ) ) )).

thf(fact_61_card__image__le,axiom,(
    ! [F_14: pname > x_a,A_56: pname > $o] :
      ( ( finite_finite_pname @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_pname_a @ F_14 @ A_56 ) ) @ ( finite_card_pname @ A_56 ) ) ) )).

thf(fact_62_card__image__le,axiom,(
    ! [F_14: ( ( nat > $o ) > $o ) > x_a,A_56: ( ( nat > $o ) > $o ) > $o] :
      ( ( finite1676163439at_o_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_nat_o_o_a @ F_14 @ A_56 ) ) @ ( finite_card_nat_o_o @ A_56 ) ) ) )).

thf(fact_63_card__image__le,axiom,(
    ! [F_14: ( ( pname > $o ) > $o ) > x_a,A_56: ( ( pname > $o ) > $o ) > $o] :
      ( ( finite1066544169me_o_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_pname_o_o_a @ F_14 @ A_56 ) ) @ ( finite221134632me_o_o @ A_56 ) ) ) )).

thf(fact_64_card__image__le,axiom,(
    ! [F_14: ( ( x_a > $o ) > $o ) > x_a,A_56: ( ( x_a > $o ) > $o ) > $o] :
      ( ( finite_finite_a_o_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_a_o_o_a @ F_14 @ A_56 ) ) @ ( finite_card_a_o_o @ A_56 ) ) ) )).

thf(fact_65_card__image__le,axiom,(
    ! [F_14: ( x_a > $o ) > x_a,A_56: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_a_o_a @ F_14 @ A_56 ) ) @ ( finite_card_a_o @ A_56 ) ) ) )).

thf(fact_66_card__image__le,axiom,(
    ! [F_14: ( pname > $o ) > x_a,A_56: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_pname_o_a @ F_14 @ A_56 ) ) @ ( finite_card_pname_o @ A_56 ) ) ) )).

thf(fact_67_card__image__le,axiom,(
    ! [F_14: ( nat > $o ) > x_a,A_56: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_nat_o_a @ F_14 @ A_56 ) ) @ ( finite_card_nat_o @ A_56 ) ) ) )).

thf(fact_68_card__image__le,axiom,(
    ! [F_14: x_a > x_a,A_56: x_a > $o] :
      ( ( finite_finite_a @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_a_a @ F_14 @ A_56 ) ) @ ( finite_card_a @ A_56 ) ) ) )).

thf(fact_69_card__image__le,axiom,(
    ! [F_14: pname > pname,A_56: pname > $o] :
      ( ( finite_finite_pname @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname @ ( image_pname_pname @ F_14 @ A_56 ) ) @ ( finite_card_pname @ A_56 ) ) ) )).

thf(fact_70_card__image__le,axiom,(
    ! [F_14: pname > nat > $o,A_56: pname > $o] :
      ( ( finite_finite_pname @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_nat_o @ ( image_pname_nat_o @ F_14 @ A_56 ) ) @ ( finite_card_pname @ A_56 ) ) ) )).

thf(fact_71_card__image__le,axiom,(
    ! [F_14: pname > pname > $o,A_56: pname > $o] :
      ( ( finite_finite_pname @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname_o @ ( image_pname_pname_o @ F_14 @ A_56 ) ) @ ( finite_card_pname @ A_56 ) ) ) )).

thf(fact_72_card__image__le,axiom,(
    ! [F_14: pname > x_a > $o,A_56: pname > $o] :
      ( ( finite_finite_pname @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a_o @ ( image_pname_a_o @ F_14 @ A_56 ) ) @ ( finite_card_pname @ A_56 ) ) ) )).

thf(fact_73_card__image__le,axiom,(
    ! [F_14: nat > x_a,A_56: nat > $o] :
      ( ( finite_finite_nat @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a @ ( image_nat_a @ F_14 @ A_56 ) ) @ ( finite_card_nat @ A_56 ) ) ) )).

thf(fact_74_card__image__le,axiom,(
    ! [F_14: nat > nat > $o,A_56: nat > $o] :
      ( ( finite_finite_nat @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_nat_o @ ( image_nat_nat_o @ F_14 @ A_56 ) ) @ ( finite_card_nat @ A_56 ) ) ) )).

thf(fact_75_card__image__le,axiom,(
    ! [F_14: nat > pname > $o,A_56: nat > $o] :
      ( ( finite_finite_nat @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname_o @ ( image_nat_pname_o @ F_14 @ A_56 ) ) @ ( finite_card_nat @ A_56 ) ) ) )).

thf(fact_76_card__image__le,axiom,(
    ! [F_14: nat > x_a > $o,A_56: nat > $o] :
      ( ( finite_finite_nat @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_a_o @ ( image_nat_a_o @ F_14 @ A_56 ) ) @ ( finite_card_nat @ A_56 ) ) ) )).

thf(fact_77_card__image__le,axiom,(
    ! [F_14: ( nat > $o ) > pname,A_56: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname @ ( image_nat_o_pname @ F_14 @ A_56 ) ) @ ( finite_card_nat_o @ A_56 ) ) ) )).

thf(fact_78_card__image__le,axiom,(
    ! [F_14: ( pname > $o ) > pname,A_56: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname @ ( image_pname_o_pname @ F_14 @ A_56 ) ) @ ( finite_card_pname_o @ A_56 ) ) ) )).

thf(fact_79_card__image__le,axiom,(
    ! [F_14: ( x_a > $o ) > pname,A_56: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_56 )
     => ( ord_less_eq_nat @ ( finite_card_pname @ ( image_a_o_pname @ F_14 @ A_56 ) ) @ ( finite_card_a_o @ A_56 ) ) ) )).

thf(fact_80_card__mono,axiom,(
    ! [A_55: ( nat > $o ) > $o,B_37: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ B_37 )
     => ( ( ord_less_eq_nat_o_o @ A_55 @ B_37 )
       => ( ord_less_eq_nat @ ( finite_card_nat_o @ A_55 ) @ ( finite_card_nat_o @ B_37 ) ) ) ) )).

thf(fact_81_card__mono,axiom,(
    ! [A_55: ( pname > $o ) > $o,B_37: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ B_37 )
     => ( ( ord_le1205211808me_o_o @ A_55 @ B_37 )
       => ( ord_less_eq_nat @ ( finite_card_pname_o @ A_55 ) @ ( finite_card_pname_o @ B_37 ) ) ) ) )).

thf(fact_82_card__mono,axiom,(
    ! [A_55: ( x_a > $o ) > $o,B_37: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ B_37 )
     => ( ( ord_less_eq_a_o_o @ A_55 @ B_37 )
       => ( ord_less_eq_nat @ ( finite_card_a_o @ A_55 ) @ ( finite_card_a_o @ B_37 ) ) ) ) )).

thf(fact_83_card__mono,axiom,(
    ! [A_55: pname > $o,B_37: pname > $o] :
      ( ( finite_finite_pname @ B_37 )
     => ( ( ord_less_eq_pname_o @ A_55 @ B_37 )
       => ( ord_less_eq_nat @ ( finite_card_pname @ A_55 ) @ ( finite_card_pname @ B_37 ) ) ) ) )).

thf(fact_84_card__mono,axiom,(
    ! [A_55: x_a > $o,B_37: x_a > $o] :
      ( ( finite_finite_a @ B_37 )
     => ( ( ord_less_eq_a_o @ A_55 @ B_37 )
       => ( ord_less_eq_nat @ ( finite_card_a @ A_55 ) @ ( finite_card_a @ B_37 ) ) ) ) )).

thf(fact_85_card__mono,axiom,(
    ! [A_55: nat > $o,B_37: nat > $o] :
      ( ( finite_finite_nat @ B_37 )
     => ( ( ord_less_eq_nat_o @ A_55 @ B_37 )
       => ( ord_less_eq_nat @ ( finite_card_nat @ A_55 ) @ ( finite_card_nat @ B_37 ) ) ) ) )).

thf(fact_86_card__seteq,axiom,(
    ! [A_54: ( nat > $o ) > $o,B_36: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ B_36 )
     => ( ( ord_less_eq_nat_o_o @ A_54 @ B_36 )
       => ( ( ord_less_eq_nat @ ( finite_card_nat_o @ B_36 ) @ ( finite_card_nat_o @ A_54 ) )
         => ( A_54 = B_36 ) ) ) ) )).

thf(fact_87_card__seteq,axiom,(
    ! [A_54: ( pname > $o ) > $o,B_36: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ B_36 )
     => ( ( ord_le1205211808me_o_o @ A_54 @ B_36 )
       => ( ( ord_less_eq_nat @ ( finite_card_pname_o @ B_36 ) @ ( finite_card_pname_o @ A_54 ) )
         => ( A_54 = B_36 ) ) ) ) )).

thf(fact_88_card__seteq,axiom,(
    ! [A_54: ( x_a > $o ) > $o,B_36: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ B_36 )
     => ( ( ord_less_eq_a_o_o @ A_54 @ B_36 )
       => ( ( ord_less_eq_nat @ ( finite_card_a_o @ B_36 ) @ ( finite_card_a_o @ A_54 ) )
         => ( A_54 = B_36 ) ) ) ) )).

thf(fact_89_card__seteq,axiom,(
    ! [A_54: pname > $o,B_36: pname > $o] :
      ( ( finite_finite_pname @ B_36 )
     => ( ( ord_less_eq_pname_o @ A_54 @ B_36 )
       => ( ( ord_less_eq_nat @ ( finite_card_pname @ B_36 ) @ ( finite_card_pname @ A_54 ) )
         => ( A_54 = B_36 ) ) ) ) )).

thf(fact_90_card__seteq,axiom,(
    ! [A_54: x_a > $o,B_36: x_a > $o] :
      ( ( finite_finite_a @ B_36 )
     => ( ( ord_less_eq_a_o @ A_54 @ B_36 )
       => ( ( ord_less_eq_nat @ ( finite_card_a @ B_36 ) @ ( finite_card_a @ A_54 ) )
         => ( A_54 = B_36 ) ) ) ) )).

thf(fact_91_card__seteq,axiom,(
    ! [A_54: nat > $o,B_36: nat > $o] :
      ( ( finite_finite_nat @ B_36 )
     => ( ( ord_less_eq_nat_o @ A_54 @ B_36 )
       => ( ( ord_less_eq_nat @ ( finite_card_nat @ B_36 ) @ ( finite_card_nat @ A_54 ) )
         => ( A_54 = B_36 ) ) ) ) )).

thf(fact_92_card__insert__le,axiom,(
    ! [X_19: nat > $o,A_53: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_53 )
     => ( ord_less_eq_nat @ ( finite_card_nat_o @ A_53 ) @ ( finite_card_nat_o @ ( insert_nat_o @ X_19 @ A_53 ) ) ) ) )).

thf(fact_93_card__insert__le,axiom,(
    ! [X_19: pname > $o,A_53: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_53 )
     => ( ord_less_eq_nat @ ( finite_card_pname_o @ A_53 ) @ ( finite_card_pname_o @ ( insert_pname_o @ X_19 @ A_53 ) ) ) ) )).

thf(fact_94_card__insert__le,axiom,(
    ! [X_19: x_a > $o,A_53: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_53 )
     => ( ord_less_eq_nat @ ( finite_card_a_o @ A_53 ) @ ( finite_card_a_o @ ( insert_a_o @ X_19 @ A_53 ) ) ) ) )).

thf(fact_95_card__insert__le,axiom,(
    ! [X_19: pname,A_53: pname > $o] :
      ( ( finite_finite_pname @ A_53 )
     => ( ord_less_eq_nat @ ( finite_card_pname @ A_53 ) @ ( finite_card_pname @ ( insert_pname @ X_19 @ A_53 ) ) ) ) )).

thf(fact_96_card__insert__le,axiom,(
    ! [X_19: nat,A_53: nat > $o] :
      ( ( finite_finite_nat @ A_53 )
     => ( ord_less_eq_nat @ ( finite_card_nat @ A_53 ) @ ( finite_card_nat @ ( insert_nat @ X_19 @ A_53 ) ) ) ) )).

thf(fact_97_card__insert__le,axiom,(
    ! [X_19: x_a,A_53: x_a > $o] :
      ( ( finite_finite_a @ A_53 )
     => ( ord_less_eq_nat @ ( finite_card_a @ A_53 ) @ ( finite_card_a @ ( insert_a @ X_19 @ A_53 ) ) ) ) )).

thf(fact_98_card__insert__if,axiom,(
    ! [X_18: nat > $o,A_52: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_52 )
     => ( ( ( member_nat_o @ X_18 @ A_52 )
         => ( ( finite_card_nat_o @ ( insert_nat_o @ X_18 @ A_52 ) )
            = ( finite_card_nat_o @ A_52 ) ) )
        & ( ~ ( member_nat_o @ X_18 @ A_52 )
         => ( ( finite_card_nat_o @ ( insert_nat_o @ X_18 @ A_52 ) )
            = ( suc @ ( finite_card_nat_o @ A_52 ) ) ) ) ) ) )).

thf(fact_99_card__insert__if,axiom,(
    ! [X_18: pname > $o,A_52: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_52 )
     => ( ( ( member_pname_o @ X_18 @ A_52 )
         => ( ( finite_card_pname_o @ ( insert_pname_o @ X_18 @ A_52 ) )
            = ( finite_card_pname_o @ A_52 ) ) )
        & ( ~ ( member_pname_o @ X_18 @ A_52 )
         => ( ( finite_card_pname_o @ ( insert_pname_o @ X_18 @ A_52 ) )
            = ( suc @ ( finite_card_pname_o @ A_52 ) ) ) ) ) ) )).

thf(fact_100_card__insert__if,axiom,(
    ! [X_18: x_a > $o,A_52: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_52 )
     => ( ( ( member_a_o @ X_18 @ A_52 )
         => ( ( finite_card_a_o @ ( insert_a_o @ X_18 @ A_52 ) )
            = ( finite_card_a_o @ A_52 ) ) )
        & ( ~ ( member_a_o @ X_18 @ A_52 )
         => ( ( finite_card_a_o @ ( insert_a_o @ X_18 @ A_52 ) )
            = ( suc @ ( finite_card_a_o @ A_52 ) ) ) ) ) ) )).

thf(fact_101_card__insert__if,axiom,(
    ! [X_18: nat,A_52: nat > $o] :
      ( ( finite_finite_nat @ A_52 )
     => ( ( ( member_nat @ X_18 @ A_52 )
         => ( ( finite_card_nat @ ( insert_nat @ X_18 @ A_52 ) )
            = ( finite_card_nat @ A_52 ) ) )
        & ( ~ ( member_nat @ X_18 @ A_52 )
         => ( ( finite_card_nat @ ( insert_nat @ X_18 @ A_52 ) )
            = ( suc @ ( finite_card_nat @ A_52 ) ) ) ) ) ) )).

thf(fact_102_card__insert__if,axiom,(
    ! [X_18: pname,A_52: pname > $o] :
      ( ( finite_finite_pname @ A_52 )
     => ( ( ( member_pname @ X_18 @ A_52 )
         => ( ( finite_card_pname @ ( insert_pname @ X_18 @ A_52 ) )
            = ( finite_card_pname @ A_52 ) ) )
        & ( ~ ( member_pname @ X_18 @ A_52 )
         => ( ( finite_card_pname @ ( insert_pname @ X_18 @ A_52 ) )
            = ( suc @ ( finite_card_pname @ A_52 ) ) ) ) ) ) )).

thf(fact_103_card__insert__if,axiom,(
    ! [X_18: x_a,A_52: x_a > $o] :
      ( ( finite_finite_a @ A_52 )
     => ( ( ( member_a @ X_18 @ A_52 )
         => ( ( finite_card_a @ ( insert_a @ X_18 @ A_52 ) )
            = ( finite_card_a @ A_52 ) ) )
        & ( ~ ( member_a @ X_18 @ A_52 )
         => ( ( finite_card_a @ ( insert_a @ X_18 @ A_52 ) )
            = ( suc @ ( finite_card_a @ A_52 ) ) ) ) ) ) )).

thf(fact_104_card__insert__disjoint,axiom,(
    ! [X_17: nat > $o,A_51: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ A_51 )
     => ( ~ ( member_nat_o @ X_17 @ A_51 )
       => ( ( finite_card_nat_o @ ( insert_nat_o @ X_17 @ A_51 ) )
          = ( suc @ ( finite_card_nat_o @ A_51 ) ) ) ) ) )).

thf(fact_105_card__insert__disjoint,axiom,(
    ! [X_17: pname > $o,A_51: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ A_51 )
     => ( ~ ( member_pname_o @ X_17 @ A_51 )
       => ( ( finite_card_pname_o @ ( insert_pname_o @ X_17 @ A_51 ) )
          = ( suc @ ( finite_card_pname_o @ A_51 ) ) ) ) ) )).

thf(fact_106_card__insert__disjoint,axiom,(
    ! [X_17: x_a > $o,A_51: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ A_51 )
     => ( ~ ( member_a_o @ X_17 @ A_51 )
       => ( ( finite_card_a_o @ ( insert_a_o @ X_17 @ A_51 ) )
          = ( suc @ ( finite_card_a_o @ A_51 ) ) ) ) ) )).

thf(fact_107_card__insert__disjoint,axiom,(
    ! [X_17: nat,A_51: nat > $o] :
      ( ( finite_finite_nat @ A_51 )
     => ( ~ ( member_nat @ X_17 @ A_51 )
       => ( ( finite_card_nat @ ( insert_nat @ X_17 @ A_51 ) )
          = ( suc @ ( finite_card_nat @ A_51 ) ) ) ) ) )).

thf(fact_108_card__insert__disjoint,axiom,(
    ! [X_17: pname,A_51: pname > $o] :
      ( ( finite_finite_pname @ A_51 )
     => ( ~ ( member_pname @ X_17 @ A_51 )
       => ( ( finite_card_pname @ ( insert_pname @ X_17 @ A_51 ) )
          = ( suc @ ( finite_card_pname @ A_51 ) ) ) ) ) )).

thf(fact_109_card__insert__disjoint,axiom,(
    ! [X_17: x_a,A_51: x_a > $o] :
      ( ( finite_finite_a @ A_51 )
     => ( ~ ( member_a @ X_17 @ A_51 )
       => ( ( finite_card_a @ ( insert_a @ X_17 @ A_51 ) )
          = ( suc @ ( finite_card_a @ A_51 ) ) ) ) ) )).

thf(fact_110_finite__Collect__conjI,axiom,(
    ! [Q_1: ( nat > $o ) > $o,P_4: ( nat > $o ) > $o] :
      ( ( ( finite_finite_nat_o @ ( collect_nat_o @ P_4 ) )
        | ( finite_finite_nat_o @ ( collect_nat_o @ Q_1 ) ) )
     => ( finite_finite_nat_o
        @ ( collect_nat_o
          @ ^ [X: nat > $o] :
              ( (&) @ ( P_4 @ X ) @ ( Q_1 @ X ) ) ) ) ) )).

thf(fact_111_finite__Collect__conjI,axiom,(
    ! [Q_1: ( pname > $o ) > $o,P_4: ( pname > $o ) > $o] :
      ( ( ( finite297249702name_o @ ( collect_pname_o @ P_4 ) )
        | ( finite297249702name_o @ ( collect_pname_o @ Q_1 ) ) )
     => ( finite297249702name_o
        @ ( collect_pname_o
          @ ^ [X: pname > $o] :
              ( (&) @ ( P_4 @ X ) @ ( Q_1 @ X ) ) ) ) ) )).

thf(fact_112_finite__Collect__conjI,axiom,(
    ! [Q_1: ( x_a > $o ) > $o,P_4: ( x_a > $o ) > $o] :
      ( ( ( finite_finite_a_o @ ( collect_a_o @ P_4 ) )
        | ( finite_finite_a_o @ ( collect_a_o @ Q_1 ) ) )
     => ( finite_finite_a_o
        @ ( collect_a_o
          @ ^ [X: x_a > $o] :
              ( (&) @ ( P_4 @ X ) @ ( Q_1 @ X ) ) ) ) ) )).

thf(fact_113_finite__Collect__conjI,axiom,(
    ! [Q_1: x_a > $o,P_4: x_a > $o] :
      ( ( ( finite_finite_a @ ( collect_a @ P_4 ) )
        | ( finite_finite_a @ ( collect_a @ Q_1 ) ) )
     => ( finite_finite_a
        @ ( collect_a
          @ ^ [X: x_a] :
              ( (&) @ ( P_4 @ X ) @ ( Q_1 @ X ) ) ) ) ) )).

thf(fact_114_finite__Collect__conjI,axiom,(
    ! [Q_1: pname > $o,P_4: pname > $o] :
      ( ( ( finite_finite_pname @ ( collect_pname @ P_4 ) )
        | ( finite_finite_pname @ ( collect_pname @ Q_1 ) ) )
     => ( finite_finite_pname
        @ ( collect_pname
          @ ^ [X: pname] :
              ( (&) @ ( P_4 @ X ) @ ( Q_1 @ X ) ) ) ) ) )).

thf(fact_115_finite__Collect__conjI,axiom,(
    ! [Q_1: nat > $o,P_4: nat > $o] :
      ( ( ( finite_finite_nat @ ( collect_nat @ P_4 ) )
        | ( finite_finite_nat @ ( collect_nat @ Q_1 ) ) )
     => ( finite_finite_nat
        @ ( collect_nat
          @ ^ [X: nat] :
              ( (&) @ ( P_4 @ X ) @ ( Q_1 @ X ) ) ) ) ) )).

thf(fact_116_Suc__diff__le,axiom,(
    ! [N_1: nat,M_2: nat] :
      ( ( ord_less_eq_nat @ N_1 @ M_2 )
     => ( ( minus_minus_nat @ ( suc @ M_2 ) @ N_1 )
        = ( suc @ ( minus_minus_nat @ M_2 @ N_1 ) ) ) ) )).

thf(fact_117_finite__Collect__le__nat,axiom,(
    ! [K: nat] :
      ( finite_finite_nat
      @ ( collect_nat
        @ ^ [N_2: nat] :
            ( ord_less_eq_nat @ N_2 @ K ) ) ) )).

thf(fact_118_card__Collect__le__nat,axiom,(
    ! [N_1: nat] :
      ( ( finite_card_nat
        @ ( collect_nat
          @ ^ [I_1: nat] :
              ( ord_less_eq_nat @ I_1 @ N_1 ) ) )
      = ( suc @ N_1 ) ) )).

thf(fact_119_Suc__inject,axiom,(
    ! [X_16: nat,Y_3: nat] :
      ( ( ( suc @ X_16 )
        = ( suc @ Y_3 ) )
     => ( X_16 = Y_3 ) ) )).

thf(fact_120_nat_Oinject,axiom,(
    ! [Nat_1: nat,Nat: nat] :
      ( ( ( suc @ Nat_1 )
        = ( suc @ Nat ) )
    <=> ( Nat_1 = Nat ) ) )).

thf(fact_121_Suc__n__not__n,axiom,(
    ! [N_1: nat] :
      ( ( suc @ N_1 )
     != N_1 ) )).

thf(fact_122_n__not__Suc__n,axiom,(
    ! [N_1: nat] :
      ( N_1
     != ( suc @ N_1 ) ) )).

thf(fact_123_le__antisym,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ M_2 @ N_1 )
     => ( ( ord_less_eq_nat @ N_1 @ M_2 )
       => ( M_2 = N_1 ) ) ) )).

thf(fact_124_le__trans,axiom,(
    ! [K: nat,I: nat,J: nat] :
      ( ( ord_less_eq_nat @ I @ J )
     => ( ( ord_less_eq_nat @ J @ K )
       => ( ord_less_eq_nat @ I @ K ) ) ) )).

thf(fact_125_eq__imp__le,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( M_2 = N_1 )
     => ( ord_less_eq_nat @ M_2 @ N_1 ) ) )).

thf(fact_126_nat__le__linear,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ M_2 @ N_1 )
      | ( ord_less_eq_nat @ N_1 @ M_2 ) ) )).

thf(fact_127_le__refl,axiom,(
    ! [N_1: nat] :
      ( ord_less_eq_nat @ N_1 @ N_1 ) )).

thf(fact_128_diff__commute,axiom,(
    ! [I: nat,J: nat,K: nat] :
      ( ( minus_minus_nat @ ( minus_minus_nat @ I @ J ) @ K )
      = ( minus_minus_nat @ ( minus_minus_nat @ I @ K ) @ J ) ) )).

thf(fact_129_finite__Collect__disjI,axiom,(
    ! [P_3: pname > $o,Q: pname > $o] :
      ( ( finite_finite_pname
        @ ( collect_pname
          @ ^ [X: pname] :
              ( (|) @ ( P_3 @ X ) @ ( Q @ X ) ) ) )
    <=> ( ( finite_finite_pname @ ( collect_pname @ P_3 ) )
        & ( finite_finite_pname @ ( collect_pname @ Q ) ) ) ) )).

thf(fact_130_finite__Collect__disjI,axiom,(
    ! [P_3: ( nat > $o ) > $o,Q: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o
        @ ( collect_nat_o
          @ ^ [X: nat > $o] :
              ( (|) @ ( P_3 @ X ) @ ( Q @ X ) ) ) )
    <=> ( ( finite_finite_nat_o @ ( collect_nat_o @ P_3 ) )
        & ( finite_finite_nat_o @ ( collect_nat_o @ Q ) ) ) ) )).

thf(fact_131_finite__Collect__disjI,axiom,(
    ! [P_3: ( pname > $o ) > $o,Q: ( pname > $o ) > $o] :
      ( ( finite297249702name_o
        @ ( collect_pname_o
          @ ^ [X: pname > $o] :
              ( (|) @ ( P_3 @ X ) @ ( Q @ X ) ) ) )
    <=> ( ( finite297249702name_o @ ( collect_pname_o @ P_3 ) )
        & ( finite297249702name_o @ ( collect_pname_o @ Q ) ) ) ) )).

thf(fact_132_finite__Collect__disjI,axiom,(
    ! [P_3: ( x_a > $o ) > $o,Q: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o
        @ ( collect_a_o
          @ ^ [X: x_a > $o] :
              ( (|) @ ( P_3 @ X ) @ ( Q @ X ) ) ) )
    <=> ( ( finite_finite_a_o @ ( collect_a_o @ P_3 ) )
        & ( finite_finite_a_o @ ( collect_a_o @ Q ) ) ) ) )).

thf(fact_133_finite__Collect__disjI,axiom,(
    ! [P_3: nat > $o,Q: nat > $o] :
      ( ( finite_finite_nat
        @ ( collect_nat
          @ ^ [X: nat] :
              ( (|) @ ( P_3 @ X ) @ ( Q @ X ) ) ) )
    <=> ( ( finite_finite_nat @ ( collect_nat @ P_3 ) )
        & ( finite_finite_nat @ ( collect_nat @ Q ) ) ) ) )).

thf(fact_134_finite__Collect__disjI,axiom,(
    ! [P_3: x_a > $o,Q: x_a > $o] :
      ( ( finite_finite_a
        @ ( collect_a
          @ ^ [X: x_a] :
              ( (|) @ ( P_3 @ X ) @ ( Q @ X ) ) ) )
    <=> ( ( finite_finite_a @ ( collect_a @ P_3 ) )
        & ( finite_finite_a @ ( collect_a @ Q ) ) ) ) )).

thf(fact_135_finite__insert,axiom,(
    ! [A_50: nat,A_49: nat > $o] :
      ( ( finite_finite_nat @ ( insert_nat @ A_50 @ A_49 ) )
    <=> ( finite_finite_nat @ A_49 ) ) )).

thf(fact_136_finite__insert,axiom,(
    ! [A_50: pname,A_49: pname > $o] :
      ( ( finite_finite_pname @ ( insert_pname @ A_50 @ A_49 ) )
    <=> ( finite_finite_pname @ A_49 ) ) )).

thf(fact_137_finite__insert,axiom,(
    ! [A_50: x_a,A_49: x_a > $o] :
      ( ( finite_finite_a @ ( insert_a @ A_50 @ A_49 ) )
    <=> ( finite_finite_a @ A_49 ) ) )).

thf(fact_138_finite__insert,axiom,(
    ! [A_50: nat > $o,A_49: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ ( insert_nat_o @ A_50 @ A_49 ) )
    <=> ( finite_finite_nat_o @ A_49 ) ) )).

thf(fact_139_finite__insert,axiom,(
    ! [A_50: pname > $o,A_49: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ ( insert_pname_o @ A_50 @ A_49 ) )
    <=> ( finite297249702name_o @ A_49 ) ) )).

thf(fact_140_finite__insert,axiom,(
    ! [A_50: x_a > $o,A_49: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ ( insert_a_o @ A_50 @ A_49 ) )
    <=> ( finite_finite_a_o @ A_49 ) ) )).

thf(fact_141_finite__subset,axiom,(
    ! [A_48: ( nat > $o ) > $o,B_35: ( nat > $o ) > $o] :
      ( ( ord_less_eq_nat_o_o @ A_48 @ B_35 )
     => ( ( finite_finite_nat_o @ B_35 )
       => ( finite_finite_nat_o @ A_48 ) ) ) )).

thf(fact_142_finite__subset,axiom,(
    ! [A_48: ( pname > $o ) > $o,B_35: ( pname > $o ) > $o] :
      ( ( ord_le1205211808me_o_o @ A_48 @ B_35 )
     => ( ( finite297249702name_o @ B_35 )
       => ( finite297249702name_o @ A_48 ) ) ) )).

thf(fact_143_finite__subset,axiom,(
    ! [A_48: x_a > $o,B_35: x_a > $o] :
      ( ( ord_less_eq_a_o @ A_48 @ B_35 )
     => ( ( finite_finite_a @ B_35 )
       => ( finite_finite_a @ A_48 ) ) ) )).

thf(fact_144_finite__subset,axiom,(
    ! [A_48: ( x_a > $o ) > $o,B_35: ( x_a > $o ) > $o] :
      ( ( ord_less_eq_a_o_o @ A_48 @ B_35 )
     => ( ( finite_finite_a_o @ B_35 )
       => ( finite_finite_a_o @ A_48 ) ) ) )).

thf(fact_145_finite__subset,axiom,(
    ! [A_48: nat > $o,B_35: nat > $o] :
      ( ( ord_less_eq_nat_o @ A_48 @ B_35 )
     => ( ( finite_finite_nat @ B_35 )
       => ( finite_finite_nat @ A_48 ) ) ) )).

thf(fact_146_finite__subset,axiom,(
    ! [A_48: pname > $o,B_35: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_48 @ B_35 )
     => ( ( finite_finite_pname @ B_35 )
       => ( finite_finite_pname @ A_48 ) ) ) )).

thf(fact_147_rev__finite__subset,axiom,(
    ! [A_47: ( nat > $o ) > $o,B_34: ( nat > $o ) > $o] :
      ( ( finite_finite_nat_o @ B_34 )
     => ( ( ord_less_eq_nat_o_o @ A_47 @ B_34 )
       => ( finite_finite_nat_o @ A_47 ) ) ) )).

thf(fact_148_rev__finite__subset,axiom,(
    ! [A_47: ( pname > $o ) > $o,B_34: ( pname > $o ) > $o] :
      ( ( finite297249702name_o @ B_34 )
     => ( ( ord_le1205211808me_o_o @ A_47 @ B_34 )
       => ( finite297249702name_o @ A_47 ) ) ) )).

thf(fact_149_rev__finite__subset,axiom,(
    ! [A_47: x_a > $o,B_34: x_a > $o] :
      ( ( finite_finite_a @ B_34 )
     => ( ( ord_less_eq_a_o @ A_47 @ B_34 )
       => ( finite_finite_a @ A_47 ) ) ) )).

thf(fact_150_rev__finite__subset,axiom,(
    ! [A_47: ( x_a > $o ) > $o,B_34: ( x_a > $o ) > $o] :
      ( ( finite_finite_a_o @ B_34 )
     => ( ( ord_less_eq_a_o_o @ A_47 @ B_34 )
       => ( finite_finite_a_o @ A_47 ) ) ) )).

thf(fact_151_rev__finite__subset,axiom,(
    ! [A_47: nat > $o,B_34: nat > $o] :
      ( ( finite_finite_nat @ B_34 )
     => ( ( ord_less_eq_nat_o @ A_47 @ B_34 )
       => ( finite_finite_nat @ A_47 ) ) ) )).

thf(fact_152_rev__finite__subset,axiom,(
    ! [A_47: pname > $o,B_34: pname > $o] :
      ( ( finite_finite_pname @ B_34 )
     => ( ( ord_less_eq_pname_o @ A_47 @ B_34 )
       => ( finite_finite_pname @ A_47 ) ) ) )).

thf(fact_153_Suc__leD,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ ( suc @ M_2 ) @ N_1 )
     => ( ord_less_eq_nat @ M_2 @ N_1 ) ) )).

thf(fact_154_le__SucE,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ M_2 @ ( suc @ N_1 ) )
     => ( ~ ( ord_less_eq_nat @ M_2 @ N_1 )
       => ( M_2
          = ( suc @ N_1 ) ) ) ) )).

thf(fact_155_le__SucI,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ M_2 @ N_1 )
     => ( ord_less_eq_nat @ M_2 @ ( suc @ N_1 ) ) ) )).

thf(fact_156_Suc__le__mono,axiom,(
    ! [N_1: nat,M_2: nat] :
      ( ( ord_less_eq_nat @ ( suc @ N_1 ) @ ( suc @ M_2 ) )
    <=> ( ord_less_eq_nat @ N_1 @ M_2 ) ) )).

thf(fact_157_le__Suc__eq,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ M_2 @ ( suc @ N_1 ) )
    <=> ( ( ord_less_eq_nat @ M_2 @ N_1 )
        | ( M_2
          = ( suc @ N_1 ) ) ) ) )).

thf(fact_158_not__less__eq__eq,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ~ ( ord_less_eq_nat @ M_2 @ N_1 )
    <=> ( ord_less_eq_nat @ ( suc @ N_1 ) @ M_2 ) ) )).

thf(fact_159_Suc__n__not__le__n,axiom,(
    ! [N_1: nat] :
      ~ ( ord_less_eq_nat @ ( suc @ N_1 ) @ N_1 ) )).

thf(fact_160_Suc__diff__diff,axiom,(
    ! [M_2: nat,N_1: nat,K: nat] :
      ( ( minus_minus_nat @ ( minus_minus_nat @ ( suc @ M_2 ) @ N_1 ) @ ( suc @ K ) )
      = ( minus_minus_nat @ ( minus_minus_nat @ M_2 @ N_1 ) @ K ) ) )).

thf(fact_161_diff__Suc__Suc,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ( minus_minus_nat @ ( suc @ M_2 ) @ ( suc @ N_1 ) )
      = ( minus_minus_nat @ M_2 @ N_1 ) ) )).

thf(fact_162_le__diff__iff,axiom,(
    ! [N_1: nat,K: nat,M_2: nat] :
      ( ( ord_less_eq_nat @ K @ M_2 )
     => ( ( ord_less_eq_nat @ K @ N_1 )
       => ( ( ord_less_eq_nat @ ( minus_minus_nat @ M_2 @ K ) @ ( minus_minus_nat @ N_1 @ K ) )
        <=> ( ord_less_eq_nat @ M_2 @ N_1 ) ) ) ) )).

thf(fact_163_Nat_Odiff__diff__eq,axiom,(
    ! [N_1: nat,K: nat,M_2: nat] :
      ( ( ord_less_eq_nat @ K @ M_2 )
     => ( ( ord_less_eq_nat @ K @ N_1 )
       => ( ( minus_minus_nat @ ( minus_minus_nat @ M_2 @ K ) @ ( minus_minus_nat @ N_1 @ K ) )
          = ( minus_minus_nat @ M_2 @ N_1 ) ) ) ) )).

thf(fact_164_eq__diff__iff,axiom,(
    ! [N_1: nat,K: nat,M_2: nat] :
      ( ( ord_less_eq_nat @ K @ M_2 )
     => ( ( ord_less_eq_nat @ K @ N_1 )
       => ( ( ( minus_minus_nat @ M_2 @ K )
            = ( minus_minus_nat @ N_1 @ K ) )
        <=> ( M_2 = N_1 ) ) ) ) )).

thf(fact_165_diff__diff__cancel,axiom,(
    ! [I: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ I @ N_1 )
     => ( ( minus_minus_nat @ N_1 @ ( minus_minus_nat @ N_1 @ I ) )
        = I ) ) )).

thf(fact_166_diff__le__mono,axiom,(
    ! [L: nat,M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ M_2 @ N_1 )
     => ( ord_less_eq_nat @ ( minus_minus_nat @ M_2 @ L ) @ ( minus_minus_nat @ N_1 @ L ) ) ) )).

thf(fact_167_diff__le__mono2,axiom,(
    ! [L: nat,M_2: nat,N_1: nat] :
      ( ( ord_less_eq_nat @ M_2 @ N_1 )
     => ( ord_less_eq_nat @ ( minus_minus_nat @ L @ N_1 ) @ ( minus_minus_nat @ L @ M_2 ) ) ) )).

thf(fact_168_diff__le__self,axiom,(
    ! [M_2: nat,N_1: nat] :
      ( ord_less_eq_nat @ ( minus_minus_nat @ M_2 @ N_1 ) @ M_2 ) )).

thf(fact_169_finite__surj,axiom,(
    ! [B_33: x_a > $o,F_13: pname > x_a,A_46: pname > $o] :
      ( ( finite_finite_pname @ A_46 )
     => ( ( ord_less_eq_a_o @ B_33 @ ( image_pname_a @ F_13 @ A_46 ) )
       => ( finite_finite_a @ B_33 ) ) ) )).

thf(fact_170_finite__subset__image,axiom,(
    ! [F_12: pname > x_a,A_45: pname > $o,B_32: x_a > $o] :
      ( ( finite_finite_a @ B_32 )
     => ( ( ord_less_eq_a_o @ B_32 @ ( image_pname_a @ F_12 @ A_45 ) )
       => ? [C_3: pname > $o] :
            ( ( ord_less_eq_pname_o @ C_3 @ A_45 )
            & ( finite_finite_pname @ C_3 )
            & ( B_32
              = ( image_pname_a @ F_12 @ C_3 ) ) ) ) ) )).

thf(fact_171_lift__Suc__mono__le,axiom,(
    ! [N_4: nat,N_3: nat,F_11: nat > nat > $o] :
      ( ! [N_2: nat] :
          ( ord_less_eq_nat_o @ ( F_11 @ N_2 ) @ ( F_11 @ ( suc @ N_2 ) ) )
     => ( ( ord_less_eq_nat @ N_4 @ N_3 )
       => ( ord_less_eq_nat_o @ ( F_11 @ N_4 ) @ ( F_11 @ N_3 ) ) ) ) )).

thf(fact_172_lift__Suc__mono__le,axiom,(
    ! [N_4: nat,N_3: nat,F_11: nat > pname > $o] :
      ( ! [N_2: nat] :
          ( ord_less_eq_pname_o @ ( F_11 @ N_2 ) @ ( F_11 @ ( suc @ N_2 ) ) )
     => ( ( ord_less_eq_nat @ N_4 @ N_3 )
       => ( ord_less_eq_pname_o @ ( F_11 @ N_4 ) @ ( F_11 @ N_3 ) ) ) ) )).

thf(fact_173_lift__Suc__mono__le,axiom,(
    ! [N_4: nat,N_3: nat,F_11: nat > nat] :
      ( ! [N_2: nat] :
          ( ord_less_eq_nat @ ( F_11 @ N_2 ) @ ( F_11 @ ( suc @ N_2 ) ) )
     => ( ( ord_less_eq_nat @ N_4 @ N_3 )
       => ( ord_less_eq_nat @ ( F_11 @ N_4 ) @ ( F_11 @ N_3 ) ) ) ) )).

thf(fact_174_lift__Suc__mono__le,axiom,(
    ! [N_4: nat,N_3: nat,F_11: nat > x_a > $o] :
      ( ! [N_2: nat] :
          ( ord_less_eq_a_o @ ( F_11 @ N_2 ) @ ( F_11 @ ( suc @ N_2 ) ) )
     => ( ( ord_less_eq_nat @ N_4 @ N_3 )
       => ( ord_less_eq_a_o @ ( F_11 @ N_4 ) @ ( F_11 @ N_3 ) ) ) ) )).

thf(fact_175_pigeonhole__infinite,axiom,(
    ! [F_10: pname > x_a,A_43: pname > $o] :
      ( ~ ( finite_finite_pname @ A_43 )
     => ( ( finite_finite_a @ ( image_pname_a @ F_10 @ A_43 ) )
       => ? [X: pname] :
            ( ( member_pname @ X @ A_43 )
            & ~ ( finite_finite_pname
                @ ( collect_pname
                  @ ^ [A_44: pname] :
                      ( (&) @ ( member_pname @ A_44 @ A_43 )
                      @ ( ( F_10 @ A_44 )
                        = ( F_10 @ X ) ) ) ) ) ) ) ) )).

thf(fact_176_image__eqI,axiom,(
    ! [A_42: pname > $o,B_31: x_a,F_9: pname > x_a,X_15: pname] :
      ( ( B_31
        = ( F_9 @ X_15 ) )
     => ( ( member_pname @ X_15 @ A_42 )
       => ( member_a @ B_31 @ ( image_pname_a @ F_9 @ A_42 ) ) ) ) )).

thf(fact_177_equalityI,axiom,(
    ! [A_41: nat > $o,B_30: nat > $o] :
      ( ( ord_less_eq_nat_o @ A_41 @ B_30 )
     => ( ( ord_less_eq_nat_o @ B_30 @ A_41 )
       => ( A_41 = B_30 ) ) ) )).

thf(fact_178_equalityI,axiom,(
    ! [A_41: pname > $o,B_30: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_41 @ B_30 )
     => ( ( ord_less_eq_pname_o @ B_30 @ A_41 )
       => ( A_41 = B_30 ) ) ) )).

thf(fact_179_equalityI,axiom,(
    ! [A_41: x_a > $o,B_30: x_a > $o] :
      ( ( ord_less_eq_a_o @ A_41 @ B_30 )
     => ( ( ord_less_eq_a_o @ B_30 @ A_41 )
       => ( A_41 = B_30 ) ) ) )).

thf(fact_180_subsetD,axiom,(
    ! [C_2: nat,A_40: nat > $o,B_29: nat > $o] :
      ( ( ord_less_eq_nat_o @ A_40 @ B_29 )
     => ( ( member_nat @ C_2 @ A_40 )
       => ( member_nat @ C_2 @ B_29 ) ) ) )).

thf(fact_181_subsetD,axiom,(
    ! [C_2: x_a,A_40: x_a > $o,B_29: x_a > $o] :
      ( ( ord_less_eq_a_o @ A_40 @ B_29 )
     => ( ( member_a @ C_2 @ A_40 )
       => ( member_a @ C_2 @ B_29 ) ) ) )).

thf(fact_182_subsetD,axiom,(
    ! [C_2: pname,A_40: pname > $o,B_29: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_40 @ B_29 )
     => ( ( member_pname @ C_2 @ A_40 )
       => ( member_pname @ C_2 @ B_29 ) ) ) )).

thf(fact_183_insertCI,axiom,(
    ! [B_28: nat,A_39: nat,B_27: nat > $o] :
      ( ( ~ ( member_nat @ A_39 @ B_27 )
       => ( A_39 = B_28 ) )
     => ( member_nat @ A_39 @ ( insert_nat @ B_28 @ B_27 ) ) ) )).

thf(fact_184_insertCI,axiom,(
    ! [B_28: pname,A_39: pname,B_27: pname > $o] :
      ( ( ~ ( member_pname @ A_39 @ B_27 )
       => ( A_39 = B_28 ) )
     => ( member_pname @ A_39 @ ( insert_pname @ B_28 @ B_27 ) ) ) )).

thf(fact_185_insertCI,axiom,(
    ! [B_28: x_a,A_39: x_a,B_27: x_a > $o] :
      ( ( ~ ( member_a @ A_39 @ B_27 )
       => ( A_39 = B_28 ) )
     => ( member_a @ A_39 @ ( insert_a @ B_28 @ B_27 ) ) ) )).

thf(fact_186_insertE,axiom,(
    ! [A_38: nat,B_26: nat,A_37: nat > $o] :
      ( ( member_nat @ A_38 @ ( insert_nat @ B_26 @ A_37 ) )
     => ( ( A_38 != B_26 )
       => ( member_nat @ A_38 @ A_37 ) ) ) )).

thf(fact_187_insertE,axiom,(
    ! [A_38: pname,B_26: pname,A_37: pname > $o] :
      ( ( member_pname @ A_38 @ ( insert_pname @ B_26 @ A_37 ) )
     => ( ( A_38 != B_26 )
       => ( member_pname @ A_38 @ A_37 ) ) ) )).

thf(fact_188_insertE,axiom,(
    ! [A_38: x_a,B_26: x_a,A_37: x_a > $o] :
      ( ( member_a @ A_38 @ ( insert_a @ B_26 @ A_37 ) )
     => ( ( A_38 != B_26 )
       => ( member_a @ A_38 @ A_37 ) ) ) )).

thf(fact_189_insertI1,axiom,(
    ! [A_36: nat,B_25: nat > $o] :
      ( member_nat @ A_36 @ ( insert_nat @ A_36 @ B_25 ) ) )).

thf(fact_190_insertI1,axiom,(
    ! [A_36: pname,B_25: pname > $o] :
      ( member_pname @ A_36 @ ( insert_pname @ A_36 @ B_25 ) ) )).

thf(fact_191_insertI1,axiom,(
    ! [A_36: x_a,B_25: x_a > $o] :
      ( member_a @ A_36 @ ( insert_a @ A_36 @ B_25 ) ) )).

thf(fact_192_insert__compr,axiom,(
    ! [A_35: nat,B_24: nat > $o] :
      ( ( insert_nat @ A_35 @ B_24 )
      = ( collect_nat
        @ ^ [X: nat] :
            ( (|) @ ( X = A_35 ) @ ( member_nat @ X @ B_24 ) ) ) ) )).

thf(fact_193_insert__compr,axiom,(
    ! [A_35: pname,B_24: pname > $o] :
      ( ( insert_pname @ A_35 @ B_24 )
      = ( collect_pname
        @ ^ [X: pname] :
            ( (|) @ ( X = A_35 ) @ ( member_pname @ X @ B_24 ) ) ) ) )).

thf(fact_194_insert__compr,axiom,(
    ! [A_35: x_a,B_24: x_a > $o] :
      ( ( insert_a @ A_35 @ B_24 )
      = ( collect_a
        @ ^ [X: x_a] :
            ( (|) @ ( X = A_35 ) @ ( member_a @ X @ B_24 ) ) ) ) )).

thf(fact_195_insert__compr,axiom,(
    ! [A_35: nat > $o,B_24: ( nat > $o ) > $o] :
      ( ( insert_nat_o @ A_35 @ B_24 )
      = ( collect_nat_o
        @ ^ [X: nat > $o] :
            ( (|) @ ( X = A_35 ) @ ( member_nat_o @ X @ B_24 ) ) ) ) )).

thf(fact_196_insert__compr,axiom,(
    ! [A_35: pname > $o,B_24: ( pname > $o ) > $o] :
      ( ( insert_pname_o @ A_35 @ B_24 )
      = ( collect_pname_o
        @ ^ [X: pname > $o] :
            ( (|) @ ( X = A_35 ) @ ( member_pname_o @ X @ B_24 ) ) ) ) )).

thf(fact_197_insert__compr,axiom,(
    ! [A_35: x_a > $o,B_24: ( x_a > $o ) > $o] :
      ( ( insert_a_o @ A_35 @ B_24 )
      = ( collect_a_o
        @ ^ [X: x_a > $o] :
            ( (|) @ ( X = A_35 ) @ ( member_a_o @ X @ B_24 ) ) ) ) )).

thf(fact_198_insert__Collect,axiom,(
    ! [A_34: nat,P_2: nat > $o] :
      ( ( insert_nat @ A_34 @ ( collect_nat @ P_2 ) )
      = ( collect_nat
        @ ^ [U: nat] :
            ( (=>) @ ( (~) @ ( U = A_34 ) ) @ ( P_2 @ U ) ) ) ) )).

thf(fact_199_insert__Collect,axiom,(
    ! [A_34: pname,P_2: pname > $o] :
      ( ( insert_pname @ A_34 @ ( collect_pname @ P_2 ) )
      = ( collect_pname
        @ ^ [U: pname] :
            ( (=>) @ ( (~) @ ( U = A_34 ) ) @ ( P_2 @ U ) ) ) ) )).

thf(fact_200_insert__Collect,axiom,(
    ! [A_34: x_a,P_2: x_a > $o] :
      ( ( insert_a @ A_34 @ ( collect_a @ P_2 ) )
      = ( collect_a
        @ ^ [U: x_a] :
            ( (=>) @ ( (~) @ ( U = A_34 ) ) @ ( P_2 @ U ) ) ) ) )).

thf(fact_201_insert__Collect,axiom,(
    ! [A_34: nat > $o,P_2: ( nat > $o ) > $o] :
      ( ( insert_nat_o @ A_34 @ ( collect_nat_o @ P_2 ) )
      = ( collect_nat_o
        @ ^ [U: nat > $o] :
            ( (=>) @ ( (~) @ ( U = A_34 ) ) @ ( P_2 @ U ) ) ) ) )).

thf(fact_202_insert__Collect,axiom,(
    ! [A_34: pname > $o,P_2: ( pname > $o ) > $o] :
      ( ( insert_pname_o @ A_34 @ ( collect_pname_o @ P_2 ) )
      = ( collect_pname_o
        @ ^ [U: pname > $o] :
            ( (=>) @ ( (~) @ ( U = A_34 ) ) @ ( P_2 @ U ) ) ) ) )).

thf(fact_203_insert__Collect,axiom,(
    ! [A_34: x_a > $o,P_2: ( x_a > $o ) > $o] :
      ( ( insert_a_o @ A_34 @ ( collect_a_o @ P_2 ) )
      = ( collect_a_o
        @ ^ [U: x_a > $o] :
            ( (=>) @ ( (~) @ ( U = A_34 ) ) @ ( P_2 @ U ) ) ) ) )).

thf(fact_204_insert__absorb2,axiom,(
    ! [X_14: nat,A_33: nat > $o] :
      ( ( insert_nat @ X_14 @ ( insert_nat @ X_14 @ A_33 ) )
      = ( insert_nat @ X_14 @ A_33 ) ) )).

thf(fact_205_insert__absorb2,axiom,(
    ! [X_14: pname,A_33: pname > $o] :
      ( ( insert_pname @ X_14 @ ( insert_pname @ X_14 @ A_33 ) )
      = ( insert_pname @ X_14 @ A_33 ) ) )).

thf(fact_206_insert__absorb2,axiom,(
    ! [X_14: x_a,A_33: x_a > $o] :
      ( ( insert_a @ X_14 @ ( insert_a @ X_14 @ A_33 ) )
      = ( insert_a @ X_14 @ A_33 ) ) )).

thf(fact_207_insert__commute,axiom,(
    ! [X_13: nat,Y_2: nat,A_32: nat > $o] :
      ( ( insert_nat @ X_13 @ ( insert_nat @ Y_2 @ A_32 ) )
      = ( insert_nat @ Y_2 @ ( insert_nat @ X_13 @ A_32 ) ) ) )).

thf(fact_208_insert__commute,axiom,(
    ! [X_13: pname,Y_2: pname,A_32: pname > $o] :
      ( ( insert_pname @ X_13 @ ( insert_pname @ Y_2 @ A_32 ) )
      = ( insert_pname @ Y_2 @ ( insert_pname @ X_13 @ A_32 ) ) ) )).

thf(fact_209_insert__commute,axiom,(
    ! [X_13: x_a,Y_2: x_a,A_32: x_a > $o] :
      ( ( insert_a @ X_13 @ ( insert_a @ Y_2 @ A_32 ) )
      = ( insert_a @ Y_2 @ ( insert_a @ X_13 @ A_32 ) ) ) )).

thf(fact_210_insert__iff,axiom,(
    ! [A_31: nat,B_23: nat,A_30: nat > $o] :
      ( ( member_nat @ A_31 @ ( insert_nat @ B_23 @ A_30 ) )
    <=> ( ( A_31 = B_23 )
        | ( member_nat @ A_31 @ A_30 ) ) ) )).

thf(fact_211_insert__iff,axiom,(
    ! [A_31: pname,B_23: pname,A_30: pname > $o] :
      ( ( member_pname @ A_31 @ ( insert_pname @ B_23 @ A_30 ) )
    <=> ( ( A_31 = B_23 )
        | ( member_pname @ A_31 @ A_30 ) ) ) )).

thf(fact_212_insert__iff,axiom,(
    ! [A_31: x_a,B_23: x_a,A_30: x_a > $o] :
      ( ( member_a @ A_31 @ ( insert_a @ B_23 @ A_30 ) )
    <=> ( ( A_31 = B_23 )
        | ( member_a @ A_31 @ A_30 ) ) ) )).

thf(fact_213_insert__code,axiom,(
    ! [Y_1: nat,A_29: nat > $o,X_12: nat] :
      ( ( insert_nat @ Y_1 @ A_29 @ X_12 )
    <=> ( ( Y_1 = X_12 )
        | ( A_29 @ X_12 ) ) ) )).

thf(fact_214_insert__code,axiom,(
    ! [Y_1: pname,A_29: pname > $o,X_12: pname] :
      ( ( insert_pname @ Y_1 @ A_29 @ X_12 )
    <=> ( ( Y_1 = X_12 )
        | ( A_29 @ X_12 ) ) ) )).

thf(fact_215_insert__code,axiom,(
    ! [Y_1: x_a,A_29: x_a > $o,X_12: x_a] :
      ( ( insert_a @ Y_1 @ A_29 @ X_12 )
    <=> ( ( Y_1 = X_12 )
        | ( A_29 @ X_12 ) ) ) )).

thf(fact_216_insert__ident,axiom,(
    ! [B_22: nat > $o,X_11: nat,A_28: nat > $o] :
      ( ~ ( member_nat @ X_11 @ A_28 )
     => ( ~ ( member_nat @ X_11 @ B_22 )
       => ( ( ( insert_nat @ X_11 @ A_28 )
            = ( insert_nat @ X_11 @ B_22 ) )
        <=> ( A_28 = B_22 ) ) ) ) )).

thf(fact_217_insert__ident,axiom,(
    ! [B_22: pname > $o,X_11: pname,A_28: pname > $o] :
      ( ~ ( member_pname @ X_11 @ A_28 )
     => ( ~ ( member_pname @ X_11 @ B_22 )
       => ( ( ( insert_pname @ X_11 @ A_28 )
            = ( insert_pname @ X_11 @ B_22 ) )
        <=> ( A_28 = B_22 ) ) ) ) )).

thf(fact_218_insert__ident,axiom,(
    ! [B_22: x_a > $o,X_11: x_a,A_28: x_a > $o] :
      ( ~ ( member_a @ X_11 @ A_28 )
     => ( ~ ( member_a @ X_11 @ B_22 )
       => ( ( ( insert_a @ X_11 @ A_28 )
            = ( insert_a @ X_11 @ B_22 ) )
        <=> ( A_28 = B_22 ) ) ) ) )).

thf(fact_219_insertI2,axiom,(
    ! [B_21: nat,A_27: nat,B_20: nat > $o] :
      ( ( member_nat @ A_27 @ B_20 )
     => ( member_nat @ A_27 @ ( insert_nat @ B_21 @ B_20 ) ) ) )).

thf(fact_220_insertI2,axiom,(
    ! [B_21: pname,A_27: pname,B_20: pname > $o] :
      ( ( member_pname @ A_27 @ B_20 )
     => ( member_pname @ A_27 @ ( insert_pname @ B_21 @ B_20 ) ) ) )).

thf(fact_221_insertI2,axiom,(
    ! [B_21: x_a,A_27: x_a,B_20: x_a > $o] :
      ( ( member_a @ A_27 @ B_20 )
     => ( member_a @ A_27 @ ( insert_a @ B_21 @ B_20 ) ) ) )).

thf(fact_222_insert__absorb,axiom,(
    ! [A_26: nat,A_25: nat > $o] :
      ( ( member_nat @ A_26 @ A_25 )
     => ( ( insert_nat @ A_26 @ A_25 )
        = A_25 ) ) )).

thf(fact_223_insert__absorb,axiom,(
    ! [A_26: pname,A_25: pname > $o] :
      ( ( member_pname @ A_26 @ A_25 )
     => ( ( insert_pname @ A_26 @ A_25 )
        = A_25 ) ) )).

thf(fact_224_insert__absorb,axiom,(
    ! [A_26: x_a,A_25: x_a > $o] :
      ( ( member_a @ A_26 @ A_25 )
     => ( ( insert_a @ A_26 @ A_25 )
        = A_25 ) ) )).

thf(fact_225_subset__refl,axiom,(
    ! [A_24: nat > $o] :
      ( ord_less_eq_nat_o @ A_24 @ A_24 ) )).

thf(fact_226_subset__refl,axiom,(
    ! [A_24: pname > $o] :
      ( ord_less_eq_pname_o @ A_24 @ A_24 ) )).

thf(fact_227_subset__refl,axiom,(
    ! [A_24: x_a > $o] :
      ( ord_less_eq_a_o @ A_24 @ A_24 ) )).

thf(fact_228_set__eq__subset,axiom,(
    ! [A_23: nat > $o,B_19: nat > $o] :
      ( ( A_23 = B_19 )
    <=> ( ( ord_less_eq_nat_o @ A_23 @ B_19 )
        & ( ord_less_eq_nat_o @ B_19 @ A_23 ) ) ) )).

thf(fact_229_set__eq__subset,axiom,(
    ! [A_23: pname > $o,B_19: pname > $o] :
      ( ( A_23 = B_19 )
    <=> ( ( ord_less_eq_pname_o @ A_23 @ B_19 )
        & ( ord_less_eq_pname_o @ B_19 @ A_23 ) ) ) )).

thf(fact_230_set__eq__subset,axiom,(
    ! [A_23: x_a > $o,B_19: x_a > $o] :
      ( ( A_23 = B_19 )
    <=> ( ( ord_less_eq_a_o @ A_23 @ B_19 )
        & ( ord_less_eq_a_o @ B_19 @ A_23 ) ) ) )).

thf(fact_231_equalityD1,axiom,(
    ! [A_22: nat > $o,B_18: nat > $o] :
      ( ( A_22 = B_18 )
     => ( ord_less_eq_nat_o @ A_22 @ B_18 ) ) )).

thf(fact_232_equalityD1,axiom,(
    ! [A_22: pname > $o,B_18: pname > $o] :
      ( ( A_22 = B_18 )
     => ( ord_less_eq_pname_o @ A_22 @ B_18 ) ) )).

thf(fact_233_equalityD1,axiom,(
    ! [A_22: x_a > $o,B_18: x_a > $o] :
      ( ( A_22 = B_18 )
     => ( ord_less_eq_a_o @ A_22 @ B_18 ) ) )).

thf(fact_234_equalityD2,axiom,(
    ! [A_21: nat > $o,B_17: nat > $o] :
      ( ( A_21 = B_17 )
     => ( ord_less_eq_nat_o @ B_17 @ A_21 ) ) )).

thf(fact_235_equalityD2,axiom,(
    ! [A_21: pname > $o,B_17: pname > $o] :
      ( ( A_21 = B_17 )
     => ( ord_less_eq_pname_o @ B_17 @ A_21 ) ) )).

thf(fact_236_equalityD2,axiom,(
    ! [A_21: x_a > $o,B_17: x_a > $o] :
      ( ( A_21 = B_17 )
     => ( ord_less_eq_a_o @ B_17 @ A_21 ) ) )).

thf(fact_237_in__mono,axiom,(
    ! [X_10: nat,A_20: nat > $o,B_16: nat > $o] :
      ( ( ord_less_eq_nat_o @ A_20 @ B_16 )
     => ( ( member_nat @ X_10 @ A_20 )
       => ( member_nat @ X_10 @ B_16 ) ) ) )).

thf(fact_238_in__mono,axiom,(
    ! [X_10: x_a,A_20: x_a > $o,B_16: x_a > $o] :
      ( ( ord_less_eq_a_o @ A_20 @ B_16 )
     => ( ( member_a @ X_10 @ A_20 )
       => ( member_a @ X_10 @ B_16 ) ) ) )).

thf(fact_239_in__mono,axiom,(
    ! [X_10: pname,A_20: pname > $o,B_16: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_20 @ B_16 )
     => ( ( member_pname @ X_10 @ A_20 )
       => ( member_pname @ X_10 @ B_16 ) ) ) )).

thf(fact_240_set__rev__mp,axiom,(
    ! [B_15: nat > $o,X_9: nat,A_19: nat > $o] :
      ( ( member_nat @ X_9 @ A_19 )
     => ( ( ord_less_eq_nat_o @ A_19 @ B_15 )
       => ( member_nat @ X_9 @ B_15 ) ) ) )).

thf(fact_241_set__rev__mp,axiom,(
    ! [B_15: x_a > $o,X_9: x_a,A_19: x_a > $o] :
      ( ( member_a @ X_9 @ A_19 )
     => ( ( ord_less_eq_a_o @ A_19 @ B_15 )
       => ( member_a @ X_9 @ B_15 ) ) ) )).

thf(fact_242_set__rev__mp,axiom,(
    ! [B_15: pname > $o,X_9: pname,A_19: pname > $o] :
      ( ( member_pname @ X_9 @ A_19 )
     => ( ( ord_less_eq_pname_o @ A_19 @ B_15 )
       => ( member_pname @ X_9 @ B_15 ) ) ) )).

thf(fact_243_set__mp,axiom,(
    ! [X_8: nat,A_18: nat > $o,B_14: nat > $o] :
      ( ( ord_less_eq_nat_o @ A_18 @ B_14 )
     => ( ( member_nat @ X_8 @ A_18 )
       => ( member_nat @ X_8 @ B_14 ) ) ) )).

thf(fact_244_set__mp,axiom,(
    ! [X_8: x_a,A_18: x_a > $o,B_14: x_a > $o] :
      ( ( ord_less_eq_a_o @ A_18 @ B_14 )
     => ( ( member_a @ X_8 @ A_18 )
       => ( member_a @ X_8 @ B_14 ) ) ) )).

thf(fact_245_set__mp,axiom,(
    ! [X_8: pname,A_18: pname > $o,B_14: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_18 @ B_14 )
     => ( ( member_pname @ X_8 @ A_18 )
       => ( member_pname @ X_8 @ B_14 ) ) ) )).

thf(fact_246_subset__trans,axiom,(
    ! [C_1: nat > $o,A_17: nat > $o,B_13: nat > $o] :
      ( ( ord_less_eq_nat_o @ A_17 @ B_13 )
     => ( ( ord_less_eq_nat_o @ B_13 @ C_1 )
       => ( ord_less_eq_nat_o @ A_17 @ C_1 ) ) ) )).

thf(fact_247_subset__trans,axiom,(
    ! [C_1: pname > $o,A_17: pname > $o,B_13: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_17 @ B_13 )
     => ( ( ord_less_eq_pname_o @ B_13 @ C_1 )
       => ( ord_less_eq_pname_o @ A_17 @ C_1 ) ) ) )).

thf(fact_248_subset__trans,axiom,(
    ! [C_1: x_a > $o,A_17: x_a > $o,B_13: x_a > $o] :
      ( ( ord_less_eq_a_o @ A_17 @ B_13 )
     => ( ( ord_less_eq_a_o @ B_13 @ C_1 )
       => ( ord_less_eq_a_o @ A_17 @ C_1 ) ) ) )).

thf(fact_249_equalityE,axiom,(
    ! [A_16: nat > $o,B_12: nat > $o] :
      ( ( A_16 = B_12 )
     => ~ ( ( ord_less_eq_nat_o @ A_16 @ B_12 )
         => ~ ( ord_less_eq_nat_o @ B_12 @ A_16 ) ) ) )).

thf(fact_250_equalityE,axiom,(
    ! [A_16: pname > $o,B_12: pname > $o] :
      ( ( A_16 = B_12 )
     => ~ ( ( ord_less_eq_pname_o @ A_16 @ B_12 )
         => ~ ( ord_less_eq_pname_o @ B_12 @ A_16 ) ) ) )).

thf(fact_251_equalityE,axiom,(
    ! [A_16: x_a > $o,B_12: x_a > $o] :
      ( ( A_16 = B_12 )
     => ~ ( ( ord_less_eq_a_o @ A_16 @ B_12 )
         => ~ ( ord_less_eq_a_o @ B_12 @ A_16 ) ) ) )).

thf(fact_252_mem__def,axiom,(
    ! [X_7: nat,A_15: nat > $o] :
      ( ( member_nat @ X_7 @ A_15 )
    <=> ( A_15 @ X_7 ) ) )).

thf(fact_253_mem__def,axiom,(
    ! [X_7: x_a,A_15: x_a > $o] :
      ( ( member_a @ X_7 @ A_15 )
    <=> ( A_15 @ X_7 ) ) )).

thf(fact_254_mem__def,axiom,(
    ! [X_7: pname,A_15: pname > $o] :
      ( ( member_pname @ X_7 @ A_15 )
    <=> ( A_15 @ X_7 ) ) )).

thf(fact_255_Collect__def,axiom,(
    ! [P_1: pname > $o] :
      ( ( collect_pname @ P_1 )
      = P_1 ) )).

thf(fact_256_Collect__def,axiom,(
    ! [P_1: ( nat > $o ) > $o] :
      ( ( collect_nat_o @ P_1 )
      = P_1 ) )).

thf(fact_257_Collect__def,axiom,(
    ! [P_1: ( pname > $o ) > $o] :
      ( ( collect_pname_o @ P_1 )
      = P_1 ) )).

thf(fact_258_Collect__def,axiom,(
    ! [P_1: ( x_a > $o ) > $o] :
      ( ( collect_a_o @ P_1 )
      = P_1 ) )).

thf(fact_259_Collect__def,axiom,(
    ! [P_1: nat > $o] :
      ( ( collect_nat @ P_1 )
      = P_1 ) )).

thf(fact_260_image__iff,axiom,(
    ! [Z: x_a,F_8: pname > x_a,A_14: pname > $o] :
      ( ( member_a @ Z @ ( image_pname_a @ F_8 @ A_14 ) )
    <=> ? [X: pname] :
          ( ( member_pname @ X @ A_14 )
          & ( Z
            = ( F_8 @ X ) ) ) ) )).

thf(fact_261_imageI,axiom,(
    ! [F_7: pname > x_a,X_6: pname,A_13: pname > $o] :
      ( ( member_pname @ X_6 @ A_13 )
     => ( member_a @ ( F_7 @ X_6 ) @ ( image_pname_a @ F_7 @ A_13 ) ) ) )).

thf(fact_262_rev__image__eqI,axiom,(
    ! [B_11: x_a,F_6: pname > x_a,X_5: pname,A_12: pname > $o] :
      ( ( member_pname @ X_5 @ A_12 )
     => ( ( B_11
          = ( F_6 @ X_5 ) )
       => ( member_a @ B_11 @ ( image_pname_a @ F_6 @ A_12 ) ) ) ) )).

thf(fact_263_insert__compr__raw,axiom,(
    ! [X: nat,Xa: nat > $o] :
      ( ( insert_nat @ X @ Xa )
      = ( collect_nat
        @ ^ [Y: nat] :
            ( (|) @ ( Y = X ) @ ( member_nat @ Y @ Xa ) ) ) ) )).

thf(fact_264_insert__compr__raw,axiom,(
    ! [X: pname,Xa: pname > $o] :
      ( ( insert_pname @ X @ Xa )
      = ( collect_pname
        @ ^ [Y: pname] :
            ( (|) @ ( Y = X ) @ ( member_pname @ Y @ Xa ) ) ) ) )).

thf(fact_265_insert__compr__raw,axiom,(
    ! [X: x_a,Xa: x_a > $o] :
      ( ( insert_a @ X @ Xa )
      = ( collect_a
        @ ^ [Y: x_a] :
            ( (|) @ ( Y = X ) @ ( member_a @ Y @ Xa ) ) ) ) )).

thf(fact_266_insert__compr__raw,axiom,(
    ! [X: nat > $o,Xa: ( nat > $o ) > $o] :
      ( ( insert_nat_o @ X @ Xa )
      = ( collect_nat_o
        @ ^ [Y: nat > $o] :
            ( (|) @ ( Y = X ) @ ( member_nat_o @ Y @ Xa ) ) ) ) )).

thf(fact_267_insert__compr__raw,axiom,(
    ! [X: pname > $o,Xa: ( pname > $o ) > $o] :
      ( ( insert_pname_o @ X @ Xa )
      = ( collect_pname_o
        @ ^ [Y: pname > $o] :
            ( (|) @ ( Y = X ) @ ( member_pname_o @ Y @ Xa ) ) ) ) )).

thf(fact_268_insert__compr__raw,axiom,(
    ! [X: x_a > $o,Xa: ( x_a > $o ) > $o] :
      ( ( insert_a_o @ X @ Xa )
      = ( collect_a_o
        @ ^ [Y: x_a > $o] :
            ( (|) @ ( Y = X ) @ ( member_a_o @ Y @ Xa ) ) ) ) )).

thf(fact_269_subset__insertI,axiom,(
    ! [B_10: nat > $o,A_11: nat] :
      ( ord_less_eq_nat_o @ B_10 @ ( insert_nat @ A_11 @ B_10 ) ) )).

thf(fact_270_subset__insertI,axiom,(
    ! [B_10: pname > $o,A_11: pname] :
      ( ord_less_eq_pname_o @ B_10 @ ( insert_pname @ A_11 @ B_10 ) ) )).

thf(fact_271_subset__insertI,axiom,(
    ! [B_10: x_a > $o,A_11: x_a] :
      ( ord_less_eq_a_o @ B_10 @ ( insert_a @ A_11 @ B_10 ) ) )).

thf(fact_272_insert__subset,axiom,(
    ! [X_4: nat,A_10: nat > $o,B_9: nat > $o] :
      ( ( ord_less_eq_nat_o @ ( insert_nat @ X_4 @ A_10 ) @ B_9 )
    <=> ( ( member_nat @ X_4 @ B_9 )
        & ( ord_less_eq_nat_o @ A_10 @ B_9 ) ) ) )).

thf(fact_273_insert__subset,axiom,(
    ! [X_4: pname,A_10: pname > $o,B_9: pname > $o] :
      ( ( ord_less_eq_pname_o @ ( insert_pname @ X_4 @ A_10 ) @ B_9 )
    <=> ( ( member_pname @ X_4 @ B_9 )
        & ( ord_less_eq_pname_o @ A_10 @ B_9 ) ) ) )).

thf(fact_274_insert__subset,axiom,(
    ! [X_4: x_a,A_10: x_a > $o,B_9: x_a > $o] :
      ( ( ord_less_eq_a_o @ ( insert_a @ X_4 @ A_10 ) @ B_9 )
    <=> ( ( member_a @ X_4 @ B_9 )
        & ( ord_less_eq_a_o @ A_10 @ B_9 ) ) ) )).

thf(fact_275_subset__insert,axiom,(
    ! [B_8: nat > $o,X_3: nat,A_9: nat > $o] :
      ( ~ ( member_nat @ X_3 @ A_9 )
     => ( ( ord_less_eq_nat_o @ A_9 @ ( insert_nat @ X_3 @ B_8 ) )
      <=> ( ord_less_eq_nat_o @ A_9 @ B_8 ) ) ) )).

thf(fact_276_subset__insert,axiom,(
    ! [B_8: pname > $o,X_3: pname,A_9: pname > $o] :
      ( ~ ( member_pname @ X_3 @ A_9 )
     => ( ( ord_less_eq_pname_o @ A_9 @ ( insert_pname @ X_3 @ B_8 ) )
      <=> ( ord_less_eq_pname_o @ A_9 @ B_8 ) ) ) )).

thf(fact_277_subset__insert,axiom,(
    ! [B_8: x_a > $o,X_3: x_a,A_9: x_a > $o] :
      ( ~ ( member_a @ X_3 @ A_9 )
     => ( ( ord_less_eq_a_o @ A_9 @ ( insert_a @ X_3 @ B_8 ) )
      <=> ( ord_less_eq_a_o @ A_9 @ B_8 ) ) ) )).

thf(fact_278_subset__insertI2,axiom,(
    ! [B_7: nat,A_8: nat > $o,B_6: nat > $o] :
      ( ( ord_less_eq_nat_o @ A_8 @ B_6 )
     => ( ord_less_eq_nat_o @ A_8 @ ( insert_nat @ B_7 @ B_6 ) ) ) )).

thf(fact_279_subset__insertI2,axiom,(
    ! [B_7: pname,A_8: pname > $o,B_6: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_8 @ B_6 )
     => ( ord_less_eq_pname_o @ A_8 @ ( insert_pname @ B_7 @ B_6 ) ) ) )).

thf(fact_280_subset__insertI2,axiom,(
    ! [B_7: x_a,A_8: x_a > $o,B_6: x_a > $o] :
      ( ( ord_less_eq_a_o @ A_8 @ B_6 )
     => ( ord_less_eq_a_o @ A_8 @ ( insert_a @ B_7 @ B_6 ) ) ) )).

thf(fact_281_insert__mono,axiom,(
    ! [A_7: nat,C: nat > $o,D: nat > $o] :
      ( ( ord_less_eq_nat_o @ C @ D )
     => ( ord_less_eq_nat_o @ ( insert_nat @ A_7 @ C ) @ ( insert_nat @ A_7 @ D ) ) ) )).

thf(fact_282_insert__mono,axiom,(
    ! [A_7: pname,C: pname > $o,D: pname > $o] :
      ( ( ord_less_eq_pname_o @ C @ D )
     => ( ord_less_eq_pname_o @ ( insert_pname @ A_7 @ C ) @ ( insert_pname @ A_7 @ D ) ) ) )).

thf(fact_283_insert__mono,axiom,(
    ! [A_7: x_a,C: x_a > $o,D: x_a > $o] :
      ( ( ord_less_eq_a_o @ C @ D )
     => ( ord_less_eq_a_o @ ( insert_a @ A_7 @ C ) @ ( insert_a @ A_7 @ D ) ) ) )).

thf(fact_284_image__insert,axiom,(
    ! [F_5: pname > x_a,A_6: pname,B_5: pname > $o] :
      ( ( image_pname_a @ F_5 @ ( insert_pname @ A_6 @ B_5 ) )
      = ( insert_a @ ( F_5 @ A_6 ) @ ( image_pname_a @ F_5 @ B_5 ) ) ) )).

thf(fact_285_insert__image,axiom,(
    ! [F_4: pname > x_a,X_2: pname,A_5: pname > $o] :
      ( ( member_pname @ X_2 @ A_5 )
     => ( ( insert_a @ ( F_4 @ X_2 ) @ ( image_pname_a @ F_4 @ A_5 ) )
        = ( image_pname_a @ F_4 @ A_5 ) ) ) )).

thf(fact_286_subset__image__iff,axiom,(
    ! [B_4: x_a > $o,F_3: pname > x_a,A_4: pname > $o] :
      ( ( ord_less_eq_a_o @ B_4 @ ( image_pname_a @ F_3 @ A_4 ) )
    <=> ? [AA: pname > $o] :
          ( ( ord_less_eq_pname_o @ AA @ A_4 )
          & ( B_4
            = ( image_pname_a @ F_3 @ AA ) ) ) ) )).

thf(fact_287_image__mono,axiom,(
    ! [F_2: pname > x_a,A_3: pname > $o,B_3: pname > $o] :
      ( ( ord_less_eq_pname_o @ A_3 @ B_3 )
     => ( ord_less_eq_a_o @ ( image_pname_a @ F_2 @ A_3 ) @ ( image_pname_a @ F_2 @ B_3 ) ) ) )).

thf(fact_288_imageE,axiom,(
    ! [B_2: x_a,F_1: pname > x_a,A_2: pname > $o] :
      ( ( member_a @ B_2 @ ( image_pname_a @ F_1 @ A_2 ) )
     => ~ ! [X: pname] :
            ( ( B_2
              = ( F_1 @ X ) )
           => ~ ( member_pname @ X @ A_2 ) ) ) )).

thf(fact_289_subsetI,axiom,(
    ! [B_1: nat > $o,A_1: nat > $o] :
      ( ! [X: nat] :
          ( ( member_nat @ X @ A_1 )
         => ( member_nat @ X @ B_1 ) )
     => ( ord_less_eq_nat_o @ A_1 @ B_1 ) ) )).

thf(fact_290_subsetI,axiom,(
    ! [B_1: x_a > $o,A_1: x_a > $o] :
      ( ! [X: x_a] :
          ( ( member_a @ X @ A_1 )
         => ( member_a @ X @ B_1 ) )
     => ( ord_less_eq_a_o @ A_1 @ B_1 ) ) )).

thf(fact_291_subsetI,axiom,(
    ! [B_1: pname > $o,A_1: pname > $o] :
      ( ! [X: pname] :
          ( ( member_pname @ X @ A_1 )
         => ( member_pname @ X @ B_1 ) )
     => ( ord_less_eq_pname_o @ A_1 @ B_1 ) ) )).

thf(fact_292_zero__induct__lemma,axiom,(
    ! [I: nat,P: nat > $o,K: nat] :
      ( ( P @ K )
     => ( ! [N_2: nat] :
            ( ( P @ ( suc @ N_2 ) )
           => ( P @ N_2 ) )
       => ( P @ ( minus_minus_nat @ K @ I ) ) ) ) )).

thf(fact_293_Suc__le__D,axiom,(
    ! [N_1: nat,M_1: nat] :
      ( ( ord_less_eq_nat @ ( suc @ N_1 ) @ M_1 )
     => ? [M: nat] :
          ( M_1
          = ( suc @ M ) ) ) )).

thf(fact_294_image__subsetI,axiom,(
    ! [F: pname > x_a,B: x_a > $o,A: pname > $o] :
      ( ! [X: pname] :
          ( ( member_pname @ X @ A )
         => ( member_a @ ( F @ X ) @ B ) )
     => ( ord_less_eq_a_o @ ( image_pname_a @ F @ A ) @ B ) ) )).

thf(fact_295_order__refl,axiom,(
    ! [X_1: nat > $o] :
      ( ord_less_eq_nat_o @ X_1 @ X_1 ) )).

thf(fact_296_order__refl,axiom,(
    ! [X_1: pname > $o] :
      ( ord_less_eq_pname_o @ X_1 @ X_1 ) )).

thf(fact_297_order__refl,axiom,(
    ! [X_1: nat] :
      ( ord_less_eq_nat @ X_1 @ X_1 ) )).

thf(fact_298_order__refl,axiom,(
    ! [X_1: x_a > $o] :
      ( ord_less_eq_a_o @ X_1 @ X_1 ) )).

thf(fact_299_finite__nat__set__iff__bounded__le,axiom,(
    ! [N: nat > $o] :
      ( ( finite_finite_nat @ N )
    <=> ? [M: nat] :
        ! [X: nat] :
          ( ( member_nat @ X @ N )
         => ( ord_less_eq_nat @ X @ M ) ) ) )).

%----Conjectures (7)
thf(conj_0,hypothesis,
    ( finite_finite_pname @ u )).

thf(conj_1,hypothesis,
    ( ord_less_eq_a_o @ g @ ( image_pname_a @ mgt_call @ u ) )).

thf(conj_2,hypothesis,
    ( ord_less_eq_nat @ ( suc @ na ) @ ( finite_card_a @ ( image_pname_a @ mgt_call @ u ) ) )).

thf(conj_3,hypothesis,
    ( ( finite_card_a @ g )
    = ( minus_minus_nat @ ( finite_card_a @ ( image_pname_a @ mgt_call @ u ) ) @ ( suc @ na ) ) )).

thf(conj_4,hypothesis,
    ( member_pname @ pn @ u )).

thf(conj_5,hypothesis,(
    ~ ( member_a @ ( mgt_call @ pn ) @ g ) )).

thf(conj_6,conjecture,
    ( ord_less_eq_a_o @ ( insert_a @ ( mgt_call @ pn ) @ g ) @ ( image_pname_a @ mgt_call @ u ) )).

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