%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW238+1 : TPTP v8.1.2. Released v5.2.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n012.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 : Fri Sep 1 00:49:33 EDT 2023 % Result : Theorem 59.26s 8.49s % Output : Proof 223.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW238+1 : TPTP v8.1.2. Released v5.2.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n012.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 17:59:25 EDT 2023 % 0.19/0.34 % CPUTime : % 0.19/0.63 ________ _____ % 0.19/0.63 ___ __ \_________(_)________________________________ % 0.19/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.63 % 0.19/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.63 (2023-06-19) % 0.19/0.63 % 0.19/0.63 (c) Philipp Rümmer, 2009-2023 % 0.19/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.63 Amanda Stjerna. % 0.19/0.63 Free software under BSD-3-Clause. % 0.19/0.63 % 0.19/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.63 % 0.19/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.64 Running up to 7 provers in parallel. % 0.19/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 17.34/3.22 Prover 1: Preprocessing ... % 17.34/3.23 Prover 4: Preprocessing ... % 18.92/3.24 Prover 6: Preprocessing ... % 18.92/3.24 Prover 2: Preprocessing ... % 18.92/3.24 Prover 0: Preprocessing ... % 18.92/3.24 Prover 3: Preprocessing ... % 18.92/3.24 Prover 5: Preprocessing ... % 49.61/7.30 Prover 1: Warning: ignoring some quantifiers % 50.38/7.38 Prover 3: Warning: ignoring some quantifiers % 51.84/7.54 Prover 3: Constructing countermodel ... % 51.84/7.56 Prover 1: Constructing countermodel ... % 53.90/7.81 Prover 6: Proving ... % 55.73/8.06 Prover 4: Warning: ignoring some quantifiers % 58.34/8.42 Prover 4: Constructing countermodel ... % 59.06/8.48 Prover 3: proved (7834ms) % 59.06/8.48 % 59.26/8.49 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 59.26/8.49 % 59.26/8.50 Prover 6: stopped % 59.26/8.51 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 59.26/8.52 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 61.87/8.91 Prover 5: Proving ... % 61.87/8.91 Prover 5: stopped % 61.87/8.93 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 65.81/9.35 Prover 0: Proving ... % 65.81/9.35 Prover 0: stopped % 65.81/9.35 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 72.10/10.18 Prover 8: Preprocessing ... % 72.10/10.18 Prover 2: Proving ... % 72.10/10.18 Prover 2: stopped % 72.10/10.18 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 73.27/10.33 Prover 7: Preprocessing ... % 74.62/10.52 Prover 10: Preprocessing ... % 77.46/10.90 Prover 11: Preprocessing ... % 80.41/11.27 Prover 13: Preprocessing ... % 86.92/12.12 Prover 10: Warning: ignoring some quantifiers % 87.64/12.18 Prover 8: Warning: ignoring some quantifiers % 88.21/12.32 Prover 7: Warning: ignoring some quantifiers % 88.21/12.38 Prover 10: Constructing countermodel ... % 89.36/12.45 Prover 8: Constructing countermodel ... % 90.90/12.62 Prover 7: Constructing countermodel ... % 102.30/14.12 Prover 13: Warning: ignoring some quantifiers % 103.26/14.22 Prover 11: Warning: ignoring some quantifiers % 105.99/14.57 Prover 13: Constructing countermodel ... % 105.99/14.60 Prover 11: Constructing countermodel ... % 116.86/15.99 Prover 1: stopped % 116.86/15.99 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 123.96/17.08 Prover 16: Preprocessing ... % 137.68/18.77 Prover 16: Warning: ignoring some quantifiers % 138.33/18.86 Prover 16: Constructing countermodel ... % 142.53/19.35 Prover 13: stopped % 142.68/19.37 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 149.87/20.34 Prover 19: Preprocessing ... % 154.23/20.88 Prover 16: stopped % 161.70/21.84 Prover 19: Warning: ignoring some quantifiers % 162.42/22.05 Prover 19: Constructing countermodel ... % 199.57/27.04 Prover 19: stopped % 207.89/27.99 Prover 4: stopped % 212.47/28.86 Prover 7: stopped % 222.56/30.70 Prover 10: Found proof (size 91) % 222.56/30.70 Prover 10: proved (21769ms) % 222.56/30.71 Prover 8: stopped % 222.56/30.71 Prover 11: stopped % 222.56/30.71 % 222.56/30.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 222.56/30.71 % 223.12/30.73 % SZS output start Proof for theBenchmark % 223.12/30.76 Assumptions after simplification: % 223.12/30.76 --------------------------------- % 223.12/30.76 % 223.12/30.76 (arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) % 223.12/30.77 $i(tc_Complex_Ocomplex) & class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) % 223.12/30.77 % 223.12/30.77 (conj_0) % 223.12/30.79 $i(v_aa____) & $i(v_c____) & $i(v_z____) & $i(tc_Complex_Ocomplex) & % 223.12/30.79 $i(tc_RealDef_Oreal) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 223.12/30.79 ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 223.12/30.79 (c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = v0 & % 223.12/30.79 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v4) = v5 & % 223.12/30.79 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v2) = v3 & % 223.12/30.79 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v6 & % 223.12/30.79 c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v_aa____, v2) = v4 & % 223.12/30.79 c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v5, v6) = v7 & hAPP(v1, % 223.12/30.79 v_c____) = v2 & hAPP(v0, v_z____) = v1 & $i(v7) & $i(v6) & $i(v5) & $i(v4) % 223.12/30.79 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ % 223.12/30.79 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v3, v7)) % 223.12/30.79 % 223.12/30.79 (fact__096cmod_A_Iz_A_K_Ac_J_A_060_061_Acmod_A_Iz_A_K_Ac_A_L_Aa_J_A_L_Acmod_Aa_096) % 223.12/30.80 $i(v_aa____) & $i(v_c____) & $i(v_z____) & $i(tc_Complex_Ocomplex) & % 223.12/30.80 $i(tc_RealDef_Oreal) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 223.12/30.80 ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 223.12/30.80 (c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = v0 & % 223.12/30.80 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v4) = v5 & % 223.12/30.80 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v2) = v3 & % 223.12/30.80 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v6 & % 223.12/30.80 c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v2, v_aa____) = v4 & % 223.12/30.80 c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v5, v6) = v7 & hAPP(v1, % 223.12/30.80 v_c____) = v2 & hAPP(v0, v_z____) = v1 & $i(v7) & $i(v6) & $i(v5) & $i(v4) % 223.12/30.80 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 223.12/30.80 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v3, v7)) % 223.12/30.80 % 223.12/30.80 (fact_ath) % 223.12/30.80 $i(v_da____) & $i(tc_RealDef_Oreal) & ? [v0: $i] : % 223.12/30.80 (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = v0 & $i(v0) & ! [v1: % 223.12/30.80 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 223.12/30.80 (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v2, v1) = v4) | ~ $i(v3) | % 223.12/30.80 ~ $i(v2) | ~ $i(v1) | ~ % 223.12/30.80 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v3, v4) | % 223.12/30.80 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v_da____, v2) | ? % 223.12/30.80 [v5: $i] : (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v0, v1) = v5 & % 223.12/30.80 $i(v5) & ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v5, % 223.12/30.80 v3)))) % 223.12/30.80 % 223.12/30.80 (fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) % 223.12/30.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 223.12/30.80 (c_Groups_Oplus__class_Oplus(v2, v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 223.12/30.80 $i(v0) | ~ class_Rings_Ocomm__semiring__1(v2) | % 223.12/30.80 (c_Groups_Oplus__class_Oplus(v2, v1, v0) = v3 & $i(v3))) % 223.12/30.80 % 223.12/30.80 (fact_h) % 223.12/30.80 $i(v_da____) & $i(v_aa____) & $i(v_c____) & $i(v_z____) & % 223.12/30.80 $i(tc_Complex_Ocomplex) & $i(tc_RealDef_Oreal) & ? [v0: $i] : ? [v1: $i] : % 223.12/30.80 ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 223.12/30.80 (c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal, v2, v3) = v4 & % 223.12/30.80 c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = v0 & % 223.12/30.80 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v1 & % 223.12/30.80 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_c____) = v3 & % 223.12/30.80 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_z____) = v5 & % 223.12/30.80 c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v0, v1) = v2 & $i(v5) & $i(v4) % 223.12/30.80 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 223.12/30.80 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v4, v5)) % 223.12/30.80 % 223.12/30.80 (fact_reduce__poly__simple) % 223.12/30.81 $i(tc_Nat_Onat) & $i(tc_Complex_Ocomplex) & $i(tc_RealDef_Oreal) & ? [v0: $i] % 223.12/30.81 : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 223.12/30.81 (c_Power_Opower__class_Opower(tc_Complex_Ocomplex) = v4 & % 223.12/30.81 c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v2 & % 223.12/30.81 c_Groups_Oone__class_Oone(tc_RealDef_Oreal) = v5 & % 223.12/30.81 c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = v1 & % 223.12/30.81 c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = v0 & % 223.12/30.81 c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = v3 & $i(v5) & $i(v4) & % 223.12/30.81 $i(v3) & $i(v2) & $i(v1) & $i(v0) & ? [v6: $i] : ! [v7: $i] : ! [v8: $i] % 223.12/30.81 : (v7 = v0 | v6 = v1 | ~ (hAPP(v3, v7) = v8) | ~ $i(v7) | ~ $i(v6) | ? % 223.12/30.81 [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? % 223.12/30.81 [v14: $i] : (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v13) = % 223.12/30.81 v14 & c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v2, v12) = v13 & % 223.12/30.81 hAPP(v10, v6) = v11 & hAPP(v8, v11) = v12 & hAPP(v4, v9) = v10 & $i(v14) % 223.12/30.81 & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & % 223.12/30.81 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal, v14, v5)))) % 223.12/30.81 % 223.12/30.81 (fact_th0) % 223.12/30.81 $i(v_da____) & $i(v_aa____) & $i(v_c____) & $i(v_z____) & % 223.12/30.81 $i(tc_Complex_Ocomplex) & $i(tc_RealDef_Oreal) & ? [v0: $i] : ? [v1: $i] : % 223.12/30.81 ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 223.12/30.81 (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = v0 & % 223.12/30.81 c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = v3 & % 223.12/30.81 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v5) = v6 & % 223.12/30.81 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v1 & % 223.12/30.81 c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v0, v1) = v2 & hAPP(v4, % 223.12/30.81 v_c____) = v5 & hAPP(v3, v_z____) = v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3) % 223.12/30.81 & $i(v2) & $i(v1) & $i(v0) & % 223.12/30.81 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v2, v6)) % 223.12/30.81 % 223.12/30.81 (function-axioms) % 223.12/30.82 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 223.12/30.82 $i] : ! [v6: $i] : (v1 = v0 | ~ (c_Polynomial_Opoly__rec(v6, v5, v4, v3, % 223.12/30.82 v2) = v1) | ~ (c_Polynomial_Opoly__rec(v6, v5, v4, v3, v2) = v0)) & ! % 223.12/30.82 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 223.12/30.82 : (v1 = v0 | ~ (c_If(v5, v4, v3, v2) = v1) | ~ (c_If(v5, v4, v3, v2) = v0)) % 223.12/30.82 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = % 223.12/30.82 v0 | ~ (c_Groups_Ominus__class_Ominus(v4, v3, v2) = v1) | ~ % 223.12/30.82 (c_Groups_Ominus__class_Ominus(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 223.12/30.82 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 223.12/30.82 (c_Divides_Odiv__class_Omod(v4, v3, v2) = v1) | ~ % 223.12/30.82 (c_Divides_Odiv__class_Omod(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 223.12/30.82 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 223.12/30.82 (c_Divides_Odiv__class_Odiv(v4, v3, v2) = v1) | ~ % 223.12/30.82 (c_Divides_Odiv__class_Odiv(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 223.12/30.82 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 223.12/30.82 (c_Power_Opower_Opower(v4, v3, v2) = v1) | ~ (c_Power_Opower_Opower(v4, v3, % 223.12/30.82 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 223.12/30.82 [v4: $i] : (v1 = v0 | ~ (c_Polynomial_Opcompose(v4, v3, v2) = v1) | ~ % 223.12/30.82 (c_Polynomial_Opcompose(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 223.12/30.82 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (c_Polynomial_Oorder(v4, % 223.12/30.82 v3, v2) = v1) | ~ (c_Polynomial_Oorder(v4, v3, v2) = v0)) & ! [v0: $i] % 223.12/30.82 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 223.12/30.82 (c_Polynomial_OpCons(v4, v3, v2) = v1) | ~ (c_Polynomial_OpCons(v4, v3, v2) % 223.12/30.82 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 223.12/30.82 $i] : (v1 = v0 | ~ (c_Rings_Oinverse__class_Odivide(v4, v3, v2) = v1) | ~ % 223.12/30.82 (c_Rings_Oinverse__class_Odivide(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 223.12/30.82 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 223.12/30.82 (c_Groups_Oplus__class_Oplus(v4, v3, v2) = v1) | ~ % 223.12/30.82 (c_Groups_Oplus__class_Oplus(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 223.12/30.82 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_RealDef_Oreal(v3, v2) = v1) | % 223.12/30.82 ~ (c_RealDef_Oreal(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 223.12/30.82 : ! [v3: $i] : (v1 = v0 | ~ (c_NthRoot_Oroot(v3, v2) = v1) | ~ % 223.12/30.82 (c_NthRoot_Oroot(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 223.12/30.82 ! [v3: $i] : (v1 = v0 | ~ % 223.12/30.82 (c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(v3, v2) = v1) | ~ % 223.12/30.82 (c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(v3, v2) = v0)) & ! [v0: % 223.12/30.82 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_fequal(v3, % 223.12/30.82 v2) = v1) | ~ (c_fequal(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 223.12/30.82 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_Polynomial_Opoly(v3, v2) = v1) | ~ % 223.12/30.82 (c_Polynomial_Opoly(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 223.12/30.82 : ! [v3: $i] : (v1 = v0 | ~ (tc_fun(v3, v2) = v1) | ~ (tc_fun(v3, v2) = % 223.12/30.82 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 223.12/30.82 ~ (c_Groups_Oabs__class_Oabs(v3, v2) = v1) | ~ % 223.12/30.82 (c_Groups_Oabs__class_Oabs(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 223.12/30.82 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_RealVector_Onorm__class_Onorm(v3, % 223.12/30.82 v2) = v1) | ~ (c_RealVector_Onorm__class_Onorm(v3, v2) = v0)) & ! [v0: % 223.12/30.82 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP(v3, v2) % 223.12/30.82 = v1) | ~ (hAPP(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 223.12/30.82 : (v1 = v0 | ~ (c_Power_Opower__class_Opower(v2) = v1) | ~ % 223.12/30.82 (c_Power_Opower__class_Opower(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 223.12/30.82 [v2: $i] : (v1 = v0 | ~ (c_RComplete_Onatfloor(v2) = v1) | ~ % 223.12/30.82 (c_RComplete_Onatfloor(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 223.12/30.82 : (v1 = v0 | ~ (c_RComplete_Onatceiling(v2) = v1) | ~ % 223.12/30.82 (c_RComplete_Onatceiling(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 223.12/30.82 $i] : (v1 = v0 | ~ (c_Groups_Oone__class_Oone(v2) = v1) | ~ % 223.12/30.82 (c_Groups_Oone__class_Oone(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 223.12/30.82 $i] : (v1 = v0 | ~ (tc_Polynomial_Opoly(v2) = v1) | ~ % 223.12/30.82 (tc_Polynomial_Opoly(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 223.12/30.82 (v1 = v0 | ~ (c_Groups_Ozero__class_Ozero(v2) = v1) | ~ % 223.12/30.82 (c_Groups_Ozero__class_Ozero(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 223.12/30.82 [v2: $i] : (v1 = v0 | ~ (c_Groups_Otimes__class_Otimes(v2) = v1) | ~ % 223.12/30.82 (c_Groups_Otimes__class_Otimes(v2) = v0)) % 223.12/30.82 % 223.12/30.82 Further assumptions not needed in the proof: % 223.12/30.82 -------------------------------------------- % 223.56/30.83 arity_Complex__Ocomplex__Fields_Ofield, % 223.56/30.83 arity_Complex__Ocomplex__Fields_Ofield__inverse__zero, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Oab__group__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Oab__semigroup__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Oab__semigroup__mult, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Ocancel__ab__semigroup__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Ocancel__comm__monoid__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Ocancel__semigroup__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Ocomm__monoid__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Ocomm__monoid__mult, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Ogroup__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Omonoid__add, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Omonoid__mult, % 223.56/30.83 arity_Complex__Ocomplex__Groups_Oone, arity_Complex__Ocomplex__Groups_Ozero, % 223.56/30.83 arity_Complex__Ocomplex__Int_Oring__char__0, % 223.56/30.83 arity_Complex__Ocomplex__Power_Opower, % 223.56/30.83 arity_Complex__Ocomplex__RealVector_Oreal__field, % 223.56/30.83 arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra, % 223.56/30.83 arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra__1, % 223.56/30.83 arity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra, % 223.56/30.83 arity_Complex__Ocomplex__RealVector_Oreal__normed__field, % 223.56/30.83 arity_Complex__Ocomplex__RealVector_Oreal__normed__vector, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Ocomm__ring, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Ocomm__ring__1, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Ocomm__semiring, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Ocomm__semiring__0, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Odivision__ring, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Odivision__ring__inverse__zero, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Odvd, arity_Complex__Ocomplex__Rings_Oidom, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Omult__zero, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Ono__zero__divisors, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Oring, arity_Complex__Ocomplex__Rings_Oring__1, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Oring__1__no__zero__divisors, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Osemiring, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Osemiring__0, % 223.56/30.83 arity_Complex__Ocomplex__Rings_Ozero__neq__one, % 223.56/30.83 arity_Complex__Ocomplex__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 223.56/30.83 arity_HOL__Obool__Orderings_Oord, arity_HOL__Obool__Orderings_Oorder, % 223.56/30.83 arity_HOL__Obool__Orderings_Opreorder, arity_Int__Oint__Divides_Oring__div, % 223.56/30.83 arity_Int__Oint__Divides_Osemiring__div, % 223.56/30.83 arity_Int__Oint__Groups_Oab__group__add, % 223.56/30.83 arity_Int__Oint__Groups_Oab__semigroup__add, % 223.56/30.83 arity_Int__Oint__Groups_Oab__semigroup__mult, % 223.56/30.83 arity_Int__Oint__Groups_Ocancel__ab__semigroup__add, % 223.56/30.83 arity_Int__Oint__Groups_Ocancel__comm__monoid__add, % 223.56/30.83 arity_Int__Oint__Groups_Ocancel__semigroup__add, % 223.56/30.83 arity_Int__Oint__Groups_Ocomm__monoid__add, % 223.56/30.83 arity_Int__Oint__Groups_Ocomm__monoid__mult, % 223.56/30.83 arity_Int__Oint__Groups_Ogroup__add, % 223.56/30.83 arity_Int__Oint__Groups_Olinordered__ab__group__add, % 223.56/30.83 arity_Int__Oint__Groups_Omonoid__add, arity_Int__Oint__Groups_Omonoid__mult, % 223.56/30.83 arity_Int__Oint__Groups_Oone, arity_Int__Oint__Groups_Oordered__ab__group__add, % 223.56/30.83 arity_Int__Oint__Groups_Oordered__ab__group__add__abs, % 223.56/30.83 arity_Int__Oint__Groups_Oordered__ab__semigroup__add, % 223.56/30.83 arity_Int__Oint__Groups_Oordered__ab__semigroup__add__imp__le, % 223.56/30.83 arity_Int__Oint__Groups_Oordered__cancel__ab__semigroup__add, % 223.56/30.83 arity_Int__Oint__Groups_Oordered__comm__monoid__add, % 223.56/30.83 arity_Int__Oint__Groups_Ozero, arity_Int__Oint__Int_Oring__char__0, % 223.56/30.83 arity_Int__Oint__Orderings_Olinorder, arity_Int__Oint__Orderings_Oord, % 223.56/30.83 arity_Int__Oint__Orderings_Oorder, arity_Int__Oint__Orderings_Opreorder, % 223.56/30.83 arity_Int__Oint__Power_Opower, arity_Int__Oint__Rings_Ocomm__ring, % 223.56/30.83 arity_Int__Oint__Rings_Ocomm__ring__1, arity_Int__Oint__Rings_Ocomm__semiring, % 223.56/30.83 arity_Int__Oint__Rings_Ocomm__semiring__0, % 223.56/30.83 arity_Int__Oint__Rings_Ocomm__semiring__1, arity_Int__Oint__Rings_Odvd, % 223.56/30.83 arity_Int__Oint__Rings_Oidom, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__comm__semiring__strict, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__idom, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__ring, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__ring__strict, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__semidom, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__semiring, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__semiring__1, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__semiring__1__strict, % 223.56/30.83 arity_Int__Oint__Rings_Olinordered__semiring__strict, % 223.56/30.83 arity_Int__Oint__Rings_Omult__zero, arity_Int__Oint__Rings_Ono__zero__divisors, % 223.56/30.83 arity_Int__Oint__Rings_Oordered__cancel__semiring, % 223.56/30.83 arity_Int__Oint__Rings_Oordered__comm__semiring, % 223.56/30.83 arity_Int__Oint__Rings_Oordered__ring, % 223.56/30.83 arity_Int__Oint__Rings_Oordered__ring__abs, % 223.56/30.83 arity_Int__Oint__Rings_Oordered__semiring, arity_Int__Oint__Rings_Oring, % 223.56/30.83 arity_Int__Oint__Rings_Oring__1, % 223.56/30.83 arity_Int__Oint__Rings_Oring__1__no__zero__divisors, % 223.56/30.83 arity_Int__Oint__Rings_Oring__no__zero__divisors, % 223.56/30.83 arity_Int__Oint__Rings_Osemiring, arity_Int__Oint__Rings_Osemiring__0, % 223.56/30.83 arity_Int__Oint__Rings_Ozero__neq__one, % 223.56/30.83 arity_Int__Oint__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 223.56/30.83 arity_Nat__Onat__Divides_Osemiring__div, % 223.56/30.83 arity_Nat__Onat__Groups_Oab__semigroup__add, % 223.56/30.83 arity_Nat__Onat__Groups_Oab__semigroup__mult, % 223.56/30.83 arity_Nat__Onat__Groups_Ocancel__ab__semigroup__add, % 223.56/30.83 arity_Nat__Onat__Groups_Ocancel__comm__monoid__add, % 223.56/30.83 arity_Nat__Onat__Groups_Ocancel__semigroup__add, % 223.56/30.83 arity_Nat__Onat__Groups_Ocomm__monoid__add, % 223.56/30.83 arity_Nat__Onat__Groups_Ocomm__monoid__mult, % 223.56/30.83 arity_Nat__Onat__Groups_Omonoid__add, arity_Nat__Onat__Groups_Omonoid__mult, % 223.56/30.83 arity_Nat__Onat__Groups_Oone, % 223.56/30.83 arity_Nat__Onat__Groups_Oordered__ab__semigroup__add, % 223.56/30.83 arity_Nat__Onat__Groups_Oordered__ab__semigroup__add__imp__le, % 223.56/30.83 arity_Nat__Onat__Groups_Oordered__cancel__ab__semigroup__add, % 223.56/30.83 arity_Nat__Onat__Groups_Oordered__comm__monoid__add, % 223.56/30.83 arity_Nat__Onat__Groups_Ozero, arity_Nat__Onat__Orderings_Olinorder, % 223.56/30.83 arity_Nat__Onat__Orderings_Oord, arity_Nat__Onat__Orderings_Oorder, % 223.56/30.83 arity_Nat__Onat__Orderings_Opreorder, arity_Nat__Onat__Power_Opower, % 223.56/30.83 arity_Nat__Onat__Rings_Ocomm__semiring, % 223.56/30.83 arity_Nat__Onat__Rings_Ocomm__semiring__0, % 223.56/30.83 arity_Nat__Onat__Rings_Ocomm__semiring__1, arity_Nat__Onat__Rings_Odvd, % 223.56/30.83 arity_Nat__Onat__Rings_Olinordered__comm__semiring__strict, % 223.56/30.83 arity_Nat__Onat__Rings_Olinordered__semidom, % 223.56/30.83 arity_Nat__Onat__Rings_Olinordered__semiring, % 223.56/30.83 arity_Nat__Onat__Rings_Olinordered__semiring__strict, % 223.56/30.83 arity_Nat__Onat__Rings_Omult__zero, arity_Nat__Onat__Rings_Ono__zero__divisors, % 223.56/30.83 arity_Nat__Onat__Rings_Oordered__cancel__semiring, % 223.56/30.83 arity_Nat__Onat__Rings_Oordered__comm__semiring, % 223.56/30.83 arity_Nat__Onat__Rings_Oordered__semiring, arity_Nat__Onat__Rings_Osemiring, % 223.56/30.83 arity_Nat__Onat__Rings_Osemiring__0, arity_Nat__Onat__Rings_Ozero__neq__one, % 223.56/30.83 arity_Nat__Onat__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 223.56/30.83 arity_Polynomial__Opoly__Divides_Oring__div, % 223.56/30.83 arity_Polynomial__Opoly__Divides_Osemiring__div, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oab__group__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oab__semigroup__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oab__semigroup__mult, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Ocancel__ab__semigroup__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Ocancel__comm__monoid__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Ocancel__semigroup__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Ocomm__monoid__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Ocomm__monoid__mult, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Ogroup__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Olinordered__ab__group__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Omonoid__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Omonoid__mult, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oone, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oordered__ab__group__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oordered__ab__group__add__abs, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oordered__ab__semigroup__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oordered__ab__semigroup__add__imp__le, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oordered__cancel__ab__semigroup__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Oordered__comm__monoid__add, % 223.56/30.83 arity_Polynomial__Opoly__Groups_Ozero, % 223.56/30.83 arity_Polynomial__Opoly__Int_Oring__char__0, % 223.56/30.83 arity_Polynomial__Opoly__Orderings_Olinorder, % 223.56/30.83 arity_Polynomial__Opoly__Orderings_Oord, % 223.56/30.83 arity_Polynomial__Opoly__Orderings_Oorder, % 223.56/30.83 arity_Polynomial__Opoly__Orderings_Opreorder, % 223.56/30.83 arity_Polynomial__Opoly__Power_Opower, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Ocomm__ring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Ocomm__ring__1, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Ocomm__semiring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Ocomm__semiring__0, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Ocomm__semiring__1, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Odvd, arity_Polynomial__Opoly__Rings_Oidom, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__comm__semiring__strict, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__idom, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__ring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__ring__strict, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__semidom, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__semiring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__semiring__1, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__semiring__1__strict, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Olinordered__semiring__strict, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Omult__zero, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Ono__zero__divisors, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oordered__cancel__semiring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oordered__comm__semiring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oordered__ring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oordered__ring__abs, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oordered__semiring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oring, arity_Polynomial__Opoly__Rings_Oring__1, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oring__1__no__zero__divisors, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Oring__no__zero__divisors, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Osemiring, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Osemiring__0, % 223.56/30.83 arity_Polynomial__Opoly__Rings_Ozero__neq__one, % 223.56/30.83 arity_Polynomial__Opoly__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 223.56/30.83 arity_RealDef__Oreal__Fields_Ofield, % 223.56/30.83 arity_RealDef__Oreal__Fields_Ofield__inverse__zero, % 223.56/30.83 arity_RealDef__Oreal__Fields_Olinordered__field, % 223.56/30.83 arity_RealDef__Oreal__Fields_Olinordered__field__inverse__zero, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oab__group__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oab__semigroup__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oab__semigroup__mult, % 223.56/30.83 arity_RealDef__Oreal__Groups_Ocancel__ab__semigroup__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Ocancel__comm__monoid__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Ocancel__semigroup__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Ocomm__monoid__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Ocomm__monoid__mult, % 223.56/30.83 arity_RealDef__Oreal__Groups_Ogroup__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Olinordered__ab__group__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Omonoid__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Omonoid__mult, arity_RealDef__Oreal__Groups_Oone, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oordered__ab__group__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Oordered__comm__monoid__add, % 223.56/30.83 arity_RealDef__Oreal__Groups_Ozero, arity_RealDef__Oreal__Int_Oring__char__0, % 223.56/30.83 arity_RealDef__Oreal__Orderings_Olinorder, arity_RealDef__Oreal__Orderings_Oord, % 223.56/30.83 arity_RealDef__Oreal__Orderings_Oorder, % 223.56/30.83 arity_RealDef__Oreal__Orderings_Opreorder, arity_RealDef__Oreal__Power_Opower, % 223.56/30.83 arity_RealDef__Oreal__RealVector_Oreal__field, % 223.56/30.83 arity_RealDef__Oreal__RealVector_Oreal__normed__algebra, % 223.56/30.83 arity_RealDef__Oreal__RealVector_Oreal__normed__algebra__1, % 223.56/30.83 arity_RealDef__Oreal__RealVector_Oreal__normed__div__algebra, % 223.56/30.83 arity_RealDef__Oreal__RealVector_Oreal__normed__field, % 223.56/30.83 arity_RealDef__Oreal__RealVector_Oreal__normed__vector, % 223.56/30.83 arity_RealDef__Oreal__Rings_Ocomm__ring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Ocomm__ring__1, % 223.56/30.83 arity_RealDef__Oreal__Rings_Ocomm__semiring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Ocomm__semiring__0, % 223.56/30.83 arity_RealDef__Oreal__Rings_Ocomm__semiring__1, % 223.56/30.83 arity_RealDef__Oreal__Rings_Odivision__ring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Odivision__ring__inverse__zero, % 223.56/30.83 arity_RealDef__Oreal__Rings_Odvd, arity_RealDef__Oreal__Rings_Oidom, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__comm__semiring__strict, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__idom, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__ring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__ring__strict, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__semidom, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__semiring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__semiring__1, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__semiring__1__strict, % 223.56/30.83 arity_RealDef__Oreal__Rings_Olinordered__semiring__strict, % 223.56/30.83 arity_RealDef__Oreal__Rings_Omult__zero, % 223.56/30.83 arity_RealDef__Oreal__Rings_Ono__zero__divisors, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oordered__cancel__semiring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oordered__comm__semiring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oordered__ring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oordered__ring__abs, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oordered__semiring, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oring, arity_RealDef__Oreal__Rings_Oring__1, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oring__1__no__zero__divisors, % 223.56/30.83 arity_RealDef__Oreal__Rings_Oring__no__zero__divisors, % 223.56/30.83 arity_RealDef__Oreal__Rings_Osemiring, arity_RealDef__Oreal__Rings_Osemiring__0, % 223.56/30.83 arity_RealDef__Oreal__Rings_Ozero__neq__one, % 223.56/30.83 arity_RealDef__Oreal__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 223.56/30.83 arity_fun__Orderings_Oord, arity_fun__Orderings_Oorder, % 223.56/30.83 arity_fun__Orderings_Opreorder, fact_BseqD, fact_BseqI, fact_BseqI2_H, % 223.56/30.83 fact_Bseq__def, fact_DERIV__mult__lemma, fact_DIVISION__BY__ZERO, % 223.56/30.83 fact_Divides_Otransfer__nat__int__function__closures_I1_J, % 223.56/30.83 fact_Divides_Otransfer__nat__int__function__closures_I2_J, % 223.56/30.83 fact_LIMSEQ__inverse__realpow__zero__lemma, fact_Nat_Oadd__0__right, % 223.56/30.83 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J, % 223.56/30.83 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J, % 223.56/30.83 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J, % 223.56/30.83 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J, % 223.56/30.83 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J, % 223.56/30.83 fact__0960_A_060_Acmod_Ac_096, fact_ab__semigroup__add__class_Oadd__ac_I1_J, % 223.56/30.83 fact_ab__semigroup__mult__class_Omult__ac_I1_J, fact_abs__add__abs, % 223.56/30.83 fact_abs__add__one__gt__zero, fact_abs__add__one__not__less__self, % 223.56/30.83 fact_abs__diff__less__iff, fact_abs__diff__triangle__ineq, fact_abs__div, % 223.56/30.83 fact_abs__div__pos, fact_abs__divide, fact_abs__dvd__iff, fact_abs__eq__0, % 223.56/30.83 fact_abs__eq__mult, fact_abs__ge__self, fact_abs__ge__zero, % 223.56/30.83 fact_abs__idempotent, fact_abs__le__D1, fact_abs__le__zero__iff, % 223.56/30.83 fact_abs__minus__commute, fact_abs__mult, fact_abs__mult__less, % 223.56/30.83 fact_abs__mult__pos, fact_abs__mult__self, fact_abs__norm__cancel, % 223.56/30.83 fact_abs__not__less__zero, fact_abs__of__nonneg, fact_abs__of__pos, % 223.56/30.83 fact_abs__one, fact_abs__real__of__nat__cancel, fact_abs__triangle__ineq, % 223.56/30.83 fact_abs__triangle__ineq2, fact_abs__triangle__ineq2__sym, % 223.56/30.83 fact_abs__triangle__ineq3, fact_abs__triangle__ineq4, fact_abs__zero, % 223.56/30.83 fact_abs__zmult__eq__1, fact_add1__zle__eq, fact_add_Ocomm__neutral, % 223.56/30.83 fact_add__0, fact_add__0__iff, fact_add__0__left, fact_add__0__right, % 223.56/30.83 fact_add__diff__cancel, fact_add__divide__distrib, fact_add__divide__eq__iff, % 223.56/30.83 fact_add__eq__self__zero, fact_add__frac__eq, fact_add__frac__num, % 223.56/30.83 fact_add__gr__0, fact_add__imp__eq, fact_add__increasing, fact_add__increasing2, % 223.56/30.83 fact_add__is__0, fact_add__leD1, fact_add__leD2, fact_add__leE, % 223.56/30.83 fact_add__le__cancel__left, fact_add__le__cancel__right, % 223.56/30.83 fact_add__le__imp__le__left, fact_add__le__imp__le__right, % 223.56/30.83 fact_add__le__less__mono, fact_add__le__mono, fact_add__le__mono1, % 223.56/30.83 fact_add__left__cancel, fact_add__left__imp__eq, fact_add__left__mono, % 223.56/30.83 fact_add__lessD1, fact_add__less__cancel__left, fact_add__less__cancel__right, % 223.56/30.83 fact_add__less__imp__less__left, fact_add__less__imp__less__right, % 223.56/30.83 fact_add__less__le__mono, fact_add__less__mono, fact_add__less__mono1, % 223.56/30.83 fact_add__mono, fact_add__mult__distrib, fact_add__mult__distrib2, % 223.56/30.83 fact_add__neg__neg, fact_add__neg__nonpos, fact_add__nonneg__eq__0__iff, % 223.56/30.83 fact_add__nonneg__nonneg, fact_add__nonneg__pos, fact_add__nonpos__neg, % 223.56/30.83 fact_add__nonpos__nonpos, fact_add__num__frac, fact_add__pCons, % 223.56/30.83 fact_add__poly__code_I1_J, fact_add__poly__code_I2_J, fact_add__pos__nonneg, % 223.56/30.83 fact_add__pos__pos, fact_add__right__cancel, fact_add__right__imp__eq, % 223.56/30.83 fact_add__right__mono, fact_add__scale__eq__noteq, fact_add__strict__increasing, % 223.56/30.83 fact_add__strict__increasing2, fact_add__strict__left__mono, % 223.56/30.83 fact_add__strict__mono, fact_add__strict__right__mono, fact_assms, fact_c0, % 223.56/30.83 fact_calculation, fact_combine__common__factor, fact_comm__mult__left__mono, % 223.56/30.83 fact_comm__mult__strict__left__mono, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I8_J, % 223.56/30.83 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J, % 223.56/30.83 fact_comm__semiring__class_Odistrib, fact_complex__mod__triangle__sub, % 223.56/30.83 fact_convex__bound__le, fact_convex__bound__lt, fact_crossproduct__eq, % 223.56/30.83 fact_crossproduct__noteq, fact_cs0, fact_cs0_H, fact_decr__lemma, % 223.56/30.83 fact_decseq__def, fact_diff__0__right, fact_diff__add__cancel, % 223.56/30.83 fact_diff__divide__distrib, fact_diff__divide__eq__iff, fact_diff__eq__diff__eq, % 223.56/30.83 fact_diff__eq__diff__less, fact_diff__eq__diff__less__eq, fact_diff__frac__eq, % 223.56/30.83 fact_diff__pCons, fact_diff__self, fact_div__0, fact_div__add, % 223.56/30.83 fact_div__add1__eq, fact_div__add__self1, fact_div__add__self2, fact_div__by__0, % 223.56/30.83 fact_div__by__1, fact_div__dvd__div, fact_div__le__dividend, fact_div__le__mono, % 223.56/30.83 fact_div__le__mono2, fact_div__less, fact_div__less__dividend, % 223.56/30.83 fact_div__mod__equality, fact_div__mod__equality2, fact_div__mult1__eq, % 223.56/30.83 fact_div__mult2__eq, fact_div__mult__div__if__dvd, fact_div__mult__mult1, % 223.56/30.83 fact_div__mult__mult1__if, fact_div__mult__mult2, fact_div__mult__self1, % 223.56/30.83 fact_div__mult__self1__is__id, fact_div__mult__self1__is__m, % 223.56/30.83 fact_div__mult__self2, fact_div__mult__self2__is__id, % 223.56/30.83 fact_div__mult__self__is__m, fact_div__mult__swap, fact_div__neg__neg__trivial, % 223.56/30.83 fact_div__neg__pos__less0, fact_div__nonneg__neg__le0, % 223.56/30.83 fact_div__nonpos__pos__le0, fact_div__pos__pos__trivial, fact_div__power, % 223.56/30.83 fact_div__self, fact_divide_Oadd, fact_divide_Obounded, fact_divide_Odiff, % 223.56/30.83 fact_divide_Ononneg__bounded, fact_divide_Opos__bounded, fact_divide_Ozero, % 223.56/30.83 fact_divide__1, fact_divide__add__eq__iff, fact_divide__diff__eq__iff, % 223.56/30.83 fact_divide__eq__eq, fact_divide__eq__imp, fact_divide__le__0__iff, % 223.56/30.83 fact_divide__le__eq, fact_divide__left__mono, fact_divide__left__mono__neg, % 223.56/30.83 fact_divide__less__0__iff, fact_divide__less__eq, fact_divide__neg__neg, % 223.56/30.83 fact_divide__neg__pos, fact_divide__nonneg__neg, fact_divide__nonneg__pos, % 223.56/30.83 fact_divide__nonpos__neg, fact_divide__nonpos__pos, fact_divide__pos__neg, % 223.56/30.83 fact_divide__pos__pos, fact_divide__right__mono, fact_divide__right__mono__neg, % 223.56/30.83 fact_divide__self, fact_divide__self__if, fact_divide__strict__left__mono, % 223.56/30.83 fact_divide__strict__left__mono__neg, fact_divide__strict__right__mono, % 223.56/30.83 fact_divide__strict__right__mono__neg, fact_divide__zero, % 223.56/30.83 fact_divide__zero__left, fact_divisors__zero, fact_divmod__int__rel__div__eq, % 223.56/30.83 fact_divmod__int__rel__mod__eq, % 223.56/30.83 fact_double__add__le__zero__iff__single__add__le__zero, % 223.56/30.83 fact_double__add__less__zero__iff__single__add__less__zero, % 223.56/30.83 fact_double__eq__0__iff, fact_double__zero__sym, fact_dvdI, fact_dvd_Oantisym, % 223.56/30.83 fact_dvd_Oantisym__conv, fact_dvd_Oeq__iff, fact_dvd_Oeq__refl, % 223.56/30.83 fact_dvd_Ole__imp__less__or__eq, fact_dvd_Ole__less, fact_dvd_Ole__less__trans, % 223.56/30.83 fact_dvd_Ole__neq__trans, fact_dvd_Oless__asym, fact_dvd_Oless__asym_H, % 223.56/30.83 fact_dvd_Oless__imp__le, fact_dvd_Oless__imp__neq, fact_dvd_Oless__imp__not__eq, % 223.56/30.83 fact_dvd_Oless__imp__not__eq2, fact_dvd_Oless__imp__not__less, % 223.56/30.83 fact_dvd_Oless__le, fact_dvd_Oless__le__trans, fact_dvd_Oless__not__sym, % 223.56/30.83 fact_dvd_Oless__trans, fact_dvd_Oneq__le__trans, fact_dvd_Oord__eq__le__trans, % 223.56/30.83 fact_dvd_Oord__eq__less__trans, fact_dvd_Oord__le__eq__trans, % 223.56/30.83 fact_dvd_Oord__less__eq__trans, fact_dvd_Oorder__refl, fact_dvd_Oorder__trans, % 223.56/30.83 fact_dvd__0__left, fact_dvd__0__right, fact_dvd__abs__iff, fact_dvd__add, % 223.56/30.83 fact_dvd__antisym, fact_dvd__diff, fact_dvd__div__div__eq__mult, % 223.56/30.83 fact_dvd__div__eq__mult, fact_dvd__div__mult, fact_dvd__div__mult__self, % 223.56/30.83 fact_dvd__eq__mod__eq__0, fact_dvd__if__abs__eq, fact_dvd__imp__le, % 223.56/30.83 fact_dvd__imp__le__int, fact_dvd__imp__mod__0, fact_dvd__mod, % 223.56/30.83 fact_dvd__mod__iff, fact_dvd__mod__imp__dvd, fact_dvd__mult, fact_dvd__mult2, % 223.56/30.83 fact_dvd__mult__cancel, fact_dvd__mult__cancel1, fact_dvd__mult__cancel2, % 223.56/30.83 fact_dvd__mult__cancel__left, fact_dvd__mult__cancel__right, % 223.56/30.83 fact_dvd__mult__div__cancel, fact_dvd__mult__left, fact_dvd__mult__right, % 223.56/30.83 fact_dvd__pos__nat, fact_dvd__power, fact_dvd__power__le, fact_dvd__power__same, % 223.56/30.83 fact_dvd__reduce, fact_dvd__refl, fact_dvd__trans, fact_dvd__triv__left, % 223.56/30.83 fact_dvd__triv__right, fact_eq__add__iff1, fact_eq__add__iff2, % 223.56/30.83 fact_eq__divide__eq, fact_eq__divide__imp, fact_eq__iff__diff__eq__0, % 223.56/30.83 fact_eq__imp__le, fact_even__less__0__iff, fact_ex__least__nat__less, fact_ext, % 223.56/30.83 fact_field__le__epsilon, fact_field__le__mult__one__interval, % 223.56/30.83 fact_field__power__not__zero, fact_frac__eq__eq, fact_frac__le, fact_frac__less, % 223.56/30.83 fact_frac__less2, fact_gcd__lcm__complete__lattice__nat_Obot__least, % 223.56/30.83 fact_gcd__lcm__complete__lattice__nat_Otop__greatest, % 223.56/30.83 fact_ge__natfloor__plus__one__imp__gt, fact_gr0I, fact_gr__implies__not0, % 223.56/30.83 fact_gt__half__sum, fact_incr__lemma, fact_incr__mult__lemma, fact_incseq__def, % 223.56/30.83 fact_inf__period_I3_J, fact_inf__period_I4_J, fact_int__0__less__1, % 223.56/30.83 fact_int__0__neq__1, fact_int__div__less__self, % 223.56/30.83 fact_int__one__le__iff__zero__less, fact_le0, fact_leD, fact_leI, % 223.56/30.83 fact_le__0__eq, fact_le__Suc__ex__iff, fact_le__add1, fact_le__add2, % 223.56/30.83 fact_le__add__iff1, fact_le__add__iff2, fact_le__antisym, fact_le__cube, % 223.56/30.83 fact_le__divide__eq, fact_le__eq__less__or__eq, fact_le__funD, fact_le__funE, % 223.56/30.83 fact_le__fun__def, fact_le__iff__add, fact_le__iff__diff__le__0, % 223.56/30.83 fact_le__imp__0__less, fact_le__imp__power__dvd, fact_le__mult__natfloor, % 223.56/30.83 fact_le__natfloor, fact_le__natfloor__eq, fact_le__natfloor__eq__one, % 223.56/30.83 fact_le__neq__implies__less, fact_le__refl, fact_le__square, fact_le__trans, % 223.56/30.83 fact_left__add__mult__distrib, fact_lemmaCauchy, fact_less__1__mult, % 223.56/30.83 fact_less__add__eq__less, fact_less__add__iff1, fact_less__add__iff2, % 223.56/30.83 fact_less__add__one, fact_less__bin__lemma, fact_less__divide__eq, % 223.56/30.83 fact_less__eq__nat_Osimps_I1_J, fact_less__eq__real__def, fact_less__fun__def, % 223.56/30.83 fact_less__half__sum, fact_less__iff__diff__less__0, fact_less__imp__le__nat, % 223.56/30.83 fact_less__imp__neq, fact_less__irrefl__nat, fact_less__le__not__le, % 223.56/30.83 fact_less__nat__zero__code, fact_less__natfloor, fact_less__not__refl, % 223.56/30.83 fact_less__not__refl2, fact_less__not__refl3, fact_less__or__eq__imp__le, % 223.56/30.83 fact_less__zeroE, fact_linorder__antisym__conv1, fact_linorder__antisym__conv2, % 223.56/30.83 fact_linorder__antisym__conv3, fact_linorder__cases, fact_linorder__le__cases, % 223.56/30.83 fact_linorder__le__less__linear, fact_linorder__less__linear, % 223.56/30.83 fact_linorder__linear, fact_linorder__neqE, % 223.56/30.83 fact_linorder__neqE__linordered__idom, fact_linorder__neqE__nat, % 223.56/30.83 fact_linorder__neq__iff, fact_linorder__not__le, fact_linorder__not__less, % 223.56/30.83 fact_mod__0, fact_mod__add__cong, fact_mod__add__eq, fact_mod__add__left__eq, % 223.56/30.83 fact_mod__add__right__eq, fact_mod__add__self1, fact_mod__add__self2, % 223.56/30.83 fact_mod__by__0, fact_mod__by__1, fact_mod__diff__cong, fact_mod__diff__eq, % 223.56/30.83 fact_mod__diff__left__eq, fact_mod__diff__right__eq, fact_mod__div__equality, % 223.56/30.83 fact_mod__div__equality2, fact_mod__div__trivial, fact_mod__eq__0__iff, % 223.56/30.83 fact_mod__le__divisor, fact_mod__lemma, fact_mod__less, fact_mod__less__divisor, % 223.56/30.83 fact_mod__less__eq__dividend, fact_mod__mod__cancel, fact_mod__mod__trivial, % 223.56/30.83 fact_mod__mult2__eq, fact_mod__mult__cong, fact_mod__mult__distrib, % 223.56/30.83 fact_mod__mult__distrib2, fact_mod__mult__eq, fact_mod__mult__left__eq, % 223.56/30.83 fact_mod__mult__mult1, fact_mod__mult__mult2, fact_mod__mult__right__eq, % 223.56/30.83 fact_mod__mult__self1, fact_mod__mult__self1__is__0, fact_mod__mult__self2, % 223.56/30.83 fact_mod__mult__self2__is__0, fact_mod__mult__self3, % 223.56/30.83 fact_mod__neg__neg__trivial, fact_mod__pos__neg__trivial, % 223.56/30.83 fact_mod__pos__pos__trivial, fact_mod__self, fact_mult_Oadd__left, % 223.56/30.83 fact_mult_Oadd__right, fact_mult_Obounded, fact_mult_Ocomm__neutral, % 223.56/30.83 fact_mult_Odiff__left, fact_mult_Odiff__right, fact_mult_Ononneg__bounded, % 223.56/30.83 fact_mult_Opos__bounded, fact_mult_Oprod__diff__prod, fact_mult_Ozero__left, % 223.56/30.83 fact_mult_Ozero__right, fact_mult__0, fact_mult__0__right, fact_mult__1, % 223.56/30.83 fact_mult__1__left, fact_mult__1__right, fact_mult__cancel1, fact_mult__cancel2, % 223.56/30.83 fact_mult__diff__mult, fact_mult__divide__mult__cancel__left, % 223.56/30.83 fact_mult__divide__mult__cancel__right, fact_mult__dvd__mono, % 223.56/30.83 fact_mult__eq__0__iff, fact_mult__eq__self__implies__10, % 223.56/30.83 fact_mult__imp__div__pos__le, fact_mult__imp__div__pos__less, % 223.56/30.83 fact_mult__imp__le__div__pos, fact_mult__imp__less__div__pos, fact_mult__is__0, % 223.56/30.83 fact_mult__le__0__iff, fact_mult__le__cancel1, fact_mult__le__cancel2, % 223.56/30.83 fact_mult__le__cancel__left__neg, fact_mult__le__cancel__left__pos, % 223.56/30.83 fact_mult__le__less__imp__less, fact_mult__le__mono, fact_mult__le__mono1, % 223.56/30.83 fact_mult__le__mono2, fact_mult__left_Oadd, fact_mult__left_Obounded, % 223.56/30.83 fact_mult__left_Odiff, fact_mult__left_Ononneg__bounded, % 223.56/30.83 fact_mult__left_Opos__bounded, fact_mult__left_Ozero, % 223.56/30.83 fact_mult__left__le__imp__le, fact_mult__left__le__one__le, % 223.56/30.83 fact_mult__left__less__imp__less, fact_mult__left__mono, % 223.56/30.83 fact_mult__left__mono__neg, fact_mult__less__cancel1, fact_mult__less__cancel2, % 223.56/30.83 fact_mult__less__cancel__left__disj, fact_mult__less__cancel__left__neg, % 223.56/30.83 fact_mult__less__cancel__left__pos, fact_mult__less__cancel__right__disj, % 223.56/30.83 fact_mult__less__imp__less__left, fact_mult__less__imp__less__right, % 223.56/30.83 fact_mult__less__le__imp__less, fact_mult__less__mono1, fact_mult__less__mono2, % 223.56/30.83 fact_mult__mono, fact_mult__mono_H, fact_mult__neg__neg, fact_mult__neg__pos, % 223.56/30.83 fact_mult__nonneg__nonneg, fact_mult__nonneg__nonpos, % 223.56/30.83 fact_mult__nonneg__nonpos2, fact_mult__nonpos__nonneg, % 223.56/30.83 fact_mult__nonpos__nonpos, fact_mult__poly__0__left, fact_mult__poly__0__right, % 223.56/30.83 fact_mult__poly__add__left, fact_mult__pos__neg, fact_mult__pos__neg2, % 223.56/30.83 fact_mult__pos__pos, fact_mult__right_Oadd, fact_mult__right_Obounded, % 223.56/30.83 fact_mult__right_Odiff, fact_mult__right_Ononneg__bounded, % 223.56/30.83 fact_mult__right_Opos__bounded, fact_mult__right_Ozero, % 223.56/30.83 fact_mult__right__le__imp__le, fact_mult__right__le__one__le, % 223.56/30.83 fact_mult__right__less__imp__less, fact_mult__right__mono, % 223.56/30.83 fact_mult__right__mono__neg, fact_mult__strict__left__mono, % 223.56/30.83 fact_mult__strict__left__mono__neg, fact_mult__strict__mono, % 223.56/30.83 fact_mult__strict__mono_H, fact_mult__strict__right__mono, % 223.56/30.83 fact_mult__strict__right__mono__neg, fact_mult__zero__left, % 223.56/30.83 fact_mult__zero__right, fact_nat__0__less__mult__iff, % 223.56/30.83 fact_nat__1__eq__mult__iff, fact_nat__add__assoc, fact_nat__add__commute, % 223.56/30.83 fact_nat__add__left__cancel, fact_nat__add__left__cancel__le, % 223.56/30.83 fact_nat__add__left__cancel__less, fact_nat__add__left__commute, % 223.56/30.83 fact_nat__add__right__cancel, fact_nat__dvd__1__iff__1, % 223.56/30.83 fact_nat__dvd__not__less, fact_nat__le__linear, fact_nat__le__real__less, % 223.56/30.83 fact_nat__less__cases, fact_nat__less__le, fact_nat__less__real__le, % 223.56/30.83 fact_nat__mod__eq__lemma, fact_nat__mult__1, fact_nat__mult__1__right, % 223.56/30.83 fact_nat__mult__assoc, fact_nat__mult__commute, fact_nat__mult__div__cancel1, % 223.56/30.83 fact_nat__mult__div__cancel__disj, fact_nat__mult__dvd__cancel1, % 223.56/30.83 fact_nat__mult__dvd__cancel__disj, fact_nat__mult__eq__1__iff, % 223.56/30.83 fact_nat__mult__eq__cancel1, fact_nat__mult__eq__cancel__disj, % 223.56/30.83 fact_nat__mult__le__cancel1, fact_nat__mult__less__cancel1, fact_nat__neq__iff, % 223.56/30.83 fact_nat__power__less__imp__less, fact_nat__zero__less__power__iff, % 223.56/30.83 fact_natceiling__add, fact_natceiling__add__one, fact_natceiling__eq, % 223.56/30.83 fact_natceiling__le, fact_natceiling__le__eq, fact_natceiling__le__eq__one, % 223.56/30.83 fact_natceiling__mono, fact_natceiling__neg, fact_natceiling__one, % 223.56/30.83 fact_natceiling__real__of__nat, fact_natceiling__zero, fact_natfloor__add, % 223.56/30.83 fact_natfloor__add__one, fact_natfloor__div__nat, fact_natfloor__eq, % 223.56/30.83 fact_natfloor__mono, fact_natfloor__neg, fact_natfloor__one, % 223.56/30.83 fact_natfloor__power, fact_natfloor__real__of__nat, fact_natfloor__zero, % 223.56/30.83 fact_neg__divide__le__eq, fact_neg__divide__less__eq, % 223.56/30.83 fact_neg__imp__zdiv__neg__iff, fact_neg__imp__zdiv__nonneg__iff, % 223.56/30.83 fact_neg__le__divide__eq, fact_neg__less__divide__eq, fact_neg__mod__bound, % 223.56/30.83 fact_neg__mod__conj, fact_neg__mod__sign, fact_neq0__conv, % 223.56/30.83 fact_no__zero__divisors, fact_nonneg1__imp__zdiv__pos__iff, % 223.56/30.83 fact_nonzero__abs__divide, fact_nonzero__divide__eq__eq, % 223.56/30.83 fact_nonzero__eq__divide__eq, fact_nonzero__norm__divide, % 223.56/30.83 fact_nonzero__power__divide, fact_norm__add__less, % 223.56/30.83 fact_norm__diff__triangle__ineq, fact_norm__divide, fact_norm__eq__zero, % 223.56/30.83 fact_norm__ge__zero, fact_norm__le__zero__iff, fact_norm__minus__commute, % 223.56/30.83 fact_norm__mult, fact_norm__mult__ineq, fact_norm__mult__less, % 223.56/30.83 fact_norm__not__less__zero, fact_norm__one, fact_norm__power, % 223.56/30.83 fact_norm__power__ineq, fact_norm__ratiotest__lemma, fact_norm__triangle__ineq, % 223.56/30.83 fact_norm__triangle__ineq2, fact_norm__triangle__ineq3, % 223.56/30.83 fact_norm__triangle__ineq4, fact_norm__zero, fact_not__add__less1, % 223.56/30.83 fact_not__add__less2, fact_not__leE, fact_not__less0, % 223.56/30.83 fact_not__less__iff__gr__or__eq, fact_not__one__le__zero, % 223.56/30.83 fact_not__one__less__zero, fact_not__pos__poly__0, % 223.56/30.83 fact_not__real__of__nat__less__zero, fact_not__real__square__gt__zero, % 223.56/30.83 fact_not__square__less__zero, fact_not__sum__squares__lt__zero, % 223.56/30.83 fact_odd__less__0, fact_odd__nonzero, fact_one__dvd, fact_one__le__power, % 223.56/30.83 fact_one__less__power, fact_one__neq__zero, fact_one__poly__def, % 223.56/30.83 fact_one__reorient, fact_ord__eq__le__trans, fact_ord__eq__less__trans, % 223.56/30.83 fact_ord__le__eq__trans, fact_ord__less__eq__trans, fact_order__antisym, % 223.56/30.83 fact_order__antisym__conv, fact_order__eq__iff, fact_order__eq__refl, % 223.56/30.83 fact_order__le__imp__less__or__eq, fact_order__le__less, % 223.56/30.83 fact_order__le__less__trans, fact_order__le__neq__trans, fact_order__less__asym, % 223.56/30.83 fact_order__less__asym_H, fact_order__less__imp__le, % 223.56/30.83 fact_order__less__imp__not__eq, fact_order__less__imp__not__eq2, % 223.56/30.83 fact_order__less__imp__not__less, fact_order__less__irrefl, % 223.56/30.83 fact_order__less__le, fact_order__less__le__trans, fact_order__less__not__sym, % 223.56/30.83 fact_order__less__trans, fact_order__neq__le__trans, fact_order__refl, % 223.56/30.84 fact_order__root, fact_order__trans, fact_pCons_Ohyps, fact_pCons_Oprems, % 223.56/30.84 fact_pCons__0__0, fact_pCons__eq__0__iff, fact_pCons__eq__iff, fact_pcompose__0, % 223.56/30.84 fact_pcompose__pCons, fact_plus__nat_Oadd__0, fact_poly__0, fact_poly__1, % 223.56/30.84 fact_poly__add, fact_poly__bound__exists, fact_poly__diff, % 223.56/30.84 fact_poly__div__mult__right, fact_poly__eq__iff, fact_poly__mod__mult__right, % 223.56/30.84 fact_poly__mult, fact_poly__pCons, fact_poly__pcompose, fact_poly__power, % 223.56/30.84 fact_poly__rec_Osimps, fact_poly__rec__0, fact_poly__rec__pCons, % 223.56/30.84 fact_poly__zero, fact_pos__add__strict, fact_pos__divide__le__eq, % 223.56/30.84 fact_pos__divide__less__eq, fact_pos__imp__zdiv__neg__iff, % 223.56/30.84 fact_pos__imp__zdiv__nonneg__iff, fact_pos__imp__zdiv__pos__iff, % 223.56/30.84 fact_pos__le__divide__eq, fact_pos__less__divide__eq, fact_pos__mod__bound, % 223.56/30.84 fact_pos__mod__conj, fact_pos__mod__sign, fact_pos__poly__add, % 223.56/30.84 fact_pos__poly__mult, fact_pos__poly__pCons, fact_pos__zmult__eq__1__iff, % 223.56/30.84 fact_pow__divides__eq__int, fact_pow__divides__eq__nat, % 223.56/30.84 fact_pow__divides__pow__int, fact_pow__divides__pow__nat, % 223.56/30.84 fact_power_Opower_Opower__0, fact_power__0, fact_power__0__left, % 223.56/30.84 fact_power__Suc__less, fact_power__abs, fact_power__add, fact_power__commutes, % 223.56/30.84 fact_power__decreasing, fact_power__divide, fact_power__dvd__imp__le, % 223.56/30.84 fact_power__eq__0__iff, fact_power__eq__imp__eq__base, fact_power__gt1__lemma, % 223.56/30.84 fact_power__increasing, fact_power__increasing__iff, fact_power__inject__exp, % 223.56/30.84 fact_power__le__dvd, fact_power__le__imp__le__exp, % 223.56/30.84 fact_power__less__imp__less__base, fact_power__less__imp__less__exp, % 223.56/30.84 fact_power__less__power__Suc, fact_power__mono, fact_power__mult, % 223.56/30.84 fact_power__mult__distrib, fact_power__one, fact_power__one__over, % 223.56/30.84 fact_power__one__right, fact_power__power__power, fact_power__real__of__nat, % 223.56/30.84 fact_power__strict__decreasing, fact_power__strict__increasing, % 223.56/30.84 fact_power__strict__increasing__iff, fact_power__strict__mono, % 223.56/30.84 fact_psize__eq__0__iff, fact_q__neg__lemma, fact_q__pos__lemma, % 223.56/30.84 fact_rabs__ratiotest__lemma, fact_real__0__le__divide__iff, % 223.56/30.84 fact_real__add__left__mono, fact_real__add__mult__distrib, % 223.56/30.84 fact_real__divide__square__eq, fact_real__le__antisym, fact_real__le__linear, % 223.56/30.84 fact_real__le__refl, fact_real__le__trans, fact_real__less__def, % 223.56/30.84 fact_real__mult__1, fact_real__mult__assoc, fact_real__mult__commute, % 223.56/30.84 fact_real__mult__le__cancel__iff1, fact_real__mult__le__cancel__iff2, % 223.56/30.84 fact_real__mult__left__cancel, fact_real__mult__less__iff1, % 223.56/30.84 fact_real__mult__less__mono2, fact_real__mult__order, % 223.56/30.84 fact_real__mult__right__cancel, fact_real__natceiling__ge, % 223.56/30.84 fact_real__natfloor__add__one__gt, fact_real__natfloor__le, % 223.56/30.84 fact_real__norm__def, fact_real__of__nat__1, fact_real__of__nat__add, % 223.56/30.84 fact_real__of__nat__div, fact_real__of__nat__div4, fact_real__of__nat__div__aux, % 223.56/30.84 fact_real__of__nat__ge__zero, fact_real__of__nat__gt__zero__cancel__iff, % 223.56/30.84 fact_real__of__nat__inject, fact_real__of__nat__le__iff, % 223.56/30.84 fact_real__of__nat__le__zero__cancel__iff, fact_real__of__nat__less__iff, % 223.56/30.84 fact_real__of__nat__mult, fact_real__of__nat__power, fact_real__of__nat__zero, % 223.56/30.84 fact_real__of__nat__zero__iff, fact_real__root__abs, fact_real__root__commute, % 223.56/30.84 fact_real__root__decreasing, fact_real__root__divide, % 223.56/30.84 fact_real__root__eq__0__iff, fact_real__root__eq__1__iff, % 223.56/30.84 fact_real__root__eq__iff, fact_real__root__ge__0__iff, % 223.56/30.84 fact_real__root__ge__1__iff, fact_real__root__ge__zero, % 223.56/30.84 fact_real__root__gt__0__iff, fact_real__root__gt__1__iff, % 223.56/30.84 fact_real__root__gt__zero, fact_real__root__increasing, % 223.56/30.84 fact_real__root__le__0__iff, fact_real__root__le__1__iff, % 223.56/30.84 fact_real__root__le__iff, fact_real__root__le__mono, fact_real__root__less__iff, % 223.56/30.84 fact_real__root__less__mono, fact_real__root__less__mono__lemma, % 223.56/30.84 fact_real__root__lt__0__iff, fact_real__root__lt__1__iff, fact_real__root__mult, % 223.56/30.84 fact_real__root__mult__exp, fact_real__root__mult__lemma, fact_real__root__one, % 223.56/30.84 fact_real__root__pos2, fact_real__root__pos__mult__exp, % 223.56/30.84 fact_real__root__pos__pos, fact_real__root__pos__unique, % 223.56/30.84 fact_real__root__pow__pos, fact_real__root__pow__pos2, fact_real__root__power, % 223.56/30.84 fact_real__root__strict__decreasing, fact_real__root__strict__increasing, % 223.56/30.84 fact_real__root__zero, fact_real__squared__diff__one__factored, % 223.56/30.84 fact_real__two__squares__add__zero__iff, fact_real__zero__not__eq__one, % 223.56/30.84 fact_realpow__pos__nth, fact_realpow__pos__nth__unique, fact_right__inverse__eq, % 223.56/30.84 fact_right__minus__eq, fact_self__quotient__aux1, fact_self__quotient__aux2, % 223.56/30.84 fact_semiring__div__class_Omod__div__equality_H, fact_split__div, % 223.56/30.84 fact_split__mod, fact_split__mult__neg__le, fact_split__mult__pos__le, % 223.56/30.84 fact_split__neg__lemma, fact_split__pos__lemma, fact_split__zdiv, % 223.56/30.84 fact_split__zmod, fact_sum__squares__eq__zero__iff, fact_sum__squares__ge__zero, % 223.56/30.84 fact_sum__squares__gt__zero__iff, fact_sum__squares__le__zero__iff, % 223.56/30.84 fact_termination__basic__simps_I1_J, fact_termination__basic__simps_I2_J, % 223.56/30.84 fact_termination__basic__simps_I3_J, fact_termination__basic__simps_I4_J, % 223.56/30.84 fact_termination__basic__simps_I5_J, fact_times__divide__eq__right, % 223.56/30.84 fact_times__divide__times__eq, fact_trans__le__add1, fact_trans__le__add2, % 223.56/30.84 fact_trans__less__add1, fact_trans__less__add2, fact_unique__quotient__lemma, % 223.56/30.84 fact_unique__quotient__lemma__neg, fact_unity__coeff__ex, fact_xt1_I10_J, % 223.56/30.84 fact_xt1_I11_J, fact_xt1_I12_J, fact_xt1_I1_J, fact_xt1_I2_J, fact_xt1_I3_J, % 223.56/30.84 fact_xt1_I4_J, fact_xt1_I5_J, fact_xt1_I6_J, fact_xt1_I7_J, fact_xt1_I8_J, % 223.56/30.84 fact_xt1_I9_J, fact_zabs__less__one__iff, fact_zadd__0, fact_zadd__0__right, % 223.56/30.84 fact_zadd__assoc, fact_zadd__commute, fact_zadd__left__commute, % 223.56/30.84 fact_zadd__left__mono, fact_zadd__strict__right__mono, fact_zadd__zless__mono, % 223.56/30.84 fact_zadd__zmult__distrib, fact_zadd__zmult__distrib2, fact_zdiff__zmod__left, % 223.56/30.84 fact_zdiff__zmod__right, fact_zdiff__zmult__distrib, % 223.56/30.84 fact_zdiff__zmult__distrib2, fact_zdiv__eq__0__iff, fact_zdiv__mono1, % 223.56/30.84 fact_zdiv__mono1__neg, fact_zdiv__mono2, fact_zdiv__mono2__lemma, % 223.56/30.84 fact_zdiv__mono2__neg, fact_zdiv__mono2__neg__lemma, fact_zdiv__self, % 223.56/30.84 fact_zdiv__zadd1__eq, fact_zdiv__zero, fact_zdiv__zmod__equality, % 223.56/30.84 fact_zdiv__zmod__equality2, fact_zdiv__zmult1__eq, fact_zdiv__zmult2__eq, % 223.56/30.84 fact_zdvd1__eq, fact_zdvd__antisym__abs, fact_zdvd__antisym__nonneg, % 223.56/30.84 fact_zdvd__imp__le, fact_zdvd__mono, fact_zdvd__mult__cancel, % 223.56/30.84 fact_zdvd__mult__cancel1, fact_zdvd__mult__div__cancel, fact_zdvd__not__zless, % 223.56/30.84 fact_zdvd__period, fact_zdvd__reduce, fact_zdvd__zdiffD, fact_zdvd__zmod, % 223.56/30.84 fact_zdvd__zmod__imp__zdvd, fact_zero__le__divide__iff, % 223.56/30.84 fact_zero__le__double__add__iff__zero__le__single__add, % 223.56/30.84 fact_zero__le__mult__iff, fact_zero__le__natceiling, fact_zero__le__natfloor, % 223.56/30.84 fact_zero__le__one, fact_zero__le__power, fact_zero__le__power__abs, % 223.56/30.84 fact_zero__le__square, fact_zero__le__zpower__abs, fact_zero__less__abs__iff, % 223.56/30.84 fact_zero__less__divide__iff, % 223.56/30.84 fact_zero__less__double__add__iff__zero__less__single__add, % 223.56/30.84 fact_zero__less__mult__pos, fact_zero__less__mult__pos2, % 223.56/30.84 fact_zero__less__norm__iff, fact_zero__less__one, fact_zero__less__power, % 223.56/30.84 fact_zero__less__power__nat__eq, fact_zero__less__two, % 223.56/30.84 fact_zero__less__zpower__abs__iff, fact_zero__neq__one, fact_zero__reorient, % 223.56/30.84 fact_zle__add1__eq__le, fact_zle__antisym, fact_zle__diff1__eq, % 223.56/30.84 fact_zle__linear, fact_zle__refl, fact_zle__trans, fact_zless__add1__eq, % 223.56/30.84 fact_zless__imp__add1__zle, fact_zless__le, fact_zless__linear, % 223.56/30.84 fact_zmod__eq__0__iff, fact_zmod__eq__dvd__iff, fact_zmod__le__nonneg__dividend, % 223.56/30.84 fact_zmod__self, fact_zmod__simps_I1_J, fact_zmod__simps_I2_J, % 223.56/30.84 fact_zmod__simps_I3_J, fact_zmod__simps_I4_J, fact_zmod__zdiv__equality, % 223.56/30.84 fact_zmod__zdiv__equality_H, fact_zmod__zdiv__trivial, fact_zmod__zero, % 223.56/30.84 fact_zmod__zmult1__eq, fact_zmod__zmult2__eq, fact_zmult2__lemma__aux1, % 223.56/30.84 fact_zmult2__lemma__aux2, fact_zmult2__lemma__aux3, fact_zmult2__lemma__aux4, % 223.56/30.84 fact_zmult__1, fact_zmult__1__right, fact_zmult__assoc, fact_zmult__commute, % 223.56/30.84 fact_zmult__div__cancel, fact_zmult__zless__mono2, fact_zpower__zadd__distrib, % 223.56/30.84 fact_zpower__zmod, fact_zpower__zpower, help_c__fequal__1, help_c__fequal__2 % 223.56/30.84 % 223.56/30.84 Those formulas are unsatisfiable: % 223.56/30.84 --------------------------------- % 223.56/30.84 % 223.56/30.84 Begin of proof % 223.56/30.84 | % 223.56/30.84 | ALPHA: (fact__096cmod_A_Iz_A_K_Ac_J_A_060_061_Acmod_A_Iz_A_K_Ac_A_L_Aa_J_A_L_Acmod_Aa_096) % 223.56/30.84 | implies: % 223.56/30.84 | (1) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 223.56/30.84 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 223.56/30.84 | (c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = v0 & % 223.56/30.84 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v4) = v5 & % 223.56/30.84 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v2) = v3 & % 223.56/30.84 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v6 & % 223.56/30.84 | c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v2, v_aa____) = v4 & % 223.56/30.84 | c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v5, v6) = v7 & hAPP(v1, % 223.56/30.84 | v_c____) = v2 & hAPP(v0, v_z____) = v1 & $i(v7) & $i(v6) & $i(v5) & % 223.56/30.84 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 223.56/30.84 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v3, v7)) % 223.56/30.84 | % 223.56/30.84 | ALPHA: (fact_th0) implies: % 223.56/30.84 | (2) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 223.56/30.84 | ? [v5: $i] : ? [v6: $i] : (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, % 223.56/30.84 | v_da____) = v0 & c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) % 223.56/30.84 | = v3 & c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v5) = v6 % 223.56/30.84 | & c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v1 % 223.56/30.84 | & c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v0, v1) = v2 & % 223.56/30.84 | hAPP(v4, v_c____) = v5 & hAPP(v3, v_z____) = v4 & $i(v6) & $i(v5) & % 223.56/30.84 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 223.56/30.84 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v2, v6)) % 223.56/30.84 | % 223.56/30.84 | ALPHA: (fact_ath) implies: % 223.56/30.84 | (3) ? [v0: $i] : (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = % 223.56/30.84 | v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 223.56/30.84 | ( ~ (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v2, v1) = v4) | ~ % 223.56/30.84 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 223.56/30.84 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v3, v4) | % 223.56/30.84 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v_da____, v2) | % 223.56/30.84 | ? [v5: $i] : (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v0, % 223.56/30.84 | v1) = v5 & $i(v5) & ~ % 223.56/30.84 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v5, v3)))) % 223.56/30.84 | % 223.56/30.84 | ALPHA: (fact_h) implies: % 223.56/30.85 | (4) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 223.56/30.85 | ? [v5: $i] : (c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal, v2, v3) % 223.56/30.85 | = v4 & c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = v0 & % 223.56/30.85 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v1 & % 223.56/30.85 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_c____) = v3 & % 223.56/30.85 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_z____) = v5 & % 223.56/30.85 | c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v0, v1) = v2 & $i(v5) & % 223.56/30.85 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 223.56/30.85 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v4, v5)) % 223.56/30.85 | % 223.56/30.85 | ALPHA: (fact_reduce__poly__simple) implies: % 223.56/30.85 | (5) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 223.56/30.85 | ? [v5: $i] : (c_Power_Opower__class_Opower(tc_Complex_Ocomplex) = v4 & % 223.56/30.85 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v2 & % 223.56/30.85 | c_Groups_Oone__class_Oone(tc_RealDef_Oreal) = v5 & % 223.56/30.85 | c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = v1 & % 223.56/30.85 | c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = v0 & % 223.56/30.85 | c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = v3 & $i(v5) & % 223.56/30.85 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ? [v6: $i] : ! [v7: % 223.56/30.85 | $i] : ! [v8: $i] : (v7 = v0 | v6 = v1 | ~ (hAPP(v3, v7) = v8) | % 223.56/30.85 | ~ $i(v7) | ~ $i(v6) | ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : % 223.56/30.85 | ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 223.56/30.85 | (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v13) = v14 & % 223.56/30.85 | c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v2, v12) = v13 & % 223.56/30.85 | hAPP(v10, v6) = v11 & hAPP(v8, v11) = v12 & hAPP(v4, v9) = v10 & % 223.56/30.85 | $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & % 223.56/30.85 | c_Orderings_Oord__class_Oless(tc_RealDef_Oreal, v14, v5)))) % 223.56/30.85 | % 223.56/30.85 | ALPHA: (arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) implies: % 223.56/30.85 | (6) class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) % 223.56/30.85 | % 223.56/30.85 | ALPHA: (conj_0) implies: % 223.56/30.85 | (7) $i(tc_Complex_Ocomplex) % 223.56/30.85 | (8) $i(v_aa____) % 223.56/30.85 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 223.56/30.85 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 223.56/30.85 | (c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = v0 & % 223.56/30.85 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v4) = v5 & % 223.56/30.85 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v2) = v3 & % 223.56/30.85 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = v6 & % 223.56/30.85 | c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v_aa____, v2) = v4 & % 223.56/30.85 | c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v5, v6) = v7 & hAPP(v1, % 223.56/30.85 | v_c____) = v2 & hAPP(v0, v_z____) = v1 & $i(v7) & $i(v6) & $i(v5) & % 223.56/30.85 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ % 223.56/30.85 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v3, v7)) % 223.56/30.85 | % 223.56/30.85 | ALPHA: (function-axioms) implies: % 223.56/30.85 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 223.56/30.85 | (c_Groups_Otimes__class_Otimes(v2) = v1) | ~ % 223.56/30.85 | (c_Groups_Otimes__class_Otimes(v2) = v0)) % 223.56/30.85 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 223.56/30.85 | (hAPP(v3, v2) = v1) | ~ (hAPP(v3, v2) = v0)) % 223.56/30.85 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 223.56/30.85 | (c_RealVector_Onorm__class_Onorm(v3, v2) = v1) | ~ % 223.56/30.85 | (c_RealVector_Onorm__class_Onorm(v3, v2) = v0)) % 223.56/30.85 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 223.56/30.85 | (c_Groups_Oabs__class_Oabs(v3, v2) = v1) | ~ % 223.56/30.85 | (c_Groups_Oabs__class_Oabs(v3, v2) = v0)) % 223.56/30.86 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 223.56/30.86 | (v1 = v0 | ~ (c_Groups_Oplus__class_Oplus(v4, v3, v2) = v1) | ~ % 223.56/30.86 | (c_Groups_Oplus__class_Oplus(v4, v3, v2) = v0)) % 223.56/30.86 | % 223.56/30.86 | DELTA: instantiating (3) with fresh symbol all_1096_0 gives: % 223.56/30.86 | (15) c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = all_1096_0 & % 223.56/30.86 | $i(all_1096_0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 223.56/30.86 | : ( ~ (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v1, v0) = v3) | % 223.56/30.86 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v2, v3) | % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v_da____, v1) | % 223.56/30.86 | ? [v4: $i] : (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, % 223.56/30.86 | all_1096_0, v0) = v4 & $i(v4) & ~ % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v4, v2))) % 223.56/30.86 | % 223.56/30.86 | ALPHA: (15) implies: % 223.56/30.86 | (16) c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = all_1096_0 % 223.56/30.86 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 223.56/30.86 | (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, v1, v0) = v3) | ~ % 223.56/30.86 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v2, v3) | % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v_da____, v1) | % 223.56/30.86 | ? [v4: $i] : (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, % 223.56/30.86 | all_1096_0, v0) = v4 & $i(v4) & ~ % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v4, v2))) % 223.56/30.86 | % 223.56/30.86 | DELTA: instantiating (4) with fresh symbols all_1221_0, all_1221_1, % 223.56/30.86 | all_1221_2, all_1221_3, all_1221_4, all_1221_5 gives: % 223.56/30.86 | (18) c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal, all_1221_3, % 223.56/30.86 | all_1221_2) = all_1221_1 & % 223.56/30.86 | c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = all_1221_5 & % 223.56/30.86 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = % 223.56/30.86 | all_1221_4 & c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, % 223.56/30.86 | v_c____) = all_1221_2 & % 223.56/30.86 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_z____) = % 223.56/30.86 | all_1221_0 & c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1221_5, % 223.56/30.86 | all_1221_4) = all_1221_3 & $i(all_1221_0) & $i(all_1221_1) & % 223.56/30.86 | $i(all_1221_2) & $i(all_1221_3) & $i(all_1221_4) & $i(all_1221_5) & % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1221_1, % 223.56/30.86 | all_1221_0) % 223.56/30.86 | % 223.56/30.86 | ALPHA: (18) implies: % 223.56/30.86 | (19) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1221_5, all_1221_4) % 223.56/30.86 | = all_1221_3 % 223.56/30.86 | (20) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = % 223.56/30.86 | all_1221_4 % 223.56/30.86 | (21) c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = all_1221_5 % 223.56/30.86 | % 223.56/30.86 | DELTA: instantiating (2) with fresh symbols all_1360_0, all_1360_1, % 223.56/30.86 | all_1360_2, all_1360_3, all_1360_4, all_1360_5, all_1360_6 gives: % 223.56/30.86 | (22) c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = all_1360_6 & % 223.56/30.86 | c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1360_3 & % 223.56/30.86 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1360_1) = % 223.56/30.86 | all_1360_0 & c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, % 223.56/30.86 | v_aa____) = all_1360_5 & % 223.56/30.86 | c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1360_6, all_1360_5) % 223.56/30.86 | = all_1360_4 & hAPP(all_1360_2, v_c____) = all_1360_1 & % 223.56/30.86 | hAPP(all_1360_3, v_z____) = all_1360_2 & $i(all_1360_0) & % 223.56/30.86 | $i(all_1360_1) & $i(all_1360_2) & $i(all_1360_3) & $i(all_1360_4) & % 223.56/30.86 | $i(all_1360_5) & $i(all_1360_6) & % 223.56/30.86 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1360_4, % 223.56/30.86 | all_1360_0) % 223.56/30.86 | % 223.56/30.86 | ALPHA: (22) implies: % 223.56/30.86 | (23) c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1360_4, % 223.56/30.86 | all_1360_0) % 223.56/30.86 | (24) $i(all_1360_5) % 223.56/30.86 | (25) hAPP(all_1360_3, v_z____) = all_1360_2 % 223.56/30.86 | (26) hAPP(all_1360_2, v_c____) = all_1360_1 % 223.56/30.86 | (27) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1360_6, all_1360_5) % 223.56/30.86 | = all_1360_4 % 223.56/30.86 | (28) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = % 223.56/30.86 | all_1360_5 % 223.56/30.86 | (29) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1360_1) = % 223.56/30.86 | all_1360_0 % 223.56/30.86 | (30) c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1360_3 % 223.56/30.86 | (31) c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal, v_da____) = all_1360_6 % 223.56/30.86 | % 223.56/30.86 | DELTA: instantiating (1) with fresh symbols all_1459_0, all_1459_1, % 223.56/30.86 | all_1459_2, all_1459_3, all_1459_4, all_1459_5, all_1459_6, all_1459_7 % 223.56/30.86 | gives: % 223.56/30.87 | (32) c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1459_7 & % 223.56/30.87 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1459_3) = % 223.56/30.87 | all_1459_2 & c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, % 223.56/30.87 | all_1459_5) = all_1459_4 & % 223.56/30.87 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = % 223.56/30.87 | all_1459_1 & c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, % 223.56/30.87 | all_1459_5, v_aa____) = all_1459_3 & % 223.56/30.87 | c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1459_2, all_1459_1) % 223.56/30.87 | = all_1459_0 & hAPP(all_1459_6, v_c____) = all_1459_5 & % 223.56/30.87 | hAPP(all_1459_7, v_z____) = all_1459_6 & $i(all_1459_0) & % 223.56/30.87 | $i(all_1459_1) & $i(all_1459_2) & $i(all_1459_3) & $i(all_1459_4) & % 223.56/30.87 | $i(all_1459_5) & $i(all_1459_6) & $i(all_1459_7) & % 223.56/30.87 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1459_4, % 223.56/30.87 | all_1459_0) % 223.56/30.87 | % 223.56/30.87 | ALPHA: (32) implies: % 223.56/30.87 | (33) c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1459_4, % 223.56/30.87 | all_1459_0) % 223.56/30.87 | (34) $i(all_1459_5) % 223.56/30.87 | (35) $i(all_1459_4) % 223.56/30.87 | (36) $i(all_1459_2) % 223.56/30.87 | (37) hAPP(all_1459_7, v_z____) = all_1459_6 % 223.56/30.87 | (38) hAPP(all_1459_6, v_c____) = all_1459_5 % 223.56/30.87 | (39) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1459_2, all_1459_1) % 223.56/30.87 | = all_1459_0 % 223.56/30.87 | (40) c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, all_1459_5, v_aa____) % 223.56/30.87 | = all_1459_3 % 223.56/30.87 | (41) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = % 223.56/30.87 | all_1459_1 % 223.56/30.87 | (42) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1459_5) = % 223.56/30.87 | all_1459_4 % 223.56/30.87 | (43) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1459_3) = % 223.56/30.87 | all_1459_2 % 223.56/30.87 | (44) c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1459_7 % 223.56/30.87 | % 223.56/30.87 | DELTA: instantiating (9) with fresh symbols all_1479_0, all_1479_1, % 223.56/30.87 | all_1479_2, all_1479_3, all_1479_4, all_1479_5, all_1479_6, all_1479_7 % 223.56/30.87 | gives: % 223.56/30.87 | (45) c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1479_7 & % 223.56/30.87 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1479_3) = % 223.56/30.87 | all_1479_2 & c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, % 223.56/30.87 | all_1479_5) = all_1479_4 & % 223.56/30.87 | c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = % 223.56/30.87 | all_1479_1 & c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, % 223.56/30.87 | v_aa____, all_1479_5) = all_1479_3 & % 223.56/30.87 | c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1479_2, all_1479_1) % 223.56/30.87 | = all_1479_0 & hAPP(all_1479_6, v_c____) = all_1479_5 & % 223.56/30.87 | hAPP(all_1479_7, v_z____) = all_1479_6 & $i(all_1479_0) & % 223.56/30.87 | $i(all_1479_1) & $i(all_1479_2) & $i(all_1479_3) & $i(all_1479_4) & % 223.56/30.87 | $i(all_1479_5) & $i(all_1479_6) & $i(all_1479_7) & ~ % 223.56/30.87 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1479_4, % 223.56/30.87 | all_1479_0) % 223.56/30.87 | % 223.56/30.87 | ALPHA: (45) implies: % 223.56/30.87 | (46) ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1479_4, % 223.56/30.87 | all_1479_0) % 223.56/30.87 | (47) hAPP(all_1479_7, v_z____) = all_1479_6 % 223.56/30.87 | (48) hAPP(all_1479_6, v_c____) = all_1479_5 % 223.56/30.87 | (49) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1479_2, all_1479_1) % 223.56/30.87 | = all_1479_0 % 223.56/30.87 | (50) c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v_aa____, all_1479_5) % 223.56/30.87 | = all_1479_3 % 223.56/30.87 | (51) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v_aa____) = % 223.56/30.87 | all_1479_1 % 223.56/30.87 | (52) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1479_5) = % 223.56/30.87 | all_1479_4 % 223.56/30.87 | (53) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1479_3) = % 223.56/30.87 | all_1479_2 % 223.56/30.87 | (54) c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1479_7 % 223.56/30.87 | % 223.56/30.87 | DELTA: instantiating (5) with fresh symbols all_1722_0, all_1722_1, % 223.56/30.87 | all_1722_2, all_1722_3, all_1722_4, all_1722_5 gives: % 223.56/30.87 | (55) c_Power_Opower__class_Opower(tc_Complex_Ocomplex) = all_1722_1 & % 223.56/30.87 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1722_3 & % 223.56/30.87 | c_Groups_Oone__class_Oone(tc_RealDef_Oreal) = all_1722_0 & % 223.56/30.87 | c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = all_1722_4 & % 223.56/30.87 | c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = all_1722_5 & % 223.56/30.87 | c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1722_2 & % 223.56/30.87 | $i(all_1722_0) & $i(all_1722_1) & $i(all_1722_2) & $i(all_1722_3) & % 223.56/30.87 | $i(all_1722_4) & $i(all_1722_5) & ? [v0: any] : ! [v1: any] : ! % 223.56/30.87 | [v2: $i] : (v1 = all_1722_5 | v0 = all_1722_4 | ~ (hAPP(all_1722_2, % 223.56/30.87 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : % 223.56/30.87 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 223.56/30.87 | (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, v7) = v8 & % 223.56/30.87 | c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, all_1722_3, v6) = % 223.56/30.87 | v7 & hAPP(v4, v0) = v5 & hAPP(v2, v5) = v6 & hAPP(all_1722_1, v3) % 223.56/30.87 | = v4 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 223.56/30.87 | c_Orderings_Oord__class_Oless(tc_RealDef_Oreal, v8, all_1722_0))) % 223.56/30.87 | % 223.56/30.87 | ALPHA: (55) implies: % 223.56/30.87 | (56) c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex) = all_1722_2 % 223.56/30.87 | % 223.56/30.88 | GROUND_INST: instantiating (12) with all_1360_5, all_1459_1, v_aa____, % 223.56/30.88 | tc_Complex_Ocomplex, simplifying with (28), (41) gives: % 223.56/30.88 | (57) all_1459_1 = all_1360_5 % 223.56/30.88 | % 223.56/30.88 | GROUND_INST: instantiating (12) with all_1459_1, all_1479_1, v_aa____, % 223.56/30.88 | tc_Complex_Ocomplex, simplifying with (41), (51) gives: % 223.56/30.88 | (58) all_1479_1 = all_1459_1 % 223.56/30.88 | % 223.56/30.88 | GROUND_INST: instantiating (12) with all_1221_4, all_1479_1, v_aa____, % 223.56/30.88 | tc_Complex_Ocomplex, simplifying with (20), (51) gives: % 223.56/30.88 | (59) all_1479_1 = all_1221_4 % 223.56/30.88 | % 223.56/30.88 | GROUND_INST: instantiating (10) with all_1479_7, all_1722_2, % 223.56/30.88 | tc_Complex_Ocomplex, simplifying with (54), (56) gives: % 223.56/30.88 | (60) all_1722_2 = all_1479_7 % 223.56/30.88 | % 223.56/30.88 | GROUND_INST: instantiating (10) with all_1459_7, all_1722_2, % 223.56/30.88 | tc_Complex_Ocomplex, simplifying with (44), (56) gives: % 223.56/30.88 | (61) all_1722_2 = all_1459_7 % 223.56/30.88 | % 223.56/30.88 | GROUND_INST: instantiating (10) with all_1360_3, all_1722_2, % 223.56/30.88 | tc_Complex_Ocomplex, simplifying with (30), (56) gives: % 223.56/30.88 | (62) all_1722_2 = all_1360_3 % 223.56/30.88 | % 223.56/30.88 | GROUND_INST: instantiating (13) with all_1221_5, all_1360_6, v_da____, % 223.56/30.88 | tc_RealDef_Oreal, simplifying with (21), (31) gives: % 223.56/30.88 | (63) all_1360_6 = all_1221_5 % 223.56/30.88 | % 223.56/30.88 | GROUND_INST: instantiating (13) with all_1096_0, all_1360_6, v_da____, % 223.56/30.88 | tc_RealDef_Oreal, simplifying with (16), (31) gives: % 223.56/30.88 | (64) all_1360_6 = all_1096_0 % 223.56/30.88 | % 223.56/30.88 | COMBINE_EQS: (60), (62) imply: % 223.56/30.88 | (65) all_1479_7 = all_1360_3 % 223.56/30.88 | % 223.56/30.88 | COMBINE_EQS: (60), (61) imply: % 223.56/30.88 | (66) all_1479_7 = all_1459_7 % 223.56/30.88 | % 223.56/30.88 | COMBINE_EQS: (58), (59) imply: % 223.56/30.88 | (67) all_1459_1 = all_1221_4 % 223.56/30.88 | % 223.56/30.88 | SIMP: (67) implies: % 223.56/30.88 | (68) all_1459_1 = all_1221_4 % 223.56/30.88 | % 223.56/30.88 | COMBINE_EQS: (65), (66) imply: % 223.56/30.88 | (69) all_1459_7 = all_1360_3 % 223.56/30.88 | % 223.56/30.88 | COMBINE_EQS: (57), (68) imply: % 223.56/30.88 | (70) all_1360_5 = all_1221_4 % 223.56/30.88 | % 223.56/30.88 | SIMP: (70) implies: % 223.56/30.88 | (71) all_1360_5 = all_1221_4 % 223.56/30.88 | % 223.56/30.88 | COMBINE_EQS: (63), (64) imply: % 223.56/30.88 | (72) all_1221_5 = all_1096_0 % 223.56/30.88 | % 223.56/30.88 | SIMP: (72) implies: % 223.56/30.88 | (73) all_1221_5 = all_1096_0 % 223.56/30.88 | % 223.56/30.88 | REDUCE: (49), (59) imply: % 223.56/30.88 | (74) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1479_2, all_1221_4) % 223.56/30.88 | = all_1479_0 % 223.56/30.88 | % 223.56/30.88 | REDUCE: (39), (68) imply: % 223.56/30.88 | (75) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1459_2, all_1221_4) % 223.56/30.88 | = all_1459_0 % 223.56/30.88 | % 223.56/30.88 | REDUCE: (27), (64), (71) imply: % 223.56/30.88 | (76) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1096_0, all_1221_4) % 223.56/30.88 | = all_1360_4 % 223.56/30.88 | % 223.56/30.88 | REDUCE: (19), (73) imply: % 223.56/30.88 | (77) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1096_0, all_1221_4) % 223.56/30.88 | = all_1221_3 % 223.56/30.88 | % 223.56/30.88 | REDUCE: (47), (65) imply: % 223.56/30.88 | (78) hAPP(all_1360_3, v_z____) = all_1479_6 % 223.56/30.88 | % 223.56/30.88 | REDUCE: (37), (69) imply: % 223.56/30.89 | (79) hAPP(all_1360_3, v_z____) = all_1459_6 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (24), (71) imply: % 223.56/30.89 | (80) $i(all_1221_4) % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (11) with all_1360_2, all_1479_6, v_z____, % 223.56/30.89 | all_1360_3, simplifying with (25), (78) gives: % 223.56/30.89 | (81) all_1479_6 = all_1360_2 % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (11) with all_1459_6, all_1479_6, v_z____, % 223.56/30.89 | all_1360_3, simplifying with (78), (79) gives: % 223.56/30.89 | (82) all_1479_6 = all_1459_6 % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (14) with all_1221_3, all_1360_4, all_1221_4, % 223.56/30.89 | all_1096_0, tc_RealDef_Oreal, simplifying with (76), (77) gives: % 223.56/30.89 | (83) all_1360_4 = all_1221_3 % 223.56/30.89 | % 223.56/30.89 | COMBINE_EQS: (81), (82) imply: % 223.56/30.89 | (84) all_1459_6 = all_1360_2 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (48), (81) imply: % 223.56/30.89 | (85) hAPP(all_1360_2, v_c____) = all_1479_5 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (38), (84) imply: % 223.56/30.89 | (86) hAPP(all_1360_2, v_c____) = all_1459_5 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (23), (83) imply: % 223.56/30.89 | (87) c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1221_3, % 223.56/30.89 | all_1360_0) % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (11) with all_1360_1, all_1479_5, v_c____, % 223.56/30.89 | all_1360_2, simplifying with (26), (85) gives: % 223.56/30.89 | (88) all_1479_5 = all_1360_1 % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (11) with all_1459_5, all_1479_5, v_c____, % 223.56/30.89 | all_1360_2, simplifying with (85), (86) gives: % 223.56/30.89 | (89) all_1479_5 = all_1459_5 % 223.56/30.89 | % 223.56/30.89 | COMBINE_EQS: (88), (89) imply: % 223.56/30.89 | (90) all_1459_5 = all_1360_1 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (52), (88) imply: % 223.56/30.89 | (91) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1360_1) = % 223.56/30.89 | all_1479_4 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (42), (90) imply: % 223.56/30.89 | (92) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1360_1) = % 223.56/30.89 | all_1459_4 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (40), (90) imply: % 223.56/30.89 | (93) c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, all_1360_1, v_aa____) % 223.56/30.89 | = all_1459_3 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (50), (88) imply: % 223.56/30.89 | (94) c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, v_aa____, all_1360_1) % 223.56/30.89 | = all_1479_3 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (34), (90) imply: % 223.56/30.89 | (95) $i(all_1360_1) % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (12) with all_1360_0, all_1479_4, all_1360_1, % 223.56/30.89 | tc_Complex_Ocomplex, simplifying with (29), (91) gives: % 223.56/30.89 | (96) all_1479_4 = all_1360_0 % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (12) with all_1459_4, all_1479_4, all_1360_1, % 223.56/30.89 | tc_Complex_Ocomplex, simplifying with (91), (92) gives: % 223.56/30.89 | (97) all_1479_4 = all_1459_4 % 223.56/30.89 | % 223.56/30.89 | COMBINE_EQS: (96), (97) imply: % 223.56/30.89 | (98) all_1459_4 = all_1360_0 % 223.56/30.89 | % 223.56/30.89 | REDUCE: (35), (98) imply: % 223.56/30.89 | (99) $i(all_1360_0) % 223.56/30.89 | % 223.56/30.89 | REDUCE: (33), (98) imply: % 223.56/30.89 | (100) c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1360_0, % 223.56/30.89 | all_1459_0) % 223.56/30.89 | % 223.56/30.89 | REDUCE: (46), (96) imply: % 223.56/30.89 | (101) ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1360_0, % 223.56/30.89 | all_1479_0) % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating (17) with all_1221_4, all_1459_2, all_1360_0, % 223.56/30.89 | all_1459_0, simplifying with (36), (75), (80), (99), (100) gives: % 223.56/30.89 | (102) c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v_da____, % 223.56/30.89 | all_1459_2) | ? [v0: $i] : % 223.56/30.89 | (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1096_0, % 223.56/30.89 | all_1221_4) = v0 & $i(v0) & ~ % 223.56/30.89 | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v0, % 223.56/30.89 | all_1360_0)) % 223.56/30.89 | % 223.56/30.89 | GROUND_INST: instantiating % 223.56/30.89 | (fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) % 223.56/30.89 | with v_aa____, all_1360_1, tc_Complex_Ocomplex, all_1479_3, % 223.56/30.89 | simplifying with (6), (7), (8), (94), (95) gives: % 223.56/30.89 | (103) c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, all_1360_1, % 223.56/30.89 | v_aa____) = all_1479_3 & $i(all_1479_3) % 223.56/30.89 | % 223.56/30.89 | ALPHA: (103) implies: % 223.56/30.89 | (104) c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex, all_1360_1, % 223.56/30.89 | v_aa____) = all_1479_3 % 223.56/30.89 | % 223.56/30.89 | BETA: splitting (102) gives: % 223.56/30.89 | % 223.56/30.89 | Case 1: % 223.56/30.89 | | % 223.56/30.89 | | % 223.56/30.89 | | GROUND_INST: instantiating (14) with all_1459_3, all_1479_3, v_aa____, % 223.56/30.89 | | all_1360_1, tc_Complex_Ocomplex, simplifying with (93), (104) % 223.56/30.89 | | gives: % 223.56/30.89 | | (105) all_1479_3 = all_1459_3 % 223.56/30.89 | | % 223.56/30.89 | | REDUCE: (53), (105) imply: % 223.56/30.89 | | (106) c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex, all_1459_3) = % 223.56/30.89 | | all_1479_2 % 223.56/30.89 | | % 223.56/30.89 | | GROUND_INST: instantiating (12) with all_1459_2, all_1479_2, all_1459_3, % 223.56/30.90 | | tc_Complex_Ocomplex, simplifying with (43), (106) gives: % 223.56/30.90 | | (107) all_1479_2 = all_1459_2 % 223.56/30.90 | | % 223.56/30.90 | | REDUCE: (74), (107) imply: % 223.56/30.90 | | (108) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1459_2, % 223.56/30.90 | | all_1221_4) = all_1479_0 % 223.56/30.90 | | % 223.56/30.90 | | GROUND_INST: instantiating (14) with all_1459_0, all_1479_0, all_1221_4, % 223.56/30.90 | | all_1459_2, tc_RealDef_Oreal, simplifying with (75), (108) % 223.56/30.90 | | gives: % 223.56/30.90 | | (109) all_1479_0 = all_1459_0 % 223.56/30.90 | | % 223.56/30.90 | | REDUCE: (101), (109) imply: % 223.92/30.90 | | (110) ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1360_0, % 223.92/30.90 | | all_1459_0) % 223.92/30.90 | | % 223.92/30.90 | | PRED_UNIFY: (100), (110) imply: % 223.92/30.90 | | (111) $false % 223.92/30.90 | | % 223.92/30.90 | | CLOSE: (111) is inconsistent. % 223.92/30.90 | | % 223.92/30.90 | Case 2: % 223.92/30.90 | | % 223.92/30.90 | | (112) ? [v0: $i] : (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, % 223.92/30.90 | | all_1096_0, all_1221_4) = v0 & $i(v0) & ~ % 223.92/30.90 | | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, v0, % 223.92/30.90 | | all_1360_0)) % 223.92/30.90 | | % 223.92/30.90 | | DELTA: instantiating (112) with fresh symbol all_2046_0 gives: % 223.92/30.90 | | (113) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1096_0, % 223.92/30.90 | | all_1221_4) = all_2046_0 & $i(all_2046_0) & ~ % 223.92/30.90 | | c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_2046_0, % 223.92/30.90 | | all_1360_0) % 223.92/30.90 | | % 223.92/30.90 | | ALPHA: (113) implies: % 223.92/30.90 | | (114) ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_2046_0, % 223.92/30.90 | | all_1360_0) % 223.92/30.90 | | (115) c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal, all_1096_0, % 223.92/30.90 | | all_1221_4) = all_2046_0 % 223.92/30.90 | | % 223.92/30.90 | | GROUND_INST: instantiating (14) with all_1221_3, all_2046_0, all_1221_4, % 223.92/30.90 | | all_1096_0, tc_RealDef_Oreal, simplifying with (77), (115) % 223.92/30.90 | | gives: % 223.92/30.90 | | (116) all_2046_0 = all_1221_3 % 223.92/30.90 | | % 223.92/30.90 | | REDUCE: (114), (116) imply: % 223.92/30.90 | | (117) ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal, all_1221_3, % 223.92/30.90 | | all_1360_0) % 223.92/30.90 | | % 223.92/30.90 | | PRED_UNIFY: (87), (117) imply: % 223.92/30.90 | | (118) $false % 223.92/30.90 | | % 223.92/30.90 | | CLOSE: (118) is inconsistent. % 223.92/30.90 | | % 223.92/30.90 | End of split % 223.92/30.90 | % 223.92/30.90 End of proof % 223.92/30.90 % SZS output end Proof for theBenchmark % 223.92/30.90 % 223.92/30.90 30272ms %------------------------------------------------------------------------------