<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">%------------------------------------------------------------------------------
% File     : COM110_5 : TPTP v7.2.0. Released v6.0.0.
% Domain   : Number Theory
% Problem  : Quantifier elimination for Presburger arithmetic line 255
% Version  : Especial.
% English  : 

% Refs     : [BN10]  Boehme &amp; Nipkow (2010), Sledgehammer: Judgement Day
%          : [Nip08] Nipkow (2008), Linear Quantifier Elimination
%          : [Bla13] Blanchette (2011), Email to Geoff Sutcliffe
% Source   : [Bla13]
% Names    : qe_255 [Bla13]

% Status   : Unknown
% Rating   : 1.00 v6.4.0
% Syntax   : Number of formulae    :  205 (  55 unit;  62 type)
%            Number of atoms       :  273 ( 118 equality)
%            Maximal formula depth :   11 (   4 average)
%            Number of connectives :  160 (  30   ~;  15   |;  10   &amp;)
%                                         (  23 &lt;=&gt;;  82  =&gt;;   0  &lt;=;   0 &lt;~&gt;)
%                                         (   0  ~|;   0  ~&amp;)
%            Number of type conns  :   29 (  19   &gt;;  10   *;   0   +;   0  &lt;&lt;)
%            Number of predicates  :   89 (  66 propositional; 0-2 arity)
%            Number of functors    :   43 (  14 constant; 0-4 arity)
%            Number of variables   :  395 (  19 sgn; 340   !;   4   ?)
%                                         ( 395   :;  51  !&gt;;   0  ?*)
%            Maximal term depth    :   25 (   3 average)
% SPC      : TF1_UNK_EQU_NAR

% Comments : This file was generated by Isabelle (most likely Sledgehammer)
%            2011-12-13 16:24:47
%------------------------------------------------------------------------------
%----Should-be-implicit typings (6)
tff(ty_tc_HOL_Obool,type,(
    bool: $tType )).

tff(ty_tc_Int_Oint,type,(
    int: $tType )).

tff(ty_tc_List_Olist,type,(
    list: $tType &gt; $tType )).

tff(ty_tc_PresArith_Oatom,type,(
    atom: $tType )).

tff(ty_tc_fun,type,(
    fun: ( $tType * $tType ) &gt; $tType )).

tff(ty_tc_prod,type,(
    product_prod: ( $tType * $tType ) &gt; $tType )).

