%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP397_10 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:39:33 AM UTC 2026
% Result : Satisfiable 0.86s 0.62s
% Output : FiniteModel 1.44s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] : ( X = 'fmb_$i_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',type,
'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$1',type,
'fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun$',type,
'A_ell2_a_ell2_cblinfun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun$1',type,
'fmb_A_ell2_a_ell2_cblinfun$_1': 'A_ell2_a_ell2_cblinfun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun$_1' ) ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$1',type,
'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',type,
'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff('declare_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$1',type,
'fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1': 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('finite_domain_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',axiom,
! [X: 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] : ( X = 'fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$1',type,
'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun$',type,
'B_ell2_b_ell2_cblinfun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun$1',type,
'fmb_B_ell2_b_ell2_cblinfun$_1': 'B_ell2_b_ell2_cblinfun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$',type,
'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$1',type,
'fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$_1': 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$_1' ) ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$1',type,
'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$1',type,
'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$1',type,
'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_Nat_set_nat_fun$',type,
'Nat_set_nat_fun$': $tType ).
tff('declare_Nat_set_nat_fun$1',type,
'fmb_Nat_set_nat_fun$_1': 'Nat_set_nat_fun$' ).
tff('finite_domain_Nat_set_nat_fun$',axiom,
! [X: 'Nat_set_nat_fun$'] : ( X = 'fmb_Nat_set_nat_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$',type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$1',type,
'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$_1': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$_1' ) ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$',type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$': $tType ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$1',type,
'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$_1': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$' ).
tff('finite_domain_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$',axiom,
! [X: 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$'] : ( X = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$_1' ) ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$',type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$1',type,
'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_Nat_nat_fun_set$',type,
'Nat_nat_fun_set$': $tType ).
tff('declare_Nat_nat_fun_set$1',type,
'fmb_Nat_nat_fun_set$_1': 'Nat_nat_fun_set$' ).
tff('finite_domain_Nat_nat_fun_set$',axiom,
! [X: 'Nat_nat_fun_set$'] : ( X = 'fmb_Nat_nat_fun_set$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$',type,
'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$1',type,
'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$_1': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$_1' ) ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$1',type,
'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_C_ell2_c_ell2_cblinfun$',type,
'C_ell2_c_ell2_cblinfun$': $tType ).
tff('declare_C_ell2_c_ell2_cblinfun$1',type,
'fmb_C_ell2_c_ell2_cblinfun$_1': 'C_ell2_c_ell2_cblinfun$' ).
tff('finite_domain_C_ell2_c_ell2_cblinfun$',axiom,
! [X: 'C_ell2_c_ell2_cblinfun$'] : ( X = 'fmb_C_ell2_c_ell2_cblinfun$_1' ) ).
tff('declare_C_ell2_c_ell2_cblinfun_bool_fun$',type,
'C_ell2_c_ell2_cblinfun_bool_fun$': $tType ).
tff('declare_C_ell2_c_ell2_cblinfun_bool_fun$1',type,
'fmb_C_ell2_c_ell2_cblinfun_bool_fun$_1': 'C_ell2_c_ell2_cblinfun_bool_fun$' ).
tff('finite_domain_C_ell2_c_ell2_cblinfun_bool_fun$',axiom,
! [X: 'C_ell2_c_ell2_cblinfun_bool_fun$'] : ( X = 'fmb_C_ell2_c_ell2_cblinfun_bool_fun$_1' ) ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$1',type,
'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$1',type,
'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$1',type,
'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_Nat_nat_fun_nat_nat_fun_fun$',type,
'Nat_nat_fun_nat_nat_fun_fun$': $tType ).
tff('declare_Nat_nat_fun_nat_nat_fun_fun$1',type,
'fmb_Nat_nat_fun_nat_nat_fun_fun$_1': 'Nat_nat_fun_nat_nat_fun_fun$' ).
tff('finite_domain_Nat_nat_fun_nat_nat_fun_fun$',axiom,
! [X: 'Nat_nat_fun_nat_nat_fun_fun$'] : ( X = 'fmb_Nat_nat_fun_nat_nat_fun_fun$_1' ) ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$1',type,
'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1': 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_Nat_nat_fun$',type,
'Nat_nat_fun$': $tType ).
tff('declare_Nat_nat_fun$1',type,
'fmb_Nat_nat_fun$_1': 'Nat_nat_fun$' ).
tff('finite_domain_Nat_nat_fun$',axiom,
! [X: 'Nat_nat_fun$'] : ( X = 'fmb_Nat_nat_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',type,
'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$1',type,
'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$',type,
'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$_1': 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$1',type,
'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_Nat$',type,
'Nat$': $tType ).
tff('declare_Nat$1',type,
'fmb_Nat$_1': 'Nat$' ).
tff('finite_domain_Nat$',axiom,
! [X: 'Nat$'] : ( X = 'fmb_Nat$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$',type,
'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$1',type,
'fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$_1': 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_bool_fun$',type,
'A_ell2_a_ell2_cblinfun_bool_fun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_bool_fun$1',type,
'fmb_A_ell2_a_ell2_cblinfun_bool_fun$_1': 'A_ell2_a_ell2_cblinfun_bool_fun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_bool_fun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_bool_fun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_bool_fun$_1' ) ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$1',type,
'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1': 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$1',type,
'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$1',type,
'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',type,
'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$1',type,
'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$1',type,
'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$',type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$_1': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',type,
'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_set$',type,
'B_ell2_b_ell2_cblinfun_set$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_set$1',type,
'fmb_B_ell2_b_ell2_cblinfun_set$_1': 'B_ell2_b_ell2_cblinfun_set$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_set$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_set$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_set$_1' ) ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$1',type,
'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_set$',type,
'A_ell2_a_ell2_cblinfun_set$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_set$1',type,
'fmb_A_ell2_a_ell2_cblinfun_set$_1': 'A_ell2_a_ell2_cblinfun_set$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_set$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_set$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_set$_1' ) ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$1',type,
'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$1',type,
'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$1',type,
'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$1',type,
'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$',type,
'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$1',type,
'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$_1': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$_1' ) ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$',type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$1',type,
'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$',type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$1',type,
'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1': 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',type,
'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$1',type,
'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1': 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$',type,
'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff('declare_C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$1',type,
'fmb_C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$_1': 'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$' ).
tff('finite_domain_C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$',axiom,
! [X: 'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$'] : ( X = 'fmb_C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$',type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$_1': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$_1' ) ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$1',type,
'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1': 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$',type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$': $tType ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$1',type,
'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$_1': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' ).
tff('finite_domain_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$',axiom,
! [X: 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$'] : ( X = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$_1' ) ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$',type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$': $tType ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$1',type,
'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$_1': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$' ).
tff('finite_domain_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$',axiom,
! [X: 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$'] : ( X = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$_1' ) ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$',type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$': $tType ).
tff('declare_A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$1',type,
'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$_1': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$' ).
tff('finite_domain_A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$',axiom,
! [X: 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$'] : ( X = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$_1' ) ).
tff('declare_C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',type,
'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$1',type,
'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1': 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',type,
'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff('declare_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$1',type,
'fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('finite_domain_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',axiom,
! [X: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( X = 'fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$1',type,
'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_bool_fun$',type,
'B_ell2_b_ell2_cblinfun_bool_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_bool_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_bool_fun$_1': 'B_ell2_b_ell2_cblinfun_bool_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_bool_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_bool_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_bool_fun$_1' ) ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$1',type,
'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$',axiom,
! [X: 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_Nat_set$',type,
'Nat_set$': $tType ).
tff('declare_Nat_set$1',type,
'fmb_Nat_set$_1': 'Nat_set$' ).
tff('finite_domain_Nat_set$',axiom,
! [X: 'Nat_set$'] : ( X = 'fmb_Nat_set$_1' ) ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$1',type,
'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',type,
'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff('declare_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$1',type,
'fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1': 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('finite_domain_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',axiom,
! [X: 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( X = 'fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ) ).
tff('declare_C_ell2_c_ell2_cblinfun_set$',type,
'C_ell2_c_ell2_cblinfun_set$': $tType ).
tff('declare_C_ell2_c_ell2_cblinfun_set$1',type,
'fmb_C_ell2_c_ell2_cblinfun_set$_1': 'C_ell2_c_ell2_cblinfun_set$' ).
tff('finite_domain_C_ell2_c_ell2_cblinfun_set$',axiom,
! [X: 'C_ell2_c_ell2_cblinfun_set$'] : ( X = 'fmb_C_ell2_c_ell2_cblinfun_set$_1' ) ).
tff('declare_C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',type,
'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$1',type,
'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1': 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',type,
'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff('declare_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$1',type,
'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1': 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('finite_domain_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$',axiom,
! [X: 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$'] : ( X = 'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ) ).
tff('declare_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$',type,
'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$': $tType ).
tff('declare_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$1',type,
'fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$_1': 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$' ).
tff('finite_domain_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$',axiom,
! [X: 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$'] : ( X = 'fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$_1' ) ).
tff('declare_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',type,
'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff('declare_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$1',type,
'fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1': 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('finite_domain_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',axiom,
! [X: 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( X = 'fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ) ).
tff('declare_top$i',type,
'top$i': 'C_ell2_c_ell2_cblinfun_bool_fun$' ).
tff('top$i_definition',axiom,
'top$i' = 'fmb_C_ell2_c_ell2_cblinfun_bool_fun$_1' ).
tff('declare_top$d',type,
'top$d': 'B_ell2_b_ell2_cblinfun_bool_fun$' ).
tff('top$d_definition',axiom,
'top$d' = 'fmb_B_ell2_b_ell2_cblinfun_bool_fun$_1' ).
tff('declare_f$',type,
'f$': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('f$_definition',axiom,
'f$' = 'fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_top$c',type,
'top$c': 'A_ell2_a_ell2_cblinfun_bool_fun$' ).
tff('top$c_definition',axiom,
'top$c' = 'fmb_A_ell2_a_ell2_cblinfun_bool_fun$_1' ).
tff('declare_id$a',type,
'id$a': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('id$a_definition',axiom,
'id$a' = 'fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_id$g',type,
'id$g': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('id$g_definition',axiom,
'id$g' = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_id$f',type,
'id$f': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('id$f_definition',axiom,
'id$f' = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_id$j',type,
'id$j': 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('id$j_definition',axiom,
'id$j' = 'fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_top$j',type,
'top$j': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$' ).
tff('top$j_definition',axiom,
'top$j' = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$_1' ).
tff('declare_id$c',type,
'id$c': 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$' ).
tff('id$c_definition',axiom,
'id$c' = 'fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$_1' ).
tff('declare_top$a',type,
'top$a': 'B_ell2_b_ell2_cblinfun_set$' ).
tff('top$a_definition',axiom,
'top$a' = 'fmb_B_ell2_b_ell2_cblinfun_set$_1' ).
tff('declare_top$g',type,
'top$g': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$' ).
tff('top$g_definition',axiom,
'top$g' = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$_1' ).
tff('declare_id$e',type,
'id$e': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('id$e_definition',axiom,
'id$e' = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_i$',type,
'i$': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('i$_definition',axiom,
'i$' = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_top$m',type,
'top$m': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' ).
tff('top$m_definition',axiom,
'top$m' = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$_1' ).
tff('declare_top$l',type,
'top$l': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$' ).
tff('top$l_definition',axiom,
'top$l' = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$_1' ).
tff('declare_id$i',type,
'id$i': 'Nat_nat_fun_nat_nat_fun_fun$' ).
tff('id$i_definition',axiom,
'id$i' = 'fmb_Nat_nat_fun_nat_nat_fun_fun$_1' ).
tff('declare_id_cblinfun$',type,
'id_cblinfun$': 'B_ell2_b_ell2_cblinfun$' ).
tff('id_cblinfun$_definition',axiom,
'id_cblinfun$' = 'fmb_B_ell2_b_ell2_cblinfun$_1' ).
tff('declare_top$b',type,
'top$b': 'C_ell2_c_ell2_cblinfun_set$' ).
tff('top$b_definition',axiom,
'top$b' = 'fmb_C_ell2_c_ell2_cblinfun_set$_1' ).
tff('declare_g$',type,
'g$': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('g$_definition',axiom,
'g$' = 'fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_id$b',type,
'id$b': 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$' ).
tff('id$b_definition',axiom,
'id$b' = 'fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$_1' ).
tff('declare_top$f',type,
'top$f': 'Nat_nat_fun_set$' ).
tff('top$f_definition',axiom,
'top$f' = 'fmb_Nat_nat_fun_set$_1' ).
tff('declare_j$',type,
'j$': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('j$_definition',axiom,
'j$' = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_id_cblinfun$a',type,
'id_cblinfun$a': 'A_ell2_a_ell2_cblinfun$' ).
tff('id_cblinfun$a_definition',axiom,
'id_cblinfun$a' = 'fmb_A_ell2_a_ell2_cblinfun$_1' ).
tff('declare_id$d',type,
'id$d': 'Nat_nat_fun$' ).
tff('id$d_definition',axiom,
'id$d' = 'fmb_Nat_nat_fun$_1' ).
tff('declare_top$e',type,
'top$e': 'Nat_set$' ).
tff('top$e_definition',axiom,
'top$e' = 'fmb_Nat_set$_1' ).
tff('declare_top$k',type,
'top$k': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$' ).
tff('top$k_definition',axiom,
'top$k' = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$_1' ).
tff('declare_suc$',type,
'suc$': 'Nat_nat_fun$' ).
tff('suc$_definition',axiom,
'suc$' = 'fmb_Nat_nat_fun$_1' ).
tff('declare_top$h',type,
'top$h': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$' ).
tff('top$h_definition',axiom,
'top$h' = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$_1' ).
tff('declare_id$',type,
'id$': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('id$_definition',axiom,
'id$' = 'fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_top$',type,
'top$': 'A_ell2_a_ell2_cblinfun_set$' ).
tff('top$_definition',axiom,
'top$' = 'fmb_A_ell2_a_ell2_cblinfun_set$_1' ).
tff('declare_id$h',type,
'id$h': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('id$h_definition',axiom,
'id$h' = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$v',type,
'register_tensor$v': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$v',axiom,
'register_tensor$v'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_image$b',type,
'image$b': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun_set$' ).
tff('function_image$b',axiom,
'image$b'('fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') = 'fmb_C_ell2_c_ell2_cblinfun_set$_1' ).
tff('declare_inv_into$n',type,
'inv_into$n': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$n',axiom,
'inv_into$n'('fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$_1','fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1') = 'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$af',type,
'comp$af': ( 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_comp$af',axiom,
'comp$af'('fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1','fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$d',type,
'inv_into$d': ( 'Nat_set$' * 'Nat_nat_fun$' ) > 'Nat_nat_fun$' ).
tff('function_inv_into$d',axiom,
'inv_into$d'('fmb_Nat_set$_1','fmb_Nat_nat_fun$_1') = 'fmb_Nat_nat_fun$_1' ).
tff('declare_image$',type,
'image$': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun_set$' ).
tff('function_image$',axiom,
'image$'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') = 'fmb_C_ell2_c_ell2_cblinfun_set$_1' ).
tff('declare_register_tensor$f',type,
'register_tensor$f': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$f',axiom,
'register_tensor$f'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$',type,
'inv_into$': ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_inv_into$',axiom,
'inv_into$'('fmb_A_ell2_a_ell2_cblinfun_set$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$o',type,
'fun_app$o': ( 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun_set$' ).
tff('function_fun_app$o',axiom,
'fun_app$o'('fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') = 'fmb_A_ell2_a_ell2_cblinfun_set$_1' ).
tff('declare_fun_app$k',type,
'fun_app$k': ( 'Nat_nat_fun_nat_nat_fun_fun$' * 'Nat_nat_fun$' ) > 'Nat_nat_fun$' ).
tff('function_fun_app$k',axiom,
'fun_app$k'('fmb_Nat_nat_fun_nat_nat_fun_fun$_1','fmb_Nat_nat_fun$_1') = 'fmb_Nat_nat_fun$_1' ).
tff('declare_inv_into$b',type,
'inv_into$b': ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_inv_into$b',axiom,
'inv_into$b'('fmb_A_ell2_a_ell2_cblinfun_set$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$b',type,
'fun_app$b': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff('function_fun_app$b',axiom,
'fun_app$b'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun$_1') = 'fmb_C_ell2_c_ell2_cblinfun$_1' ).
tff('declare_register_tensor$h',type,
'register_tensor$h': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$h',axiom,
'register_tensor$h'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_image$h',type,
'image$h': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun_set$' ).
tff('function_image$h',axiom,
'image$h'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') = 'fmb_A_ell2_a_ell2_cblinfun_set$_1' ).
tff('declare_comp$h',type,
'comp$h': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$h',axiom,
'comp$h'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_comp$p',type,
'comp$p': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$p',axiom,
'comp$p'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$g',type,
'inv_into$g': ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_inv_into$g',axiom,
'inv_into$g'('fmb_B_ell2_b_ell2_cblinfun_set$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$f',type,
'inv_into$f': ( 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_inv_into$f',axiom,
'inv_into$f'('fmb_C_ell2_c_ell2_cblinfun_set$_1','fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$e',type,
'register_tensor$e': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$e',axiom,
'register_tensor$e'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$d',type,
'register_tensor$d': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$d',axiom,
'register_tensor$d'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$e',type,
'comp$e': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_comp$e',axiom,
'comp$e'('fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$e',type,
'inv_into$e': ( 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_inv_into$e',axiom,
'inv_into$e'('fmb_C_ell2_c_ell2_cblinfun_set$_1','fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_comp$ae',type,
'comp$ae': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_comp$ae',axiom,
'comp$ae'('fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1','fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$l',type,
'fun_app$l': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff('function_fun_app$l',axiom,
'fun_app$l'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun$_1') = 'fmb_A_ell2_a_ell2_cblinfun$_1' ).
tff('declare_fun_app$t',type,
'fun_app$t': ( 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff('function_fun_app$t',axiom,
'fun_app$t'('fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') = 'fmb_A_ell2_a_ell2_cblinfun$_1' ).
tff('declare_register_tensor$u',type,
'register_tensor$u': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$u',axiom,
'register_tensor$u'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_image$a',type,
'image$a': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun_set$' ).
tff('function_image$a',axiom,
'image$a'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') = 'fmb_C_ell2_c_ell2_cblinfun_set$_1' ).
tff('declare_comp$j',type,
'comp$j': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_comp$j',axiom,
'comp$j'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$h',type,
'fun_app$h': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff('function_fun_app$h',axiom,
'fun_app$h'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun$_1') = 'fmb_A_ell2_a_ell2_cblinfun$_1' ).
tff('declare_register_tensor$m',type,
'register_tensor$m': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$m',axiom,
'register_tensor$m'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_collect$',type,
'collect$': 'C_ell2_c_ell2_cblinfun_bool_fun$' > 'C_ell2_c_ell2_cblinfun_set$' ).
tff('function_collect$',axiom,
'collect$'('fmb_C_ell2_c_ell2_cblinfun_bool_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_set$_1' ).
tff('declare_register_tensor$b',type,
'register_tensor$b': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$b',axiom,
'register_tensor$b'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$a',type,
'register_tensor$a': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$a',axiom,
'register_tensor$a'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$ai',type,
'comp$ai': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('function_comp$ai',axiom,
'comp$ai'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1','fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$g',type,
'comp$g': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$g',axiom,
'comp$g'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$r',type,
'inv_into$r': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$r',axiom,
'inv_into$r'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$_1','fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$f',type,
'fun_app$f': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_fun_app$f',axiom,
'fun_app$f'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$i',type,
'register_tensor$i': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$i',axiom,
'register_tensor$i'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$',type,
'comp$': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$' ).
tff('function_comp$',axiom,
'comp$'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$_1' ).
tff('declare_comp$ag',type,
'comp$ag': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('function_comp$ag',axiom,
'comp$ag'('fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1','fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_image$g',type,
'image$g': ( 'Nat_nat_fun$' * 'Nat_set$' ) > 'Nat_set$' ).
tff('function_image$g',axiom,
'image$g'('fmb_Nat_nat_fun$_1','fmb_Nat_set$_1') = 'fmb_Nat_set$_1' ).
tff('declare_comp$ad',type,
'comp$ad': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('function_comp$ad',axiom,
'comp$ad'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1','fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$n',type,
'comp$n': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_comp$n',axiom,
'comp$n'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_collect$a',type,
'collect$a': 'A_ell2_a_ell2_cblinfun_bool_fun$' > 'A_ell2_a_ell2_cblinfun_set$' ).
tff('function_collect$a',axiom,
'collect$a'('fmb_A_ell2_a_ell2_cblinfun_bool_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_set$_1' ).
tff('declare_comp$q',type,
'comp$q': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$q',axiom,
'comp$q'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$m',type,
'inv_into$m': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$m',axiom,
'inv_into$m'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$_1','fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$s',type,
'register_tensor$s': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$s',axiom,
'register_tensor$s'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_commutant$a',type,
'commutant$a': 'A_ell2_a_ell2_cblinfun_set$' > 'A_ell2_a_ell2_cblinfun_set$' ).
tff('function_commutant$a',axiom,
'commutant$a'('fmb_A_ell2_a_ell2_cblinfun_set$_1') = 'fmb_A_ell2_a_ell2_cblinfun_set$_1' ).
tff('declare_comp$s',type,
'comp$s': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$s',axiom,
'comp$s'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$l',type,
'register_tensor$l': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$l',axiom,
'register_tensor$l'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_commutant$',type,
'commutant$': 'C_ell2_c_ell2_cblinfun_set$' > 'C_ell2_c_ell2_cblinfun_set$' ).
tff('function_commutant$',axiom,
'commutant$'('fmb_C_ell2_c_ell2_cblinfun_set$_1') = 'fmb_C_ell2_c_ell2_cblinfun_set$_1' ).
tff('declare_fun_app$e',type,
'fun_app$e': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff('function_fun_app$e',axiom,
'fun_app$e'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun$_1') = 'fmb_B_ell2_b_ell2_cblinfun$_1' ).
tff('declare_comp$r',type,
'comp$r': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$r',axiom,
'comp$r'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_image$c',type,
'image$c': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$' ).
tff('function_image$c',axiom,
'image$c'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$_1' ).
tff('declare_fun_app$i',type,
'fun_app$i': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_fun_app$i',axiom,
'fun_app$i'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$k',type,
'inv_into$k': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$k',axiom,
'inv_into$k'('fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$_1','fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$a',type,
'comp$a': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$' ).
tff('function_comp$a',axiom,
'comp$a'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$_1' ).
tff('declare_fun_app$s',type,
'fun_app$s': ( 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff('function_fun_app$s',axiom,
'fun_app$s'('fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') = 'fmb_B_ell2_b_ell2_cblinfun$_1' ).
tff('declare_fun_app$c',type,
'fun_app$c': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff('function_fun_app$c',axiom,
'fun_app$c'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun$_1') = 'fmb_C_ell2_c_ell2_cblinfun$_1' ).
tff('declare_comp$aa',type,
'comp$aa': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_comp$aa',axiom,
'comp$aa'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1','fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$w',type,
'comp$w': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$w',axiom,
'comp$w'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$w',type,
'register_tensor$w': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$w',axiom,
'register_tensor$w'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$j',type,
'fun_app$j': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff('function_fun_app$j',axiom,
'fun_app$j'('fmb_Nat_nat_fun$_1','fmb_Nat$_1') = 'fmb_Nat$_1' ).
tff('declare_inv_into$l',type,
'inv_into$l': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$l',axiom,
'inv_into$l'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$_1','fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$',type,
'register_tensor$': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$',axiom,
'register_tensor$'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$j',type,
'inv_into$j': ( 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$j',axiom,
'inv_into$j'('fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$_1','fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$t',type,
'register_tensor$t': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$t',axiom,
'register_tensor$t'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_image$i',type,
'image$i': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun_set$' ).
tff('function_image$i',axiom,
'image$i'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') = 'fmb_B_ell2_b_ell2_cblinfun_set$_1' ).
tff('declare_collect$b',type,
'collect$b': 'B_ell2_b_ell2_cblinfun_bool_fun$' > 'B_ell2_b_ell2_cblinfun_set$' ).
tff('function_collect$b',axiom,
'collect$b'('fmb_B_ell2_b_ell2_cblinfun_bool_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_set$_1' ).
tff('declare_comp$o',type,
'comp$o': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$o',axiom,
'comp$o'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$q',type,
'register_tensor$q': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$q',axiom,
'register_tensor$q'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$aj',type,
'comp$aj': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('function_comp$aj',axiom,
'comp$aj'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1','fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$i',type,
'inv_into$i': ( 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_inv_into$i',axiom,
'inv_into$i'('fmb_C_ell2_c_ell2_cblinfun_set$_1','fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_commutant$b',type,
'commutant$b': 'B_ell2_b_ell2_cblinfun_set$' > 'B_ell2_b_ell2_cblinfun_set$' ).
tff('function_commutant$b',axiom,
'commutant$b'('fmb_B_ell2_b_ell2_cblinfun_set$_1') = 'fmb_B_ell2_b_ell2_cblinfun_set$_1' ).
tff('declare_inv_into$q',type,
'inv_into$q': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$q',axiom,
'inv_into$q'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$_1','fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1') = 'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$i',type,
'comp$i': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$i',axiom,
'comp$i'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_image$f',type,
'image$f': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun_set$' ).
tff('function_image$f',axiom,
'image$f'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') = 'fmb_B_ell2_b_ell2_cblinfun_set$_1' ).
tff('declare_fun_app$p',type,
'fun_app$p': ( 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun_set$' ).
tff('function_fun_app$p',axiom,
'fun_app$p'('fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') = 'fmb_B_ell2_b_ell2_cblinfun_set$_1' ).
tff('declare_comp$v',type,
'comp$v': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$v',axiom,
'comp$v'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$o',type,
'inv_into$o': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$o',axiom,
'inv_into$o'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$_1','fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1') = 'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$m',type,
'fun_app$m': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff('function_fun_app$m',axiom,
'fun_app$m'('fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun$_1') = 'fmb_C_ell2_c_ell2_cblinfun$_1' ).
tff('declare_register_tensor$z',type,
'register_tensor$z': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$z',axiom,
'register_tensor$z'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$ac',type,
'comp$ac': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('function_comp$ac',axiom,
'comp$ac'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1','fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$k',type,
'register_tensor$k': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$k',axiom,
'register_tensor$k'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$c',type,
'inv_into$c': ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_inv_into$c',axiom,
'inv_into$c'('fmb_B_ell2_b_ell2_cblinfun_set$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_comp$ab',type,
'comp$ab': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff('function_comp$ab',axiom,
'comp$ab'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1','fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$ab',type,
'register_tensor$ab': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$ab',axiom,
'register_tensor$ab'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$l',type,
'comp$l': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$l',axiom,
'comp$l'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_comp$m',type,
'comp$m': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$m',axiom,
'comp$m'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_uu$',type,
'uu$': 'C_ell2_c_ell2_cblinfun_set$' > 'C_ell2_c_ell2_cblinfun_bool_fun$' ).
tff('function_uu$',axiom,
'uu$'('fmb_C_ell2_c_ell2_cblinfun_set$_1') = 'fmb_C_ell2_c_ell2_cblinfun_bool_fun$_1' ).
tff('declare_register_tensor$j',type,
'register_tensor$j': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$j',axiom,
'register_tensor$j'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$d',type,
'fun_app$d': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff('function_fun_app$d',axiom,
'fun_app$d'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun$_1') = 'fmb_A_ell2_a_ell2_cblinfun$_1' ).
tff('declare_register_tensor$o',type,
'register_tensor$o': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$o',axiom,
'register_tensor$o'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$g',type,
'fun_app$g': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff('function_fun_app$g',axiom,
'fun_app$g'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun$_1') = 'fmb_B_ell2_b_ell2_cblinfun$_1' ).
tff('declare_register_tensor$c',type,
'register_tensor$c': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$c',axiom,
'register_tensor$c'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$y',type,
'register_tensor$y': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$y',axiom,
'register_tensor$y'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$ad',type,
'register_tensor$ad': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$ad',axiom,
'register_tensor$ad'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$ac',type,
'register_tensor$ac': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$ac',axiom,
'register_tensor$ac'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$r',type,
'register_tensor$r': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$r',axiom,
'register_tensor$r'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$u',type,
'fun_app$u': ( 'Nat_set_nat_fun$' * 'Nat_set$' ) > 'Nat$' ).
tff('function_fun_app$u',axiom,
'fun_app$u'('fmb_Nat_set_nat_fun$_1','fmb_Nat_set$_1') = 'fmb_Nat$_1' ).
tff('declare_comp$b',type,
'comp$b': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$' ).
tff('function_comp$b',axiom,
'comp$b'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$_1' ).
tff('declare_register_tensor$ae',type,
'register_tensor$ae': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$ae',axiom,
'register_tensor$ae'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_image$e',type,
'image$e': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun_set$' ).
tff('function_image$e',axiom,
'image$e'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') = 'fmb_A_ell2_a_ell2_cblinfun_set$_1' ).
tff('declare_fun_app$v',type,
'fun_app$v': ( 'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff('function_fun_app$v',axiom,
'fun_app$v'('fmb_C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') = 'fmb_C_ell2_c_ell2_cblinfun$_1' ).
tff('declare_comp$y',type,
'comp$y': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_comp$y',axiom,
'comp$y'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_comp$d',type,
'comp$d': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_comp$d',axiom,
'comp$d'('fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_comp$x',type,
'comp$x': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$x',axiom,
'comp$x'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_comp$u',type,
'comp$u': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$u',axiom,
'comp$u'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$h',type,
'inv_into$h': ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_inv_into$h',axiom,
'inv_into$h'('fmb_A_ell2_a_ell2_cblinfun_set$_1','fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$a',type,
'fun_app$a': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_fun_app$a',axiom,
'fun_app$a'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$p',type,
'register_tensor$p': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$p',axiom,
'register_tensor$p'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$t',type,
'comp$t': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff('function_comp$t',axiom,
'comp$t'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1' ).
tff('declare_comp$k',type,
'comp$k': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_comp$k',axiom,
'comp$k'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$p',type,
'inv_into$p': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('function_inv_into$p',axiom,
'inv_into$p'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$_1','fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1') = 'fmb_A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$n',type,
'register_tensor$n': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$n',axiom,
'register_tensor$n'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$g',type,
'register_tensor$g': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$g',axiom,
'register_tensor$g'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$z',type,
'comp$z': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff('function_comp$z',axiom,
'comp$z'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1' ).
tff('declare_comp$ah',type,
'comp$ah': ( 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff('function_comp$ah',axiom,
'comp$ah'('fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1','fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1') = 'fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_register_tensor$x',type,
'register_tensor$x': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$x',axiom,
'register_tensor$x'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') = 'fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$_1' ).
tff('declare_fun_app$n',type,
'fun_app$n': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff('function_fun_app$n',axiom,
'fun_app$n'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun$_1') = 'fmb_B_ell2_b_ell2_cblinfun$_1' ).
tff('declare_comp$c',type,
'comp$c': 'Nat_nat_fun$' > 'Nat_nat_fun_nat_nat_fun_fun$' ).
tff('function_comp$c',axiom,
'comp$c'('fmb_Nat_nat_fun$_1') = 'fmb_Nat_nat_fun_nat_nat_fun_fun$_1' ).
tff('declare_register_tensor$aa',type,
'register_tensor$aa': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff('function_register_tensor$aa',axiom,
'register_tensor$aa'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$_1' ).
tff('declare_comp$f',type,
'comp$f': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_comp$f',axiom,
'comp$f'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_inv_into$a',type,
'inv_into$a': ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff('function_inv_into$a',axiom,
'inv_into$a'('fmb_B_ell2_b_ell2_cblinfun_set$_1','fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') = 'fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1' ).
tff('declare_image$d',type,
'image$d': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$' ).
tff('function_image$d',axiom,
'image$d'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') = 'fmb_B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$_1' ).
tff('declare_register$k',type,
'register$k': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$k',axiom,
'register$k'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1') ).
tff('declare_register$j',type,
'register$j': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$j',axiom,
'register$j'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') ).
tff('declare_clinear$g',type,
'clinear$g': 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$g',axiom,
'clinear$g'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_fun_app$q',type,
'fun_app$q': ( 'A_ell2_a_ell2_cblinfun_bool_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > $o ).
tff('predicate_fun_app$q',axiom,
'fun_app$q'('fmb_A_ell2_a_ell2_cblinfun_bool_fun$_1','fmb_A_ell2_a_ell2_cblinfun$_1') ).
tff('declare_inj_on$',type,
'inj_on$': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$',axiom,
'inj_on$'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') ).
tff('declare_register$n',type,
'register$n': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$n',axiom,
'register$n'('fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$d',type,
'inj_on$d': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$d',axiom,
'inj_on$d'('fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') ).
tff('declare_member$a',type,
'member$a': ( 'A_ell2_a_ell2_cblinfun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff('predicate_member$a',axiom,
'member$a'('fmb_A_ell2_a_ell2_cblinfun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') ).
tff('declare_iso_register$h',type,
'iso_register$h': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$h',axiom,
'iso_register$h'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$_1') ).
tff('declare_clinear$b',type,
'clinear$b': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$b',axiom,
'clinear$b'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_iso_register$d',type,
'iso_register$d': 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$d',axiom,
~ 'iso_register$d'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_iso_register$',type,
'iso_register$': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$',axiom,
'iso_register$'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$a',type,
'inj_on$a': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$a',axiom,
'inj_on$a'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') ).
tff('declare_inj_on$m',type,
'inj_on$m': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$m',axiom,
'inj_on$m'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') ).
tff('declare_inj_on$j',type,
'inj_on$j': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$' ) > $o ).
tff('predicate_inj_on$j',axiom,
'inj_on$j'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$_1') ).
tff('declare_member$b',type,
'member$b': ( 'B_ell2_b_ell2_cblinfun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff('predicate_member$b',axiom,
'member$b'('fmb_B_ell2_b_ell2_cblinfun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') ).
tff('declare_register$q',type,
'register$q': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$q',axiom,
'register$q'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$e',type,
'inj_on$e': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$e',axiom,
'inj_on$e'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') ).
tff('declare_iso_register$f',type,
'iso_register$f': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$f',axiom,
'iso_register$f'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_clinear$d',type,
'clinear$d': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$d',axiom,
'clinear$d'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_iso_register$c',type,
'iso_register$c': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$c',axiom,
~ 'iso_register$c'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_member$c',type,
'member$c': ( 'Nat$' * 'Nat_set$' ) > $o ).
tff('predicate_member$c',axiom,
~ 'member$c'('fmb_Nat$_1','fmb_Nat_set$_1') ).
tff('declare_iso_register$e',type,
'iso_register$e': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$e',axiom,
'iso_register$e'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_register$b',type,
'register$b': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$b',axiom,
'register$b'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_clinear$a',type,
'clinear$a': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$a',axiom,
'clinear$a'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_bijection$b',type,
'bijection$b': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_bijection$b',axiom,
~ 'bijection$b'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_register$p',type,
'register$p': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$p',axiom,
'register$p'('fmb_A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1') ).
tff('declare_register$f',type,
'register$f': 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$f',axiom,
~ 'register$f'('fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$b',type,
'inj_on$b': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$b',axiom,
'inj_on$b'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') ).
tff('declare_iso_register$b',type,
'iso_register$b': 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$b',axiom,
~ 'iso_register$b'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_register$r',type,
'register$r': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$r',axiom,
'register$r'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$_1') ).
tff('declare_register$h',type,
'register$h': 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$h',axiom,
~ 'register$h'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_iso_register$a',type,
'iso_register$a': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$a',axiom,
~ 'iso_register$a'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_register$c',type,
'register$c': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$c',axiom,
'register$c'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_bijection$',type,
'bijection$': 'Nat_nat_fun$' > $o ).
tff('predicate_bijection$',axiom,
~ 'bijection$'('fmb_Nat_nat_fun$_1') ).
tff('declare_inj_on$k',type,
'inj_on$k': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$' ) > $o ).
tff('predicate_inj_on$k',axiom,
'inj_on$k'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$_1') ).
tff('declare_register$',type,
'register$': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$',axiom,
'register$'('fmb_B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_register$l',type,
'register$l': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$l',axiom,
'register$l'('fmb_B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$_1') ).
tff('declare_clinear$c',type,
'clinear$c': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$c',axiom,
'clinear$c'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_register$m',type,
'register$m': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$m',axiom,
'register$m'('fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$h',type,
'inj_on$h': ( 'Nat_nat_fun_nat_nat_fun_fun$' * 'Nat_nat_fun_set$' ) > $o ).
tff('predicate_inj_on$h',axiom,
'inj_on$h'('fmb_Nat_nat_fun_nat_nat_fun_fun$_1','fmb_Nat_nat_fun_set$_1') ).
tff('declare_iso_register$g',type,
'iso_register$g': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_iso_register$g',axiom,
'iso_register$g'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_register$d',type,
'register$d': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$d',axiom,
'register$d'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_clinear$',type,
'clinear$': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$',axiom,
'clinear$'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_bijection$a',type,
'bijection$a': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_bijection$a',axiom,
~ 'bijection$a'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_member$',type,
'member$': ( 'C_ell2_c_ell2_cblinfun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff('predicate_member$',axiom,
'member$'('fmb_C_ell2_c_ell2_cblinfun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') ).
tff('declare_clinear$f',type,
'clinear$f': 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$f',axiom,
~ 'clinear$f'('fmb_C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$c',type,
'inj_on$c': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$c',axiom,
'inj_on$c'('fmb_B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_set$_1') ).
tff('declare_inj_on$f',type,
'inj_on$f': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$f',axiom,
'inj_on$f'('fmb_A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1','fmb_A_ell2_a_ell2_cblinfun_set$_1') ).
tff('declare_register$o',type,
'register$o': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$o',axiom,
'register$o'('fmb_A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$_1') ).
tff('declare_fun_app$r',type,
'fun_app$r': ( 'B_ell2_b_ell2_cblinfun_bool_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > $o ).
tff('predicate_fun_app$r',axiom,
'fun_app$r'('fmb_B_ell2_b_ell2_cblinfun_bool_fun$_1','fmb_B_ell2_b_ell2_cblinfun$_1') ).
tff('declare_register$g',type,
'register$g': 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$g',axiom,
~ 'register$g'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$g',type,
'inj_on$g': ( 'Nat_nat_fun$' * 'Nat_set$' ) > $o ).
tff('predicate_inj_on$g',axiom,
'inj_on$g'('fmb_Nat_nat_fun$_1','fmb_Nat_set$_1') ).
tff('declare_inj_on$i',type,
'inj_on$i': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$' ) > $o ).
tff('predicate_inj_on$i',axiom,
'inj_on$i'('fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$_1','fmb_B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$_1') ).
tff('declare_register$i',type,
'register$i': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$i',axiom,
'register$i'('fmb_B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$_1') ).
tff('declare_clinear$h',type,
'clinear$h': 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$h',axiom,
'clinear$h'('fmb_C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$_1') ).
tff('declare_register$a',type,
'register$a': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$a',axiom,
'register$a'('fmb_A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$_1') ).
tff('declare_inj_on$l',type,
'inj_on$l': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff('predicate_inj_on$l',axiom,
'inj_on$l'('fmb_C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1','fmb_C_ell2_c_ell2_cblinfun_set$_1') ).
tff('declare_clinear$e',type,
'clinear$e': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_clinear$e',axiom,
'clinear$e'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
tff('declare_fun_app$',type,
'fun_app$': ( 'C_ell2_c_ell2_cblinfun_bool_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > $o ).
tff('predicate_fun_app$',axiom,
'fun_app$'('fmb_C_ell2_c_ell2_cblinfun_bool_fun$_1','fmb_C_ell2_c_ell2_cblinfun$_1') ).
tff('declare_register$e',type,
'register$e': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff('predicate_register$e',axiom,
'register$e'('fmb_A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$_1') ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP397_10 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n018.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 12:59:08 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/0.62 % (2330459)Will run a generic schedule for satisfiability detection.
% 0.86/0.62 % (2330484)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2377038001:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.86/0.62 % (2330479)% WARNING: option uhcvi not known.
% 0.86/0.62 % (2330481)dis+10_1_sil=32000:sp=arity:random_seed=4092655789:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.86/0.62 % (2330480)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4050537485:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.86/0.62 % (2330477)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=485981451_2999 on theBenchmark for (2999ds/0Mi)
% 0.86/0.62 % (2330479)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2191215882:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.86/0.62 % (2330482)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3433214415:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.86/0.62 % (2330483)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2432231483:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.86/0.62 % (2330484)Instruction limit reached!
% 0.86/0.62 % (2330484)------------------------------
% 0.86/0.62 % (2330484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.86/0.62 % (2330484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.86/0.62 % (2330484)CaDiCaL version: 2.1.3
% 0.86/0.62 % (2330484)Termination reason: Instruction limit
% 0.86/0.62 % (2330484)Termination phase: Saturation
% 0.86/0.62 % (2330484)Time elapsed: 0.058 s
% 0.86/0.62 % (2330484)Peak memory usage: 16 MB
% 0.86/0.62 % (2330484)Instructions burned: 161 (million)
% 0.86/0.62 % (2330520)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=484367734:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 0.86/0.62 % (2330481)Instruction limit reached!
% 0.86/0.62 % (2330481)------------------------------
% 0.86/0.62 % (2330481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.86/0.62 % (2330481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.86/0.62 % (2330481)CaDiCaL version: 2.1.3
% 0.86/0.62 % (2330481)Termination reason: Instruction limit
% 0.86/0.62 % (2330481)Termination phase: Saturation
% 0.86/0.62 % (2330481)Time elapsed: 0.065 s
% 0.86/0.62 % (2330481)Peak memory usage: 14 MB
% 0.86/0.62 % (2330481)Instructions burned: 105 (million)
% 0.86/0.62 % (2330482)Instruction limit reached!
% 0.86/0.62 % (2330482)------------------------------
% 0.86/0.62 % (2330482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.86/0.62 % (2330482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.86/0.62 % (2330482)CaDiCaL version: 2.1.3
% 0.86/0.62 % (2330482)Termination reason: Instruction limit
% 0.86/0.62 % (2330482)Termination phase: Saturation
% 0.86/0.62 % (2330482)Time elapsed: 0.066 s
% 0.86/0.62 % (2330482)Peak memory usage: 14 MB
% 0.86/0.62 % (2330482)Instructions burned: 117 (million)
% 0.86/0.62 % (2330483)Instruction limit reached!
% 0.86/0.62 % (2330483)------------------------------
% 0.86/0.62 % (2330483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.86/0.62 % (2330483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.86/0.62 % (2330483)CaDiCaL version: 2.1.3
% 0.86/0.62 % (2330483)Termination reason: Instruction limit
% 0.86/0.62 % (2330483)Termination phase: Saturation
% 0.86/0.62 % (2330483)Time elapsed: 0.079 s
% 0.86/0.62 % (2330483)Peak memory usage: 15 MB
% 0.86/0.62 % (2330483)Instructions burned: 131 (million)
% 0.86/0.62 % (2330522)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1515906420:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.86/0.62 % (2330523)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2569235715:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.86/0.62 % (2330524)ott-21_1_sil=16000:fs=off:random_seed=1672783314:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.86/0.62 % TRYING [1]
% 0.86/0.62 % Finite Model Found!
% 0.86/0.62 % SZS status Satisfiable for theBenchmark
% 0.86/0.62 % (2330520) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2330459-2330520"...
% 0.86/0.62 % (2330520)...printing done.
% 0.86/0.62 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.44/0.63 % (2330520)------------------------------
% 1.44/0.63 % (2330520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.63 % (2330520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.63 % (2330520)CaDiCaL version: 2.1.3
% 1.44/0.63 % (2330520)Termination reason: Satisfiable
% 1.44/0.63 % (2330520)Time elapsed: 0.090 s
% 1.44/0.63 % (2330520)Peak memory usage: 18 MB
% 1.44/0.63 % (2330520)Instructions burned: 373 (million)
% 1.44/0.63 % (2330459)Success in time 0.21 s
% 1.44/0.63 % Vampire exiting
%------------------------------------------------------------------------------