Beagle---0.9.52.THM-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Beagle---0.9.52
% Problem  : ITP001_1 : TPTP v9.0.0. Released v8.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s

% Computer : n013.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Apr  9 06:53:45 PM UTC 2025

% Result   : Theorem 18.56s 5.94s
% Output   : CNFRefutation 18.88s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : ITP001_1 : TPTP v9.0.0. Released v8.1.0.
% 0.03/0.13  % Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34  % Computer : n013.cluster.edu
% 0.14/0.34  % Model    : x86_64 x86_64
% 0.14/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34  % Memory   : 8042.1875MB
% 0.14/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34  % CPULimit : 300
% 0.14/0.34  % WCLimit  : 300
% 0.14/0.34  % DateTime : Tue Apr  8 02:23:32 EDT 2025
% 0.14/0.34  % CPUTime  : 
% 18.56/5.94  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.88/5.95  
% 18.88/5.95  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.88/5.96  %$ bij_betw$p > bij_betw$o > bij_betw$n > bij_betw$m > bij_betw$l > bij_betw$k > bij_betw$j > bij_betw$i > bij_betw$h > bij_betw$g > bij_betw$f > bij_betw$e > bij_betw$d > bij_betw$c > bij_betw$b > bij_betw$a > bij_betw$ > member$e > member$d > member$c > member$b > member$a > member$ > less_eq$a > less_eq$ > inj_on$d > inj_on$c > inj_on$b > inj_on$a > inj_on$ > fun_app$u > fun_app$s > fun_app$g > fun_app$f > register$ > permutation$a > permutation$ > finite$q > finite$p > finite$o > finite$n > finite$m > finite$l > finite$k > finite$j > finite$i > finite$h > finite$g > finite$f > finite$e > finite$d > finite$c > finite$b > finite$a > finite$ > evenperm$a > evenperm$ > bijection$a > bijection$ > vimage$c > vimage$b > vimage$a > vimage$ > transpose$a > the_inv_into$a > the_inv_into$ > inv_into$e > inv_into$d > inv_into$c > inv_into$a > inv_into$ > inf$b > inf$a > inf$ > image$d > image$c > image$b > image$a > image$ > fun_app$t > fun_app$r > fun_app$q > fun_app$p > fun_app$o > fun_app$n > fun_app$m > fun_app$l > fun_app$k > fun_app$j > fun_app$i > fun_app$h > fun_app$e > fun_app$d > fun_app$c > fun_app$b > fun_app$a > fun_app$ > compow$a > comp$q > comp$o > comp$n > comp$m > comp$l > comp$k > comp$j > comp$i > comp$h > comp$g > comp$f > comp$e > comp$d > comp$c > comp$b > comp$a > #nlpp > uub$ > transpose$ > sign$a > sign$ > plus$a > of_nat$ > nat$ > inv_into$b > compow$ > comp$r > comp$p > comp$ > collect$d > collect$c > collect$b > collect$a > collect$ > card$g > card$f > card$e > card$d > card$c > card$b > card$a > card$ > uua$ > uu$ > top$x > top$w > top$v > top$u > top$t > top$s > top$r > top$q > top$p > top$o > top$n > top$m > top$l > top$k > top$j > top$i > top$h > top$g > top$f > top$e > top$d > top$c > top$b > top$a > top$ > swap$c > swap$b > swap$a > swap$ > plus$ > id$e > id$d > id$c > id$b > id$a > id$ > assoc$a > assoc$ > #skF_73 > #skF_81 > #skF_40 > #skF_145 > #skF_10 > #skF_36 > #skF_34 > #skF_2 > #skF_116 > #skF_47 > #skF_120 > #skF_20 > #skF_50 > #skF_117 > #skF_33 > #skF_140 > #skF_31 > #skF_110 > #skF_16 > #skF_59 > #skF_8 > #skF_74 > #skF_131 > #skF_7 > #skF_146 > #skF_95 > #skF_121 > #skF_108 > #skF_170 > #skF_114 > #skF_39 > #skF_98 > #skF_123 > #skF_135 > #skF_89 > #skF_163 > #skF_49 > #skF_154 > #skF_35 > #skF_105 > #skF_24 > #skF_129 > #skF_97 > #skF_99 > #skF_63 > #skF_61 > #skF_141 > #skF_143 > #skF_128 > #skF_41 > #skF_137 > #skF_169 > #skF_5 > #skF_62 > #skF_167 > #skF_86 > #skF_21 > #skF_88 > #skF_69 > #skF_147 > #skF_83 > #skF_93 > #skF_177 > #skF_142 > #skF_124 > #skF_96 > #skF_127 > #skF_32 > #skF_9 > #skF_148 > #skF_91 > #skF_130 > #skF_106 > #skF_152 > #skF_57 > #skF_136 > #skF_65 > #skF_153 > #skF_43 > #skF_12 > #skF_149 > #skF_52 > #skF_157 > #skF_77 > #skF_6 > #skF_44 > #skF_156 > #skF_82 > #skF_17 > #skF_30 > #skF_37 > #skF_162 > #skF_90 > #skF_132 > #skF_87 > #skF_67 > #skF_1 > #skF_133 > #skF_19 > #skF_160 > #skF_115 > #skF_76 > #skF_54 > #skF_107 > #skF_151 > #skF_113 > #skF_28 > #skF_46 > #skF_51 > #skF_26 > #skF_42 > #skF_158 > #skF_23 > #skF_78 > #skF_92 > #skF_55 > #skF_58 > #skF_165 > #skF_66 > #skF_84 > #skF_172 > #skF_101 > #skF_11 > #skF_79 > #skF_166 > #skF_25 > #skF_85 > #skF_4 > #skF_102 > #skF_64 > #skF_53 > #skF_14 > #skF_139 > #skF_155 > #skF_48 > #skF_168 > #skF_75 > #skF_161 > #skF_176 > #skF_45 > #skF_159 > #skF_94 > #skF_29 > #skF_138 > #skF_118 > #skF_38 > #skF_72 > #skF_3 > #skF_112 > #skF_80 > #skF_171 > #skF_27 > #skF_13 > #skF_60 > #skF_70 > #skF_173 > #skF_174 > #skF_144 > #skF_104 > #skF_15 > #skF_125 > #skF_111 > #skF_150 > #skF_56 > #skF_175 > #skF_68 > #skF_18 > #skF_22 > #skF_122 > #skF_103 > #skF_134 > #skF_164 > #skF_126 > #skF_100 > #skF_71 > #skF_119
% 18.88/5.96  
% 18.88/5.96  %Foreground sorts:
% 18.88/5.96  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$: $tType ).
% 18.88/5.96  tff(Int_set$, type, Int_set$: $tType ).
% 18.88/5.96  tff(Nat$, type, Nat$: $tType ).
% 18.88/5.96  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$: $tType ).
% 18.88/5.97  tff(C_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, type, C_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_int_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_int_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set_set$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(Int_int_fun$, type, Int_int_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_option_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_option_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_int_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_int_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_c_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_c_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(Int_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, type, Int_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$: $tType ).
% 18.88/5.97  tff(Int_int_bool_fun_fun$, type, Int_int_bool_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(Int_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, type, Int_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(Nat_bool_fun$, type, Nat_bool_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_bool_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_bool_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_bool_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_bool_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_option_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_option_set$: $tType ).
% 18.88/5.97  tff(B_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, type, B_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_b_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_b_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set_set$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_bool_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_bool_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(Int_bool_fun$, type, Int_bool_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$: $tType ).
% 18.88/5.97  tff(A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, type, A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  tff(A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, type, A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.88/5.97  
% 18.88/5.97  %Background operators:
% 18.88/5.97  tff('#skF_109', type, '#skF_109': $int).
% 18.88/5.97  tff('#skE_2', type, '#skE_2': $int).
% 18.88/5.97  tff('#skE_1', type, '#skE_1': $int).
% 18.88/5.97  tff('#skE_4', type, '#skE_4': $int).
% 18.88/5.97  tff('#skE_3', type, '#skE_3': $int).
% 18.88/5.97  
% 18.88/5.97  %Foreground operators:
% 18.88/5.97  tff(bij_betw$f, type, bij_betw$f: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff(finite$m, type, finite$m: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_option_set$ > $o).
% 18.88/5.97  tff('#skF_73', type, '#skF_73': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$p, type, top$p: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$).
% 18.88/5.97  tff('#skF_81', type, '#skF_81': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_40', type, '#skF_40': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_145', type, '#skF_145': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_10', type, '#skF_10': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(plus$, type, plus$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff('#skF_36', type, '#skF_36': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(the_inv_into$a, type, the_inv_into$a: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_34', type, '#skF_34': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(fun_app$r, type, fun_app$r: (Int_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * $int) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(finite$h, type, finite$h: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$ > $o).
% 18.88/5.97  tff(collect$a, type, collect$a: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_bool_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$).
% 18.88/5.97  tff('#skF_2', type, '#skF_2': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_116', type, '#skF_116': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_47', type, '#skF_47': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_120', type, '#skF_120': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(bij_betw$a, type, bij_betw$a: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(comp$m, type, comp$m: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_20', type, '#skF_20': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inf$, type, inf$: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(comp$b, type, comp$b: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(fun_app$g, type, fun_app$g: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_bool_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > $o).
% 18.88/5.97  tff('#skF_50', type, '#skF_50': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inv_into$a, type, inv_into$a: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(card$b, type, card$b: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$ > Nat$).
% 18.88/5.97  tff(comp$j, type, comp$j: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(card$f, type, card$f: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_option_set$ > Nat$).
% 18.88/5.97  tff('#skF_117', type, '#skF_117': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$f, type, top$f: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_bool_fun$).
% 18.88/5.97  tff('#skF_33', type, '#skF_33': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_140', type, '#skF_140': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_31', type, '#skF_31': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_110', type, '#skF_110': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_16', type, '#skF_16': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_59', type, '#skF_59': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_8', type, '#skF_8': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(finite$l, type, finite$l: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_option_set$ > $o).
% 18.88/5.97  tff(finite$f, type, finite$f: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$ > $o).
% 18.88/5.97  tff('#skF_74', type, '#skF_74': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_131', type, '#skF_131': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$n, type, top$n: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$).
% 18.88/5.97  tff(top$d, type, top$d: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$).
% 18.88/5.97  tff('#skF_7', type, '#skF_7': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$n, type, comp$n: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff('#skF_146', type, '#skF_146': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_95', type, '#skF_95': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_121', type, '#skF_121': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(fun_app$, type, fun_app$: (Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff('#skF_108', type, '#skF_108': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$t, type, top$t: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set_set$).
% 18.88/5.97  tff('#skF_170', type, '#skF_170': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_114', type, '#skF_114': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_39', type, '#skF_39': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(fun_app$n, type, fun_app$n: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(fun_app$d, type, fun_app$d: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(card$a, type, card$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ > Nat$).
% 18.88/5.97  tff('#skF_98', type, '#skF_98': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_123', type, '#skF_123': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_135', type, '#skF_135': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(finite$i, type, finite$i: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$ > $o).
% 18.88/5.97  tff('#skF_89', type, '#skF_89': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_163', type, '#skF_163': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 18.88/5.97  tff(comp$g, type, comp$g: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(bij_betw$k, type, bij_betw$k: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff(plus$a, type, plus$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(comp$k, type, comp$k: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(bij_betw$i, type, bij_betw$i: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff(fun_app$p, type, fun_app$p: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_int_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > $int).
% 18.88/5.97  tff('#skF_49', type, '#skF_49': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(image$, type, image$: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(member$d, type, member$d: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(less_eq$, type, less_eq$: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff('#skF_154', type, '#skF_154': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_35', type, '#skF_35': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$l, type, top$l: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$).
% 18.88/5.97  tff(evenperm$a, type, evenperm$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > $o).
% 18.88/5.97  tff(swap$c, type, swap$c: C_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_105', type, '#skF_105': (Int_set$ * Int_int_fun$ * Int_int_fun$ * Int_set$) > $int).
% 18.88/5.97  tff(finite$k, type, finite$k: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set_set$ > $o).
% 18.88/5.97  tff('#skF_24', type, '#skF_24': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(collect$, type, collect$: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$).
% 18.88/5.97  tff(inv_into$d, type, inv_into$d: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_b_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_fun$) > B_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_129', type, '#skF_129': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_97', type, '#skF_97': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(finite$n, type, finite$n: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$ > $o).
% 18.88/5.97  tff('#skF_99', type, '#skF_99': (Int_int_fun$ * Int_set$ * Int_set$) > Int_int_fun$).
% 18.88/5.97  tff('#skF_63', type, '#skF_63': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_61', type, '#skF_61': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(collect$c, type, collect$c: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_bool_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(register$, type, register$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > $o).
% 18.88/5.97  tff('#skF_141', type, '#skF_141': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_143', type, '#skF_143': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(permutation$, type, permutation$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > $o).
% 18.88/5.97  tff('#skF_128', type, '#skF_128': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$d, type, comp$d: (Int_int_fun$ * Int_int_fun$) > Int_int_fun$).
% 18.88/5.97  tff('#skF_41', type, '#skF_41': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_137', type, '#skF_137': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_169', type, '#skF_169': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_5', type, '#skF_5': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(swap$b, type, swap$b: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_c_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(inf$a, type, inf$a: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(inv_into$, type, inv_into$: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_62', type, '#skF_62': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_167', type, '#skF_167': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_86', type, '#skF_86': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(compow$, type, compow$: Nat$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff('#skF_21', type, '#skF_21': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_88', type, '#skF_88': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_69', type, '#skF_69': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_147', type, '#skF_147': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(bij_betw$l, type, bij_betw$l: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff('#skF_83', type, '#skF_83': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_93', type, '#skF_93': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_177', type, '#skF_177': (Nat$ * Nat$) > Nat$).
% 18.88/5.97  tff(bij_betw$m, type, bij_betw$m: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_int_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * Int_set$) > $o).
% 18.88/5.97  tff(top$w, type, top$w: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_option_set$).
% 18.88/5.97  tff('#skF_142', type, '#skF_142': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_124', type, '#skF_124': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_96', type, '#skF_96': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_127', type, '#skF_127': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_32', type, '#skF_32': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_9', type, '#skF_9': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$l, type, comp$l: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(comp$p, type, comp$p: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff('#skF_148', type, '#skF_148': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(bijection$, type, bijection$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > $o).
% 18.88/5.97  tff(fun_app$u, type, fun_app$u: (Nat_bool_fun$ * Nat$) > $o).
% 18.88/5.97  tff('#skF_91', type, '#skF_91': Int_int_fun$ > $int).
% 18.88/5.97  tff(card$c, type, card$c: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$ > Nat$).
% 18.88/5.97  tff('#skF_130', type, '#skF_130': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inf$b, type, inf$b: (Int_set$ * Int_set$) > Int_set$).
% 18.88/5.97  tff('#skF_106', type, '#skF_106': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(the_inv_into$, type, the_inv_into$: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_152', type, '#skF_152': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_57', type, '#skF_57': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_136', type, '#skF_136': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_65', type, '#skF_65': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(fun_app$o, type, fun_app$o: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_int_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > $int).
% 18.88/5.97  tff(swap$, type, swap$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_b_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_153', type, '#skF_153': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inj_on$a, type, inj_on$a: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(comp$o, type, comp$o: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_43', type, '#skF_43': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(member$c, type, member$c: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff(finite$c, type, finite$c: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ > $o).
% 18.88/5.97  tff(member$, type, member$: ($int * Int_set$) > $o).
% 18.88/5.97  tff('#skF_12', type, '#skF_12': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(member$b, type, member$b: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff('#skF_149', type, '#skF_149': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_52', type, '#skF_52': Int_int_fun$ > $int).
% 18.88/5.97  tff(id$b, type, id$b: Int_int_fun$).
% 18.88/5.97  tff(fun_app$t, type, fun_app$t: (Int_int_bool_fun_fun$ * $int) > Int_bool_fun$).
% 18.88/5.97  tff('#skF_157', type, '#skF_157': ($int * Int_int_fun$ * $int * $int) > $int).
% 18.88/5.97  tff(bij_betw$p, type, bij_betw$p: (Int_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * Int_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff('#skF_77', type, '#skF_77': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(transpose$a, type, transpose$a: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_6', type, '#skF_6': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_44', type, '#skF_44': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(fun_app$j, type, fun_app$j: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_156', type, '#skF_156': ($int * $int * Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff(bij_betw$j, type, bij_betw$j: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff('#skF_82', type, '#skF_82': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_17', type, '#skF_17': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_30', type, '#skF_30': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_37', type, '#skF_37': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(finite$g, type, finite$g: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$ > $o).
% 18.88/5.97  tff(top$x, type, top$x: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$).
% 18.88/5.97  tff(top$c, type, top$c: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$).
% 18.88/5.97  tff('#skF_162', type, '#skF_162': ($int * Int_int_fun$ * $int * $int) > $int).
% 18.88/5.97  tff(assoc$a, type, assoc$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_90', type, '#skF_90': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_132', type, '#skF_132': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_87', type, '#skF_87': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$h, type, comp$h: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff('#skF_67', type, '#skF_67': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_1', type, '#skF_1': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$q, type, comp$q: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_133', type, '#skF_133': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$f, type, comp$f: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(top$j, type, top$j: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_bool_fun$).
% 18.88/5.97  tff('#skF_19', type, '#skF_19': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(image$d, type, image$d: (Int_int_fun$ * Int_set$) > Int_set$).
% 18.88/5.97  tff(collect$b, type, collect$b: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$).
% 18.88/5.97  tff(comp$e, type, comp$e: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(uua$, type, uua$: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_160', type, '#skF_160': ($int * $int * Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff('#skF_115', type, '#skF_115': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_76', type, '#skF_76': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$k, type, top$k: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$).
% 18.88/5.97  tff('#skF_54', type, '#skF_54': Int_int_fun$ > $int).
% 18.88/5.97  tff(fun_app$c, type, fun_app$c: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_107', type, '#skF_107': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_151', type, '#skF_151': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_113', type, '#skF_113': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(card$g, type, card$g: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_option_set$ > Nat$).
% 18.88/5.97  tff('#skF_28', type, '#skF_28': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_46', type, '#skF_46': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(fun_app$i, type, fun_app$i: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(fun_app$q, type, fun_app$q: (Int_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * $int) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$h, type, top$h: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_bool_fun$).
% 18.88/5.97  tff(finite$p, type, finite$p: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$ > $o).
% 18.88/5.97  tff(fun_app$l, type, fun_app$l: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(finite$, type, finite$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$ > $o).
% 18.88/5.97  tff(top$b, type, top$b: Int_set$).
% 18.88/5.97  tff(vimage$, type, vimage$: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(fun_app$h, type, fun_app$h: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(top$q, type, top$q: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$).
% 18.88/5.97  tff('#skF_51', type, '#skF_51': Int_int_fun$ > $int).
% 18.88/5.97  tff('#skF_26', type, '#skF_26': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_42', type, '#skF_42': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_158', type, '#skF_158': ($int * Int_int_fun$ * $int * $int) > $int).
% 18.88/5.97  tff('#skF_23', type, '#skF_23': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_78', type, '#skF_78': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_92', type, '#skF_92': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(bij_betw$b, type, bij_betw$b: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff('#skF_55', type, '#skF_55': Int_int_fun$ > $int).
% 18.88/5.97  tff('#skF_58', type, '#skF_58': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(image$a, type, image$a: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff('#skF_165', type, '#skF_165': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 18.88/5.97  tff(member$a, type, member$a: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff('#skF_66', type, '#skF_66': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inj_on$d, type, inj_on$d: (Int_int_fun$ * Int_set$) > $o).
% 18.88/5.97  tff(finite$d, type, finite$d: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$ > $o).
% 18.88/5.97  tff('#skF_84', type, '#skF_84': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_172', type, '#skF_172': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_101', type, '#skF_101': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_11', type, '#skF_11': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_79', type, '#skF_79': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_166', type, '#skF_166': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 18.88/5.97  tff('#skF_25', type, '#skF_25': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_85', type, '#skF_85': (Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff(finite$a, type, finite$a: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ > $o).
% 18.88/5.97  tff('#skF_4', type, '#skF_4': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(vimage$a, type, vimage$a: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(bij_betw$h, type, bij_betw$h: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff('#skF_102', type, '#skF_102': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inv_into$b, type, inv_into$b: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(fun_app$s, type, fun_app$s: (Int_bool_fun$ * $int) > $o).
% 18.88/5.97  tff(sign$a, type, sign$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > $int).
% 18.88/5.97  tff(finite$b, type, finite$b: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$ > $o).
% 18.88/5.97  tff('#skF_64', type, '#skF_64': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_53', type, '#skF_53': Int_int_fun$ > $int).
% 18.88/5.97  tff('#skF_14', type, '#skF_14': (Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff('#skF_139', type, '#skF_139': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(finite$e, type, finite$e: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$ > $o).
% 18.88/5.97  tff(compow$a, type, compow$a: (Nat$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(fun_app$b, type, fun_app$b: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_155', type, '#skF_155': ($int * $int * Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff(comp$i, type, comp$i: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_48', type, '#skF_48': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_168', type, '#skF_168': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_75', type, '#skF_75': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_161', type, '#skF_161': ($int * Int_int_fun$ * $int * $int) > $int).
% 18.88/5.97  tff(inj_on$b, type, inj_on$b: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff('#skF_176', type, '#skF_176': (Nat$ * Nat$) > Nat$).
% 18.88/5.97  tff(transpose$, type, transpose$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(id$e, type, id$e: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(image$c, type, image$c: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(inj_on$, type, inj_on$: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(fun_app$a, type, fun_app$a: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$u, type, top$u: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set_set$).
% 18.88/5.97  tff(vimage$c, type, vimage$c: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(top$m, type, top$m: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$).
% 18.88/5.97  tff(top$s, type, top$s: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_prod_set$).
% 18.88/5.97  tff(id$d, type, id$d: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff('#skF_45', type, '#skF_45': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(bij_betw$d, type, bij_betw$d: (Int_int_fun$ * Int_set$ * Int_set$) > $o).
% 18.88/5.97  tff('#skF_159', type, '#skF_159': ($int * $int * Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff(fun_app$f, type, fun_app$f: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_bool_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > $o).
% 18.88/5.97  tff('#skF_94', type, '#skF_94': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(card$e, type, card$e: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$ > Nat$).
% 18.88/5.97  tff(bij_betw$, type, bij_betw$: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(comp$a, type, comp$a: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(fun_app$k, type, fun_app$k: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(bij_betw$o, type, bij_betw$o: (Int_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * Int_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(finite$q, type, finite$q: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$ > $o).
% 18.88/5.97  tff('#skF_29', type, '#skF_29': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_138', type, '#skF_138': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$r, type, comp$r: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff('#skF_118', type, '#skF_118': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(evenperm$, type, evenperm$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > $o).
% 18.88/5.97  tff(finite$j, type, finite$j: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set_set$ > $o).
% 18.88/5.97  tff('#skF_38', type, '#skF_38': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_72', type, '#skF_72': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(bij_betw$c, type, bij_betw$c: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(of_nat$, type, of_nat$: Nat$ > $int).
% 18.88/5.97  tff(bij_betw$g, type, bij_betw$g: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff(nat$, type, nat$: $int > Nat$).
% 18.88/5.97  tff(member$e, type, member$e: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff(fun_app$e, type, fun_app$e: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$g, type, top$g: $o).
% 18.88/5.97  tff('#skF_3', type, '#skF_3': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_112', type, '#skF_112': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_80', type, '#skF_80': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_171', type, '#skF_171': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inv_into$c, type, inv_into$c: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(top$i, type, top$i: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_bool_fun$).
% 18.88/5.97  tff('#skF_27', type, '#skF_27': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(id$c, type, id$c: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(uu$, type, uu$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(top$v, type, top$v: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_option_set$).
% 18.88/5.97  tff('#skF_13', type, '#skF_13': Int_int_fun$ > $int).
% 18.88/5.97  tff('#skF_60', type, '#skF_60': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(id$a, type, id$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(card$d, type, card$d: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_sum_set$ > Nat$).
% 18.88/5.97  tff(id$, type, id$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_70', type, '#skF_70': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(inj_on$c, type, inj_on$c: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff('#skF_173', type, '#skF_173': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_174', type, '#skF_174': (Nat_bool_fun$ * Nat$ * Nat$) > Nat$).
% 18.88/5.97  tff(bij_betw$e, type, bij_betw$e: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$) > $o).
% 18.88/5.97  tff(permutation$a, type, permutation$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > $o).
% 18.88/5.97  tff(image$b, type, image$b: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff('#skF_144', type, '#skF_144': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_104', type, '#skF_104': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_15', type, '#skF_15': (Int_int_fun$ * $int) > $int).
% 18.88/5.97  tff(assoc$, type, assoc$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_125', type, '#skF_125': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(card$, type, card$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ > Nat$).
% 18.88/5.97  tff(collect$d, type, collect$d: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_bool_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff('#skF_111', type, '#skF_111': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_150', type, '#skF_150': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$r, type, top$r: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_prod_set$).
% 18.88/5.97  tff(less_eq$a, type, less_eq$a: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > $o).
% 18.88/5.97  tff('#skF_56', type, '#skF_56': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(inv_into$e, type, inv_into$e: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_c_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_fun$) > C_a_b_prod_prod_ell2_c_a_b_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_175', type, '#skF_175': (Nat_bool_fun$ * Nat$ * Nat$) > Nat$).
% 18.88/5.97  tff('#skF_68', type, '#skF_68': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$, type, top$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff('#skF_18', type, '#skF_18': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$).
% 18.88/5.97  tff(sign$, type, sign$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > $int).
% 18.88/5.97  tff(top$a, type, top$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff('#skF_22', type, '#skF_22': A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_122', type, '#skF_122': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_103', type, '#skF_103': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(comp$c, type, comp$c: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_134', type, '#skF_134': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$e, type, top$e: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_set$).
% 18.88/5.97  tff('#skF_164', type, '#skF_164': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 18.88/5.97  tff(vimage$b, type, vimage$b: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$).
% 18.88/5.97  tff(comp$, type, comp$: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$).
% 18.88/5.97  tff(uub$, type, uub$: $int > Int_int_fun$).
% 18.88/5.97  tff(fun_app$m, type, fun_app$m: (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff('#skF_126', type, '#skF_126': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(top$o, type, top$o: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_sum_set$).
% 18.88/5.97  tff('#skF_100', type, '#skF_100': (A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$) > A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(swap$a, type, swap$a: B_c_prod_a_prod_ell2_b_c_prod_a_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$).
% 18.88/5.97  tff(bij_betw$n, type, bij_betw$n: (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_int_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * Int_set$) > $o).
% 18.88/5.97  tff('#skF_71', type, '#skF_71': A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun_fun$ > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff('#skF_119', type, '#skF_119': (A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ * A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_set$ * A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$) > A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$).
% 18.88/5.97  tff(bijection$a, type, bijection$a: A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$ > $o).
% 18.88/5.97  tff(finite$o, type, finite$o: A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun_set$ > $o).
% 18.88/5.97  
% 18.88/5.98  tff(f_44, negated_conjecture, ~bij_betw$(assoc$, top$, top$a), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture3)).
% 18.88/5.98  tff(f_117, axiom, (![A__questionmark_v0:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$]: (fun_app$d(assoc$, fun_app$e(assoc$a, A__questionmark_v0)) = A__questionmark_v0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom14)).
% 18.88/5.98  tff(f_2086, axiom, (![A__questionmark_v0:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$]: ((image$b(A__questionmark_v0, top$) = top$a) <=> (![A__questionmark_v1:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$]: (?[A__questionmark_v2:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$]: (A__questionmark_v1 = fun_app$d(A__questionmark_v0, A__questionmark_v2)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom332)).
% 18.88/5.98  tff(f_2397, axiom, (![A__questionmark_v0:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, A__questionmark_v1:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$]: (inj_on$b(A__questionmark_v0, A__questionmark_v1) => bij_betw$(A__questionmark_v0, A__questionmark_v1, image$b(A__questionmark_v0, A__questionmark_v1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom384)).
% 18.88/5.98  tff(f_120, axiom, (![A__questionmark_v0:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$]: (fun_app$e(assoc$a, fun_app$d(assoc$, A__questionmark_v0)) = A__questionmark_v0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom15)).
% 18.88/5.98  tff(f_2093, axiom, (![A__questionmark_v0:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$]: ((image$(A__questionmark_v0, top$a) = top$) <=> (![A__questionmark_v1:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$]: (?[A__questionmark_v2:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$]: (A__questionmark_v1 = fun_app$e(A__questionmark_v0, A__questionmark_v2)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom333)).
% 18.88/5.98  tff(f_582, axiom, (inv_into$(top$a, assoc$a) = assoc$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom66)).
% 18.88/5.98  tff(f_2488, axiom, (![A__questionmark_v0:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$]: ((image$(A__questionmark_v0, top$a) = top$) => inj_on$b(inv_into$(top$a, A__questionmark_v0), top$))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom399)).
% 18.88/5.98  tff(c_8, plain, (~bij_betw$(assoc$, top$, top$a)), inference(cnfTransformation, [status(thm)], [f_44])).
% 18.88/5.98  tff(c_30, plain, (![A__questionmark_v0_25:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$]: (fun_app$d(assoc$, fun_app$e(assoc$a, A__questionmark_v0_25))=A__questionmark_v0_25)), inference(cnfTransformation, [status(thm)], [f_117])).
% 18.88/5.98  tff(c_3524, plain, (![A__questionmark_v0_2112:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, A__questionmark_v2_2113:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$]: (image$b(A__questionmark_v0_2112, top$)=top$a | fun_app$d(A__questionmark_v0_2112, A__questionmark_v2_2113)!='#skF_141'(A__questionmark_v0_2112))), inference(cnfTransformation, [status(thm)], [f_2086])).
% 18.88/5.98  tff(c_3526, plain, (![A__questionmark_v0_25:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$]: (image$b(assoc$, top$)=top$a | A__questionmark_v0_25!='#skF_141'(assoc$))), inference(superposition, [status(thm), theory('equality')], [c_30, c_3524])).
% 18.88/5.98  tff(c_3528, plain, (![A__questionmark_v0_25:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$]: (A__questionmark_v0_25!='#skF_141'(assoc$))), inference(splitLeft, [status(thm)], [c_3526])).
% 18.88/5.98  tff(c_3533, plain, $false, inference(reflexivity, [status(thm), theory('equality')], [c_3528])).
% 18.88/5.98  tff(c_3534, plain, (image$b(assoc$, top$)=top$a), inference(splitRight, [status(thm)], [c_3526])).
% 18.88/5.98  tff(c_1106, plain, (![A__questionmark_v0_1468:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_a_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_fun$, A__questionmark_v1_1469:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_set$]: (bij_betw$(A__questionmark_v0_1468, A__questionmark_v1_1469, image$b(A__questionmark_v0_1468, A__questionmark_v1_1469)) | ~inj_on$b(A__questionmark_v0_1468, A__questionmark_v1_1469))), inference(cnfTransformation, [status(thm)], [f_2397])).
% 18.88/5.98  tff(c_3538, plain, (bij_betw$(assoc$, top$, top$a) | ~inj_on$b(assoc$, top$)), inference(superposition, [status(thm), theory('equality')], [c_3534, c_1106])).
% 18.88/5.98  tff(c_3541, plain, (~inj_on$b(assoc$, top$)), inference(negUnitSimplification, [status(thm)], [c_8, c_3538])).
% 18.88/5.98  tff(c_32, plain, (![A__questionmark_v0_26:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$]: (fun_app$e(assoc$a, fun_app$d(assoc$, A__questionmark_v0_26))=A__questionmark_v0_26)), inference(cnfTransformation, [status(thm)], [f_120])).
% 18.88/5.98  tff(c_3571, plain, (![A__questionmark_v0_2120:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$, A__questionmark_v2_2121:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun$]: (image$(A__questionmark_v0_2120, top$a)=top$ | fun_app$e(A__questionmark_v0_2120, A__questionmark_v2_2121)!='#skF_143'(A__questionmark_v0_2120))), inference(cnfTransformation, [status(thm)], [f_2093])).
% 18.88/5.98  tff(c_3573, plain, (![A__questionmark_v0_26:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$]: (image$(assoc$a, top$a)=top$ | A__questionmark_v0_26!='#skF_143'(assoc$a))), inference(superposition, [status(thm), theory('equality')], [c_32, c_3571])).
% 18.88/5.98  tff(c_3575, plain, (![A__questionmark_v0_26:A_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun$]: (A__questionmark_v0_26!='#skF_143'(assoc$a))), inference(splitLeft, [status(thm)], [c_3573])).
% 18.88/5.98  tff(c_3580, plain, $false, inference(reflexivity, [status(thm), theory('equality')], [c_3575])).
% 18.88/5.98  tff(c_3581, plain, (image$(assoc$a, top$a)=top$), inference(splitRight, [status(thm)], [c_3573])).
% 18.88/5.98  tff(c_278, plain, (inv_into$(top$a, assoc$a)=assoc$), inference(cnfTransformation, [status(thm)], [f_582])).
% 18.88/5.98  tff(c_3652, plain, (![A__questionmark_v0_2128:A_b_prod_c_prod_ell2_a_b_prod_c_prod_ell2_cblinfun_a_b_c_prod_prod_ell2_a_b_c_prod_prod_ell2_cblinfun_fun$]: (inj_on$b(inv_into$(top$a, A__questionmark_v0_2128), top$) | image$(A__questionmark_v0_2128, top$a)!=top$)), inference(cnfTransformation, [status(thm)], [f_2488])).
% 18.88/5.98  tff(c_3655, plain, (inj_on$b(assoc$, top$) | image$(assoc$a, top$a)!=top$), inference(superposition, [status(thm), theory('equality')], [c_278, c_3652])).
% 18.88/5.98  tff(c_3657, plain, (inj_on$b(assoc$, top$)), inference(demodulation, [status(thm), theory('equality')], [c_3581, c_3655])).
% 18.88/5.98  tff(c_3659, plain, $false, inference(negUnitSimplification, [status(thm)], [c_3541, c_3657])).
% 18.88/5.98  % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------