%----Explicit typings (56)
tff(sy_cl_Rings_Oring,type,(
    ring: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Oplus,type,(
    cl_Groups_Oplus: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Ozero,type,(
    zero: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Ominus,type,(
    cl_Groups_Ominus: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Divides_Oring__div,type,(
    ring_div: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Ogroup__add,type,(
    group_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Finite__Set_Ofinite,type,(
    finite_finite: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Omonoid__add,type,(
    monoid_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Orderings_Olinorder,type,(
    linorder: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Divides_Osemiring__div,type,(
    semiring_div: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Ocomm__monoid__add,type,(
    comm_monoid_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Oab__semigroup__add,type,(
    ab_semigroup_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Ocancel__semigroup__add,type,(
    cancel_semigroup_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Ocancel__ab__semigroup__add,type,(
    cancel146912293up_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Olinordered__ab__group__add,type,(
    linord219039673up_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_cl_Groups_Olinordered__ab__semigroup__add,type,(
    linord2061991079up_add: 
      !&gt;[A: $tType] : $o )).

tff(sy_c_Big__Operators_Olinorder__class_OMax,type,(
    big_linorder_Max: 
      !&gt;[A: $tType] :
        ( fun(A,bool) &gt; A ) )).

tff(sy_c_COMBB,type,(
    combb: 
      !&gt;[B: $tType,C: $tType,A: $tType] : fun(fun(B,C),fun(fun(A,B),fun(A,C))) )).

tff(sy_c_COMBC,type,(
    combc: 
      !&gt;[A: $tType,B: $tType,C: $tType] : fun(fun(A,fun(B,C)),fun(B,fun(A,C))) )).

tff(sy_c_COMBI,type,(
    combi: 
      !&gt;[A: $tType] : fun(A,A) )).

tff(sy_c_COMBK,type,(
    combk: 
      !&gt;[A: $tType,B: $tType] :
        ( A &gt; fun(B,A) ) )).

tff(sy_c_COMBS,type,(
    combs: 
      !&gt;[A: $tType,B: $tType,C: $tType] : fun(fun(A,fun(B,C)),fun(fun(A,B),fun(A,C))) )).

tff(sy_c_Divides_Odiv__class_Omod,type,(
    div_mod: 
      !&gt;[A: $tType] :
        ( ( A * A ) &gt; A ) )).

tff(sy_c_Finite__Set_Ofinite,type,(
    finite_finite1: 
      !&gt;[A: $tType] :
        ( fun(A,bool) &gt; $o ) )).

tff(sy_c_Groups_Ominus__class_Ominus,type,(
    minus_minus: 
      !&gt;[A: $tType] : fun(A,fun(A,A)) )).

tff(sy_c_Groups_Oplus__class_Oplus,type,(
    plus_plus: 
      !&gt;[A: $tType] :
        ( A &gt; fun(A,A) ) )).

tff(sy_c_Groups_Ozero__class_Ozero,type,(
    zero_zero: 
      !&gt;[A: $tType] : A )).

tff(sy_c_ListVector_Oiprod,type,(
    iprod: 
      !&gt;[A: $tType] : fun(list(A),fun(list(A),A)) )).

tff(sy_c_List_Ofilter,type,(
    filter: 
      !&gt;[A: $tType] :
        ( ( fun(A,bool) * list(A) ) &gt; list(A) ) )).

tff(sy_c_List_Olist_OCons,type,(
    cons: 
      !&gt;[A: $tType] :
        ( ( A * list(A) ) &gt; list(A) ) )).

tff(sy_c_List_Olist_ONil,type,(
    nil: 
      !&gt;[A: $tType] : list(A) )).

tff(sy_c_List_Omap,type,(
    map: 
      !&gt;[A: $tType,B: $tType] :
        ( ( fun(A,B) * list(A) ) &gt; list(B) ) )).

tff(sy_c_List_Oset,type,(
    set: 
      !&gt;[A: $tType] :
        ( list(A) &gt; fun(A,bool) ) )).

tff(sy_c_Orderings_Obot__class_Obot,type,(
    bot_bot: 
      !&gt;[A: $tType] : A )).

tff(sy_c_PresArith_OI_092_060_094isub_062Z,type,(
    i_Z: ( atom * list(int) ) &gt; $o )).

tff(sy_c_PresArith_Oatom_Oatom__case,type,(
    atom_case: 
      !&gt;[T: $tType] :
        ( ( fun(int,fun(list(int),T)) * fun(int,fun(int,fun(list(int),T))) * fun(int,fun(int,fun(list(int),T))) ) &gt; fun(atom,T) ) )).

tff(sy_c_PresArith_Odivisor,type,(
    divisor: fun(atom,int) )).

tff(sy_c_PresArith_Olbounds,type,(
    lbounds: list(atom) &gt; list(product_prod(int,list(int))) )).

tff(sy_c_PresArith_Ozlcms,type,(
    zlcms: list(int) &gt; int )).

tff(sy_c_Product__Type_OPair,type,(
    product_Pair: 
      !&gt;[A: $tType,B: $tType] : fun(A,fun(B,product_prod(A,B))) )).

tff(sy_c_Set_OCollect,type,(
    collect: 
      !&gt;[A: $tType] :
        ( fun(A,bool) &gt; fun(A,bool) ) )).

tff(sy_c_aa,type,(
    aa: 
      !&gt;[A: $tType,B: $tType] :
        ( ( fun(A,B) * A ) &gt; B ) )).

tff(sy_c_fEx,type,(
    fEx: 
      !&gt;[A: $tType] : fun(fun(A,bool),bool) )).

tff(sy_c_fFalse,type,(
    fFalse: bool )).

tff(sy_c_fTrue,type,(
    fTrue: bool )).

tff(sy_c_fconj,type,(
    fconj: fun(bool,fun(bool,bool)) )).

tff(sy_c_fdisj,type,(
    fdisj: fun(bool,fun(bool,bool)) )).

tff(sy_c_fequal,type,(
    fequal: 
      !&gt;[A: $tType] : fun(A,fun(A,bool)) )).

tff(sy_c_member,type,(
    member: 
      !&gt;[A: $tType] : fun(A,fun(fun(A,bool),bool)) )).

tff(sy_c_pp,type,(
    pp: bool &gt; $o )).

tff(sy_v_a____,type,(
    a: atom )).

tff(sy_v_as,type,(
    as: list(atom) )).

tff(sy_v_li____,type,(
    li: int )).

tff(sy_v_lks____,type,(
    lks: list(int) )).

tff(sy_v_x____,type,(
    x: int )).

tff(sy_v_xs,type,(
    xs: list(int) )).

%----Relevant facts (99)
tff(fact_0__096is__dvd_Aa_096,axiom,(
    pp(aa(atom,bool,atom_case(bool,combk(fun(list(int),bool),int,combk(bool,list(int),fFalse)),combk(fun(int,fun(list(int),bool)),int,combk(fun(list(int),bool),int,combk(bool,list(int),fTrue))),combk(fun(int,fun(list(int),bool)),int,combk(fun(list(int),bool),int,combk(bool,list(int),fTrue)))),a)) )).

tff(fact_1__096_Ili_M_Alks_J_A_058_Aset_A_Ilbounds_Aas_J_096,axiom,(
    pp(aa(fun(product_prod(int,list(int)),bool),bool,aa(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),member(product_prod(int,list(int))),aa(list(int),product_prod(int,list(int)),aa(int,fun(list(int),product_prod(int,list(int))),product_Pair(int,list(int)),li),lks)),set(product_prod(int,list(int)),lbounds(as)))) )).

tff(fact_2_lm,axiom,(
    big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) = aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)) )).

tff(fact_3__096lbounds_Aas_A_126_061_A_091_093_096,axiom,(
    lbounds(as) != nil(product_prod(int,list(int))) )).

tff(fact_4__096Max_A_123i_A_N_A_092_060langle_062ks_Mxs_092_060rangle_062_A_124ks_Ai_O_A_Ii_M_Aks_J_A_058_Aset_A_Ilbounds_Aas_J_125_058_A_123i_A_N_A_092_060langle_062ks_Mxs_092_060rangle_062_A_124ks_Ai_O_A_Ii_M_Aks_J_A_058_Aset_A_Ilbounds_Aas_J_125_096,axiom,(
    pp(aa(fun(int,bool),bool,aa(int,fun(fun(int,bool),bool),member(int),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))) )).

tff(fact_5__096a_A_058_Aset_Aas_096,axiom,(
    pp(aa(fun(atom,bool),bool,aa(atom,fun(fun(atom,bool),bool),member(atom),a),set(atom,as))) )).

tff(fact_6__096_B_Bthesis_O_A_I_B_Bli_Alks_O_A_091_124_A_Ili_M_Alks_J_A_058_Aset_A_Ilbounds_Aas_J_059_AMax_A_123i_A_N_A_092_060langle_062ks_Mxs_092_060rangle_062_A_124ks_Ai_O_A_Ii_M_Aks_J_A_058_Aset_A_Ilbounds_Aas_J_125_A_061_Ali_A_N_A_092_060langle_062lks_Mxs_092_060rangle_062_A_124_093_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096,axiom,(
    ~ ! [Li: int,Lks: list(int)] :
        ( pp(aa(fun(product_prod(int,list(int)),bool),bool,aa(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),member(product_prod(int,list(int))),aa(list(int),product_prod(int,list(int)),aa(int,fun(list(int),product_prod(int,list(int))),product_Pair(int,list(int)),Li),Lks)),set(product_prod(int,list(int)),lbounds(as))))
       =&gt; big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) != aa(int,int,aa(int,fun(int,int),minus_minus(int),Li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),Lks),xs)) ) )).

tff(fact_7__096finite_A_123i_A_N_A_092_060langle_062ks_Mxs_092_060rangle_062_A_124ks_Ai_O_A_Ii_M_Aks_J_A_058_Aset_A_Ilbounds_Aas_J_125_096,axiom,(
    finite_finite1(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) )).

tff(fact_8__096_123i_A_N_A_092_060langle_062ks_Mxs_092_060rangle_062_A_124ks_Ai_O_A_Ii_M_Aks_J_A_058_Aset_A_Ilbounds_Aas_J_125_A_126_061_A_123_125_096,axiom,(
    collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))) != bot_bot(fun(int,bool)) )).

tff(fact_9_set__filter,axiom,(
    ! [A: $tType,Xsa: list(A),P1: fun(A,bool)] : set(A,filter(A,P1,Xsa)) = collect(A,aa(fun(A,bool),fun(A,bool),aa(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool)),combs(A,bool,bool),aa(fun(A,bool),fun(A,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(A,bool),fun(A,fun(bool,bool))),combb(bool,fun(bool,bool),A),fconj),aa(fun(A,bool),fun(A,bool),aa(fun(A,fun(fun(A,bool),bool)),fun(fun(A,bool),fun(A,bool)),combc(A,fun(A,bool),bool),member(A)),set(A,Xsa)))),P1)) )).

tff(fact_10_map__eq__conv,axiom,(
    ! [A: $tType,B: $tType,G: fun(B,A),Xsa: list(B),F: fun(B,A)] :
      ( map(B,A,F,Xsa) = map(B,A,G,Xsa)
    &lt;=&gt; ! [X3: B] :
          ( pp(aa(fun(B,bool),bool,aa(B,fun(fun(B,bool),bool),member(B),X3),set(B,Xsa)))
         =&gt; aa(B,A,F,X3) = aa(B,A,G,X3) ) ) )).

tff(fact_11_mod__add__self2,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [B3: A,A2: A] : div_mod(A,aa(A,A,plus_plus(A,A2),B3),B3) = div_mod(A,A2,B3) ) )).

