%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 04:12:01 EDT 2023 % Result : Theorem 33.02s 5.21s % Output : Proof 60.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n013.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Sun Aug 27 14:01:17 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.60 ________ _____ % 0.20/0.60 ___ __ \_________(_)________________________________ % 0.20/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.60 % 0.20/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.60 (2023-06-19) % 0.20/0.60 % 0.20/0.60 (c) Philipp Rümmer, 2009-2023 % 0.20/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.60 Amanda Stjerna. % 0.20/0.60 Free software under BSD-3-Clause. % 0.20/0.60 % 0.20/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.60 % 0.20/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.62 Running up to 7 provers in parallel. % 0.20/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.50/1.21 Prover 6: Warning: Problem contains reals, using incomplete axiomatisation % 3.50/1.22 Prover 1: Warning: Problem contains reals, using incomplete axiomatisation % 3.50/1.22 Prover 0: Warning: Problem contains reals, using incomplete axiomatisation % 3.50/1.22 Prover 4: Warning: Problem contains reals, using incomplete axiomatisation % 3.86/1.22 Prover 2: Warning: Problem contains reals, using incomplete axiomatisation % 3.86/1.22 Prover 5: Warning: Problem contains reals, using incomplete axiomatisation % 3.86/1.22 Prover 3: Warning: Problem contains reals, using incomplete axiomatisation % 15.40/2.84 Prover 5: Preprocessing ... % 15.40/2.84 Prover 2: Preprocessing ... % 15.40/2.88 Prover 0: Preprocessing ... % 15.40/2.88 Prover 6: Preprocessing ... % 15.40/2.88 Prover 3: Preprocessing ... % 16.16/2.97 Prover 4: Preprocessing ... % 16.16/2.97 Prover 1: Preprocessing ... % 32.54/5.13 Prover 5: Constructing countermodel ... % 33.02/5.20 Prover 5: proved (4560ms) % 33.02/5.21 % 33.02/5.21 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.02/5.21 % 33.02/5.21 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 33.63/5.28 Prover 7: Warning: Problem contains reals, using incomplete axiomatisation % 36.16/5.62 Prover 1: Warning: ignoring some quantifiers % 37.46/5.78 Prover 3: Warning: ignoring some quantifiers % 37.93/5.85 Prover 3: Constructing countermodel ... % 37.93/5.86 Prover 6: Proving ... % 37.93/5.87 Prover 6: stopped % 37.93/5.87 Prover 1: Constructing countermodel ... % 37.93/5.87 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 37.93/5.88 Prover 3: stopped % 37.93/5.90 Prover 8: Warning: Problem contains reals, using incomplete axiomatisation % 37.93/5.90 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 38.84/5.98 Prover 10: Warning: Problem contains reals, using incomplete axiomatisation % 38.84/5.99 Prover 2: Constructing countermodel ... % 38.84/5.99 Prover 2: stopped % 38.84/6.01 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 39.51/6.05 Prover 11: Warning: Problem contains reals, using incomplete axiomatisation % 39.51/6.16 Prover 7: Preprocessing ... % 44.93/6.79 Prover 4: Warning: ignoring some quantifiers % 46.79/7.08 Prover 11: Preprocessing ... % 46.79/7.10 Prover 8: Preprocessing ... % 47.32/7.11 Prover 10: Preprocessing ... % 47.32/7.11 Prover 4: Constructing countermodel ... % 49.67/7.42 Prover 0: Proving ... % 49.67/7.42 Prover 0: stopped % 49.67/7.46 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 49.67/7.48 Prover 13: Warning: Problem contains reals, using incomplete axiomatisation % 54.38/8.08 Prover 7: Warning: ignoring some quantifiers % 55.11/8.14 Prover 13: Preprocessing ... % 55.11/8.17 Prover 1: Found proof (size 8) % 55.11/8.17 Prover 1: proved (7549ms) % 55.11/8.17 Prover 4: stopped % 55.56/8.21 Prover 10: Warning: ignoring some quantifiers % 55.56/8.32 Prover 7: Constructing countermodel ... % 55.56/8.34 Prover 7: stopped % 55.56/8.38 Prover 10: Constructing countermodel ... % 56.94/8.39 Prover 10: stopped % 57.21/8.47 Prover 8: Warning: ignoring some quantifiers % 57.21/8.49 Prover 13: stopped % 57.89/8.57 Prover 8: Constructing countermodel ... % 57.89/8.59 Prover 8: stopped % 58.88/8.86 Prover 11: Warning: ignoring some quantifiers % 59.48/8.99 Prover 11: Constructing countermodel ... % 59.48/9.00 Prover 11: stopped % 59.48/9.00 % 59.48/9.00 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.48/9.00 % 59.48/9.00 % SZS output start Proof for theBenchmark % 59.48/9.03 Assumptions after simplification: % 59.48/9.03 --------------------------------- % 59.48/9.03 % 59.48/9.03 (axiom2) % 59.48/9.05 is_unit_register$(empty_var$) = 0 & % 59.48/9.05 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$(empty_var$) % 59.48/9.05 % 59.48/9.05 (conjecture1) % 59.48/9.05 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$(empty_var$) & ? [v0: % 59.48/9.05 int] : ( ~ (v0 = 0) & is_unit_register$(empty_var$) = v0) % 59.48/9.05 % 59.48/9.05 (function-axioms) % 60.34/9.19 ! [v0: B_ell2_b_ell2_cblinfun$] : ! [v1: B_ell2_b_ell2_cblinfun$] : ! [v2: % 60.34/9.19 B_b_b_complement_domain_prod_ell2_b_b_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v3: % 60.34/9.19 B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.19 : ! [v4: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.19 (register_pair$g(v4, v3, v2) = v1) | ~ (register_pair$g(v4, v3, v2) = v0)) % 60.34/9.19 & ! [v0: A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! % 60.34/9.19 [v2: % 60.34/9.19 B_b_a_complement_domain_prod_ell2_b_b_a_complement_domain_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v3: % 60.34/9.19 B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.19 : ! [v4: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.19 (register_pair$f(v4, v3, v2) = v1) | ~ (register_pair$f(v4, v3, v2) = v0)) % 60.34/9.19 & ! [v0: A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! % 60.34/9.19 [v2: % 60.34/9.19 A_a_a_complement_domain_prod_ell2_a_a_a_complement_domain_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v3: % 60.34/9.19 A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.19 : ! [v4: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.19 (register_pair$e(v4, v3, v2) = v1) | ~ (register_pair$e(v4, v3, v2) = v0)) % 60.34/9.19 & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 % 60.34/9.19 | ~ (real_$quotient(v3, v2) = v1) | ~ (real_$quotient(v3, v2) = v0)) & ! % 60.34/9.19 [v0: $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 60.34/9.19 (real_$sum(v3, v2) = v1) | ~ (real_$sum(v3, v2) = v0)) & ! [v0: % 60.34/9.19 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 60.34/9.19 $real] : (v1 = v0 | ~ (real_$greatereq(v3, v2) = v1) | ~ % 60.34/9.19 (real_$greatereq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.19 MultipleValueBool] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 60.34/9.19 (real_$greater(v3, v2) = v1) | ~ (real_$greater(v3, v2) = v0)) & ! [v0: % 60.34/9.19 $real] : ! [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 60.34/9.19 (real_$difference(v3, v2) = v1) | ~ (real_$difference(v3, v2) = v0)) & ! % 60.34/9.19 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Complex$] : ! % 60.34/9.19 [v3: Complex$] : (v1 = v0 | ~ (less$(v3, v2) = v1) | ~ (less$(v3, v2) = v0)) % 60.34/9.19 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : % 60.34/9.19 ! [v3: $real] : (v1 = v0 | ~ (real_$less(v3, v2) = v1) | ~ (real_$less(v3, % 60.34/9.19 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 60.34/9.19 ! [v2: Complex_complex_cblinfun$] : ! [v3: Complex_complex_cblinfun$] : (v1 = % 60.34/9.19 v0 | ~ (less_eq$a(v3, v2) = v1) | ~ (less_eq$a(v3, v2) = v0)) & ! [v0: % 60.34/9.19 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $real] : ! [v3: % 60.34/9.19 $real] : (v1 = v0 | ~ (real_$lesseq(v3, v2) = v1) | ~ (real_$lesseq(v3, % 60.34/9.19 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 60.34/9.19 ! [v2: Complex$] : ! [v3: Complex$] : (v1 = v0 | ~ (less_eq$(v3, v2) = v1) | % 60.34/9.19 ~ (less_eq$(v3, v2) = v0)) & ! [v0: % 60.34/9.19 B_a_prod_a_b_complement_domain_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v1: % 60.34/9.19 B_a_prod_a_b_complement_domain_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v2: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : % 60.34/9.19 ! [v3: B_a_prod_ell2_b_a_prod_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$v(v3, % 60.34/9.19 v2) = v1) | ~ (tensor_op$v(v3, v2) = v0)) & ! [v0: % 60.34/9.19 B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v1: % 60.34/9.19 B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v2: % 60.34/9.19 B_a_prod_a_b_complement_domain_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v3: % 60.34/9.19 B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.19 : (v1 = v0 | ~ (cblinfun_compose$i(v3, v2) = v1) | ~ (cblinfun_compose$i(v3, % 60.34/9.19 v2) = v0)) & ! [v0: % 60.34/9.19 B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.19 : ! [v1: % 60.34/9.19 B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 B_a_a_b_complement_domain_prod_prod_ell2_b_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 B_a_prod_a_b_complement_domain_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : (v1 = v0 | ~ (cblinfun_compose$h(v3, v2) = v1) | ~ (cblinfun_compose$h(v3, % 60.34/9.20 v2) = v0)) & ! [v0: % 60.34/9.20 B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 B_a_a_b_complement_domain_prod_prod_ell2_b_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$u(v3, v2) = v1) % 60.34/9.20 | ~ (tensor_op$u(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_a_b_complement_domain_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_prod_a_b_complement_domain_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : % 60.34/9.20 ! [v3: A_a_prod_ell2_a_a_prod_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$t(v3, % 60.34/9.20 v2) = v1) | ~ (tensor_op$t(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_prod_a_b_complement_domain_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : (v1 = v0 | ~ (cblinfun_compose$g(v3, v2) = v1) | ~ (cblinfun_compose$g(v3, % 60.34/9.20 v2) = v0)) & ! [v0: % 60.34/9.20 A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_a_b_complement_domain_prod_prod_ell2_a_a_prod_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_prod_a_b_complement_domain_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : (v1 = v0 | ~ (cblinfun_compose$f(v3, v2) = v1) | ~ (cblinfun_compose$f(v3, % 60.34/9.20 v2) = v0)) & ! [v0: % 60.34/9.20 A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_a_b_complement_domain_prod_prod_ell2_a_a_a_b_complement_domain_prod_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$s(v3, v2) = v1) % 60.34/9.20 | ~ (tensor_op$s(v3, v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 60.34/9.20 $real] : ! [v3: $real] : (v1 = v0 | ~ (times$a(v3, v2) = v1) | ~ % 60.34/9.20 (times$a(v3, v2) = v0)) & ! [v0: % 60.34/9.20 Complex_complex_complex_prod_complex_complex_prod_fun_fun$] : ! [v1: % 60.34/9.20 Complex_complex_complex_prod_complex_complex_prod_fun_fun$] : ! [v2: % 60.34/9.20 Complex_complex_complex_fun_fun$] : ! [v3: % 60.34/9.20 Complex_complex_complex_fun_fun$] : (v1 = v0 | ~ (scale$(v3, v2) = v1) | ~ % 60.34/9.20 (scale$(v3, v2) = v0)) & ! [v0: Complex_complex_prod$] : ! [v1: % 60.34/9.20 Complex_complex_prod$] : ! [v2: Complex$] : ! [v3: Complex$] : (v1 = v0 | % 60.34/9.20 ~ (pair$e(v3, v2) = v1) | ~ (pair$e(v3, v2) = v0)) & ! [v0: $real] : ! % 60.34/9.20 [v1: $real] : ! [v2: $real] : ! [v3: $real] : (v1 = v0 | ~ % 60.34/9.20 (real_$product(v3, v2) = v1) | ~ (real_$product(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod$] : ! [v1: A_a_b_complement_domain_prod$] : ! % 60.34/9.20 [v2: A_b_complement_domain$] : ! [v3: A$] : (v1 = v0 | ~ (pair$d(v3, v2) = % 60.34/9.20 v1) | ~ (pair$d(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: A_ell2_b_ell2_cblinfun$] : % 60.34/9.20 ! [v3: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$r(v3, v2) = v1) | % 60.34/9.20 ~ (tensor_op$r(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: A_a_prod_ell2$] : ! [v3: % 60.34/9.20 A_b_prod_ell2$] : (v1 = v0 | ~ (butterfly$x(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$x(v3, v2) = v0)) & ! [v0: A_b_prod_ell2_a_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: A_b_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2_a_ell2_cblinfun$] : ! [v3: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$q(v3, v2) = v1) | ~ (tensor_op$q(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_b_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: A_b_prod_ell2$] : ! [v3: % 60.34/9.20 A_a_prod_ell2$] : (v1 = v0 | ~ (butterfly$w(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$w(v3, v2) = v0)) & ! [v0: A_b_prod_ell2_b_b_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: A_b_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v3: A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$p(v3, v2) = v1) | ~ (tensor_op$p(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_b_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v2: A_b_prod_ell2$] : ! [v3: % 60.34/9.20 B_b_prod_ell2$] : (v1 = v0 | ~ (butterfly$v(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$v(v3, v2) = v0)) & ! [v0: B_b_prod_ell2_a_b_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: B_b_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v3: B_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$o(v3, v2) = v1) | ~ (tensor_op$o(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_b_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_b_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: B_b_prod_ell2$] : ! [v3: % 60.34/9.20 A_b_prod_ell2$] : (v1 = v0 | ~ (butterfly$u(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$u(v3, v2) = v0)) & ! [v0: A_a_prod_ell2_b_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: A_a_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun$] : ! [v3: A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$n(v3, v2) = v1) | ~ (tensor_op$n(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_a_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v2: A_a_prod_ell2$] : ! [v3: % 60.34/9.20 B_a_prod_ell2$] : (v1 = v0 | ~ (butterfly$t(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$t(v3, v2) = v0)) & ! [v0: B_a_prod_ell2_a_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: B_a_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun$] : ! [v3: B_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$m(v3, v2) = v1) | ~ (tensor_op$m(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_a_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_a_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: B_a_prod_ell2$] : ! [v3: % 60.34/9.20 A_a_prod_ell2$] : (v1 = v0 | ~ (butterfly$s(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$s(v3, v2) = v0)) & ! [v0: A_a_prod_ell2_b_b_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: A_a_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_ell2_b_ell2_cblinfun$] : ! [v3: A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$l(v3, v2) = v1) | ~ (tensor_op$l(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_a_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v2: A_a_prod_ell2$] : ! [v3: % 60.34/9.20 B_b_prod_ell2$] : (v1 = v0 | ~ (butterfly$r(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$r(v3, v2) = v0)) & ! [v0: A_b_prod_ell2_b_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: A_b_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2_a_ell2_cblinfun$] : ! [v3: A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$k(v3, v2) = v1) | ~ (tensor_op$k(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_b_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v2: A_b_prod_ell2$] : ! [v3: % 60.34/9.20 B_a_prod_ell2$] : (v1 = v0 | ~ (butterfly$q(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$q(v3, v2) = v0)) & ! [v0: A_ell2_b_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_ell2_b_ell2_cblinfun$] : ! [v2: A_ell2$] : ! [v3: B_ell2$] : (v1 = v0 | % 60.34/9.20 ~ (butterfly$o(v3, v2) = v1) | ~ (butterfly$o(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: A_ell2_b_ell2_cblinfun$] : % 60.34/9.20 ! [v3: B_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$j(v3, v2) = v1) | % 60.34/9.20 ~ (tensor_op$j(v3, v2) = v0)) & ! [v0: A_b_prod$] : ! [v1: A_b_prod$] : ! % 60.34/9.20 [v2: B$] : ! [v3: A$] : (v1 = v0 | ~ (pair$b(v3, v2) = v1) | ~ (pair$b(v3, % 60.34/9.20 v2) = v0)) & ! [v0: B_a_prod$] : ! [v1: B_a_prod$] : ! [v2: A$] : ! % 60.34/9.20 [v3: B$] : (v1 = v0 | ~ (pair$c(v3, v2) = v1) | ~ (pair$c(v3, v2) = v0)) & % 60.34/9.20 ! [v0: B_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_a_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: B_a_prod_ell2$] : ! [v3: % 60.34/9.20 A_b_prod_ell2$] : (v1 = v0 | ~ (butterfly$p(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$p(v3, v2) = v0)) & ! [v0: B_ell2_a_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_ell2_a_ell2_cblinfun$] : ! [v2: B_ell2$] : ! [v3: A_ell2$] : (v1 = v0 | % 60.34/9.20 ~ (butterfly$m(v3, v2) = v1) | ~ (butterfly$m(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_b_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_b_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: B_ell2_a_ell2_cblinfun$] : % 60.34/9.20 ! [v3: B_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$i(v3, v2) = v1) | % 60.34/9.20 ~ (tensor_op$i(v3, v2) = v0)) & ! [v0: A_a_prod$] : ! [v1: A_a_prod$] : ! % 60.34/9.20 [v2: A$] : ! [v3: A$] : (v1 = v0 | ~ (pair$(v3, v2) = v1) | ~ (pair$(v3, % 60.34/9.20 v2) = v0)) & ! [v0: B_b_prod$] : ! [v1: B_b_prod$] : ! [v2: B$] : ! % 60.34/9.20 [v3: B$] : (v1 = v0 | ~ (pair$a(v3, v2) = v1) | ~ (pair$a(v3, v2) = v0)) & % 60.34/9.20 ! [v0: B_b_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_b_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: B_b_prod_ell2$] : ! [v3: % 60.34/9.20 A_a_prod_ell2$] : (v1 = v0 | ~ (butterfly$n(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$n(v3, v2) = v0)) & ! [v0: A_b_complement_domain_ell2$] : ! [v1: % 60.34/9.20 A_b_complement_domain_ell2$] : ! [v2: A_b_complement_domain_ell2$] : ! % 60.34/9.20 [v3: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : (v1 = % 60.34/9.20 v0 | ~ (cblinfun_apply$f(v3, v2) = v1) | ~ (cblinfun_apply$f(v3, v2) = % 60.34/9.20 v0)) & ! [v0: A_a_b_complement_domain_prod_ell2$] : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2$] : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2$] : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : (v1 = v0 | ~ (cblinfun_apply$e(v3, v2) = v1) | ~ (cblinfun_apply$e(v3, v2) % 60.34/9.20 = v0)) & ! [v0: B_b_prod_ell2$] : ! [v1: B_b_prod_ell2$] : ! [v2: % 60.34/9.20 B_ell2$] : ! [v3: B_ell2$] : (v1 = v0 | ~ (tensor_ell2$d(v3, v2) = v1) | % 60.34/9.20 ~ (tensor_ell2$d(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_b_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_b_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v2: B_b_prod_ell2$] : ! [v3: % 60.34/9.20 B_b_prod_ell2$] : (v1 = v0 | ~ (butterfly$l(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$l(v3, v2) = v0)) & ! [v0: B_b_prod_ell2_b_b_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: B_b_prod_ell2_b_b_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v3: B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$h(v3, v2) = v1) | ~ (tensor_op$h(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_a_prod_ell2$] : ! [v1: B_a_prod_ell2$] : ! [v2: A_ell2$] : ! [v3: % 60.34/9.20 B_ell2$] : (v1 = v0 | ~ (tensor_ell2$c(v3, v2) = v1) | ~ % 60.34/9.20 (tensor_ell2$c(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_a_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_a_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v2: B_a_prod_ell2$] : ! [v3: % 60.34/9.20 B_a_prod_ell2$] : (v1 = v0 | ~ (butterfly$k(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$k(v3, v2) = v0)) & ! [v0: B_a_prod_ell2_b_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: B_a_prod_ell2_b_a_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun$] : ! [v3: B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$g(v3, v2) = v1) | ~ (tensor_op$g(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_prod_ell2$] : ! [v1: A_b_prod_ell2$] : ! [v2: B_ell2$] : ! [v3: % 60.34/9.20 A_ell2$] : (v1 = v0 | ~ (tensor_ell2$b(v3, v2) = v1) | ~ % 60.34/9.20 (tensor_ell2$b(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_b_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: A_b_prod_ell2$] : ! [v3: % 60.34/9.20 A_b_prod_ell2$] : (v1 = v0 | ~ (butterfly$j(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$j(v3, v2) = v0)) & ! [v0: A_b_prod_ell2_a_b_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: A_b_prod_ell2_a_b_prod_ell2_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v3: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (tensor_op$f(v3, v2) = v1) | ~ (tensor_op$f(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_a_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: A_ell2_a_ell2_cblinfun$] : % 60.34/9.20 ! [v3: A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$] : (v1 % 60.34/9.20 = v0 | ~ (fun_app$ak(v3, v2) = v1) | ~ (fun_app$ak(v3, v2) = v0)) & ! % 60.34/9.20 [v0: A_a_prod_ell2$] : ! [v1: A_a_prod_ell2$] : ! [v2: A_ell2$] : ! [v3: % 60.34/9.20 A_ell2$] : (v1 = v0 | ~ (tensor_ell2$a(v3, v2) = v1) | ~ % 60.34/9.20 (tensor_ell2$a(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_a_prod_ell2_a_a_prod_ell2_cblinfun$] : ! [v2: A_a_prod_ell2$] : ! [v3: % 60.34/9.20 A_a_prod_ell2$] : (v1 = v0 | ~ (butterfly$i(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$i(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2$] : ! [v3: A_b_complement_domain_ell2$] : (v1 = % 60.34/9.20 v0 | ~ (butterfly$h(v3, v2) = v1) | ~ (butterfly$h(v3, v2) = v0)) & ! % 60.34/9.20 [v0: A_a_b_complement_domain_prod_ell2$] : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2$] : ! [v2: A_b_complement_domain_ell2$] : % 60.34/9.20 ! [v3: A_ell2$] : (v1 = v0 | ~ (tensor_ell2$(v3, v2) = v1) | ~ % 60.34/9.20 (tensor_ell2$(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: A_a_b_complement_domain_prod_ell2$] : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2$] : (v1 = v0 | ~ (butterfly$g(v3, v2) = % 60.34/9.20 v1) | ~ (butterfly$g(v3, v2) = v0)) & ! [v0: B_ell2$] : ! [v1: B_ell2$] % 60.34/9.20 : ! [v2: A_ell2$] : ! [v3: A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (cblinfun_apply$c(v3, v2) = v1) | ~ (cblinfun_apply$c(v3, v2) = v0)) & ! % 60.34/9.20 [v0: A_ell2$] : ! [v1: A_ell2$] : ! [v2: B_ell2$] : ! [v3: % 60.34/9.20 B_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (cblinfun_apply$d(v3, v2) = v1) | % 60.34/9.20 ~ (cblinfun_apply$d(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : (v1 = v0 | ~ (cblinfun_compose$d(v3, v2) = v1) | ~ (cblinfun_compose$d(v3, % 60.34/9.20 v2) = v0)) & ! [v0: Complex_b_ell2_cblinfun$] : ! [v1: % 60.34/9.20 Complex_b_ell2_cblinfun$] : ! [v2: Complex$] : ! [v3: B_ell2$] : (v1 = v0 % 60.34/9.20 | ~ (butterfly$e(v3, v2) = v1) | ~ (butterfly$e(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_ell2_complex_cblinfun$] : ! [v1: B_ell2_complex_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2$] : ! [v3: Complex$] : (v1 = v0 | ~ (butterfly$f(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$f(v3, v2) = v0)) & ! [v0: B_ell2_b_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v2: B_ell2_complex_cblinfun$] : ! [v3: % 60.34/9.20 Complex_b_ell2_cblinfun$] : (v1 = v0 | ~ (cblinfun_compose$c(v3, v2) = v1) % 60.34/9.20 | ~ (cblinfun_compose$c(v3, v2) = v0)) & ! [v0: Complex_a_ell2_cblinfun$] % 60.34/9.20 : ! [v1: Complex_a_ell2_cblinfun$] : ! [v2: Complex$] : ! [v3: A_ell2$] : % 60.34/9.20 (v1 = v0 | ~ (butterfly$c(v3, v2) = v1) | ~ (butterfly$c(v3, v2) = v0)) & ! % 60.34/9.20 [v0: A_ell2_complex_cblinfun$] : ! [v1: A_ell2_complex_cblinfun$] : ! [v2: % 60.34/9.20 A_ell2$] : ! [v3: Complex$] : (v1 = v0 | ~ (butterfly$d(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$d(v3, v2) = v0)) & ! [v0: A_ell2_a_ell2_cblinfun$] : ! [v1: % 60.34/9.20 A_ell2_a_ell2_cblinfun$] : ! [v2: A_ell2_complex_cblinfun$] : ! [v3: % 60.34/9.20 Complex_a_ell2_cblinfun$] : (v1 = v0 | ~ (cblinfun_compose$b(v3, v2) = v1) % 60.34/9.20 | ~ (cblinfun_compose$b(v3, v2) = v0)) & ! [v0: B_ell2_b_ell2_cblinfun$] : % 60.34/9.20 ! [v1: B_ell2_b_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$aj(v3, v2) = v1) | ~ (fun_app$aj(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_pair$h(v3, v2) = v1) | ~ (register_pair$h(v3, v2) = v0)) & ! % 60.34/9.20 [v0: A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$ai(v3, v2) = v1) | ~ (fun_app$ai(v3, v2) = v0)) & ! % 60.34/9.20 [v0: Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.20 Complex$] : ! [v3: Complex$] : (v1 = v0 | ~ (butterfly$b(v3, v2) = v1) | % 60.34/9.20 ~ (butterfly$b(v3, v2) = v0)) & ! [v0: Complex$] : ! [v1: Complex$] : ! % 60.34/9.20 [v2: B_ell2$] : ! [v3: B_ell2$] : (v1 = v0 | ~ (cinner$a(v3, v2) = v1) | ~ % 60.34/9.20 (cinner$a(v3, v2) = v0)) & ! [v0: B_ell2$] : ! [v1: B_ell2$] : ! [v2: % 60.34/9.20 B_ell2$] : ! [v3: B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.20 (cblinfun_apply$b(v3, v2) = v1) | ~ (cblinfun_apply$b(v3, v2) = v0)) & ! % 60.34/9.20 [v0: Complex$] : ! [v1: Complex$] : ! [v2: A_ell2$] : ! [v3: A_ell2$] : (v1 % 60.34/9.20 = v0 | ~ (cinner$(v3, v2) = v1) | ~ (cinner$(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_ell2$] : ! [v1: A_ell2$] : ! [v2: A_ell2$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (cblinfun_apply$a(v3, v2) = v1) | % 60.34/9.20 ~ (cblinfun_apply$a(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_b_b_complement_domain_prod_ell2_b_b_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 B_b_b_complement_domain_prod_ell2_b_b_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun$] : % 60.34/9.20 ! [v3: B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$d(v3, v2) = v1) | % 60.34/9.20 ~ (tensor_op$d(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_b_a_complement_domain_prod_ell2_b_b_a_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 B_b_a_complement_domain_prod_ell2_b_b_a_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun$] : % 60.34/9.20 ! [v3: B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$c(v3, v2) = v1) | % 60.34/9.20 ~ (tensor_op$c(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_a_complement_domain_prod_ell2_a_a_a_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_a_complement_domain_prod_ell2_a_a_a_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun$] : % 60.34/9.20 ! [v3: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$b(v3, v2) = v1) | % 60.34/9.20 ~ (tensor_op$b(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: A_ell2_a_ell2_cblinfun$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$ah(v3, v2) = v1) | ~ (fun_app$ah(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : % 60.34/9.20 ! [v3: % 60.34/9.20 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$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$ag(v3, v2) = v1) | ~ (fun_app$ag(v3, v2) = v0)) & ! % 60.34/9.20 [v0: A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! % 60.34/9.20 [v1: A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! % 60.34/9.20 [v2: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_pair$d(v3, v2) = v1) | ~ (register_pair$d(v3, v2) = v0)) & ! % 60.34/9.20 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (compatible$d(v3, v2) = v1) | ~ (compatible$d(v3, v2) = v0)) & ! [v0: % 60.34/9.20 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$] % 60.34/9.20 : ! [v1: % 60.34/9.20 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$] % 60.34/9.20 : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (register_pair$c(v3, v2) = v1) | ~ (register_pair$c(v3, v2) = % 60.34/9.20 v0)) & ! [v0: % 60.34/9.20 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$] % 60.34/9.20 : ! [v1: % 60.34/9.20 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$] % 60.34/9.20 : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_pair$b(v3, v2) = v1) | ~ (register_pair$b(v3, v2) = v0)) & ! % 60.34/9.20 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (complements$v(v3, v2) = v1) | ~ (complements$v(v3, v2) = % 60.34/9.20 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (compatible$c(v3, v2) = v1) | ~ (compatible$c(v3, v2) = v0)) % 60.34/9.20 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (compatible$b(v3, v2) = v1) | ~ (compatible$b(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$aw(v3, v2) = v1) | ~ (comp$aw(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$av(v3, v2) = v1) | ~ (comp$av(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (register_pair$a(v3, v2) = v1) | ~ (register_pair$a(v3, v2) = % 60.34/9.20 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (compatible$a(v3, v2) = v1) | ~ (compatible$a(v3, v2) = v0)) % 60.34/9.20 & ! [v0: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.20 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun_a_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$as(v3, v2) = v1) | ~ (comp$as(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$at(v3, v2) = v1) | ~ (comp$at(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$au(v3, v2) = v1) | ~ (comp$au(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 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$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$ar(v3, v2) = v1) | ~ (comp$ar(v3, v2) = v0)) & ! [v0: % 60.34/9.20 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (compatible$(v3, v2) = v1) | ~ (compatible$(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v1: B_ell2_b_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$af(v3, v2) = v1) | ~ (fun_app$af(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_pair$(v3, v2) = v1) | ~ (register_pair$(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 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$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$ae(v3, v2) = v1) | ~ (fun_app$ae(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: A_ell2_a_ell2_cblinfun$] : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : (v1 = v0 % 60.34/9.20 | ~ (tensor_op$a(v3, v2) = v1) | ~ (tensor_op$a(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 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$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | ~ (fun_app$ad(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 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$] % 60.34/9.20 : ! [v1: % 60.34/9.20 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$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$h(v3, v2) = v1) | ~ (register_tensor$h(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 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$] % 60.34/9.20 : (v1 = v0 | ~ (fun_app$ac(v3, v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.20 : ! [v2: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : % 60.34/9.20 ! [v3: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$(v3, v2) = v1) | ~ % 60.34/9.20 (tensor_op$(v3, v2) = v0)) & ! [v0: B_ell2_b_ell2_cblinfun$] : ! [v1: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v2: B_ell2$] : ! [v3: B_ell2$] : (v1 = v0 | % 60.34/9.20 ~ (butterfly$a(v3, v2) = v1) | ~ (butterfly$a(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! [v2: % 60.34/9.20 A_ell2$] : ! [v3: A_ell2$] : (v1 = v0 | ~ (butterfly$(v3, v2) = v1) | ~ % 60.34/9.20 (butterfly$(v3, v2) = v0)) & ! [v0: % 60.34/9.20 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$] % 60.34/9.20 : ! [v1: % 60.34/9.20 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$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (register_tensor$g(v3, v2) = v1) | ~ (register_tensor$g(v3, % 60.34/9.20 v2) = v0)) & ! [v0: % 60.34/9.20 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$f(v3, v2) = v1) | ~ (register_tensor$f(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$aq(v3, v2) = v1) | ~ (comp$aq(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 B_c_prod_ell2_b_c_prod_ell2_cblinfun_b_c_prod_ell2_b_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$e(v3, v2) = v1) | ~ (register_tensor$e(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$ap(v3, v2) = v1) | ~ (comp$ap(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$ao(v3, v2) = v1) | ~ (comp$ao(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$an(v3, v2) = v1) | ~ (comp$an(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$am(v3, v2) = v1) | ~ (comp$am(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$al(v3, v2) = v1) | ~ (comp$al(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$d(v3, v2) = v1) | ~ (register_tensor$d(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$ak(v3, v2) = v1) | ~ (comp$ak(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$c(v3, v2) = v1) | ~ (register_tensor$c(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$b(v3, v2) = v1) | ~ (register_tensor$b(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_a_prod_ell2_c_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$aj(v3, v2) = v1) | ~ (comp$aj(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$ai(v3, v2) = v1) | ~ (comp$ai(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_b_prod_ell2_c_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$a(v3, v2) = v1) | ~ (register_tensor$a(v3, v2) = v0)) & ! % 60.34/9.20 [v0: % 60.34/9.20 C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$ah(v3, v2) = v1) | ~ (comp$ah(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 C_c_prod_ell2_c_c_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (register_tensor$(v3, v2) = v1) | ~ (register_tensor$(v3, v2) = v0)) & ! % 60.34/9.20 [v0: A_ell2$] : ! [v1: A_ell2$] : ! [v2: A_ell2$] : ! [v3: Complex$] : (v1 % 60.34/9.20 = v0 | ~ (scaleC$j(v3, v2) = v1) | ~ (scaleC$j(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_ell2$] : ! [v1: B_ell2$] : ! [v2: B_ell2$] : ! [v3: Complex$] : (v1 = % 60.34/9.20 v0 | ~ (scaleC$i(v3, v2) = v1) | ~ (scaleC$i(v3, v2) = v0)) & ! [v0: % 60.34/9.20 Complex_complex_prod_complex_complex_prod_fun$] : ! [v1: % 60.34/9.20 Complex_complex_prod_complex_complex_prod_fun$] : ! [v2: Complex$] : ! % 60.34/9.20 [v3: Complex_complex_complex_prod_complex_complex_prod_fun_fun$] : (v1 = v0 | % 60.34/9.20 ~ (fun_app$ab(v3, v2) = v1) | ~ (fun_app$ab(v3, v2) = v0)) & ! [v0: % 60.34/9.20 Complex_complex_prod$] : ! [v1: Complex_complex_prod$] : ! [v2: % 60.34/9.20 Complex_complex_prod$] : ! [v3: % 60.34/9.20 Complex_complex_prod_complex_complex_prod_fun$] : (v1 = v0 | ~ % 60.34/9.20 (fun_app$aa(v3, v2) = v1) | ~ (fun_app$aa(v3, v2) = v0)) & ! [v0: % 60.34/9.20 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (complements$u(v3, v2) = v1) | ~ (complements$u(v3, v2) = % 60.34/9.20 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (complements$t(v3, v2) = v1) | ~ (complements$t(v3, v2) = v0)) & ! [v0: % 60.34/9.20 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (complements$s(v3, v2) = v1) | ~ (complements$s(v3, v2) = v0)) & ! [v0: % 60.34/9.20 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 Unit_unit_complement_domain_ell2_unit_unit_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (complements$r(v3, v2) = v1) | ~ (complements$r(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v1: B_ell2_b_ell2_cblinfun$] : ! [v2: % 60.34/9.20 C_ell2_c_ell2_cblinfun$] : ! [v3: % 60.34/9.20 C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (fun_app$z(v3, v2) = v1) | ~ (fun_app$z(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_ell2_c_ell2_cblinfun$] : ! [v1: C_ell2_c_ell2_cblinfun$] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun$] : ! [v3: % 60.34/9.20 B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (fun_app$y(v3, v2) = v1) | ~ (fun_app$y(v3, v2) = v0)) & ! [v0: Complex$] % 60.34/9.20 : ! [v1: Complex$] : ! [v2: A_ell2_a_ell2_cblinfun$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun_complex_fun$] : (v1 = v0 | ~ (fun_app$x(v3, v2) = % 60.34/9.20 v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: A_ell2_a_ell2_cblinfun$] : ! % 60.34/9.20 [v1: A_ell2_a_ell2_cblinfun$] : ! [v2: Complex$] : ! [v3: % 60.34/9.20 Complex_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ (fun_app$w(v3, v2) = % 60.34/9.20 v1) | ~ (fun_app$w(v3, v2) = v0)) & ! [v0: Complex$] : ! [v1: Complex$] % 60.34/9.20 : ! [v2: B_ell2_b_ell2_cblinfun$] : ! [v3: % 60.34/9.20 B_ell2_b_ell2_cblinfun_complex_fun$] : (v1 = v0 | ~ (fun_app$v(v3, v2) = % 60.34/9.20 v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: B_ell2_b_ell2_cblinfun$] : ! % 60.34/9.20 [v1: B_ell2_b_ell2_cblinfun$] : ! [v2: Complex$] : ! [v3: % 60.34/9.20 Complex_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ (fun_app$u(v3, v2) = % 60.34/9.20 v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: Complex$] : ! [v1: Complex$] % 60.34/9.20 : ! [v2: C_ell2_c_ell2_cblinfun$] : ! [v3: % 60.34/9.20 C_ell2_c_ell2_cblinfun_complex_fun$] : (v1 = v0 | ~ (fun_app$t(v3, v2) = % 60.34/9.20 v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: C_ell2_c_ell2_cblinfun$] : ! % 60.34/9.20 [v1: C_ell2_c_ell2_cblinfun$] : ! [v2: Complex$] : ! [v3: % 60.34/9.20 Complex_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ (fun_app$s(v3, v2) = % 60.34/9.20 v1) | ~ (fun_app$s(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.20 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun_complex_fun$] : ! [v3: % 60.34/9.20 Complex_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ (comp$af(v3, v2) = v1) % 60.34/9.20 | ~ (comp$af(v3, v2) = v0)) & ! [v0: Complex_complex_fun$] : ! [v1: % 60.34/9.20 Complex_complex_fun$] : ! [v2: Complex_a_ell2_a_ell2_cblinfun_fun$] : ! % 60.34/9.20 [v3: A_ell2_a_ell2_cblinfun_complex_fun$] : (v1 = v0 | ~ (comp$ag(v3, v2) = % 60.34/9.20 v1) | ~ (comp$ag(v3, v2) = v0)) & ! [v0: % 60.34/9.20 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.20 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun_complex_fun$] : ! [v3: % 60.34/9.20 Complex_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ (comp$ad(v3, v2) = v1) % 60.34/9.20 | ~ (comp$ad(v3, v2) = v0)) & ! [v0: Complex_complex_fun$] : ! [v1: % 60.34/9.20 Complex_complex_fun$] : ! [v2: Complex_b_ell2_b_ell2_cblinfun_fun$] : ! % 60.34/9.20 [v3: B_ell2_b_ell2_cblinfun_complex_fun$] : (v1 = v0 | ~ (comp$ae(v3, v2) = % 60.34/9.20 v1) | ~ (comp$ae(v3, v2) = v0)) & ! [v0: % 60.34/9.20 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.20 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.20 C_ell2_c_ell2_cblinfun_complex_fun$] : ! [v3: % 60.34/9.20 Complex_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ (comp$ab(v3, v2) = v1) % 60.34/9.20 | ~ (comp$ab(v3, v2) = v0)) & ! [v0: Complex_complex_fun$] : ! [v1: % 60.34/9.20 Complex_complex_fun$] : ! [v2: Complex_c_ell2_c_ell2_cblinfun_fun$] : ! % 60.34/9.20 [v3: C_ell2_c_ell2_cblinfun_complex_fun$] : (v1 = v0 | ~ (comp$ac(v3, v2) = % 60.34/9.20 v1) | ~ (comp$ac(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.20 MultipleValueBool] : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (equivalent_registers$y(v3, v2) = v1) | ~ % 60.34/9.20 (equivalent_registers$y(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.20 [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (equivalent_registers$x(v3, v2) = v1) | ~ (equivalent_registers$x(v3, v2) = % 60.34/9.20 v0)) & ! [v0: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! % 60.34/9.20 [v1: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (comp$aa(v3, v2) = v1) | ~ (comp$aa(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (comp$z(v3, v2) = v1) | ~ (comp$z(v3, v2) = v0)) & ! [v0: % 60.34/9.20 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : (v1 = v0 | ~ (equivalent_registers$w(v3, v2) = v1) | ~ % 60.34/9.20 (equivalent_registers$w(v3, v2) = v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (comp$y(v3, v2) = v1) | ~ (comp$y(v3, v2) = v0)) & ! [v0: % 60.34/9.20 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (equivalent_registers$v(v3, v2) = v1) | ~ (equivalent_registers$v(v3, v2) = % 60.34/9.20 v0)) & ! [v0: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v1: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v2: % 60.34/9.20 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.20 : ! [v3: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (comp$x(v3, v2) = v1) | ~ (comp$x(v3, v2) = v0)) & ! [v0: % 60.34/9.20 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (equivalent_registers$u(v3, v2) = v1) | ~ (equivalent_registers$u(v3, v2) = % 60.34/9.20 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (equivalent_registers$t(v3, v2) = v1) | ~ (equivalent_registers$t(v3, v2) = % 60.34/9.20 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.20 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.20 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.20 (equivalent_registers$s(v3, v2) = v1) | ~ (equivalent_registers$s(v3, v2) = % 60.34/9.21 v0)) & ! [v0: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : (v1 = v0 | % 60.34/9.21 ~ (comp$w(v3, v2) = v1) | ~ (comp$w(v3, v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$v(v3, v2) = v1) | ~ (comp$v(v3, v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$t(v3, v2) = v1) | ~ (comp$t(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$u(v3, v2) = v1) | ~ (comp$u(v3, v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$r(v3, v2) = v1) | ~ (comp$r(v3, v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$s(v3, v2) = v1) | ~ (comp$s(v3, v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_fun$] : ! [v1: Complex_complex_fun$] : ! [v2: % 60.34/9.21 Complex_complex_fun$] : ! [v3: % 60.34/9.21 Complex_complex_fun_complex_complex_fun_fun$] : (v1 = v0 | ~ (fun_app$r(v3, % 60.34/9.21 v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.21 Complex_complex_cblinfun$] : ! [v3: Complex$] : (v1 = v0 | ~ (scaleC$f(v3, % 60.34/9.21 v2) = v1) | ~ (scaleC$f(v3, v2) = v0)) & ! [v0: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun$] : ! [v1: Unit_ell2_unit_ell2_cblinfun$] : ! % 60.34/9.21 [v2: Unit_ell2_unit_ell2_cblinfun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : (v1 = v0 | % 60.34/9.21 ~ (fun_app$q(v3, v2) = v1) | ~ (fun_app$q(v3, v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun$] : ! [v1: C_ell2_c_ell2_cblinfun$] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (fun_app$p(v3, v2) = v1) | ~ (fun_app$p(v3, v2) = v0)) & ! % 60.34/9.21 [v0: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! % 60.34/9.21 [v1: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! % 60.34/9.21 [v2: A_ell2_a_ell2_cblinfun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (fun_app$o(v3, v2) = v1) | ~ (fun_app$o(v3, v2) = v0)) & ! % 60.34/9.21 [v0: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! % 60.34/9.21 [v1: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! % 60.34/9.21 [v2: C_ell2_c_ell2_cblinfun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | ~ (fun_app$n(v3, v2) = v0)) & ! % 60.34/9.21 [v0: C_ell2_c_ell2_cblinfun$] : ! [v1: C_ell2_c_ell2_cblinfun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : ! [v1: B_ell2_b_ell2_cblinfun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$l(v3, v2) = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : ! [v1: B_ell2_b_ell2_cblinfun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$i(v3, v2) = v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$r(v3, v2) = v1) | ~ (equivalent_registers$r(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$q(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$q(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$p(v3, v2) = v1) | ~ (equivalent_registers$p(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$o(v3, v2) = v1) | ~ (equivalent_registers$o(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : (v1 = v0 | % 60.34/9.21 ~ (equivalent_registers$n(v3, v2) = v1) | ~ (equivalent_registers$n(v3, % 60.34/9.21 v2) = v0)) & ! [v0: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$p(v3, v2) = v1) | ~ (comp$p(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$o(v3, v2) = v1) | ~ (comp$o(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$n(v3, v2) = v1) | ~ (comp$n(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$m(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$m(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 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$] % 60.34/9.21 : ! [v3: % 60.34/9.21 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$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$l(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$l(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 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$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$k(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$k(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 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$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$j(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$j(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$q(v3, v2) = v1) | ~ (complements$q(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 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$] % 60.34/9.21 : ! [v3: % 60.34/9.21 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$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$i(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$i(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$h(v3, v2) = v1) | ~ (equivalent_registers$h(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (complements$p(v3, v2) = v1) | ~ (complements$p(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 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$] % 60.34/9.21 : (v1 = v0 | ~ (complements$o(v3, v2) = v1) | ~ (complements$o(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (complements$n(v3, v2) = v1) | ~ (complements$n(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 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$] % 60.34/9.21 : (v1 = v0 | ~ (complements$m(v3, v2) = v1) | ~ (complements$m(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$l(v3, v2) = v1) | ~ (complements$l(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 % 60.34/9.21 | ~ (comp$m(v3, v2) = v1) | ~ (comp$m(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$l(v3, v2) = v1) | ~ (comp$l(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$k(v3, v2) = v1) | ~ (comp$k(v3, v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$j(v3, v2) = v1) | ~ (comp$j(v3, v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$i(v3, v2) = v1) | ~ (comp$i(v3, v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$h(v3, v2) = v1) | ~ (comp$h(v3, v2) = v0)) & ! [v0: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$g(v3, v2) = v1) | ~ (comp$g(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$f(v3, v2) = v1) | ~ (comp$f(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$e(v3, v2) = v1) | ~ (comp$e(v3, v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$d(v3, v2) = v1) | ~ (comp$d(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (comp$c(v3, v2) = v1) | ~ (comp$c(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (comp$b(v3, v2) = v1) | ~ (comp$b(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (fun_app$h(v3, v2) = v1) | ~ (fun_app$h(v3, v2) = v0)) & ! % 60.34/9.21 [v0: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$(v3, v2) = v1) | ~ (comp$(v3, v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun$] : ! [v1: C_ell2_c_ell2_cblinfun$] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$f(v3, v2) = v1) | ~ (fun_app$f(v3, v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun$] : ! [v1: C_ell2_c_ell2_cblinfun$] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun$] : ! [v3: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : ! [v3: Complex$] : (v1 = v0 | ~ (scaleC$c(v3, v2) = v1) | ~ (scaleC$c(v3, % 60.34/9.21 v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, v2) = v0)) & ! % 60.34/9.21 [v0: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! % 60.34/9.21 [v1: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! % 60.34/9.21 [v2: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : ! % 60.34/9.21 [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! % 60.34/9.21 [v0: A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : ! [v1: A_ell2_a_ell2_cblinfun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$k(v3, v2) = v1) | ~ (complements$k(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (complements$j(v3, v2) = v1) | ~ (complements$j(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (complements$i(v3, v2) = v1) | ~ (complements$i(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$h(v3, v2) = v1) | ~ (complements$h(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$g(v3, v2) = v1) | ~ (complements$g(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$f(v3, v2) = v1) | ~ (complements$f(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (complements$e(v3, v2) = v1) | ~ (complements$e(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$d(v3, v2) = v1) | ~ (complements$d(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$c(v3, v2) = v1) | ~ (complements$c(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 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$] % 60.34/9.21 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$b(v3, v2) = v1) | ~ (complements$b(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 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$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (complements$a(v3, v2) = v1) | ~ (complements$a(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complements$(v3, v2) = v1) | ~ (complements$(v3, v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$g(v3, v2) = v1) | ~ (equivalent_registers$g(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$f(v3, v2) = v1) | ~ (equivalent_registers$f(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$e(v3, v2) = v1) | ~ (equivalent_registers$e(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$d(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$d(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$c(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$c(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$b(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 60.34/9.21 [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v3: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (equivalent_registers$a(v3, v2) = v1) | ~ (equivalent_registers$a(v3, v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v3: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (equivalent_registers$(v3, v2) = v1) | ~ % 60.34/9.21 (equivalent_registers$(v3, v2) = v0)) & ! [v0: Complex_complex_fun$] : ! % 60.34/9.21 [v1: Complex_complex_fun$] : ! [v2: Complex$] : ! [v3: % 60.34/9.21 Complex_complex_complex_fun_fun$] : (v1 = v0 | ~ (fun_app$a(v3, v2) = v1) | % 60.34/9.21 ~ (fun_app$a(v3, v2) = v0)) & ! [v0: Complex$] : ! [v1: Complex$] : ! % 60.34/9.21 [v2: Complex$] : ! [v3: Complex_complex_fun$] : (v1 = v0 | ~ (fun_app$(v3, % 60.34/9.21 v2) = v1) | ~ (fun_app$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 60.34/9.21 ! [v1: MultipleValueBool] : ! [v2: $real] : (v1 = v0 | ~ (real_$is_int(v2) = % 60.34/9.21 v1) | ~ (real_$is_int(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.21 MultipleValueBool] : ! [v2: $real] : (v1 = v0 | ~ (real_$is_rat(v2) = v1) % 60.34/9.21 | ~ (real_$is_rat(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 60.34/9.21 $real] : (v1 = v0 | ~ (real_$floor(v2) = v1) | ~ (real_$floor(v2) = v0)) & % 60.34/9.21 ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 60.34/9.21 (real_$ceiling(v2) = v1) | ~ (real_$ceiling(v2) = v0)) & ! [v0: $real] : % 60.34/9.21 ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (real_$truncate(v2) = v1) | ~ % 60.34/9.21 (real_$truncate(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 60.34/9.21 $real] : (v1 = v0 | ~ (real_$round(v2) = v1) | ~ (real_$round(v2) = v0)) & % 60.34/9.21 ! [v0: int] : ! [v1: int] : ! [v2: $real] : (v1 = v0 | ~ (real_$to_int(v2) % 60.34/9.21 = v1) | ~ (real_$to_int(v2) = v0)) & ! [v0: $rat] : ! [v1: $rat] : ! % 60.34/9.21 [v2: $real] : (v1 = v0 | ~ (real_$to_rat(v2) = v1) | ~ (real_$to_rat(v2) = % 60.34/9.21 v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ % 60.34/9.21 (real_$to_real(v2) = v1) | ~ (real_$to_real(v2) = v0)) & ! [v0: $real] : % 60.34/9.21 ! [v1: $real] : ! [v2: int] : (v1 = v0 | ~ (int_$to_real(v2) = v1) | ~ % 60.34/9.21 (int_$to_real(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] % 60.34/9.21 : (v1 = v0 | ~ (real_$uminus(v2) = v1) | ~ (real_$uminus(v2) = v0)) & ! % 60.34/9.21 [v0: Complex_complex_fun$] : ! [v1: Complex_complex_fun$] : ! [v2: Complex$] % 60.34/9.21 : (v1 = v0 | ~ (minus$(v2) = v1) | ~ (minus$(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (is_Proj$a(v2) = v1) | ~ % 60.34/9.21 (is_Proj$a(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.21 MultipleValueBool] : ! [v2: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.21 (is_Proj$(v2) = v1) | ~ (is_Proj$(v2) = v0)) & ! [v0: $real] : ! [v1: % 60.34/9.21 $real] : ! [v2: $real] : (v1 = v0 | ~ (ln$(v2) = v1) | ~ (ln$(v2) = v0)) % 60.34/9.21 & ! [v0: $real] : ! [v1: $real] : ! [v2: $real] : (v1 = v0 | ~ (norm$f(v2) % 60.34/9.21 = v1) | ~ (norm$f(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 60.34/9.21 Complex_complex_cblinfun$] : (v1 = v0 | ~ (norm$e(v2) = v1) | ~ % 60.34/9.21 (norm$e(v2) = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (norm$d(v2) = v1) | ~ (norm$d(v2) % 60.34/9.21 = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (norm$c(v2) = v1) | ~ (norm$c(v2) % 60.34/9.21 = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: B_ell2$] : (v1 = v0 | % 60.34/9.21 ~ (norm$b(v2) = v1) | ~ (norm$b(v2) = v0)) & ! [v0: $real] : ! [v1: % 60.34/9.21 $real] : ! [v2: A_ell2$] : (v1 = v0 | ~ (norm$a(v2) = v1) | ~ (norm$a(v2) % 60.34/9.21 = v0)) & ! [v0: $real] : ! [v1: $real] : ! [v2: Complex$] : (v1 = v0 | % 60.34/9.21 ~ (norm$(v2) = v1) | ~ (norm$(v2) = v0)) & ! [v0: $real] : ! [v1: $real] % 60.34/9.21 : ! [v2: $real] : (v1 = v0 | ~ (arcosh$(v2) = v1) | ~ (arcosh$(v2) = v0)) & % 60.34/9.21 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Complex_complex_fun$] : (v1 = v0 | ~ (clinear$(v2) = v1) | ~ (clinear$(v2) % 60.34/9.21 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Complex_complex_fun$] : (v1 = v0 | ~ (antilinear_axioms$(v2) = v1) | ~ % 60.34/9.21 (antilinear_axioms$(v2) = v0)) & ! [v0: Complex_complex_cblinfun$] : ! % 60.34/9.21 [v1: Complex_complex_cblinfun$] : ! [v2: Complex$] : (v1 = v0 | ~ % 60.34/9.21 (cblinfun_mult_left$(v2) = v1) | ~ (cblinfun_mult_left$(v2) = v0)) & ! % 60.34/9.21 [v0: Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.21 Complex$] : (v1 = v0 | ~ (cblinfun_mult_right$(v2) = v1) | ~ % 60.34/9.21 (cblinfun_mult_right$(v2) = v0)) & ! [v0: Complex_complex_cblinfun$] : ! % 60.34/9.21 [v1: Complex_complex_cblinfun$] : ! [v2: Complex$] : (v1 = v0 | ~ % 60.34/9.21 (of_complex$(v2) = v1) | ~ (of_complex$(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_fun$] : ! [v1: Complex_complex_fun$] : ! [v2: Complex$] : % 60.34/9.21 (v1 = v0 | ~ (times$(v2) = v1) | ~ (times$(v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2$] : ! [v1: A_b_complement_domain_ell2$] : ! % 60.34/9.21 [v2: A_b_complement_domain$] : (v1 = v0 | ~ (ket$g(v2) = v1) | ~ (ket$g(v2) % 60.34/9.21 = v0)) & ! [v0: A_a_b_complement_domain_prod_ell2$] : ! [v1: % 60.34/9.21 A_a_b_complement_domain_prod_ell2$] : ! [v2: A_a_b_complement_domain_prod$] % 60.34/9.21 : (v1 = v0 | ~ (ket$f(v2) = v1) | ~ (ket$f(v2) = v0)) & ! [v0: % 60.34/9.21 A_b_prod_ell2$] : ! [v1: A_b_prod_ell2$] : ! [v2: A_b_prod$] : (v1 = v0 | % 60.34/9.21 ~ (ket$d(v2) = v1) | ~ (ket$d(v2) = v0)) & ! [v0: B_a_prod_ell2$] : ! % 60.34/9.21 [v1: B_a_prod_ell2$] : ! [v2: B_a_prod$] : (v1 = v0 | ~ (ket$e(v2) = v1) | % 60.34/9.21 ~ (ket$e(v2) = v0)) & ! [v0: A_a_prod_ell2$] : ! [v1: A_a_prod_ell2$] : ! % 60.34/9.21 [v2: A_a_prod$] : (v1 = v0 | ~ (ket$b(v2) = v1) | ~ (ket$b(v2) = v0)) & ! % 60.34/9.21 [v0: B_b_prod_ell2$] : ! [v1: B_b_prod_ell2$] : ! [v2: B_b_prod$] : (v1 = v0 % 60.34/9.21 | ~ (ket$c(v2) = v1) | ~ (ket$c(v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (tensor_op$e(v2) = v1) | ~ % 60.34/9.21 (tensor_op$e(v2) = v0)) & ! [v0: B_ell2_a_ell2_cblinfun$] : ! [v1: % 60.34/9.21 B_ell2_a_ell2_cblinfun$] : ! [v2: A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.21 (adj$h(v2) = v1) | ~ (adj$h(v2) = v0)) & ! [v0: A_ell2_b_ell2_cblinfun$] : % 60.34/9.21 ! [v1: A_ell2_b_ell2_cblinfun$] : ! [v2: B_ell2_a_ell2_cblinfun$] : (v1 = v0 % 60.34/9.21 | ~ (adj$g(v2) = v1) | ~ (adj$g(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.21 Complex_complex_cblinfun$] : (v1 = v0 | ~ (adj$f(v2) = v1) | ~ (adj$f(v2) % 60.34/9.21 = v0)) & ! [v0: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : (v1 = v0 | ~ (adj$d(v2) = v1) | ~ (adj$d(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_b_ell2_cblinfun$] : ! [v1: Complex_b_ell2_cblinfun$] : ! [v2: % 60.34/9.21 B_ell2$] : (v1 = v0 | ~ (vector_to_cblinfun$a(v2) = v1) | ~ % 60.34/9.21 (vector_to_cblinfun$a(v2) = v0)) & ! [v0: B_ell2_complex_cblinfun$] : ! % 60.34/9.21 [v1: B_ell2_complex_cblinfun$] : ! [v2: Complex_b_ell2_cblinfun$] : (v1 = v0 % 60.34/9.21 | ~ (adj$c(v2) = v1) | ~ (adj$c(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_a_ell2_cblinfun$] : ! [v1: Complex_a_ell2_cblinfun$] : ! [v2: % 60.34/9.21 A_ell2$] : (v1 = v0 | ~ (vector_to_cblinfun$(v2) = v1) | ~ % 60.34/9.21 (vector_to_cblinfun$(v2) = v0)) & ! [v0: A_ell2_complex_cblinfun$] : ! % 60.34/9.21 [v1: A_ell2_complex_cblinfun$] : ! [v2: Complex_a_ell2_cblinfun$] : (v1 = v0 % 60.34/9.21 | ~ (adj$b(v2) = v1) | ~ (adj$b(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.21 Complex$] : (v1 = v0 | ~ (cblinfun_cinner_right$(v2) = v1) | ~ % 60.34/9.21 (cblinfun_cinner_right$(v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : % 60.34/9.21 (v1 = v0 | ~ (cblinfun_compose$e(v2) = v1) | ~ (cblinfun_compose$e(v2) = % 60.34/9.21 v0)) & ! [v0: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! % 60.34/9.21 [v1: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (cblinfun_compose$a(v2) = v1) | ~ % 60.34/9.21 (cblinfun_compose$a(v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (cblinfun_compose$(v2) = v1) | ~ % 60.34/9.21 (cblinfun_compose$(v2) = v0)) & ! [v0: Complex_complex_fun$] : ! [v1: % 60.34/9.21 Complex_complex_fun$] : ! [v2: Complex$] : (v1 = v0 | ~ (cinner$b(v2) = % 60.34/9.21 v1) | ~ (cinner$b(v2) = v0)) & ! [v0: % 60.34/9.21 B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 B_b_complement_domain_ell2_b_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complement$d(v2) = v1) | ~ (complement$d(v2) = v0)) & ! [v0: % 60.34/9.21 B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 B_a_complement_domain_ell2_b_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complement$c(v2) = v1) | ~ (complement$c(v2) = v0)) & ! [v0: B_ell2$] : % 60.34/9.21 ! [v1: B_ell2$] : ! [v2: B$] : (v1 = v0 | ~ (ket$a(v2) = v1) | ~ (ket$a(v2) % 60.34/9.21 = v0)) & ! [v0: A_ell2$] : ! [v1: A_ell2$] : ! [v2: A$] : (v1 = v0 | ~ % 60.34/9.21 (ket$(v2) = v1) | ~ (ket$(v2) = v0)) & ! [v0: % 60.34/9.21 A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_a_complement_domain_ell2_a_a_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complement$b(v2) = v1) | ~ (complement$b(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (regular_register$g(v2) = v1) | ~ (regular_register$g(v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (regular_register$h(v2) = v1) | ~ (regular_register$h(v2) = % 60.34/9.21 v0)) & ! [v0: % 60.34/9.21 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$] % 60.34/9.21 : ! [v1: % 60.34/9.21 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$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (complement$a(v2) = v1) | ~ (complement$a(v2) = v0)) & ! % 60.34/9.21 [v0: Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.21 Complex$] : (v1 = v0 | ~ (cblinfun_scaleC_left$(v2) = v1) | ~ % 60.34/9.21 (cblinfun_scaleC_left$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.21 MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_a_prod_ell2_a_b_complement_domain_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$r(v2) = v1) | ~ (register$r(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.21 Complex$] : (v1 = v0 | ~ (cblinfun_scaleC_right$(v2) = v1) | ~ % 60.34/9.21 (cblinfun_scaleC_right$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.21 MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.21 (unitary$c(v2) = v1) | ~ (unitary$c(v2) = v0)) & ! [v0: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: A_a_b_complement_domain_prod_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.21 (sandwich$f(v2) = v1) | ~ (sandwich$f(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (unitary$b(v2) = v1) | ~ % 60.34/9.21 (unitary$b(v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (sandwich$e(v2) = v1) | ~ % 60.34/9.21 (sandwich$e(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.21 MultipleValueBool] : ! [v2: A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ % 60.34/9.21 (unitary$(v2) = v1) | ~ (unitary$(v2) = v0)) & ! [v0: MultipleValueBool] : % 60.34/9.21 ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : (v1 = v0 % 60.34/9.21 | ~ (unitary$a(v2) = v1) | ~ (unitary$a(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_fun$] : ! [v1: Complex_complex_fun$] : ! [v2: % 60.34/9.21 Complex_complex_cblinfun$] : (v1 = v0 | ~ (cblinfun_apply$(v2) = v1) | ~ % 60.34/9.21 (cblinfun_apply$(v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (complement$(v2) = v1) | ~ (complement$(v2) = v0)) & ! [v0: % 60.34/9.21 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$] % 60.34/9.21 : ! [v1: % 60.34/9.21 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$] % 60.34/9.21 : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : (v1 = v0 | ~ (sandwich$d(v2) = v1) | ~ (sandwich$d(v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun$] : % 60.34/9.21 (v1 = v0 | ~ (sandwich$c(v2) = v1) | ~ (sandwich$c(v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun$] : (v1 = v0 | ~ (sandwich$b(v2) = v1) | ~ % 60.34/9.21 (sandwich$b(v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun$] : (v1 = v0 | ~ (sandwich$a(v2) = v1) | ~ % 60.34/9.21 (sandwich$a(v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun$] : (v1 = v0 | ~ (sandwich$(v2) = v1) | ~ % 60.34/9.21 (sandwich$(v2) = v0)) & ! [v0: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : ! [v2: Complex$] : % 60.34/9.21 (v1 = v0 | ~ (scaleC$g(v2) = v1) | ~ (scaleC$g(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$q(v2) = v1) | ~ (register$q(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$u(v2) = v1) | ~ (iso_register$u(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$t(v2) = v1) | ~ (iso_register$t(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$p(v2) = v1) | ~ (register$p(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$o(v2) = v1) | ~ (register$o(v2) = v0)) & ! [v0: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun$] : ! [v1: Unit_ell2_unit_ell2_cblinfun$] : ! % 60.34/9.21 [v2: Complex$] : (v1 = v0 | ~ (one_dim_iso$f(v2) = v1) | ~ % 60.34/9.21 (one_dim_iso$f(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 60.34/9.21 MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : (v1 = v0 | % 60.34/9.21 ~ (register$n(v2) = v1) | ~ (register$n(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$s(v2) = v1) | ~ (iso_register$s(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$r(v2) = v1) | ~ (iso_register$r(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$q(v2) = v1) | ~ (iso_register$q(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$p(v2) = v1) | ~ (iso_register$p(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$m(v2) = v1) | ~ (register$m(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$o(v2) = v1) | ~ (iso_register$o(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$l(v2) = v1) | ~ (register$l(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_fun_complex_complex_fun_fun$] : ! [v1: % 60.34/9.21 Complex_complex_fun_complex_complex_fun_fun$] : ! [v2: % 60.34/9.21 Complex_complex_fun$] : (v1 = v0 | ~ (comp$q(v2) = v1) | ~ (comp$q(v2) = % 60.34/9.21 v0)) & ! [v0: Complex_complex_cblinfun$] : ! [v1: % 60.34/9.21 Complex_complex_cblinfun$] : ! [v2: Complex_complex_cblinfun$] : (v1 = v0 | % 60.34/9.21 ~ (one_dim_iso$c(v2) = v1) | ~ (one_dim_iso$c(v2) = v0)) & ! [v0: % 60.34/9.21 Complex$] : ! [v1: Complex$] : ! [v2: Complex_complex_cblinfun$] : (v1 = % 60.34/9.21 v0 | ~ (one_dim_iso$b(v2) = v1) | ~ (one_dim_iso$b(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_cblinfun$] : ! [v1: Complex_complex_cblinfun$] : ! [v2: % 60.34/9.21 Complex$] : (v1 = v0 | ~ (one_dim_iso$a(v2) = v1) | ~ (one_dim_iso$a(v2) = % 60.34/9.21 v0)) & ! [v0: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : ! [v2: % 60.34/9.21 Complex$] : (v1 = v0 | ~ (scaleC$e(v2) = v1) | ~ (scaleC$e(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$k(v2) = v1) | ~ (register$k(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$j(v2) = v1) | ~ (register$j(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$i(v2) = v1) | ~ (register$i(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$h(v2) = v1) | ~ (register$h(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$g(v2) = v1) | ~ (register$g(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$] : (v1 = v0 % 60.34/9.21 | ~ (regular_register$f(v2) = v1) | ~ (regular_register$f(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 % 60.34/9.21 | ~ (regular_register$d(v2) = v1) | ~ (regular_register$d(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 % 60.34/9.21 | ~ (regular_register$e(v2) = v1) | ~ (regular_register$e(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (regular_register$c(v2) = v1) | ~ (regular_register$c(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (regular_register$b(v2) = v1) | ~ (regular_register$b(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (regular_register$a(v2) = v1) | ~ (regular_register$a(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$n(v2) = v1) | ~ (iso_register$n(v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$] % 60.34/9.21 : ! [v2: B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (comp$a(v2) = v1) | ~ (comp$a(v2) = v0)) & ! [v0: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : ! [v2: Complex$] : % 60.34/9.21 (v1 = v0 | ~ (scaleC$d(v2) = v1) | ~ (scaleC$d(v2) = v0)) & ! [v0: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun$] % 60.34/9.21 : ! [v2: Unit_ell2_unit_ell2_cblinfun$] : (v1 = v0 | ~ (empty_var$c(v2) = % 60.34/9.21 v1) | ~ (empty_var$c(v2) = v0)) & ! [v0: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v1: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : ! [v2: Complex$] : (v1 = v0 | ~ (scaleC$b(v2) = v1) | ~ (scaleC$b(v2) = % 60.34/9.21 v0)) & ! [v0: Complex$] : ! [v1: Complex$] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun$] : (v1 = v0 | ~ (one_dim_iso$(v2) = v1) | ~ % 60.34/9.21 (one_dim_iso$(v2) = v0)) & ! [v0: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v1: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : ! [v2: Complex$] : % 60.34/9.21 (v1 = v0 | ~ (scaleC$a(v2) = v1) | ~ (scaleC$a(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$m(v2) = v1) | ~ (iso_register$m(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$l(v2) = v1) | ~ (iso_register$l(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (is_unit_register$j(v2) = v1) | ~ (is_unit_register$j(v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 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$] % 60.34/9.21 : (v1 = v0 | ~ (is_unit_register$i(v2) = v1) | ~ (is_unit_register$i(v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$k(v2) = v1) | ~ (iso_register$k(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 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$] % 60.34/9.21 : (v1 = v0 | ~ (is_unit_register$h(v2) = v1) | ~ (is_unit_register$h(v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$j(v2) = v1) | ~ (iso_register$j(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$f(v2) = v1) | ~ (register$f(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$e(v2) = v1) | ~ (register$e(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (register$d(v2) = v1) | ~ (register$d(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (is_unit_register$g(v2) = v1) | ~ (is_unit_register$g(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$c(v2) = v1) | ~ (register$c(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (is_unit_register$f(v2) = v1) | ~ (is_unit_register$f(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$b(v2) = v1) | ~ (register$b(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$a(v2) = v1) | ~ (register$a(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (is_unit_register$e(v2) = v1) | ~ (is_unit_register$e(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (register$(v2) = v1) | ~ (register$(v2) = v0)) & ! [v0: MultipleValueBool] % 60.34/9.21 : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$i(v2) = v1) | ~ (iso_register$i(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : (v1 = v0 | % 60.34/9.21 ~ (iso_register$h(v2) = v1) | ~ (iso_register$h(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$g(v2) = v1) | ~ (iso_register$g(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$f(v2) = v1) | ~ (iso_register$f(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$e(v2) = v1) | ~ (iso_register$e(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$d(v2) = v1) | ~ (iso_register$d(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$c(v2) = v1) | ~ (iso_register$c(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_unit_ell2_unit_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$b(v2) = v1) | ~ (iso_register$b(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (iso_register$a(v2) = v1) | ~ (iso_register$a(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_a_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (iso_register$(v2) = v1) | ~ (iso_register$(v2) = v0)) & ! % 60.34/9.21 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_b_complement_domain_ell2_a_b_complement_domain_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (is_unit_register$d(v2) = v1) | ~ (is_unit_register$d(v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (is_unit_register$b(v2) = v1) | ~ (is_unit_register$b(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (is_unit_register$c(v2) = v1) | ~ (is_unit_register$c(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_a_b_complement_domain_prod_ell2_a_a_b_complement_domain_prod_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] % 60.34/9.21 : (v1 = v0 | ~ (is_unit_register$a(v2) = v1) | ~ (is_unit_register$a(v2) = % 60.34/9.21 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (regular_register$(v2) = v1) | ~ (regular_register$(v2) = v0)) & ! [v0: % 60.34/9.21 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.34/9.21 Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 | ~ % 60.34/9.21 (is_unit_register$(v2) = v1) | ~ (is_unit_register$(v2) = v0)) & ! [v0: % 60.34/9.21 Complex_complex_fun$] : ! [v1: Complex_complex_fun$] : ! [v2: Complex$] : % 60.34/9.21 (v1 = v0 | ~ (uu$(v2) = v1) | ~ (uu$(v2) = v0)) % 60.34/9.21 % 60.34/9.21 Further assumptions not needed in the proof: % 60.34/9.21 -------------------------------------------- % 60.75/9.22 axiom0, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, axiom105, % 60.75/9.22 axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, axiom112, % 60.75/9.22 axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, axiom12, % 60.75/9.22 axiom120, axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, axiom127, % 60.75/9.22 axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, axiom134, % 60.75/9.22 axiom135, axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, axiom141, % 60.75/9.22 axiom142, axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, axiom149, % 60.75/9.22 axiom15, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, axiom156, % 60.75/9.22 axiom157, axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, axiom163, % 60.75/9.22 axiom164, axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, % 60.75/9.22 axiom171, axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, % 60.75/9.22 axiom179, axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, % 60.75/9.22 axiom186, axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, % 60.75/9.22 axiom193, axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, axiom20, % 60.75/9.22 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 60.75/9.22 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 60.75/9.22 axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, axiom220, axiom221, % 60.75/9.22 axiom222, axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, % 60.75/9.22 axiom23, axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, % 60.75/9.22 axiom237, axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, % 60.75/9.22 axiom244, axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, % 60.75/9.22 axiom251, axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, % 60.75/9.22 axiom259, axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, % 60.75/9.22 axiom266, axiom267, axiom268, axiom269, axiom27, axiom270, axiom271, axiom272, % 60.75/9.22 axiom273, axiom274, axiom275, axiom276, axiom277, axiom278, axiom279, axiom28, % 60.75/9.22 axiom280, axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, axiom287, % 60.75/9.22 axiom288, axiom289, axiom29, axiom290, axiom291, axiom292, axiom293, axiom294, % 60.75/9.22 axiom295, axiom296, axiom297, axiom298, axiom299, axiom3, axiom30, axiom300, % 60.75/9.22 axiom301, axiom302, axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, % 60.75/9.22 axiom309, axiom31, axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, % 60.75/9.22 axiom316, axiom317, axiom318, axiom319, axiom32, axiom320, axiom321, axiom322, % 60.75/9.22 axiom323, axiom324, axiom325, axiom326, axiom327, axiom328, axiom329, axiom33, % 60.75/9.22 axiom330, axiom331, axiom332, axiom333, axiom334, axiom335, axiom336, axiom337, % 60.75/9.22 axiom338, axiom339, axiom34, axiom340, axiom341, axiom342, axiom343, axiom344, % 60.75/9.22 axiom345, axiom346, axiom347, axiom348, axiom349, axiom35, axiom350, axiom351, % 60.75/9.22 axiom352, axiom353, axiom354, axiom355, axiom356, axiom357, axiom358, axiom359, % 60.75/9.22 axiom36, axiom360, axiom361, axiom362, axiom363, axiom364, axiom365, axiom366, % 60.75/9.22 axiom367, axiom368, axiom369, axiom37, axiom370, axiom371, axiom372, axiom373, % 60.75/9.22 axiom374, axiom375, axiom376, axiom377, axiom378, axiom379, axiom38, axiom380, % 60.75/9.22 axiom381, axiom382, axiom383, axiom384, axiom385, axiom386, axiom387, axiom388, % 60.75/9.22 axiom389, axiom39, axiom390, axiom391, axiom392, axiom393, axiom394, axiom395, % 60.75/9.22 axiom396, axiom397, axiom398, axiom399, axiom4, axiom40, axiom400, axiom401, % 60.75/9.22 axiom402, axiom403, axiom404, axiom405, axiom406, axiom407, axiom408, axiom409, % 60.75/9.22 axiom41, axiom410, axiom411, axiom412, axiom413, axiom414, axiom415, axiom416, % 60.75/9.22 axiom417, axiom418, axiom419, axiom42, axiom420, axiom421, axiom422, axiom423, % 60.75/9.22 axiom424, axiom425, axiom426, axiom427, axiom428, axiom429, axiom43, axiom430, % 60.75/9.22 axiom431, axiom432, axiom433, axiom434, axiom435, axiom436, axiom437, axiom438, % 60.75/9.22 axiom439, axiom44, axiom440, axiom441, axiom442, axiom443, axiom444, axiom445, % 60.75/9.22 axiom446, axiom447, axiom448, axiom449, axiom45, axiom450, axiom451, axiom452, % 60.75/9.22 axiom453, axiom454, axiom455, axiom456, axiom457, axiom458, axiom459, axiom46, % 60.75/9.22 axiom460, axiom461, axiom462, axiom463, axiom464, axiom465, axiom466, axiom467, % 60.75/9.22 axiom468, axiom469, axiom47, axiom470, axiom471, axiom472, axiom473, axiom474, % 60.75/9.22 axiom475, axiom476, axiom477, axiom478, axiom479, axiom48, axiom480, axiom481, % 60.75/9.22 axiom482, axiom483, axiom484, axiom485, axiom486, axiom487, axiom488, axiom489, % 60.75/9.22 axiom49, axiom490, axiom491, axiom492, axiom493, axiom494, axiom495, axiom496, % 60.75/9.22 axiom497, axiom498, axiom499, axiom5, axiom50, axiom500, axiom501, axiom502, % 60.75/9.22 axiom503, axiom504, axiom505, axiom506, axiom507, axiom508, axiom509, axiom51, % 60.75/9.22 axiom510, axiom511, axiom512, axiom513, axiom514, axiom515, axiom516, axiom517, % 60.75/9.22 axiom518, axiom519, axiom52, axiom520, axiom521, axiom522, axiom523, axiom524, % 60.75/9.22 axiom525, axiom526, axiom527, axiom528, axiom529, axiom53, axiom530, axiom531, % 60.75/9.22 axiom532, axiom533, axiom534, axiom535, axiom536, axiom537, axiom538, axiom539, % 60.75/9.22 axiom54, axiom540, axiom541, axiom542, axiom543, axiom544, axiom545, axiom546, % 60.75/9.22 axiom547, axiom548, axiom549, axiom55, axiom550, axiom551, axiom552, axiom553, % 60.75/9.22 axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, axiom56, axiom560, % 60.75/9.22 axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, axiom567, axiom568, % 60.75/9.22 axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, axiom574, axiom575, % 60.75/9.22 axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, axiom581, axiom582, % 60.75/9.22 axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, axiom589, axiom59, % 60.75/9.22 axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, axiom596, axiom597, % 60.75/9.22 axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, axiom602, axiom603, % 60.75/9.22 axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, axiom61, axiom610, % 60.75/9.22 axiom611, axiom612, axiom613, axiom614, axiom615, axiom616, axiom617, axiom618, % 60.75/9.22 axiom619, axiom62, axiom620, axiom621, axiom622, axiom623, axiom624, axiom625, % 60.75/9.22 axiom626, axiom627, axiom628, axiom629, axiom63, axiom630, axiom631, axiom632, % 60.75/9.22 axiom633, axiom634, axiom635, axiom636, axiom637, axiom638, axiom64, axiom65, % 60.75/9.22 axiom66, axiom67, axiom68, axiom69, axiom7, axiom70, axiom71, axiom72, axiom73, % 60.75/9.22 axiom74, axiom75, axiom76, axiom77, axiom78, axiom79, axiom8, axiom80, axiom81, % 60.75/9.22 axiom82, axiom83, axiom84, axiom85, axiom86, axiom87, axiom88, axiom89, axiom9, % 60.75/9.22 axiom90, axiom91, axiom92, axiom93, axiom94, axiom95, axiom96, axiom97, axiom98, % 60.75/9.22 axiom99, formula_640, formula_641 % 60.75/9.22 % 60.75/9.22 Those formulas are unsatisfiable: % 60.75/9.22 --------------------------------- % 60.75/9.22 % 60.75/9.22 Begin of proof % 60.75/9.22 | % 60.75/9.22 | ALPHA: (axiom2) implies: % 60.75/9.22 | (1) is_unit_register$(empty_var$) = 0 % 60.75/9.22 | % 60.75/9.22 | ALPHA: (conjecture1) implies: % 60.75/9.22 | (2) ? [v0: int] : ( ~ (v0 = 0) & is_unit_register$(empty_var$) = v0) % 60.75/9.22 | % 60.75/9.22 | ALPHA: (function-axioms) implies: % 60.75/9.22 | (3) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 60.75/9.22 | Unit_ell2_unit_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$] : (v1 = v0 % 60.75/9.22 | | ~ (is_unit_register$(v2) = v1) | ~ (is_unit_register$(v2) = v0)) % 60.75/9.22 | % 60.75/9.22 | DELTA: instantiating (2) with fresh symbol all_811_0 gives: % 60.75/9.22 | (4) ~ (all_811_0 = 0) & is_unit_register$(empty_var$) = all_811_0 % 60.75/9.22 | % 60.75/9.22 | ALPHA: (4) implies: % 60.75/9.22 | (5) ~ (all_811_0 = 0) % 60.75/9.22 | (6) is_unit_register$(empty_var$) = all_811_0 % 60.75/9.22 | % 60.75/9.22 | GROUND_INST: instantiating (3) with 0, all_811_0, empty_var$, simplifying with % 60.75/9.22 | (1), (6) gives: % 60.75/9.22 | (7) all_811_0 = 0 % 60.75/9.22 | % 60.75/9.22 | REDUCE: (5), (7) imply: % 60.75/9.22 | (8) $false % 60.75/9.23 | % 60.75/9.23 | CLOSE: (8) is inconsistent. % 60.75/9.23 | % 60.75/9.23 End of proof % 60.75/9.23 % SZS output end Proof for theBenchmark % 60.75/9.23 % 60.75/9.23 8621ms %------------------------------------------------------------------------------