Beagle---0.9.52.THM-CRf.s

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

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

% Result   : Theorem 18.39s 6.74s
% Output   : CNFRefutation 18.39s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : ITP001_1 : TPTP v9.0.0. Released v8.1.0.
% 0.06/0.13  % Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34  % Computer : n011.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Tue Apr  8 02:24:03 EDT 2025
% 0.13/0.34  % CPUTime  : 
% 18.39/6.74  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.39/6.74  
% 18.39/6.74  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.39/6.76  %$ less_eq$a > less_eq$ > less$ > equivalent_registers$y > equivalent_registers$x > equivalent_registers$w > equivalent_registers$v > equivalent_registers$u > equivalent_registers$t > equivalent_registers$s > equivalent_registers$r > equivalent_registers$q > equivalent_registers$p > equivalent_registers$o > equivalent_registers$n > equivalent_registers$m > equivalent_registers$l > equivalent_registers$k > equivalent_registers$j > equivalent_registers$i > equivalent_registers$h > equivalent_registers$g > equivalent_registers$f > equivalent_registers$e > equivalent_registers$d > equivalent_registers$c > equivalent_registers$b > equivalent_registers$a > equivalent_registers$ > complements$v > complements$u > complements$t > complements$s > complements$r > complements$q > complements$p > complements$o > complements$n > complements$m > complements$l > complements$k > complements$j > complements$i > complements$h > complements$g > complements$f > complements$e > complements$d > complements$c > complements$b > complements$a > complements$ > compatible$d > compatible$c > compatible$b > compatible$a > compatible$ > unitary$c > unitary$b > unitary$a > unitary$ > regular_register$h > regular_register$g > regular_register$f > regular_register$e > regular_register$d > regular_register$c > regular_register$b > regular_register$a > regular_register$ > register$r > register$q > register$p > register$o > register$n > register$m > register$l > register$k > register$j > register$i > register$h > register$g > register$f > register$e > register$d > register$c > register$b > register$a > register$ > iso_register$u > iso_register$t > iso_register$s > iso_register$r > iso_register$q > iso_register$p > iso_register$o > iso_register$n > iso_register$m > iso_register$l > iso_register$k > iso_register$j > iso_register$i > iso_register$h > iso_register$g > iso_register$f > iso_register$e > iso_register$d > iso_register$c > iso_register$b > iso_register$a > iso_register$ > is_unit_register$j > is_unit_register$i > is_unit_register$h > is_unit_register$g > is_unit_register$f > is_unit_register$e > is_unit_register$d > is_unit_register$c > is_unit_register$b > is_unit_register$a > is_unit_register$ > is_Proj$a > is_Proj$ > clinear$ > antilinear_axioms$ > register_pair$g > register_pair$f > register_pair$e > times$a > tensor_op$v > tensor_op$u > tensor_op$t > tensor_op$s > tensor_op$r > tensor_op$q > tensor_op$p > tensor_op$o > tensor_op$n > tensor_op$m > tensor_op$l > tensor_op$k > tensor_op$j > tensor_op$i > tensor_op$h > tensor_op$g > tensor_op$f > tensor_op$d > tensor_op$c > tensor_op$b > tensor_op$a > tensor_op$ > tensor_ell2$d > tensor_ell2$c > tensor_ell2$b > tensor_ell2$a > tensor_ell2$ > scaleC$j > scaleC$i > scaleC$f > scaleC$c > scale$ > register_tensor$h > register_tensor$g > register_tensor$f > register_tensor$e > register_tensor$d > register_tensor$c > register_tensor$b > register_tensor$a > register_tensor$ > register_pair$h > register_pair$d > register_pair$c > register_pair$b > register_pair$a > register_pair$ > pair$e > pair$d > pair$c > pair$b > pair$a > pair$ > fun_app$z > fun_app$y > fun_app$x > fun_app$w > fun_app$v > fun_app$u > fun_app$t > fun_app$s > fun_app$r > fun_app$q > fun_app$p > fun_app$o > fun_app$n > fun_app$m > fun_app$l > fun_app$k > fun_app$j > fun_app$i > fun_app$h > fun_app$g > fun_app$f > fun_app$e > fun_app$d > fun_app$c > fun_app$b > fun_app$ak > fun_app$aj > fun_app$ai > fun_app$ah > fun_app$ag > fun_app$af > fun_app$ae > fun_app$ad > fun_app$ac > fun_app$ab > fun_app$aa > fun_app$a > fun_app$ > comp$z > comp$y > comp$x > comp$w > comp$v > comp$u > comp$t > comp$s > comp$r > comp$p > comp$o > comp$n > comp$m > comp$l > comp$k > comp$j > comp$i > comp$h > comp$g > comp$f > comp$e > comp$d > comp$c > comp$b > comp$aw > comp$av > comp$au > comp$at > comp$as > comp$ar > comp$aq > comp$ap > comp$ao > comp$an > comp$am > comp$al > comp$ak > comp$aj > comp$ai > comp$ah > comp$ag > comp$af > comp$ae > comp$ad > comp$ac > comp$ab > comp$aa > comp$ > cinner$a > cinner$ > cblinfun_compose$i > cblinfun_compose$h > cblinfun_compose$g > cblinfun_compose$f > cblinfun_compose$d > cblinfun_compose$c > cblinfun_compose$b > cblinfun_apply$f > cblinfun_apply$e > cblinfun_apply$d > cblinfun_apply$c > cblinfun_apply$b > cblinfun_apply$a > butterfly$x > butterfly$w > butterfly$v > butterfly$u > butterfly$t > butterfly$s > butterfly$r > butterfly$q > butterfly$p > butterfly$o > butterfly$n > butterfly$m > butterfly$l > butterfly$k > butterfly$j > butterfly$i > butterfly$h > butterfly$g > butterfly$f > butterfly$e > butterfly$d > butterfly$c > butterfly$b > butterfly$a > butterfly$ > #nlpp > vector_to_cblinfun$a > vector_to_cblinfun$ > uu$ > times$ > tensor_op$e > scaleC$g > scaleC$e > scaleC$d > scaleC$b > scaleC$a > sandwich$f > sandwich$e > sandwich$d > sandwich$c > sandwich$b > sandwich$a > sandwich$ > one_dim_iso$f > one_dim_iso$c > one_dim_iso$b > one_dim_iso$a > one_dim_iso$ > of_complex$ > norm$f > norm$e > norm$d > norm$c > norm$b > norm$a > norm$ > minus$ > ln$ > ket$g > ket$f > ket$e > ket$d > ket$c > ket$b > ket$a > ket$ > empty_var$c > complement$d > complement$c > complement$b > complement$a > complement$ > comp$q > comp$a > cinner$b > cblinfun_scaleC_right$ > cblinfun_scaleC_left$ > cblinfun_mult_right$ > cblinfun_mult_left$ > cblinfun_compose$e > cblinfun_compose$a > cblinfun_compose$ > cblinfun_cinner_right$ > cblinfun_apply$ > arcosh$ > adj$h > adj$g > adj$f > adj$d > adj$c > adj$b > zero$h > zero$g > zero$f > zero$e > zero$d > zero$c > zero$b > zero$a > zero$ > unit_register$c > unit_register$b > unit_register$a > unit_register$ > tltrue > tlfalse > swap$a > swap$ > snd$a > snd$ > scaleC$h > scaleC$ > one_dim_iso$e > one_dim_iso$d > one$a > one$ > of_complex$a > id_cblinfun$d > id_cblinfun$c > id_cblinfun$b > id_cblinfun$a > id_cblinfun$ > id$i > id$h > id$g > id$f > id$e > id$d > id$c > id$b > id$a > id$ > fst$a > fst$ > f$ > empty_var$b > empty_var$a > empty_var$ > default$e > default$d > default$c > default$b > default$a > default$ > cnj$ > assoc_ell2$c > assoc_ell2$b > assoc_ell2$a > assoc_ell2$ > adj$e > adj$a > adj$ > a$ > #skF_73 > #skF_44 > #skF_55 > #skF_38 > #skF_76 > #skF_58 > #skF_6 > #skF_1 > #skF_17 > #skF_91 > #skF_66 > #skF_9 > #skF_45 > #skF_36 > #skF_14 > #skF_67 > #skF_25 > #skF_87 > #skF_61 > #skF_35 > #skF_28 > #skF_96 > #skF_33 > #skF_2 > #skF_29 > #skF_19 > #skF_74 > #skF_24 > #skF_92 > #skF_65 > #skF_77 > #skF_75 > #skF_7 > #skF_56 > #skF_83 > #skF_86 > #skF_13 > #skF_88 > #skF_89 > #skF_27 > #skF_30 > #skF_54 > #skF_32 > #skF_12 > #skF_21 > #skF_41 > #skF_46 > #skF_23 > #skF_10 > #skF_53 > #skF_94 > #skF_63 > #skF_69 > #skF_39 > #skF_5 > #skF_81 > #skF_85 > #skF_59 > #skF_47 > #skF_79 > #skF_4 > #skF_50 > #skF_18 > #skF_31 > #skF_43 > #skF_11 > #skF_78 > #skF_64 > #skF_16 > #skF_52 > #skF_49 > #skF_90 > #skF_72 > #skF_34 > #skF_20 > #skF_26 > #skF_93 > #skF_22 > #skF_40 > #skF_62 > #skF_8 > #skF_3 > #skF_51 > #skF_48 > #skF_70 > #skF_84 > #skF_80 > #skF_37 > #skF_15 > #skF_57 > #skF_82 > #skF_71 > #skF_68 > #skF_95 > #skF_60 > #skF_42
% 18.39/6.76  
% 18.39/6.76  %Foreground sorts:
% 18.39/6.76  tff(Complex_a_ell2_a_ell2_cblinfun_fun$, type, Complex_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun$, type, A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A$, type, A$: $tType ).
% 18.39/6.76  tff(A_b_prod_ell2_b_a_prod_ell2_cblinfun$, type, A_b_prod_ell2_b_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$, type, A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$, type, Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_prod$, type, A_a_prod$: $tType ).
% 18.39/6.76  tff(A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$, type, A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_b_complement_domain_ell2_a_a_b_complement_domain_prod_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_a_b_complement_domain_prod_b_complement_domain_ell2_a_a_b_complement_domain_prod_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun$, type, A_ell2_a_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(Complex_complex_complex_prod_complex_complex_prod_fun_fun$, type, Complex_complex_complex_prod_complex_complex_prod_fun_fun$: $tType ).
% 18.39/6.76  tff(A_b_prod_ell2_a_a_prod_ell2_cblinfun$, type, A_b_prod_ell2_a_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(Complex_complex_cblinfun$, type, Complex_complex_cblinfun$: $tType ).
% 18.39/6.76  tff(C_ell2_c_ell2_cblinfun_complex_fun$, type, C_ell2_c_ell2_cblinfun_complex_fun$: $tType ).
% 18.39/6.76  tff(Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$, type, Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_ell2_complex_cblinfun$, type, B_ell2_complex_cblinfun$: $tType ).
% 18.39/6.76  tff(A_a_prod_ell2_a_b_prod_ell2_cblinfun$, type, A_a_prod_ell2_a_b_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$, type, C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod$, type, A_a_b_complement_domain_prod$: $tType ).
% 18.39/6.76  tff(A_b_prod_ell2$, type, A_b_prod_ell2$: $tType ).
% 18.39/6.76  tff(A_ell2_b_ell2_cblinfun$, type, A_ell2_b_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$, type, B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(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 ).
% 18.39/6.76  tff(A_b_complement_domain_ell2$, type, A_b_complement_domain_ell2$: $tType ).
% 18.39/6.76  tff(B$, type, B$: $tType ).
% 18.39/6.76  tff(Complex_complex_fun$, type, Complex_complex_fun$: $tType ).
% 18.39/6.76  tff(tlbool, type, tlbool: $tType ).
% 18.39/6.76  tff(B_a_a_b_complement_domain_prod_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$, type, B_a_a_b_complement_domain_prod_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(Unit_ell2_unit_ell2_cblinfun$, type, Unit_ell2_unit_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_b_prod_ell2_b_b_prod_ell2_cblinfun$, type, A_b_prod_ell2_b_b_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_b_prod_ell2_a_b_prod_ell2_cblinfun$, type, A_b_prod_ell2_a_b_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_ell2_complex_cblinfun$, type, A_ell2_complex_cblinfun$: $tType ).
% 18.39/6.76  tff(B_a_prod$, type, B_a_prod$: $tType ).
% 18.39/6.76  tff(Complex_complex_fun_complex_complex_fun_fun$, type, Complex_complex_fun_complex_complex_fun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$, type, A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Complex$, type, Complex$: $tType ).
% 18.39/6.76  tff(A_a_prod_ell2_a_a_prod_ell2_cblinfun$, type, A_a_prod_ell2_a_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Complex_complex_prod_complex_complex_prod_fun$, type, Complex_complex_prod_complex_complex_prod_fun$: $tType ).
% 18.39/6.76  tff(B_b_prod$, type, B_b_prod$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_complex_fun$, type, A_ell2_a_ell2_cblinfun_complex_fun$: $tType ).
% 18.39/6.76  tff(B_b_b_complement_domain_prod_ell2_b_b_b_complement_domain_prod_ell2_cblinfun$, type, B_b_b_complement_domain_prod_ell2_b_b_b_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_b_prod_ell2_b_b_prod_ell2_cblinfun$, type, B_b_prod_ell2_b_b_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$, type, A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_prod_ell2_b_b_prod_ell2_cblinfun$, type, A_a_prod_ell2_b_b_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_ell2$, type, B_ell2$: $tType ).
% 18.39/6.76  tff(B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$, type, B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_ell2$, type, A_ell2$: $tType ).
% 18.39/6.76  tff(Complex_complex_prod$, type, Complex_complex_prod$: $tType ).
% 18.39/6.76  tff(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 ).
% 18.39/6.76  tff(B_b_a_complement_domain_prod_ell2_b_b_a_complement_domain_prod_ell2_cblinfun$, type, B_b_a_complement_domain_prod_ell2_b_b_a_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(Complex_complex_complex_fun_fun$, type, Complex_complex_complex_fun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_ell2$, type, A_a_b_complement_domain_prod_ell2$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$, type, A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_ell2_b_ell2_cblinfun_complex_fun$, type, B_ell2_b_ell2_cblinfun_complex_fun$: $tType ).
% 18.39/6.76  tff(C_ell2_c_ell2_cblinfun$, type, C_ell2_c_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_a_prod_a_b_complement_domain_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$, type, A_a_prod_a_b_complement_domain_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$, type, Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$, type, C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Complex_b_ell2_b_ell2_cblinfun_fun$, type, Complex_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Complex_b_ell2_cblinfun$, type, Complex_b_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$, type, C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$, type, C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_a_prod_a_b_complement_domain_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$, type, B_a_prod_a_b_complement_domain_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_a_b_complement_domain_prod_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$, type, A_a_a_b_complement_domain_prod_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_a_prod_ell2_a_a_prod_ell2_cblinfun$, type, B_a_prod_ell2_a_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$, type, A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$, type, B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Complex_c_ell2_c_ell2_cblinfun_fun$, type, Complex_c_ell2_c_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain$, type, A_b_complement_domain$: $tType ).
% 18.39/6.76  tff(B_b_prod_ell2_a_a_prod_ell2_cblinfun$, type, B_b_prod_ell2_a_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_a_prod_ell2$, type, B_a_prod_ell2$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$, type, A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$, type, C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_a_complement_domain_prod_ell2_a_a_a_complement_domain_prod_ell2_cblinfun$, type, A_a_a_complement_domain_prod_ell2_a_a_a_complement_domain_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_a_prod_ell2_a_b_prod_ell2_cblinfun$, type, B_a_prod_ell2_a_b_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_a_b_complement_domain_prod_ell2_b_ell2_cblinfun$, type, A_a_b_complement_domain_prod_ell2_b_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_prod_ell2_b_a_prod_ell2_cblinfun$, type, A_a_prod_ell2_b_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$, type, A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$, type, Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(C_ell2_c_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$, type, C_ell2_c_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_ell2_b_ell2_cblinfun$, type, B_ell2_b_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun$, type, B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$, type, A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun$, type, B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$, type, C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_prod_ell2$, type, A_a_prod_ell2$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$, type, A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$, type, Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$, type, Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$, type, A_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_ell2_a_ell2_cblinfun$, type, B_ell2_a_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_b_prod$, type, A_b_prod$: $tType ).
% 18.39/6.76  tff(Complex_a_ell2_cblinfun$, type, Complex_a_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(B_b_prod_ell2$, type, B_b_prod_ell2$: $tType ).
% 18.39/6.76  tff(B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$, type, B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_a_prod_ell2_b_a_prod_ell2_cblinfun$, type, B_a_prod_ell2_b_a_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  tff(B_b_prod_ell2_a_b_prod_ell2_cblinfun$, type, B_b_prod_ell2_a_b_prod_ell2_cblinfun$: $tType ).
% 18.39/6.76  tff(A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$, type, A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$: $tType ).
% 18.39/6.76  
% 18.39/6.76  %Background operators:
% 18.39/6.76  
% 18.39/6.76  
% 18.39/6.76  %Foreground operators:
% 18.39/6.76  tff(butterfly$a, type, butterfly$a: (B_ell2$ * B_ell2$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.76  tff('#skF_73', type, '#skF_73': (A_ell2_a_ell2_cblinfun$ * A_ell2_a_ell2_cblinfun$) > A$).
% 18.39/6.76  tff(sandwich$b, type, sandwich$b: A_ell2_a_ell2_cblinfun$ > A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.76  tff(equivalent_registers$c, type, equivalent_registers$c: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(register_tensor$e, type, register_tensor$e: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$).
% 18.39/6.76  tff(comp$z, type, comp$z: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.76  tff('#skF_44', type, '#skF_44': (C_ell2_c_ell2_cblinfun_complex_fun$ * Complex_c_ell2_c_ell2_cblinfun_fun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.76  tff('#skF_55', type, '#skF_55': A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > A_ell2_b_ell2_cblinfun$).
% 18.39/6.76  tff(comp$e, type, comp$e: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.76  tff(comp$ag, type, comp$ag: (A_ell2_a_ell2_cblinfun_complex_fun$ * Complex_a_ell2_a_ell2_cblinfun_fun$) > Complex_complex_fun$).
% 18.39/6.76  tff(complements$o, type, complements$o: (A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(register_tensor$b, type, register_tensor$b: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$).
% 18.39/6.76  tff(regular_register$b, type, regular_register$b: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(arcosh$, type, arcosh$: $real > $real).
% 18.39/6.76  tff(cblinfun_apply$b, type, cblinfun_apply$b: (B_ell2_b_ell2_cblinfun$ * B_ell2$) > B_ell2$).
% 18.39/6.76  tff('#skF_38', type, '#skF_38': (Complex_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_complex_fun$) > Complex$).
% 18.39/6.76  tff(register_pair$h, type, register_pair$h: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.76  tff(norm$e, type, norm$e: Complex_complex_cblinfun$ > $real).
% 18.39/6.76  tff(tensor_op$i, type, tensor_op$i: (B_ell2_a_ell2_cblinfun$ * B_ell2_a_ell2_cblinfun$) > B_b_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.76  tff(is_unit_register$j, type, is_unit_register$j: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(fun_app$m, type, fun_app$m: (A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.76  tff('#skF_76', type, '#skF_76': (A_ell2_b_ell2_cblinfun$ * B_ell2_a_ell2_cblinfun$) > B$).
% 18.39/6.76  tff('#skF_58', type, '#skF_58': A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun$).
% 18.39/6.76  tff(register_pair$a, type, register_pair$a: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.76  tff(tensor_op$s, type, tensor_op$s: (A_ell2_a_ell2_cblinfun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.76  tff('#skF_6', type, '#skF_6': (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.76  tff(id$b, type, id$b: Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.76  tff(comp$v, type, comp$v: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.76  tff(fun_app$aa, type, fun_app$aa: (Complex_complex_prod_complex_complex_prod_fun$ * Complex_complex_prod$) > Complex_complex_prod$).
% 18.39/6.76  tff(fun_app$r, type, fun_app$r: (Complex_complex_fun_complex_complex_fun_fun$ * Complex_complex_fun$) > Complex_complex_fun$).
% 18.39/6.76  tff(one_dim_iso$c, type, one_dim_iso$c: Complex_complex_cblinfun$ > Complex_complex_cblinfun$).
% 18.39/6.76  tff(tensor_op$h, type, tensor_op$h: (B_ell2_b_ell2_cblinfun$ * B_ell2_b_ell2_cblinfun$) > B_b_prod_ell2_b_b_prod_ell2_cblinfun$).
% 18.39/6.76  tff(comp$a, type, comp$a: 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_fun$).
% 18.39/6.76  tff(compatible$, type, compatible$: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(compatible$c, type, compatible$c: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_b_complement_domain_ell2_a_a_b_complement_domain_prod_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(iso_register$n, type, iso_register$n: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(register_pair$c, type, register_pair$c: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_b_complement_domain_ell2_a_a_b_complement_domain_prod_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.76  tff(comp$s, type, comp$s: (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$).
% 18.39/6.76  tff(complements$m, type, complements$m: (A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$ * A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(comp$d, type, comp$d: (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$).
% 18.39/6.76  tff('#skF_1', type, '#skF_1': (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.76  tff(cblinfun_compose$i, type, cblinfun_compose$i: (B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$ * B_a_prod_a_b_complement_domain_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$) > B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.76  tff(of_complex$, type, of_complex$: Complex$ > Complex_complex_cblinfun$).
% 18.39/6.76  tff(iso_register$p, type, iso_register$p: A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(iso_register$k, type, iso_register$k: A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff('#skF_17', type, '#skF_17': Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ > Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.76  tff(swap$a, type, swap$a: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$).
% 18.39/6.76  tff(adj$g, type, adj$g: B_ell2_a_ell2_cblinfun$ > A_ell2_b_ell2_cblinfun$).
% 18.39/6.76  tff(clinear$, type, clinear$: Complex_complex_fun$ > $o).
% 18.39/6.76  tff('#skF_91', type, '#skF_91': (A_ell2$ * A_ell2$) > Complex$).
% 18.39/6.76  tff(comp$ak, type, comp$ak: (C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$ * C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$) > C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$).
% 18.39/6.76  tff(fun_app$aj, type, fun_app$aj: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.76  tff('#skF_66', type, '#skF_66': (Complex_complex_cblinfun$ * Complex$ * Complex$) > Complex$).
% 18.39/6.76  tff(register_pair$, type, register_pair$: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.76  tff(is_Proj$, type, is_Proj$: A_ell2_a_ell2_cblinfun$ > $o).
% 18.39/6.76  tff(tensor_op$k, type, tensor_op$k: (A_ell2_b_ell2_cblinfun$ * B_ell2_a_ell2_cblinfun$) > A_b_prod_ell2_b_a_prod_ell2_cblinfun$).
% 18.39/6.76  tff(equivalent_registers$f, type, equivalent_registers$f: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(complement$a, type, complement$a: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > A_a_b_complement_domain_prod_b_complement_domain_ell2_a_a_b_complement_domain_prod_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.76  tff(cblinfun_apply$a, type, cblinfun_apply$a: (A_ell2_a_ell2_cblinfun$ * A_ell2$) > A_ell2$).
% 18.39/6.76  tff(equivalent_registers$d, type, equivalent_registers$d: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(complements$q, type, complements$q: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(default$d, type, default$d: B_a_prod$).
% 18.39/6.76  tff(adj$f, type, adj$f: Complex_complex_cblinfun$ > Complex_complex_cblinfun$).
% 18.39/6.76  tff(comp$af, type, comp$af: (Complex_a_ell2_a_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_complex_fun$) > A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.76  tff(unitary$a, type, unitary$a: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$ > $o).
% 18.39/6.76  tff(cblinfun_compose$c, type, cblinfun_compose$c: (Complex_b_ell2_cblinfun$ * B_ell2_complex_cblinfun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.76  tff(equivalent_registers$v, type, equivalent_registers$v: (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(id_cblinfun$d, type, id_cblinfun$d: B_ell2_b_ell2_cblinfun$).
% 18.39/6.76  tff(equivalent_registers$h, type, equivalent_registers$h: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff('#skF_9', type, '#skF_9': (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.76  tff(equivalent_registers$i, type, equivalent_registers$i: (A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$ * A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(sandwich$c, type, sandwich$c: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$ > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.76  tff(equivalent_registers$, type, equivalent_registers$: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff('#skF_45', type, '#skF_45': (B_ell2_b_ell2_cblinfun_complex_fun$ * Complex_b_ell2_b_ell2_cblinfun_fun$) > Complex$).
% 18.39/6.76  tff(cinner$, type, cinner$: (A_ell2$ * A_ell2$) > Complex$).
% 18.39/6.76  tff(cblinfun_apply$c, type, cblinfun_apply$c: (A_ell2_b_ell2_cblinfun$ * A_ell2$) > B_ell2$).
% 18.39/6.76  tff(register_tensor$c, type, register_tensor$c: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$).
% 18.39/6.76  tff(comp$am, type, comp$am: (C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$ * C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$) > C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$).
% 18.39/6.76  tff(is_unit_register$c, type, is_unit_register$c: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff('#skF_36', type, '#skF_36': (Complex_complex_fun$ * Complex_complex_fun$) > Complex$).
% 18.39/6.76  tff(id$f, type, id$f: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.76  tff(regular_register$h, type, regular_register$h: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(fun_app$, type, fun_app$: (Complex_complex_fun$ * Complex$) > Complex$).
% 18.39/6.76  tff('#skF_14', type, '#skF_14': C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.76  tff(complements$e, type, complements$e: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff('#skF_67', type, '#skF_67': Complex_complex_cblinfun$ > Complex$).
% 18.39/6.76  tff(is_unit_register$e, type, is_unit_register$e: C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(tensor_ell2$, type, tensor_ell2$: (A_ell2$ * A_b_complement_domain_ell2$) > A_a_b_complement_domain_prod_ell2$).
% 18.39/6.76  tff(equivalent_registers$g, type, equivalent_registers$g: (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > $o).
% 18.39/6.76  tff(fun_app$k, type, fun_app$k: (C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.76  tff('#skF_25', type, '#skF_25': (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.76  tff(regular_register$g, type, regular_register$g: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(fun_app$d, type, fun_app$d: (Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.76  tff(iso_register$d, type, iso_register$d: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.76  tff(comp$r, type, comp$r: (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$).
% 18.39/6.76  tff(default$, type, default$: A$).
% 18.39/6.76  tff(less_eq$a, type, less_eq$a: (Complex_complex_cblinfun$ * Complex_complex_cblinfun$) > $o).
% 18.39/6.76  tff(fun_app$ah, type, fun_app$ah: (A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.76  tff('#skF_87', type, '#skF_87': (A_ell2_a_ell2_cblinfun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$ * A_ell2_a_ell2_cblinfun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > Complex$).
% 18.39/6.76  tff(fun_app$e, type, fun_app$e: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.76  tff(complement$b, type, complement$b: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.77  tff(scaleC$, type, scaleC$: Complex_complex_complex_fun_fun$).
% 18.39/6.77  tff(ket$a, type, ket$a: B$ > B_ell2$).
% 18.39/6.77  tff(f$, type, f$: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(fun_app$af, type, fun_app$af: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.77  tff(pair$, type, pair$: (A$ * A$) > A_a_prod$).
% 18.39/6.77  tff(tensor_op$q, type, tensor_op$q: (A_ell2_a_ell2_cblinfun$ * B_ell2_a_ell2_cblinfun$) > A_b_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(iso_register$o, type, iso_register$o: B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(fst$, type, fst$: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register$r, type, register$r: A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(adj$h, type, adj$h: A_ell2_b_ell2_cblinfun$ > B_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(tensor_op$d, type, tensor_op$d: (B_ell2_b_ell2_cblinfun$ * B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun$) > B_b_b_complement_domain_prod_ell2_b_b_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(complements$p, type, complements$p: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff('#skF_61', type, '#skF_61': B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun$).
% 18.39/6.77  tff(is_unit_register$a, type, is_unit_register$a: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(iso_register$g, type, iso_register$g: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(butterfly$f, type, butterfly$f: (Complex$ * B_ell2$) > B_ell2_complex_cblinfun$).
% 18.39/6.77  tff(equivalent_registers$b, type, equivalent_registers$b: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(equivalent_registers$a, type, equivalent_registers$a: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(fun_app$j, type, fun_app$j: (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(unit_register$, type, unit_register$: Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff(butterfly$q, type, butterfly$q: (B_a_prod_ell2$ * A_b_prod_ell2$) > A_b_prod_ell2_b_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(cblinfun_mult_left$, type, cblinfun_mult_left$: Complex$ > Complex_complex_cblinfun$).
% 18.39/6.77  tff('#skF_35', type, '#skF_35': (Complex_complex_fun$ * Complex_complex_fun$) > Complex$).
% 18.39/6.77  tff(empty_var$, type, empty_var$: Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_28', type, '#skF_28': (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_96', type, '#skF_96': ($real * $real) > $real).
% 18.39/6.77  tff(tensor_op$a, type, tensor_op$a: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$ * A_ell2_a_ell2_cblinfun$) > A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(register$b, type, register$b: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(complements$g, type, complements$g: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(cblinfun_apply$f, type, cblinfun_apply$f: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$ * A_b_complement_domain_ell2$) > A_b_complement_domain_ell2$).
% 18.39/6.77  tff(iso_register$b, type, iso_register$b: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(cblinfun_cinner_right$, type, cblinfun_cinner_right$: Complex$ > Complex_complex_cblinfun$).
% 18.39/6.77  tff('#skF_33', type, '#skF_33': A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.77  tff(pair$e, type, pair$e: (Complex$ * Complex$) > Complex_complex_prod$).
% 18.39/6.77  tff(iso_register$m, type, iso_register$m: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(fun_app$ak, type, fun_app$ak: (A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$) > A_a_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(tensor_ell2$c, type, tensor_ell2$c: (B_ell2$ * A_ell2$) > B_a_prod_ell2$).
% 18.39/6.77  tff('#skF_2', type, '#skF_2': (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_29', type, '#skF_29': (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(cinner$b, type, cinner$b: Complex$ > Complex_complex_fun$).
% 18.39/6.77  tff(cblinfun_compose$g, type, cblinfun_compose$g: (A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$ * A_a_prod_a_b_complement_domain_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$) > A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.77  tff(tlfalse, type, tlfalse: tlbool).
% 18.39/6.77  tff(one_dim_iso$d, type, one_dim_iso$d: Complex_complex_fun$).
% 18.39/6.77  tff(fun_app$n, type, fun_app$n: (C_ell2_c_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.77  tff('#skF_19', type, '#skF_19': B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_74', type, '#skF_74': (A_ell2_a_ell2_cblinfun$ * A_ell2_a_ell2_cblinfun$) > A$).
% 18.39/6.77  tff(zero$e, type, zero$e: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(tensor_op$j, type, tensor_op$j: (B_ell2_a_ell2_cblinfun$ * A_ell2_b_ell2_cblinfun$) > B_a_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.77  tff(antilinear_axioms$, type, antilinear_axioms$: Complex_complex_fun$ > $o).
% 18.39/6.77  tff(complements$i, type, complements$i: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(comp$aq, type, comp$aq: (B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$ * B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$) > B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(butterfly$v, type, butterfly$v: (B_b_prod_ell2$ * A_b_prod_ell2$) > A_b_prod_ell2_b_b_prod_ell2_cblinfun$).
% 18.39/6.77  tff(tensor_ell2$a, type, tensor_ell2$a: (A_ell2$ * A_ell2$) > A_a_prod_ell2$).
% 18.39/6.77  tff('#skF_24', type, '#skF_24': (B_ell2_b_ell2_cblinfun_a_ell2_a_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$).
% 18.39/6.77  tff('#skF_92', type, '#skF_92': (B_ell2$ * B_ell2$) > Complex$).
% 18.39/6.77  tff(cblinfun_apply$d, type, cblinfun_apply$d: (B_ell2_a_ell2_cblinfun$ * B_ell2$) > A_ell2$).
% 18.39/6.77  tff('#skF_65', type, '#skF_65': (Complex_complex_cblinfun$ * Complex$ * Complex$) > Complex$).
% 18.39/6.77  tff(register$m, type, register$m: C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(comp$av, type, comp$av: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$) > A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(butterfly$w, type, butterfly$w: (A_a_prod_ell2$ * A_b_prod_ell2$) > A_b_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(butterfly$h, type, butterfly$h: (A_b_complement_domain_ell2$ * A_b_complement_domain_ell2$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.77  tff('#skF_77', type, '#skF_77': (B_ell2_a_ell2_cblinfun$ * A_ell2_b_ell2_cblinfun$) > B$).
% 18.39/6.77  tff(butterfly$c, type, butterfly$c: (A_ell2$ * Complex$) > Complex_a_ell2_cblinfun$).
% 18.39/6.77  tff(is_unit_register$g, type, is_unit_register$g: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(comp$an, type, comp$an: (C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$ * C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$) > C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(tensor_op$, type, tensor_op$: (A_ell2_a_ell2_cblinfun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(comp$, type, comp$: (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$).
% 18.39/6.77  tff(equivalent_registers$l, type, equivalent_registers$l: (A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(comp$t, type, comp$t: (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$).
% 18.39/6.77  tff(norm$b, type, norm$b: B_ell2$ > $real).
% 18.39/6.77  tff(tensor_op$e, type, tensor_op$e: A_ell2_a_ell2_cblinfun$ > A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_75', type, '#skF_75': (A_ell2_b_ell2_cblinfun$ * B_ell2_a_ell2_cblinfun$) > A$).
% 18.39/6.77  tff(complements$f, type, complements$f: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(fun_app$b, type, fun_app$b: (Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(scaleC$f, type, scaleC$f: (Complex$ * Complex_complex_cblinfun$) > Complex_complex_cblinfun$).
% 18.39/6.77  tff(comp$x, type, comp$x: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(fun_app$ab, type, fun_app$ab: (Complex_complex_complex_prod_complex_complex_prod_fun_fun$ * Complex$) > Complex_complex_prod_complex_complex_prod_fun$).
% 18.39/6.77  tff(register_tensor$a, type, register_tensor$a: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(butterfly$o, type, butterfly$o: (B_ell2$ * A_ell2$) > A_ell2_b_ell2_cblinfun$).
% 18.39/6.77  tff(butterfly$d, type, butterfly$d: (Complex$ * A_ell2$) > A_ell2_complex_cblinfun$).
% 18.39/6.77  tff(comp$w, type, comp$w: (Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$) > Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register_tensor$g, type, register_tensor$g: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(iso_register$c, type, iso_register$c: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(comp$ad, type, comp$ad: (Complex_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_complex_fun$) > B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(ket$, type, ket$: A$ > A_ell2$).
% 18.39/6.77  tff(fst$a, type, fst$a: A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(sandwich$f, type, sandwich$f: A_a_b_complement_domain_prod_ell2_b_ell2_cblinfun$ > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(comp$ae, type, comp$ae: (B_ell2_b_ell2_cblinfun_complex_fun$ * Complex_b_ell2_b_ell2_cblinfun_fun$) > Complex_complex_fun$).
% 18.39/6.77  tff(cblinfun_compose$d, type, cblinfun_compose$d: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff('#skF_7', type, '#skF_7': (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_56', type, '#skF_56': A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > A_a_b_complement_domain_prod_ell2_b_ell2_cblinfun$).
% 18.39/6.77  tff(complements$u, type, complements$u: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ * Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(zero$a, type, zero$a: A_ell2$).
% 18.39/6.77  tff(unitary$, type, unitary$: A_ell2_a_ell2_cblinfun$ > $o).
% 18.39/6.77  tff(scaleC$h, type, scaleC$h: Complex_complex_complex_prod_complex_complex_prod_fun_fun$).
% 18.39/6.77  tff('#skF_83', type, '#skF_83': Complex_complex_fun$ > Complex$).
% 18.39/6.77  tff(scaleC$i, type, scaleC$i: (Complex$ * B_ell2$) > B_ell2$).
% 18.39/6.77  tff(zero$h, type, zero$h: Complex_complex_cblinfun$).
% 18.39/6.77  tff(one$a, type, one$a: Complex_complex_cblinfun$).
% 18.39/6.77  tff(pair$c, type, pair$c: (B$ * A$) > B_a_prod$).
% 18.39/6.77  tff(register$k, type, register$k: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(tensor_op$l, type, tensor_op$l: (A_ell2_b_ell2_cblinfun$ * A_ell2_b_ell2_cblinfun$) > A_a_prod_ell2_b_b_prod_ell2_cblinfun$).
% 18.39/6.77  tff('#skF_86', type, '#skF_86': Complex_complex_fun$ > Complex$).
% 18.39/6.77  tff(pair$d, type, pair$d: (A$ * A_b_complement_domain$) > A_a_b_complement_domain_prod$).
% 18.39/6.77  tff(comp$p, type, comp$p: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff(tensor_op$n, type, tensor_op$n: (A_ell2_b_ell2_cblinfun$ * A_ell2_a_ell2_cblinfun$) > A_a_prod_ell2_b_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(less_eq$, type, less_eq$: (Complex$ * Complex$) > $o).
% 18.39/6.77  tff('#skF_13', type, '#skF_13': C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register_tensor$f, type, register_tensor$f: (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$).
% 18.39/6.77  tff(iso_register$t, type, iso_register$t: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(equivalent_registers$p, type, equivalent_registers$p: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(iso_register$h, type, iso_register$h: Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(cblinfun_scaleC_left$, type, cblinfun_scaleC_left$: Complex$ > Complex_complex_cblinfun$).
% 18.39/6.77  tff(ket$g, type, ket$g: A_b_complement_domain$ > A_b_complement_domain_ell2$).
% 18.39/6.77  tff(comp$aj, type, comp$aj: (C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$ * C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$) > C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(butterfly$r, type, butterfly$r: (B_b_prod_ell2$ * A_a_prod_ell2$) > A_a_prod_ell2_b_b_prod_ell2_cblinfun$).
% 18.39/6.77  tff('#skF_88', type, '#skF_88': (A_a_prod_ell2_a_a_prod_ell2_cblinfun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$ * A_b_complement_domain_ell2$ * A_b_complement_domain_ell2$ * A_ell2$ * A_ell2$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(regular_register$e, type, regular_register$e: A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(fun_app$ad, type, fun_app$ad: (A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$ * A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(of_complex$a, type, of_complex$a: Complex_complex_fun$).
% 18.39/6.77  tff(adj$c, type, adj$c: Complex_b_ell2_cblinfun$ > B_ell2_complex_cblinfun$).
% 18.39/6.77  tff(vector_to_cblinfun$, type, vector_to_cblinfun$: A_ell2$ > Complex_a_ell2_cblinfun$).
% 18.39/6.77  tff(comp$m, type, comp$m: (A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(cblinfun_compose$f, type, cblinfun_compose$f: (A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$ * A_a_a_b_complement_domain_prod_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$) > A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.77  tff(scaleC$c, type, scaleC$c: (Complex$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(fun_app$h, type, fun_app$h: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_89', type, '#skF_89': (B_a_prod_ell2_b_a_prod_ell2_cblinfun$ * A_b_complement_domain_ell2$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$ * B_ell2$ * B_ell2$ * A_b_complement_domain_ell2$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(scaleC$d, type, scaleC$d: Complex$ > C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff(one_dim_iso$a, type, one_dim_iso$a: Complex$ > Complex_complex_cblinfun$).
% 18.39/6.77  tff(butterfly$t, type, butterfly$t: (B_a_prod_ell2$ * A_a_prod_ell2$) > A_a_prod_ell2_b_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(comp$o, type, comp$o: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(comp$q, type, comp$q: Complex_complex_fun$ > Complex_complex_fun_complex_complex_fun_fun$).
% 18.39/6.77  tff(less$, type, less$: (Complex$ * Complex$) > $o).
% 18.39/6.77  tff('#skF_27', type, '#skF_27': (A_ell2_a_ell2_cblinfun_b_ell2_b_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$).
% 18.39/6.77  tff(cblinfun_compose$, type, cblinfun_compose$: B_ell2_b_ell2_cblinfun$ > B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(empty_var$a, type, empty_var$a: Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register_tensor$, type, register_tensor$: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_30', type, '#skF_30': C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > C_ell2_c_ell2_cblinfun$).
% 18.39/6.77  tff(butterfly$g, type, butterfly$g: (A_a_b_complement_domain_prod_ell2$ * A_a_b_complement_domain_prod_ell2$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(default$c, type, default$c: A_b_prod$).
% 18.39/6.77  tff(fun_app$a, type, fun_app$a: (Complex_complex_complex_fun_fun$ * Complex$) > Complex_complex_fun$).
% 18.39/6.77  tff(id_cblinfun$a, type, id_cblinfun$a: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.77  tff(butterfly$, type, butterfly$: (A_ell2$ * A_ell2$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(complements$s, type, complements$s: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff('#skF_54', type, '#skF_54': (A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(scaleC$a, type, scaleC$a: Complex$ > A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.77  tff(comp$f, type, comp$f: (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$).
% 18.39/6.77  tff(norm$a, type, norm$a: A_ell2$ > $real).
% 18.39/6.77  tff(norm$f, type, norm$f: $real > $real).
% 18.39/6.77  tff(adj$b, type, adj$b: Complex_a_ell2_cblinfun$ > A_ell2_complex_cblinfun$).
% 18.39/6.77  tff('#skF_32', type, '#skF_32': A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff('#skF_12', type, '#skF_12': A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register$p, type, register$p: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(comp$i, type, comp$i: (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$).
% 18.39/6.77  tff(comp$c, type, comp$c: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_21', type, '#skF_21': (B_ell2_b_ell2_cblinfun_a_ell2_a_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$).
% 18.39/6.77  tff('#skF_41', type, '#skF_41': (Complex_a_ell2_a_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_complex_fun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(unit_register$a, type, unit_register$a: Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(comp$aw, type, comp$aw: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register$q, type, register$q: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff('#skF_46', type, '#skF_46': (B_ell2_b_ell2_cblinfun_complex_fun$ * Complex_b_ell2_b_ell2_cblinfun_fun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.77  tff(fun_app$v, type, fun_app$v: (B_ell2_b_ell2_cblinfun_complex_fun$ * B_ell2_b_ell2_cblinfun$) > Complex$).
% 18.39/6.77  tff(register$l, type, register$l: B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(comp$ab, type, comp$ab: (Complex_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_complex_fun$) > C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff(equivalent_registers$s, type, equivalent_registers$s: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(complements$b, type, complements$b: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(tensor_op$f, type, tensor_op$f: (A_ell2_a_ell2_cblinfun$ * B_ell2_b_ell2_cblinfun$) > A_b_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.77  tff(ket$e, type, ket$e: B_a_prod$ > B_a_prod_ell2$).
% 18.39/6.77  tff(cblinfun_compose$h, type, cblinfun_compose$h: (B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$ * B_a_a_b_complement_domain_prod_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$) > B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.77  tff(zero$, type, zero$: Complex$).
% 18.39/6.77  tff(id_cblinfun$b, type, id_cblinfun$b: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(butterfly$n, type, butterfly$n: (A_a_prod_ell2$ * B_b_prod_ell2$) > B_b_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.77  tff(id$a, type, id$a: C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff('#skF_23', type, '#skF_23': (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$).
% 18.39/6.77  tff(comp$ah, type, comp$ah: (C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$ * C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$) > C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(complement$, type, complement$: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register$a, type, register$a: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(sandwich$d, type, sandwich$d: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$ > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$).
% 18.39/6.77  tff(sandwich$a, type, sandwich$a: C_ell2_c_ell2_cblinfun$ > C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.77  tff(cblinfun_mult_right$, type, cblinfun_mult_right$: Complex$ > Complex_complex_cblinfun$).
% 18.39/6.77  tff(register$f, type, register$f: Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff('#skF_10', type, '#skF_10': A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.77  tff(equivalent_registers$w, type, equivalent_registers$w: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(fun_app$y, type, fun_app$y: (B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.77  tff(adj$, type, adj$: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.77  tff(register_pair$d, type, register_pair$d: (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_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.77  tff(tensor_op$c, type, tensor_op$c: (B_ell2_b_ell2_cblinfun$ * B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun$) > B_b_a_complement_domain_prod_ell2_b_b_a_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff(fun_app$ac, type, fun_app$ac: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.77  tff('#skF_53', type, '#skF_53': (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$).
% 18.39/6.77  tff('#skF_94', type, '#skF_94': Complex_complex_cblinfun$ > Complex$).
% 18.39/6.77  tff(equivalent_registers$o, type, equivalent_registers$o: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(iso_register$f, type, iso_register$f: A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(compatible$b, type, compatible$b: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_b_complement_domain_ell2_a_a_b_complement_domain_prod_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.77  tff(register$i, type, register$i: C_ell2_c_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(tensor_ell2$b, type, tensor_ell2$b: (A_ell2$ * B_ell2$) > A_b_prod_ell2$).
% 18.39/6.77  tff(iso_register$e, type, iso_register$e: A_ell2_a_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(register_pair$g, type, register_pair$g: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * B_b_b_complement_domain_prod_ell2_b_b_b_complement_domain_prod_ell2_cblinfun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.77  tff(norm$d, type, norm$d: B_ell2_b_ell2_cblinfun$ > $real).
% 18.39/6.77  tff('#skF_63', type, '#skF_63': (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.77  tff(iso_register$s, type, iso_register$s: C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.77  tff(register_pair$e, type, register_pair$e: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_a_a_complement_domain_prod_ell2_a_a_a_complement_domain_prod_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.77  tff(cblinfun_compose$a, type, cblinfun_compose$a: A_ell2_a_ell2_cblinfun$ > A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(register$c, type, register$c: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(butterfly$e, type, butterfly$e: (B_ell2$ * Complex$) > Complex_b_ell2_cblinfun$).
% 18.39/6.78  tff(cblinfun_scaleC_right$, type, cblinfun_scaleC_right$: Complex$ > Complex_complex_cblinfun$).
% 18.39/6.78  tff('#skF_69', type, '#skF_69': (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(comp$ar, type, comp$ar: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(complements$, type, complements$: (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(tensor_op$g, type, tensor_op$g: (B_ell2_b_ell2_cblinfun$ * A_ell2_a_ell2_cblinfun$) > B_a_prod_ell2_b_a_prod_ell2_cblinfun$).
% 18.39/6.78  tff(iso_register$j, type, iso_register$j: Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(one_dim_iso$e, type, one_dim_iso$e: Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.78  tff(fun_app$t, type, fun_app$t: (C_ell2_c_ell2_cblinfun_complex_fun$ * C_ell2_c_ell2_cblinfun$) > Complex$).
% 18.39/6.78  tff(zero$b, type, zero$b: A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(register$n, type, register$n: Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(butterfly$k, type, butterfly$k: (B_a_prod_ell2$ * B_a_prod_ell2$) > B_a_prod_ell2_b_a_prod_ell2_cblinfun$).
% 18.39/6.78  tff(regular_register$, type, regular_register$: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(scale$, type, scale$: (Complex_complex_complex_fun_fun$ * Complex_complex_complex_fun_fun$) > Complex_complex_complex_prod_complex_complex_prod_fun_fun$).
% 18.39/6.78  tff(complements$l, type, complements$l: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(snd$a, type, snd$a: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(comp$b, type, comp$b: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(fun_app$i, type, fun_app$i: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff(swap$, type, swap$: A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(id$h, type, id$h: Complex_complex_fun_complex_complex_fun_fun$).
% 18.39/6.78  tff(register_tensor$h, type, register_tensor$h: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(complements$a, type, complements$a: (A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$ * A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff('#skF_39', type, '#skF_39': (Complex_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_complex_fun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff(comp$at, type, comp$at: (A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(comp$al, type, comp$al: (C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$ * C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$) > C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(cblinfun_compose$e, type, cblinfun_compose$e: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$ > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.78  tff('#skF_5', type, '#skF_5': (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(scaleC$b, type, scaleC$b: Complex$ > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.78  tff(iso_register$, type, iso_register$: Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(tensor_op$b, type, tensor_op$b: (A_ell2_a_ell2_cblinfun$ * A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun$) > A_a_a_complement_domain_prod_ell2_a_a_a_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff(fun_app$ae, type, fun_app$ae: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$).
% 18.39/6.78  tff(butterfly$u, type, butterfly$u: (A_b_prod_ell2$ * B_b_prod_ell2$) > B_b_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_81', type, '#skF_81': Complex_complex_fun$ > Complex$).
% 18.39/6.78  tff(complements$h, type, complements$h: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(compatible$d, type, compatible$d: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(equivalent_registers$n, type, equivalent_registers$n: (Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(tensor_op$t, type, tensor_op$t: (A_a_prod_ell2_a_a_prod_ell2_cblinfun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > A_a_prod_a_b_complement_domain_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff(iso_register$u, type, iso_register$u: A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(one_dim_iso$, type, one_dim_iso$: Unit_ell2_unit_ell2_cblinfun$ > Complex$).
% 18.39/6.78  tff(equivalent_registers$x, type, equivalent_registers$x: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(scaleC$e, type, scaleC$e: Complex$ > Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.78  tff(empty_var$b, type, empty_var$b: Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.78  tff(fun_app$x, type, fun_app$x: (A_ell2_a_ell2_cblinfun_complex_fun$ * A_ell2_a_ell2_cblinfun$) > Complex$).
% 18.39/6.78  tff(id$e, type, id$e: Complex_complex_fun$).
% 18.39/6.78  tff('#skF_85', type, '#skF_85': Complex_complex_fun$ > Complex$).
% 18.39/6.78  tff('#skF_59', type, '#skF_59': A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.78  tff(pair$a, type, pair$a: (B$ * B$) > B_b_prod$).
% 18.39/6.78  tff(fun_app$g, type, fun_app$g: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff(equivalent_registers$k, type, equivalent_registers$k: (A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(one_dim_iso$b, type, one_dim_iso$b: Complex_complex_cblinfun$ > Complex$).
% 18.39/6.78  tff(complement$c, type, complement$c: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(scaleC$g, type, scaleC$g: Complex$ > B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(adj$a, type, adj$a: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(register_pair$b, type, register_pair$b: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_b_complement_domain_ell2_a_a_b_complement_domain_prod_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(cblinfun_apply$, type, cblinfun_apply$: Complex_complex_cblinfun$ > Complex_complex_fun$).
% 18.39/6.78  tff(minus$, type, minus$: Complex$ > Complex_complex_fun$).
% 18.39/6.78  tff(complements$c, type, complements$c: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(register$o, type, register$o: A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(equivalent_registers$q, type, equivalent_registers$q: (B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$ * A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(regular_register$a, type, regular_register$a: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(butterfly$i, type, butterfly$i: (A_a_prod_ell2$ * A_a_prod_ell2$) > A_a_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.78  tff(comp$k, type, comp$k: (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$).
% 18.39/6.78  tff('#skF_47', type, '#skF_47': (A_ell2_a_ell2_cblinfun_complex_fun$ * Complex_a_ell2_a_ell2_cblinfun_fun$) > Complex$).
% 18.39/6.78  tff(assoc_ell2$b, type, assoc_ell2$b: B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_79', type, '#skF_79': (B_ell2_b_ell2_cblinfun$ * B_ell2_b_ell2_cblinfun$) > B$).
% 18.39/6.78  tff(times$, type, times$: Complex$ > Complex_complex_fun$).
% 18.39/6.78  tff(comp$ac, type, comp$ac: (C_ell2_c_ell2_cblinfun_complex_fun$ * Complex_c_ell2_c_ell2_cblinfun_fun$) > Complex_complex_fun$).
% 18.39/6.78  tff(equivalent_registers$m, type, equivalent_registers$m: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff('#skF_4', type, '#skF_4': (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.78  tff(butterfly$s, type, butterfly$s: (A_a_prod_ell2$ * B_a_prod_ell2$) > B_a_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.78  tff(comp$ap, type, comp$ap: (C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$ * C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$) > C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(iso_register$l, type, iso_register$l: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(uu$, type, uu$: Complex$ > Complex_complex_fun$).
% 18.39/6.78  tff('#skF_50', type, '#skF_50': (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff(tensor_op$o, type, tensor_op$o: (B_ell2_a_ell2_cblinfun$ * B_ell2_b_ell2_cblinfun$) > B_b_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff(unit_register$c, type, unit_register$c: Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.78  tff(equivalent_registers$j, type, equivalent_registers$j: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(cnj$, type, cnj$: Complex_complex_fun$).
% 18.39/6.78  tff('#skF_18', type, '#skF_18': A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(norm$c, type, norm$c: A_ell2_a_ell2_cblinfun$ > $real).
% 18.39/6.78  tff(register$d, type, register$d: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(fun_app$z, type, fun_app$z: (C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff(tensor_op$p, type, tensor_op$p: (A_ell2_b_ell2_cblinfun$ * B_ell2_b_ell2_cblinfun$) > A_b_prod_ell2_b_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff(zero$g, type, zero$g: A_b_complement_domain_ell2$).
% 18.39/6.78  tff('#skF_31', type, '#skF_31': B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_43', type, '#skF_43': (C_ell2_c_ell2_cblinfun_complex_fun$ * Complex_c_ell2_c_ell2_cblinfun_fun$) > Complex$).
% 18.39/6.78  tff(complements$d, type, complements$d: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff('#skF_11', type, '#skF_11': B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff('#skF_78', type, '#skF_78': (B_ell2_a_ell2_cblinfun$ * A_ell2_b_ell2_cblinfun$) > A$).
% 18.39/6.78  tff(id$g, type, id$g: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$).
% 18.39/6.78  tff(butterfly$j, type, butterfly$j: (A_b_prod_ell2$ * A_b_prod_ell2$) > A_b_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff(fun_app$u, type, fun_app$u: (Complex_b_ell2_b_ell2_cblinfun_fun$ * Complex$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff(cblinfun_compose$b, type, cblinfun_compose$b: (Complex_a_ell2_cblinfun$ * A_ell2_complex_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(cblinfun_apply$e, type, cblinfun_apply$e: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$ * A_a_b_complement_domain_prod_ell2$) > A_a_b_complement_domain_prod_ell2$).
% 18.39/6.78  tff(iso_register$a, type, iso_register$a: Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(register$h, type, register$h: A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(id_cblinfun$c, type, id_cblinfun$c: C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff(unitary$c, type, unitary$c: A_a_b_complement_domain_prod_ell2_b_ell2_cblinfun$ > $o).
% 18.39/6.78  tff('#skF_64', type, '#skF_64': A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.78  tff(butterfly$x, type, butterfly$x: (A_b_prod_ell2$ * A_a_prod_ell2$) > A_a_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff(comp$ao, type, comp$ao: (C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$ * C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$) > C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(zero$c, type, zero$c: B_ell2$).
% 18.39/6.78  tff(default$a, type, default$a: B$).
% 18.39/6.78  tff(comp$h, type, comp$h: (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$).
% 18.39/6.78  tff(ket$c, type, ket$c: B_b_prod$ > B_b_prod_ell2$).
% 18.39/6.78  tff('#skF_16', type, '#skF_16': B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(complements$n, type, complements$n: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(is_unit_register$b, type, is_unit_register$b: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(a$, type, a$: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.78  tff(snd$, type, snd$: A_ell2_a_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(regular_register$d, type, regular_register$d: A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(comp$j, type, comp$j: (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$).
% 18.39/6.78  tff('#skF_52', type, '#skF_52': (B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff(tensor_op$u, type, tensor_op$u: (B_ell2_b_ell2_cblinfun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.78  tff(id_cblinfun$, type, id_cblinfun$: A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(empty_var$c, type, empty_var$c: Unit_ell2_unit_ell2_cblinfun$ > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff(is_unit_register$f, type, is_unit_register$f: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(is_unit_register$h, type, is_unit_register$h: A_b_complement_domain_a_b_complement_domain_prod_ell2_a_b_complement_domain_a_b_complement_domain_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff('#skF_49', type, '#skF_49': (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_90', type, '#skF_90': (Complex_complex_cblinfun$ * Complex$) > Complex$).
% 18.39/6.78  tff(comp$l, type, comp$l: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff('#skF_72', type, '#skF_72': (Complex_complex_cblinfun$ * Complex_complex_cblinfun$) > Complex$).
% 18.39/6.78  tff(is_unit_register$d, type, is_unit_register$d: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(comp$au, type, comp$au: (A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(unit_register$b, type, unit_register$b: Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(register$e, type, register$e: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(is_unit_register$, type, is_unit_register$: Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(id$d, type, id$d: B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(comp$as, type, comp$as: (A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(complements$r, type, complements$r: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(sandwich$, type, sandwich$: B_ell2_b_ell2_cblinfun$ > B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(comp$aa, type, comp$aa: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff('#skF_34', type, '#skF_34': Complex_complex_fun$ > Complex$).
% 18.39/6.78  tff(complements$t, type, complements$t: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(fun_app$f, type, fun_app$f: (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_20', type, '#skF_20': (A_ell2_a_ell2_cblinfun_b_ell2_b_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$).
% 18.39/6.78  tff('#skF_26', type, '#skF_26': (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$).
% 18.39/6.78  tff(ket$d, type, ket$d: A_b_prod$ > A_b_prod_ell2$).
% 18.39/6.78  tff(default$e, type, default$e: B_b_prod$).
% 18.39/6.78  tff(equivalent_registers$t, type, equivalent_registers$t: (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(ln$, type, ln$: $real > $real).
% 18.39/6.78  tff(register_pair$f, type, register_pair$f: (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * B_b_a_complement_domain_prod_ell2_b_b_a_complement_domain_prod_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(butterfly$l, type, butterfly$l: (B_b_prod_ell2$ * B_b_prod_ell2$) > B_b_prod_ell2_b_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff(fun_app$w, type, fun_app$w: (Complex_a_ell2_a_ell2_cblinfun_fun$ * Complex$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_93', type, '#skF_93': (Complex$ * Complex$) > Complex$).
% 18.39/6.78  tff(butterfly$p, type, butterfly$p: (A_b_prod_ell2$ * B_a_prod_ell2$) > B_a_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff(sandwich$e, type, sandwich$e: A_ell2_b_ell2_cblinfun$ > A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(zero$f, type, zero$f: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_22', type, '#skF_22': (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$).
% 18.39/6.78  tff('#skF_40', type, '#skF_40': (Complex_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_complex_fun$) > Complex$).
% 18.39/6.78  tff(zero$d, type, zero$d: B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_62', type, '#skF_62': (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(id$, type, id$: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(regular_register$c, type, regular_register$c: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(comp$y, type, comp$y: (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(tensor_op$v, type, tensor_op$v: (B_a_prod_ell2_b_a_prod_ell2_cblinfun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > B_a_prod_a_b_complement_domain_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff(ket$b, type, ket$b: A_a_prod$ > A_a_prod_ell2$).
% 18.39/6.78  tff(tltrue, type, tltrue: tlbool).
% 18.39/6.78  tff(adj$d, type, adj$d: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$ > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_8', type, '#skF_8': (A_ell2_a_ell2_cblinfun_b_ell2_b_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$).
% 18.39/6.78  tff(fun_app$o, type, fun_app$o: (A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_3', type, '#skF_3': (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$).
% 18.39/6.78  tff(fun_app$ag, type, fun_app$ag: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff(comp$g, type, comp$g: (Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$) > Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.78  tff(unitary$b, type, unitary$b: A_ell2_b_ell2_cblinfun$ > $o).
% 18.39/6.78  tff(equivalent_registers$u, type, equivalent_registers$u: (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(tensor_ell2$d, type, tensor_ell2$d: (B_ell2$ * B_ell2$) > B_b_prod_ell2$).
% 18.39/6.78  tff('#skF_51', type, '#skF_51': (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$).
% 18.39/6.78  tff(is_Proj$a, type, is_Proj$a: B_ell2_b_ell2_cblinfun$ > $o).
% 18.39/6.78  tff(one_dim_iso$f, type, one_dim_iso$f: Complex$ > Unit_ell2_unit_ell2_cblinfun$).
% 18.39/6.78  tff(tensor_op$r, type, tensor_op$r: (A_ell2_a_ell2_cblinfun$ * A_ell2_b_ell2_cblinfun$) > A_a_prod_ell2_a_b_prod_ell2_cblinfun$).
% 18.39/6.78  tff(is_unit_register$i, type, is_unit_register$i: A_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_b_complement_domain_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff('#skF_48', type, '#skF_48': (A_ell2_a_ell2_cblinfun_complex_fun$ * Complex_a_ell2_a_ell2_cblinfun_fun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(register$g, type, register$g: C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(comp$u, type, comp$u: (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$).
% 18.39/6.78  tff('#skF_70', type, '#skF_70': (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$).
% 18.39/6.78  tff(butterfly$m, type, butterfly$m: (A_ell2$ * B_ell2$) > B_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(register_tensor$d, type, register_tensor$d: (C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(compatible$a, type, compatible$a: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(register$j, type, register$j: A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(fun_app$l, type, fun_app$l: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$) > B_ell2_b_ell2_cblinfun$).
% 18.39/6.78  tff(iso_register$r, type, iso_register$r: C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff('#skF_84', type, '#skF_84': Complex_complex_fun$ > Complex$).
% 18.39/6.78  tff('#skF_80', type, '#skF_80': (B_ell2_b_ell2_cblinfun$ * B_ell2_b_ell2_cblinfun$) > B$).
% 18.39/6.78  tff(times$a, type, times$a: ($real * $real) > $real).
% 18.39/6.78  tff('#skF_37', type, '#skF_37': (Complex_c_ell2_c_ell2_cblinfun_fun$ * C_ell2_c_ell2_cblinfun_complex_fun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_15', type, '#skF_15': C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$).
% 18.39/6.78  tff(assoc_ell2$a, type, assoc_ell2$a: A_a_a_b_complement_domain_prod_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff(complement$d, type, complement$d: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(one$, type, one$: Complex$).
% 18.39/6.78  tff('#skF_57', type, '#skF_57': A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$).
% 18.39/6.78  tff(butterfly$b, type, butterfly$b: (Complex$ * Complex$) > Complex_complex_cblinfun$).
% 18.39/6.78  tff(assoc_ell2$c, type, assoc_ell2$c: B_a_a_b_complement_domain_prod_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$).
% 18.39/6.78  tff(fun_app$c, type, fun_app$c: (A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_82', type, '#skF_82': Complex_complex_fun$ > Complex$).
% 18.39/6.78  tff(equivalent_registers$r, type, equivalent_registers$r: (B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff('#skF_71', type, '#skF_71': (Complex_complex_cblinfun$ * Complex_complex_cblinfun$) > Complex$).
% 18.39/6.78  tff(complements$v, type, complements$v: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(assoc_ell2$, type, assoc_ell2$: A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$).
% 18.39/6.78  tff(scaleC$j, type, scaleC$j: (Complex$ * A_ell2$) > A_ell2$).
% 18.39/6.78  tff('#skF_68', type, '#skF_68': (Complex_complex_cblinfun$ * Complex_complex_cblinfun$) > Complex$).
% 18.39/6.78  tff('#skF_95', type, '#skF_95': (Complex_complex_cblinfun$ * Complex_complex_cblinfun$) > Complex$).
% 18.39/6.78  tff(vector_to_cblinfun$a, type, vector_to_cblinfun$a: B_ell2$ > Complex_b_ell2_cblinfun$).
% 18.39/6.78  tff(comp$ai, type, comp$ai: (C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$ * C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$) > C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff('#skF_60', type, '#skF_60': B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ > B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun$).
% 18.39/6.78  tff(id$i, type, id$i: A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$).
% 18.39/6.78  tff(fun_app$q, type, fun_app$q: (Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$ * Unit_ell2_unit_ell2_cblinfun$) > Unit_ell2_unit_ell2_cblinfun$).
% 18.39/6.78  tff(fun_app$p, type, fun_app$p: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff('#skF_42', type, '#skF_42': (Complex_a_ell2_a_ell2_cblinfun_fun$ * A_ell2_a_ell2_cblinfun_complex_fun$) > Complex$).
% 18.39/6.78  tff(register$, type, register$: C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(pair$b, type, pair$b: (A$ * B$) > A_b_prod$).
% 18.39/6.78  tff(fun_app$s, type, fun_app$s: (Complex_c_ell2_c_ell2_cblinfun_fun$ * Complex$) > C_ell2_c_ell2_cblinfun$).
% 18.39/6.78  tff(default$b, type, default$b: A_a_prod$).
% 18.39/6.78  tff(cinner$a, type, cinner$a: (B_ell2$ * B_ell2$) > Complex$).
% 18.39/6.78  tff(norm$, type, norm$: Complex$ > $real).
% 18.39/6.78  tff(fun_app$ai, type, fun_app$ai: (A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$) > A_ell2_a_ell2_cblinfun$).
% 18.39/6.78  tff(comp$n, type, comp$n: (B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(equivalent_registers$e, type, equivalent_registers$e: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(iso_register$i, type, iso_register$i: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(adj$e, type, adj$e: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$).
% 18.39/6.78  tff(complements$j, type, complements$j: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(id$c, type, id$c: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$).
% 18.39/6.78  tff(tensor_op$m, type, tensor_op$m: (B_ell2_a_ell2_cblinfun$ * A_ell2_a_ell2_cblinfun$) > B_a_prod_ell2_a_a_prod_ell2_cblinfun$).
% 18.39/6.78  tff(equivalent_registers$y, type, equivalent_registers$y: (A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$ * A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(regular_register$f, type, regular_register$f: A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(iso_register$q, type, iso_register$q: C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ > $o).
% 18.39/6.78  tff(complements$k, type, complements$k: (A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$ * B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$) > $o).
% 18.39/6.78  tff(ket$f, type, ket$f: A_a_b_complement_domain_prod$ > A_a_b_complement_domain_prod_ell2$).
% 18.39/6.78  
% 18.39/6.78  tff(f_40, axiom, is_unit_register$(empty_var$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom2)).
% 18.39/6.78  tff(f_38, negated_conjecture, ~is_unit_register$(empty_var$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture1)).
% 18.39/6.78  tff(c_6, plain, (is_unit_register$(empty_var$)), inference(cnfTransformation, [status(thm)], [f_40])).
% 18.39/6.78  tff(c_4, plain, (~is_unit_register$(empty_var$)), inference(cnfTransformation, [status(thm)], [f_38])).
% 18.39/6.78  tff(c_1929, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_6, c_4])).
% 18.39/6.78  % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------