tff(fact_12_mod__add__self1,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [A2: A,B3: A] : div_mod(A,aa(A,A,plus_plus(A,B3),A2),B3) = div_mod(A,A2,B3) ) )).

tff(fact_13_filter__filter,axiom,(
    ! [A: $tType,Xsa: list(A),Q1: fun(A,bool),P1: fun(A,bool)] : filter(A,P1,filter(A,Q1,Xsa)) = filter(A,aa(fun(A,bool),fun(A,bool),aa(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool)),combs(A,bool,bool),aa(fun(A,bool),fun(A,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(A,bool),fun(A,fun(bool,bool))),combb(bool,fun(bool,bool),A),fconj),Q1)),P1),Xsa) )).

tff(fact_14_map__ident,axiom,(
    ! [A: $tType,X2: list(A)] : map(A,A,combi(A),X2) = X2 )).

tff(fact_15_mod__mod__trivial,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [B3: A,A2: A] : div_mod(A,div_mod(A,A2,B3),B3) = div_mod(A,A2,B3) ) )).

tff(fact_16_add__left__cancel,axiom,(
    ! [A: $tType] :
      ( cancel_semigroup_add(A)
     =&gt; ! [C2: A,B1: A,Aa: A] :
          ( aa(A,A,plus_plus(A,Aa),B1) = aa(A,A,plus_plus(A,Aa),C2)
        &lt;=&gt; B1 = C2 ) ) )).

tff(fact_17_add__right__cancel,axiom,(
    ! [A: $tType] :
      ( cancel_semigroup_add(A)
     =&gt; ! [C2: A,Aa: A,B1: A] :
          ( aa(A,A,plus_plus(A,B1),Aa) = aa(A,A,plus_plus(A,C2),Aa)
        &lt;=&gt; B1 = C2 ) ) )).

tff(fact_18_split__paired__All,axiom,(
    ! [A: $tType,B: $tType,P1: fun(product_prod(A,B),bool)] :
      ( ! [X11: product_prod(A,B)] : pp(aa(product_prod(A,B),bool,P1,X11))
    &lt;=&gt; ! [A5: A,B4: B] : pp(aa(product_prod(A,B),bool,P1,aa(B,product_prod(A,B),aa(A,fun(B,product_prod(A,B)),product_Pair(A,B),A5),B4))) ) )).

tff(fact_19_Pair__eq,axiom,(
    ! [A: $tType,B: $tType,B6: B,A4: A,B1: B,Aa: A] :
      ( aa(B,product_prod(A,B),aa(A,fun(B,product_prod(A,B)),product_Pair(A,B),Aa),B1) = aa(B,product_prod(A,B),aa(A,fun(B,product_prod(A,B)),product_Pair(A,B),A4),B6)
    &lt;=&gt; ( Aa = A4
        &amp; B1 = B6 ) ) )).

tff(fact_20_finite__set,axiom,(
    ! [A: $tType,Xsa: list(A)] : finite_finite1(A,set(A,Xsa)) )).

tff(fact_21_map__is__Nil__conv,axiom,(
    ! [A: $tType,B: $tType,Xsa: list(B),F: fun(B,A)] :
      ( map(B,A,F,Xsa) = nil(A)
    &lt;=&gt; Xsa = nil(B) ) )).

tff(fact_22_map_Osimps_I1_J,axiom,(
    ! [B: $tType,A: $tType,F: fun(B,A)] : map(B,A,F,nil(B)) = nil(A) )).

tff(fact_23_Nil__is__map__conv,axiom,(
    ! [A: $tType,B: $tType,Xsa: list(B),F: fun(B,A)] :
      ( nil(A) = map(B,A,F,Xsa)
    &lt;=&gt; Xsa = nil(B) ) )).

tff(fact_24_filter_Osimps_I1_J,axiom,(
    ! [A: $tType,P1: fun(A,bool)] : filter(A,P1,nil(A)) = nil(A) )).

tff(fact_25_List_Oset_Osimps_I1_J,axiom,(
    ! [A: $tType] : set(A,nil(A)) = bot_bot(fun(A,bool)) )).

tff(fact_26_set__empty2,axiom,(
    ! [A: $tType,Xsa: list(A)] :
      ( bot_bot(fun(A,bool)) = set(A,Xsa)
    &lt;=&gt; Xsa = nil(A) ) )).

tff(fact_27_set__empty,axiom,(
    ! [A: $tType,Xsa: list(A)] :
      ( set(A,Xsa) = bot_bot(fun(A,bool))
    &lt;=&gt; Xsa = nil(A) ) )).

tff(fact_28_norm,axiom,(
    ! [X2: atom] :
      ( pp(aa(fun(atom,bool),bool,aa(atom,fun(fun(atom,bool),bool),member(atom),X2),set(atom,as)))
     =&gt; aa(atom,int,divisor,X2) != zero_zero(int) ) )).

tff(fact_29_filter__empty__conv,axiom,(
    ! [A: $tType,Xsa: list(A),P1: fun(A,bool)] :
      ( filter(A,P1,Xsa) = nil(A)
    &lt;=&gt; ! [X3: A] :
          ( pp(aa(fun(A,bool),bool,aa(A,fun(fun(A,bool),bool),member(A),X3),set(A,Xsa)))
         =&gt; ~ pp(aa(A,bool,P1,X3)) ) ) )).

tff(fact_30_Pair__inject,axiom,(
    ! [A: $tType,B: $tType,B5: B,A3: A,B3: B,A2: A] :
      ( aa(B,product_prod(A,B),aa(A,fun(B,product_prod(A,B)),product_Pair(A,B),A2),B3) = aa(B,product_prod(A,B),aa(A,fun(B,product_prod(A,B)),product_Pair(A,B),A3),B5)
     =&gt; ~ ( A2 = A3
         =&gt; B3 != B5 ) ) )).

tff(fact_31_add__right__imp__eq,axiom,(
    ! [A: $tType] :
      ( cancel_semigroup_add(A)
     =&gt; ! [C1: A,A2: A,B3: A] :
          ( aa(A,A,plus_plus(A,B3),A2) = aa(A,A,plus_plus(A,C1),A2)
         =&gt; B3 = C1 ) ) )).

tff(fact_32_add__imp__eq,axiom,(
    ! [A: $tType] :
      ( cancel146912293up_add(A)
     =&gt; ! [C1: A,B3: A,A2: A] :
          ( aa(A,A,plus_plus(A,A2),B3) = aa(A,A,plus_plus(A,A2),C1)
         =&gt; B3 = C1 ) ) )).

tff(fact_33_add__left__imp__eq,axiom,(
    ! [A: $tType] :
      ( cancel_semigroup_add(A)
     =&gt; ! [C1: A,B3: A,A2: A] :
          ( aa(A,A,plus_plus(A,A2),B3) = aa(A,A,plus_plus(A,A2),C1)
         =&gt; B3 = C1 ) ) )).

tff(fact_34_ab__semigroup__add__class_Oadd__ac_I1_J,axiom,(
    ! [A: $tType] :
      ( ab_semigroup_add(A)
     =&gt; ! [C1: A,B3: A,A2: A] : aa(A,A,plus_plus(A,aa(A,A,plus_plus(A,A2),B3)),C1) = aa(A,A,plus_plus(A,A2),aa(A,A,plus_plus(A,B3),C1)) ) )).

tff(fact_35_diff__eq__diff__eq,axiom,(
    ! [A: $tType] :
      ( group_add(A)
     =&gt; ! [D: A,C2: A,B1: A,Aa: A] :
          ( aa(A,A,aa(A,fun(A,A),minus_minus(A),Aa),B1) = aa(A,A,aa(A,fun(A,A),minus_minus(A),C2),D)
         =&gt; ( Aa = B1
          &lt;=&gt; C2 = D ) ) ) )).

tff(fact_36_add__diff__cancel,axiom,(
    ! [A: $tType] :
      ( group_add(A)
     =&gt; ! [B3: A,A2: A] : aa(A,A,aa(A,fun(A,A),minus_minus(A),aa(A,A,plus_plus(A,A2),B3)),B3) = A2 ) )).

tff(fact_37_diff__add__cancel,axiom,(
    ! [A: $tType] :
      ( group_add(A)
     =&gt; ! [B3: A,A2: A] : aa(A,A,plus_plus(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),B3)),B3) = A2 ) )).

tff(fact_38_mod__add__cong,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [B5: A,B3: A,A3: A,C1: A,A2: A] :
          ( div_mod(A,A2,C1) = div_mod(A,A3,C1)
         =&gt; ( div_mod(A,B3,C1) = div_mod(A,B5,C1)
           =&gt; div_mod(A,aa(A,A,plus_plus(A,A2),B3),C1) = div_mod(A,aa(A,A,plus_plus(A,A3),B5),C1) ) ) ) )).

tff(fact_39_zmod__simps_I1_J,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [B3: A,C1: A,A2: A] : div_mod(A,aa(A,A,plus_plus(A,div_mod(A,A2,C1)),B3),C1) = div_mod(A,aa(A,A,plus_plus(A,A2),B3),C1) ) )).

tff(fact_40_zmod__simps_I2_J,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [C1: A,B3: A,A2: A] : div_mod(A,aa(A,A,plus_plus(A,A2),div_mod(A,B3,C1)),C1) = div_mod(A,aa(A,A,plus_plus(A,A2),B3),C1) ) )).

tff(fact_41_mod__add__eq,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [C1: A,B3: A,A2: A] : div_mod(A,aa(A,A,plus_plus(A,A2),B3),C1) = div_mod(A,aa(A,A,plus_plus(A,div_mod(A,A2,C1)),div_mod(A,B3,C1)),C1) ) )).

tff(fact_42_mod__add__left__eq,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [C1: A,B3: A,A2: A] : div_mod(A,aa(A,A,plus_plus(A,A2),B3),C1) = div_mod(A,aa(A,A,plus_plus(A,div_mod(A,A2,C1)),B3),C1) ) )).

tff(fact_43_mod__add__right__eq,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [C1: A,B3: A,A2: A] : div_mod(A,aa(A,A,plus_plus(A,A2),B3),C1) = div_mod(A,aa(A,A,plus_plus(A,A2),div_mod(A,B3,C1)),C1) ) )).

tff(fact_44_mod__diff__cong,axiom,(
    ! [A: $tType] :
      ( ring_div(A)
     =&gt; ! [B5: A,B3: A,A3: A,C1: A,A2: A] :
          ( div_mod(A,A2,C1) = div_mod(A,A3,C1)
         =&gt; ( div_mod(A,B3,C1) = div_mod(A,B5,C1)
           =&gt; div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),B3),C1) = div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),A3),B5),C1) ) ) ) )).

tff(fact_45_mod__diff__eq,axiom,(
    ! [A: $tType] :
      ( ring_div(A)
     =&gt; ! [C1: A,B3: A,A2: A] : div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),B3),C1) = div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),div_mod(A,A2,C1)),div_mod(A,B3,C1)),C1) ) )).

tff(fact_46_mod__diff__left__eq,axiom,(
    ! [A: $tType] :
      ( ring_div(A)
     =&gt; ! [C1: A,B3: A,A2: A] : div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),B3),C1) = div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),div_mod(A,A2,C1)),B3),C1) ) )).

tff(fact_47_mod__diff__right__eq,axiom,(
    ! [A: $tType] :
      ( ring_div(A)
     =&gt; ! [C1: A,B3: A,A2: A] : div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),B3),C1) = div_mod(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),div_mod(A,B3,C1)),C1) ) )).

tff(fact_48_filter__id__conv,axiom,(
    ! [A: $tType,Xsa: list(A),P1: fun(A,bool)] :
      ( filter(A,P1,Xsa) = Xsa
    &lt;=&gt; ! [X3: A] :
          ( pp(aa(fun(A,bool),bool,aa(A,fun(fun(A,bool),bool),member(A),X3),set(A,Xsa)))
         =&gt; pp(aa(A,bool,P1,X3)) ) ) )).

tff(fact_49_zdiff__zmod__left,axiom,(
    ! [Y: int,M: int,X: int] : div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),div_mod(int,X,M)),Y),M) = div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),X),Y),M) )).

tff(fact_50_zdiff__zmod__right,axiom,(
    ! [M: int,Y: int,X: int] : div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),X),div_mod(int,Y,M)),M) = div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),X),Y),M) )).

tff(fact_51_add__Max__commute,axiom,(
    ! [A: $tType] :
      ( linord2061991079up_add(A)
     =&gt; ! [K: A,N: fun(A,bool)] :
          ( finite_finite1(A,N)
         =&gt; ( N != bot_bot(fun(A,bool))
           =&gt; aa(A,A,plus_plus(A,K),big_linorder_Max(A,N)) = big_linorder_Max(A,collect(A,aa(fun(A,fun(A,bool)),fun(A,bool),aa(fun(fun(A,bool),bool),fun(fun(A,fun(A,bool)),fun(A,bool)),combb(fun(A,bool),bool,A),fEx(A)),aa(fun(A,bool),fun(A,fun(A,bool)),aa(fun(A,fun(fun(A,bool),fun(A,bool))),fun(fun(A,bool),fun(A,fun(A,bool))),combc(A,fun(A,bool),fun(A,bool)),aa(fun(A,fun(A,fun(bool,bool))),fun(A,fun(fun(A,bool),fun(A,bool))),aa(fun(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool))),fun(fun(A,fun(A,fun(bool,bool))),fun(A,fun(fun(A,bool),fun(A,bool)))),combb(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool)),A),combs(A,bool,bool)),aa(fun(A,fun(A,bool)),fun(A,fun(A,fun(bool,bool))),aa(fun(fun(A,bool),fun(A,fun(bool,bool))),fun(fun(A,fun(A,bool)),fun(A,fun(A,fun(bool,bool)))),combb(fun(A,bool),fun(A,fun(bool,bool)),A),aa(fun(bool,fun(bool,bool)),fun(fun(A,bool),fun(A,fun(bool,bool))),combb(bool,fun(bool,bool),A),fconj)),aa(fun(A,A),fun(A,fun(A,bool)),aa(fun(A,fun(fun(A,A),fun(A,bool))),fun(fun(A,A),fun(A,fun(A,bool))),combc(A,fun(A,A),fun(A,bool)),aa(fun(A,fun(A,bool)),fun(A,fun(fun(A,A),fun(A,bool))),aa(fun(fun(A,bool),fun(fun(A,A),fun(A,bool))),fun(fun(A,fun(A,bool)),fun(A,fun(fun(A,A),fun(A,bool)))),combb(fun(A,bool),fun(fun(A,A),fun(A,bool)),A),combb(A,bool,A)),fequal(A))),plus_plus(A,K))))),aa(fun(A,bool),fun(A,bool),aa(fun(A,fun(fun(A,bool),bool)),fun(fun(A,bool),fun(A,bool)),combc(A,fun(A,bool),bool),member(A)),N))))) ) ) ) )).

tff(fact_52_finite_OemptyI,axiom,(
    ! [A: $tType] : finite_finite1(A,bot_bot(fun(A,bool))) )).

tff(fact_53_filter__False,axiom,(
    ! [A: $tType,P1: fun(A,bool),Xsa: list(A)] :
      ( ! [X1: A] :
          ( pp(aa(fun(A,bool),bool,aa(A,fun(fun(A,bool),bool),member(A),X1),set(A,Xsa)))
         =&gt; ~ pp(aa(A,bool,P1,X1)) )
     =&gt; filter(A,P1,Xsa) = nil(A) ) )).

tff(fact_54_finite__Collect__disjI,axiom,(
    ! [A: $tType,Q1: fun(A,bool),P1: fun(A,bool)] :
      ( finite_finite1(A,collect(A,aa(fun(A,bool),fun(A,bool),aa(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool)),combs(A,bool,bool),aa(fun(A,bool),fun(A,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(A,bool),fun(A,fun(bool,bool))),combb(bool,fun(bool,bool),A),fdisj),P1)),Q1)))
    &lt;=&gt; ( finite_finite1(A,collect(A,P1))
        &amp; finite_finite1(A,collect(A,Q1)) ) ) )).

tff(fact_55_finite__Collect__conjI,axiom,(
    ! [A: $tType,Q1: fun(A,bool),P1: fun(A,bool)] :
      ( ( finite_finite1(A,collect(A,P1))
        | finite_finite1(A,collect(A,Q1)) )
     =&gt; finite_finite1(A,collect(A,aa(fun(A,bool),fun(A,bool),aa(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool)),combs(A,bool,bool),aa(fun(A,bool),fun(A,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(A,bool),fun(A,fun(bool,bool))),combb(bool,fun(bool,bool),A),fconj),P1)),Q1))) ) )).

tff(fact_56_split__paired__Ex,axiom,(
    ! [A: $tType,B: $tType,P1: fun(product_prod(A,B),bool)] :
      ( ? [X11: product_prod(A,B)] : pp(aa(product_prod(A,B),bool,P1,X11))
    &lt;=&gt; ? [A5: A,B4: B] : pp(aa(product_prod(A,B),bool,P1,aa(B,product_prod(A,B),aa(A,fun(B,product_prod(A,B)),product_Pair(A,B),A5),B4))) ) )).

tff(fact_57_Max__in,axiom,(
    ! [A: $tType] :
      ( linorder(A)
     =&gt; ! [A1: fun(A,bool)] :
          ( finite_finite1(A,A1)
         =&gt; ( A1 != bot_bot(fun(A,bool))
           =&gt; pp(aa(fun(A,bool),bool,aa(A,fun(fun(A,bool),bool),member(A),big_linorder_Max(A,A1)),A1)) ) ) ) )).

tff(fact_58_x,axiom,(
    ! [X2: atom] :
      ( pp(aa(fun(atom,bool),bool,aa(atom,fun(fun(atom,bool),bool),member(atom),X2),set(atom,as)))
     =&gt; i_Z(X2,cons(int,x,xs)) ) )).

tff(fact_59_finite__Diff,axiom,(
    ! [A: $tType,B2: fun(A,bool),A1: fun(A,bool)] :
      ( finite_finite1(A,A1)
     =&gt; finite_finite1(A,aa(fun(A,bool),fun(A,bool),aa(fun(A,bool),fun(fun(A,bool),fun(A,bool)),minus_minus(fun(A,bool)),A1),B2)) ) )).

tff(fact_60_finite__code,axiom,(
    ! [A: $tType] :
      ( finite_finite(A)
     =&gt; ! [A1: fun(A,bool)] : finite_finite1(A,A1) ) )).

tff(fact_61_list_Oinject,axiom,(
    ! [A: $tType,List2: list(A),A4: A,List1: list(A),Aa: A] :
      ( cons(A,Aa,List1) = cons(A,A4,List2)
    &lt;=&gt; ( Aa = A4
        &amp; List1 = List2 ) ) )).

tff(fact_62__096EX_Ax_O_AALL_Aa_058set_Aas_O_AI_092_060_094isub_062Z_Aa_A_Ix_A_D_Axs_J_096,axiom,(
    ? [X1: int] :
    ! [Xa1: atom] :
      ( pp(aa(fun(atom,bool),bool,aa(atom,fun(fun(atom,bool),bool),member(atom),Xa1),set(atom,as)))
     =&gt; i_Z(Xa1,cons(int,X1,xs)) ) )).

tff(fact_63_double__zero__sym,axiom,(
    ! [A: $tType] :
      ( linord219039673up_add(A)
     =&gt; ! [Aa: A] :
          ( zero_zero(A) = aa(A,A,plus_plus(A,Aa),Aa)
        &lt;=&gt; Aa = zero_zero(A) ) ) )).

tff(fact_64_diff__self,axiom,(
    ! [A: $tType] :
      ( group_add(A)
     =&gt; ! [A2: A] : aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),A2) = zero_zero(A) ) )).

tff(fact_65_mod__0,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [A2: A] : div_mod(A,zero_zero(A),A2) = zero_zero(A) ) )).

tff(fact_66_mod__self,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [A2: A] : div_mod(A,A2,A2) = zero_zero(A) ) )).

tff(fact_67_map_Osimps_I2_J,axiom,(
    ! [A: $tType,B: $tType,Xsa: list(B),Xa: B,F: fun(B,A)] : map(B,A,F,cons(B,Xa,Xsa)) = cons(A,aa(B,A,F,Xa),map(B,A,F,Xsa)) )).

tff(fact_68_zmod__zero,axiom,(
    ! [B3: int] : div_mod(int,zero_zero(int),B3) = zero_zero(int) )).

tff(fact_69_zmod__self,axiom,(
    ! [A2: int] : div_mod(int,A2,A2) = zero_zero(int) )).

tff(fact_70_filter_Osimps_I2_J,axiom,(
    ! [A: $tType,Xsa: list(A),Xa: A,P1: fun(A,bool)] :
      ( ( pp(aa(A,bool,P1,Xa))
       =&gt; filter(A,P1,cons(A,Xa,Xsa)) = cons(A,Xa,filter(A,P1,Xsa)) )
      &amp; ( ~ pp(aa(A,bool,P1,Xa))
       =&gt; filter(A,P1,cons(A,Xa,Xsa)) = filter(A,P1,Xsa) ) ) )).

tff(fact_71__096I_092_060_094isub_062Z_Aa_A_Ix_A_D_Axs_J_096,axiom,(
    i_Z(a,cons(int,x,xs)) )).

tff(fact_72__096_B_Bthesis_O_A_I_B_Bx_O_AALL_Aa_058set_Aas_O_AI_092_060_094isub_062Z_Aa_A_Ix_A_D_Axs_J_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096,axiom,(
    ~ ! [X1: int] :
        ~ ! [Xa1: atom] :
            ( pp(aa(fun(atom,bool),bool,aa(atom,fun(fun(atom,bool),bool),member(atom),Xa1),set(atom,as)))
           =&gt; i_Z(Xa1,cons(int,X1,xs)) ) )).

tff(fact_73_not__Cons__self,axiom,(
    ! [A: $tType,X: A,Xs: list(A)] : Xs != cons(A,X,Xs) )).

tff(fact_74_ext,axiom,(
    ! [B: $tType,A: $tType,G: fun(A,B),F: fun(A,B)] :
      ( ! [X1: A] : aa(A,B,F,X1) = aa(A,B,G,X1)
     =&gt; F = G ) )).

tff(fact_75_mem__def,axiom,(
    ! [A: $tType,A1: fun(A,bool),Xa: A] :
      ( pp(aa(fun(A,bool),bool,aa(A,fun(fun(A,bool),bool),member(A),Xa),A1))
    &lt;=&gt; pp(aa(A,bool,A1,Xa)) ) )).

tff(fact_76_Collect__def,axiom,(
    ! [A: $tType,P1: fun(A,bool)] : collect(A,P1) = P1 )).

tff(fact_77_not__Cons__self2,axiom,(
    ! [A: $tType,Xs: list(A),X: A] : cons(A,X,Xs) != Xs )).

tff(fact_78_zero__reorient,axiom,(
    ! [A: $tType] :
      ( zero(A)
     =&gt; ! [Xa: A] :
          ( zero_zero(A) = Xa
        &lt;=&gt; Xa = zero_zero(A) ) ) )).

tff(fact_79_finite__Diff2,axiom,(
    ! [A: $tType,A1: fun(A,bool),B2: fun(A,bool)] :
      ( finite_finite1(A,B2)
     =&gt; ( finite_finite1(A,aa(fun(A,bool),fun(A,bool),aa(fun(A,bool),fun(fun(A,bool),fun(A,bool)),minus_minus(fun(A,bool)),A1),B2))
      &lt;=&gt; finite_finite1(A,A1) ) ) )).

tff(fact_80_set__ConsD,axiom,(
    ! [A: $tType,Xsa: list(A),Xa: A,Y2: A] :
      ( pp(aa(fun(A,bool),bool,aa(A,fun(fun(A,bool),bool),member(A),Y2),set(A,cons(A,Xa,Xsa))))
     =&gt; ( Y2 = Xa
        | pp(aa(fun(A,bool),bool,aa(A,fun(fun(A,bool),bool),member(A),Y2),set(A,Xsa))) ) ) )).

tff(fact_81_list_Osimps_I3_J,axiom,(
    ! [A: $tType,List: list(A),A3: A] : cons(A,A3,List) != nil(A) )).

tff(fact_82_list_Osimps_I2_J,axiom,(
    ! [A: $tType,List: list(A),A3: A] : nil(A) != cons(A,A3,List) )).

tff(fact_83_add__0__left,axiom,(
    ! [A: $tType] :
      ( monoid_add(A)
     =&gt; ! [A2: A] : aa(A,A,plus_plus(A,zero_zero(A)),A2) = A2 ) )).

tff(fact_84_add__0,axiom,(
    ! [A: $tType] :
      ( comm_monoid_add(A)
     =&gt; ! [A2: A] : aa(A,A,plus_plus(A,zero_zero(A)),A2) = A2 ) )).

tff(fact_85_add__0__right,axiom,(
    ! [A: $tType] :
      ( monoid_add(A)
     =&gt; ! [A2: A] : aa(A,A,plus_plus(A,A2),zero_zero(A)) = A2 ) )).

tff(fact_86_add_Ocomm__neutral,axiom,(
    ! [A: $tType] :
      ( comm_monoid_add(A)
     =&gt; ! [A2: A] : aa(A,A,plus_plus(A,A2),zero_zero(A)) = A2 ) )).

tff(fact_87_diff__0__right,axiom,(
    ! [A: $tType] :
      ( group_add(A)
     =&gt; ! [A2: A] : aa(A,A,aa(A,fun(A,A),minus_minus(A),A2),zero_zero(A)) = A2 ) )).

tff(fact_88_eq__iff__diff__eq__0,axiom,(
    ! [A: $tType] :
      ( group_add(A)
     =&gt; ! [B1: A,Aa: A] :
          ( Aa = B1
        &lt;=&gt; aa(A,A,aa(A,fun(A,A),minus_minus(A),Aa),B1) = zero_zero(A) ) ) )).

tff(fact_89_right__minus__eq,axiom,(
    ! [A: $tType] :
      ( group_add(A)
     =&gt; ! [B1: A,Aa: A] :
          ( aa(A,A,aa(A,fun(A,A),minus_minus(A),Aa),B1) = zero_zero(A)
        &lt;=&gt; Aa = B1 ) ) )).

tff(fact_90_mod__by__0,axiom,(
    ! [A: $tType] :
      ( semiring_div(A)
     =&gt; ! [A2: A] : div_mod(A,A2,zero_zero(A)) = A2 ) )).

tff(fact_91_finite,axiom,(
    ! [A: $tType] :
      ( finite_finite(A)
     =&gt; ! [A1: fun(A,bool)] : finite_finite1(A,A1) ) )).

tff(fact_92_finite__image__set,axiom,(
    ! [B: $tType,A: $tType,F: fun(A,B),P1: fun(A,bool)] :
      ( finite_finite1(A,collect(A,P1))
     =&gt; finite_finite1(B,collect(B,aa(fun(B,fun(A,bool)),fun(B,bool),aa(fun(fun(A,bool),bool),fun(fun(B,fun(A,bool)),fun(B,bool)),combb(fun(A,bool),bool,B),fEx(A)),aa(fun(A,bool),fun(B,fun(A,bool)),aa(fun(B,fun(fun(A,bool),fun(A,bool))),fun(fun(A,bool),fun(B,fun(A,bool))),combc(B,fun(A,bool),fun(A,bool)),aa(fun(B,fun(A,fun(bool,bool))),fun(B,fun(fun(A,bool),fun(A,bool))),aa(fun(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool))),fun(fun(B,fun(A,fun(bool,bool))),fun(B,fun(fun(A,bool),fun(A,bool)))),combb(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool)),B),combs(A,bool,bool)),aa(fun(B,fun(A,bool)),fun(B,fun(A,fun(bool,bool))),aa(fun(fun(A,bool),fun(A,fun(bool,bool))),fun(fun(B,fun(A,bool)),fun(B,fun(A,fun(bool,bool)))),combb(fun(A,bool),fun(A,fun(bool,bool)),B),aa(fun(bool,fun(bool,bool)),fun(fun(A,bool),fun(A,fun(bool,bool))),combb(bool,fun(bool,bool),A),fconj)),aa(fun(A,B),fun(B,fun(A,bool)),aa(fun(B,fun(fun(A,B),fun(A,bool))),fun(fun(A,B),fun(B,fun(A,bool))),combc(B,fun(A,B),fun(A,bool)),aa(fun(B,fun(B,bool)),fun(B,fun(fun(A,B),fun(A,bool))),aa(fun(fun(B,bool),fun(fun(A,B),fun(A,bool))),fun(fun(B,fun(B,bool)),fun(B,fun(fun(A,B),fun(A,bool)))),combb(fun(B,bool),fun(fun(A,B),fun(A,bool)),B),combb(B,bool,A)),fequal(B))),F)))),P1)))) ) )).

tff(fact_93_finite__Collect__bounded__ex,axiom,(
    ! [B: $tType,A: $tType,Q1: fun(B,fun(A,bool)),P1: fun(A,bool)] :
      ( finite_finite1(A,collect(A,P1))
     =&gt; ( finite_finite1(B,collect(B,aa(fun(B,fun(A,bool)),fun(B,bool),aa(fun(fun(A,bool),bool),fun(fun(B,fun(A,bool)),fun(B,bool)),combb(fun(A,bool),bool,B),fEx(A)),aa(fun(B,fun(A,bool)),fun(B,fun(A,bool)),aa(fun(fun(A,bool),fun(A,bool)),fun(fun(B,fun(A,bool)),fun(B,fun(A,bool))),combb(fun(A,bool),fun(A,bool),B),aa(fun(A,fun(bool,bool)),fun(fun(A,bool),fun(A,bool)),combs(A,bool,bool),aa(fun(A,bool),fun(A,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(A,bool),fun(A,fun(bool,bool))),combb(bool,fun(bool,bool),A),fconj),P1))),Q1))))
      &lt;=&gt; ! [Y1: A] :
            ( pp(aa(A,bool,P1,Y1))
           =&gt; finite_finite1(B,collect(B,aa(A,fun(B,bool),aa(fun(B,fun(A,bool)),fun(A,fun(B,bool)),combc(B,A,bool),Q1),Y1))) ) ) ) )).

tff(fact_94_iprod__Nil,axiom,(
    ! [A: $tType] :
      ( ring(A)
     =&gt; ! [Ys: list(A)] : aa(list(A),A,aa(list(A),fun(list(A),A),iprod(A),nil(A)),Ys) = zero_zero(A) ) )).

tff(fact_95_iprod__Nil2,axiom,(
    ! [A: $tType] :
      ( ring(A)
     =&gt; ! [Xs: list(A)] : aa(list(A),A,aa(list(A),fun(list(A),A),iprod(A),Xs),nil(A)) = zero_zero(A) ) )).

tff(fact_96_zlcms0__iff,axiom,(
    ! [Is: list(int)] :
      ( zlcms(Is) = zero_zero(int)
    &lt;=&gt; pp(aa(fun(int,bool),bool,aa(int,fun(fun(int,bool),bool),member(int),zero_zero(int)),set(int,Is))) ) )).

tff(fact_97_list__add__Cons,axiom,(
    ! [A: $tType] :
      ( ( cl_Groups_Oplus(A)
        &amp; zero(A) )
     =&gt; ! [Ys: list(A),Y: A,Xs: list(A),X: A] : aa(list(A),list(A),plus_plus(list(A),cons(A,X,Xs)),cons(A,Y,Ys)) = cons(A,aa(A,A,plus_plus(A,X),Y),aa(list(A),list(A),plus_plus(list(A),Xs),Ys)) ) )).

tff(fact_98_list__diff__Cons__Cons,axiom,(
    ! [A: $tType] :
      ( ( cl_Groups_Ominus(A)
        &amp; zero(A) )
     =&gt; ! [Ys: list(A),Y: A,Xs: list(A),X: A] : aa(list(A),list(A),aa(list(A),fun(list(A),list(A)),minus_minus(list(A)),cons(A,X,Xs)),cons(A,Y,Ys)) = cons(A,aa(A,A,aa(A,fun(A,A),minus_minus(A),X),Y),aa(list(A),list(A),aa(list(A),fun(list(A),list(A)),minus_minus(list(A)),Xs),Ys)) ) )).

%----Arities (23)
tff(arity_fun___Finite__Set_Ofinite,axiom,(
    ! [T_1: $tType,T_2: $tType] :
      ( ( finite_finite(T_2)
        &amp; finite_finite(T_1) )
     =&gt; finite_finite(fun(T_1,T_2)) ) )).

tff(arity_fun___Groups_Ominus,axiom,(
    ! [T_1: $tType,T_2: $tType] :
      ( cl_Groups_Ominus(T_2)
     =&gt; cl_Groups_Ominus(fun(T_1,T_2)) ) )).

tff(arity_Int_Oint___Groups_Olinordered__ab__semigroup__add,axiom,(
    linord2061991079up_add(int) )).

tff(arity_Int_Oint___Groups_Olinordered__ab__group__add,axiom,(
    linord219039673up_add(int) )).

tff(arity_Int_Oint___Groups_Ocancel__ab__semigroup__add,axiom,(
    cancel146912293up_add(int) )).

tff(arity_Int_Oint___Groups_Ocancel__semigroup__add,axiom,(
    cancel_semigroup_add(int) )).

tff(arity_Int_Oint___Groups_Oab__semigroup__add,axiom,(
    ab_semigroup_add(int) )).

tff(arity_Int_Oint___Groups_Ocomm__monoid__add,axiom,(
    comm_monoid_add(int) )).

tff(arity_Int_Oint___Divides_Osemiring__div,axiom,(
    semiring_div(int) )).

tff(arity_Int_Oint___Orderings_Olinorder,axiom,(
    linorder(int) )).

tff(arity_Int_Oint___Groups_Omonoid__add,axiom,(
    monoid_add(int) )).

tff(arity_Int_Oint___Groups_Ogroup__add,axiom,(
    group_add(int) )).

tff(arity_Int_Oint___Divides_Oring__div,axiom,(
    ring_div(int) )).

tff(arity_Int_Oint___Groups_Ominus,axiom,(
    cl_Groups_Ominus(int) )).

tff(arity_Int_Oint___Groups_Ozero,axiom,(
    zero(int) )).

tff(arity_Int_Oint___Groups_Oplus,axiom,(
    cl_Groups_Oplus(int) )).

tff(arity_Int_Oint___Rings_Oring,axiom,(
    ring(int) )).

tff(arity_HOL_Obool___Orderings_Olinorder,axiom,(
    linorder(bool) )).

tff(arity_HOL_Obool___Finite__Set_Ofinite,axiom,(
    finite_finite(bool) )).

tff(arity_HOL_Obool___Groups_Ominus,axiom,(
    cl_Groups_Ominus(bool) )).

tff(arity_List_Olist___Groups_Ominus,axiom,(
    ! [T_1: $tType] :
      ( ( zero(T_1)
        &amp; cl_Groups_Ominus(T_1) )
     =&gt; cl_Groups_Ominus(list(T_1)) ) )).

tff(arity_List_Olist___Groups_Oplus,axiom,(
    ! [T_1: $tType] :
      ( ( zero(T_1)
        &amp; cl_Groups_Oplus(T_1) )
     =&gt; cl_Groups_Oplus(list(T_1)) ) )).

tff(arity_prod___Finite__Set_Ofinite,axiom,(
    ! [T_1: $tType,T_2: $tType] :
      ( ( finite_finite(T_2)
        &amp; finite_finite(T_1) )
     =&gt; finite_finite(product_prod(T_1,T_2)) ) )).

%----Helper facts (20)
tff(help_pp_1_1_U,axiom,(
    ~ pp(fFalse) )).

tff(help_pp_2_1_U,axiom,(
    pp(fTrue) )).

tff(help_fEx_1_1_U,axiom,(
    ! [A: $tType,X: A,P: fun(A,bool)] :
      ( ~ pp(aa(A,bool,P,X))
      | pp(aa(fun(A,bool),bool,fEx(A),P)) ) )).

tff(help_COMBB_1_1_U,axiom,(
    ! [C: $tType,B: $tType,A: $tType,R: A,Q: fun(A,B),P: fun(B,C)] : aa(A,C,aa(fun(A,B),fun(A,C),aa(fun(B,C),fun(fun(A,B),fun(A,C)),combb(B,C,A),P),Q),R) = aa(B,C,P,aa(A,B,Q,R)) )).

tff(help_COMBC_1_1_U,axiom,(
    ! [A: $tType,C: $tType,B: $tType,R: A,Q: B,P: fun(A,fun(B,C))] : aa(A,C,aa(B,fun(A,C),aa(fun(A,fun(B,C)),fun(B,fun(A,C)),combc(A,B,C),P),Q),R) = aa(B,C,aa(A,fun(B,C),P,R),Q) )).

tff(help_COMBI_1_1_U,axiom,(
    ! [A: $tType,P: A] : aa(A,A,combi(A),P) = P )).

tff(help_COMBK_1_1_U,axiom,(
    ! [B: $tType,A: $tType,Q: B,P: A] : aa(B,A,combk(A,B,P),Q) = P )).

tff(help_COMBS_1_1_U,axiom,(
    ! [C: $tType,B: $tType,A: $tType,R: A,Q: fun(A,B),P: fun(A,fun(B,C))] : aa(A,C,aa(fun(A,B),fun(A,C),aa(fun(A,fun(B,C)),fun(fun(A,B),fun(A,C)),combs(A,B,C),P),Q),R) = aa(B,C,aa(A,fun(B,C),P,R),aa(A,B,Q,R)) )).

tff(help_fTrue_1_1_U,axiom,(
    pp(fTrue) )).

tff(help_fTrue_1_1_T,axiom,(
    ! [P: bool] :
      ( P = fTrue
      | P = fFalse ) )).

tff(help_fconj_1_1_U,axiom,(
    ! [Q: bool,P: bool] :
      ( ~ pp(P)
      | ~ pp(Q)
      | pp(aa(bool,bool,aa(bool,fun(bool,bool),fconj,P),Q)) ) )).

tff(help_fconj_2_1_U,axiom,(
    ! [Q: bool,P: bool] :
      ( ~ pp(aa(bool,bool,aa(bool,fun(bool,bool),fconj,P),Q))
      | pp(P) ) )).

tff(help_fconj_3_1_U,axiom,(
    ! [Q: bool,P: bool] :
      ( ~ pp(aa(bool,bool,aa(bool,fun(bool,bool),fconj,P),Q))
      | pp(Q) ) )).

tff(help_fdisj_1_1_U,axiom,(
    ! [Q: bool,P: bool] :
      ( ~ pp(P)
      | pp(aa(bool,bool,aa(bool,fun(bool,bool),fdisj,P),Q)) ) )).

tff(help_fdisj_2_1_U,axiom,(
    ! [P: bool,Q: bool] :
      ( ~ pp(Q)
      | pp(aa(bool,bool,aa(bool,fun(bool,bool),fdisj,P),Q)) ) )).

tff(help_fdisj_3_1_U,axiom,(
    ! [Q: bool,P: bool] :
      ( ~ pp(aa(bool,bool,aa(bool,fun(bool,bool),fdisj,P),Q))
      | pp(P)
      | pp(Q) ) )).

tff(help_fFalse_1_1_U,axiom,(
    ~ pp(fFalse) )).

tff(help_fFalse_1_1_T,axiom,(
    ! [P: bool] :
      ( P = fTrue
      | P = fFalse ) )).

tff(help_fequal_1_1_T,axiom,(
    ! [A: $tType,Y: A,X: A] :
      ( ~ pp(aa(A,bool,aa(A,fun(A,bool),fequal(A),X),Y))
      | X = Y ) )).

tff(help_fequal_2_1_T,axiom,(
    ! [A: $tType,Y: A,X: A] :
      ( X != Y
      | pp(aa(A,bool,aa(A,fun(A,bool),fequal(A),X),Y)) ) )).

%----Conjectures (1)
tff(conj_0,conjecture,(
    div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),aa(int,int,plus_plus(int,li),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),zlcms(map(atom,int,divisor,filter(atom,atom_case(bool,combk(fun(list(int),bool),int,combk(bool,list(int),fFalse)),combk(fun(int,fun(list(int),bool)),int,combk(fun(list(int),bool),int,combk(bool,list(int),fTrue))),combk(fun(int,fun(list(int),bool)),int,combk(fun(list(int),bool),int,combk(bool,list(int),fTrue)))),as)))))),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)),aa(atom,int,divisor,a)) = div_mod(int,aa(int,int,plus_plus(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),zlcms(map(atom,int,divisor,filter(atom,atom_case(bool,combk(fun(list(int),bool),int,combk(bool,list(int),fFalse)),combk(fun(int,fun(list(int),bool)),int,combk(fun(list(int),bool),int,combk(bool,list(int),fTrue))),combk(fun(int,fun(list(int),bool)),int,combk(fun(list(int),bool),int,combk(bool,list(int),fTrue)))),as))))),aa(atom,int,divisor,a)) )).

%------------------------------------------------------------------------------
</pre></body></html>