%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW272+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 : n014.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:39 EDT 2023 % Result : Theorem 76.05s 10.53s % Output : Proof 186.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW272+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.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Aug 27 22:37:31 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.52 ________ _____ % 0.19/0.52 ___ __ \_________(_)________________________________ % 0.19/0.52 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.52 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.52 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.52 % 0.19/0.52 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.52 (2023-06-19) % 0.19/0.52 % 0.19/0.52 (c) Philipp Rümmer, 2009-2023 % 0.19/0.52 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.52 Amanda Stjerna. % 0.19/0.52 Free software under BSD-3-Clause. % 0.19/0.52 % 0.19/0.52 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.52 % 0.19/0.52 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.53 Running up to 7 provers in parallel. % 0.19/0.54 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.54 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.54 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.54 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.54 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.54 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.54 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 16.65/3.01 Prover 1: Preprocessing ... % 18.53/3.06 Prover 0: Preprocessing ... % 18.53/3.06 Prover 5: Preprocessing ... % 18.53/3.06 Prover 2: Preprocessing ... % 18.53/3.07 Prover 3: Preprocessing ... % 18.72/3.08 Prover 6: Preprocessing ... % 18.72/3.08 Prover 4: Preprocessing ... % 51.01/7.35 Prover 1: Warning: ignoring some quantifiers % 52.17/7.47 Prover 3: Warning: ignoring some quantifiers % 52.98/7.66 Prover 1: Constructing countermodel ... % 52.98/7.66 Prover 3: Constructing countermodel ... % 54.33/7.72 Prover 6: Proving ... % 58.70/8.33 Prover 4: Warning: ignoring some quantifiers % 60.86/8.64 Prover 4: Constructing countermodel ... % 67.64/9.51 Prover 5: Proving ... % 67.64/9.53 Prover 0: Proving ... % 73.84/10.26 Prover 2: Proving ... % 76.05/10.53 Prover 3: proved (9990ms) % 76.05/10.53 % 76.05/10.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 76.05/10.53 % 76.05/10.53 Prover 2: stopped % 76.05/10.53 Prover 5: stopped % 76.05/10.54 Prover 6: stopped % 76.17/10.55 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 76.17/10.55 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 76.17/10.55 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 76.17/10.56 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 76.17/10.58 Prover 0: stopped % 76.17/10.59 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 85.17/11.88 Prover 8: Preprocessing ... % 87.37/12.03 Prover 7: Preprocessing ... % 87.37/12.04 Prover 11: Preprocessing ... % 87.98/12.12 Prover 13: Preprocessing ... % 88.83/12.19 Prover 10: Preprocessing ... % 100.80/13.73 Prover 10: Warning: ignoring some quantifiers % 101.21/13.86 Prover 8: Warning: ignoring some quantifiers % 101.96/14.00 Prover 10: Constructing countermodel ... % 103.18/14.07 Prover 7: Warning: ignoring some quantifiers % 103.18/14.08 Prover 8: Constructing countermodel ... % 105.15/14.34 Prover 7: Constructing countermodel ... % 108.59/14.78 Prover 13: Warning: ignoring some quantifiers % 108.99/14.83 Prover 11: Warning: ignoring some quantifiers % 110.53/15.03 Prover 13: Constructing countermodel ... % 110.53/15.03 Prover 11: Constructing countermodel ... % 116.12/15.88 Prover 1: stopped % 116.12/15.90 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 121.39/16.50 Prover 16: Preprocessing ... % 132.61/18.05 Prover 16: Warning: ignoring some quantifiers % 134.28/18.18 Prover 16: Constructing countermodel ... % 154.03/20.73 Prover 16: stopped % 154.03/20.73 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 154.44/20.75 Prover 13: stopped % 159.36/21.41 Prover 19: Preprocessing ... % 170.12/22.89 Prover 19: Warning: ignoring some quantifiers % 171.77/23.04 Prover 19: Constructing countermodel ... % 185.49/24.83 Prover 10: Found proof (size 293) % 185.49/24.83 Prover 10: proved (14284ms) % 185.49/24.83 Prover 19: stopped % 185.49/24.83 Prover 11: stopped % 185.49/24.83 Prover 7: stopped % 185.49/24.83 Prover 8: stopped % 185.49/24.84 Prover 4: stopped % 185.49/24.84 % 185.49/24.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 185.49/24.85 % 185.83/24.91 % SZS output start Proof for theBenchmark % 185.83/24.94 Assumptions after simplification: % 185.83/24.94 --------------------------------- % 185.83/24.94 % 185.83/24.94 (arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) % 185.83/24.95 $i(tc_Complex_Ocomplex) & class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) % 185.83/24.95 % 185.83/24.95 (conj_0) % 186.17/24.97 $i(v_s____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : % 186.17/24.97 (tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.17/24.97 c_Groups_Ozero__class_Ozero(v0) = v_s____ & $i(v0)) % 186.17/24.97 % 186.17/24.97 (fact_IH) % 186.17/24.98 $i(v_na____) & $i(tc_Nat_Onat) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? % 186.17/24.98 [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.17/24.98 (c_Power_Opower__class_Opower(v2) = v4 & c_Rings_Odvd__class_Odvd(v2) = v3 & % 186.17/24.98 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v2 & % 186.17/24.98 c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = v1 & % 186.17/24.98 c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = v0 & $i(v4) & $i(v3) & % 186.17/24.98 $i(v2) & $i(v1) & $i(v0) & ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: % 186.17/24.98 $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : (v5 = v1 | ~ (hAPP(v9, % 186.17/24.98 v5) = v10) | ~ (hAPP(v8, v10) = v11) | ~ (hAPP(v4, v7) = v9) | ~ % 186.17/24.98 (hAPP(v3, v6) = v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ % 186.17/24.98 c_Orderings_Oord__class_Oless(tc_Nat_Onat, v5, v_na____) | hBOOL(v11) | ? % 186.17/24.98 [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? [v15: $i] : ? [v16: $i] : ? % 186.17/24.98 [v17: $i] : ($i(v15) & ((v16 = v0 & ~ (v17 = v0) & % 186.17/24.98 c_Polynomial_Opoly(tc_Complex_Ocomplex, v7) = v13 & % 186.17/24.98 c_Polynomial_Opoly(tc_Complex_Ocomplex, v6) = v12 & hAPP(v13, v15) = % 186.17/24.98 v17 & hAPP(v12, v15) = v0 & $i(v17) & $i(v13) & $i(v12)) | ( ~ (v14 % 186.17/24.98 = v5) & c_Polynomial_Odegree(tc_Complex_Ocomplex, v6) = v14 & % 186.17/24.98 $i(v14)))))) % 186.17/24.98 % 186.17/24.98 (fact__096_091_058_N_Aa_M_A1_058_093_Advd_Aq_096) % 186.17/24.98 $i(v_a____) & $i(v_qa____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? [v1: % 186.17/24.98 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 186.17/24.98 ? [v7: $i] : ? [v8: $i] : % 186.17/24.98 (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v2 & % 186.17/24.98 c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v3 & % 186.17/24.98 c_Rings_Odvd__class_Odvd(v0) = v1 & c_Polynomial_OpCons(tc_Complex_Ocomplex, % 186.17/24.98 v3, v4) = v5 & c_Polynomial_OpCons(tc_Complex_Ocomplex, v2, v5) = v6 & % 186.17/24.98 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.17/24.98 c_Groups_Ozero__class_Ozero(v0) = v4 & hAPP(v7, v_qa____) = v8 & hAPP(v1, % 186.17/24.98 v6) = v7 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 186.17/24.98 $i(v1) & $i(v0) & hBOOL(v8)) % 186.17/24.98 % 186.17/24.98 (fact__096_B_Bthesis_O_A_I_B_Br_O_Aq_A_061_A_091_058_N_Aa_M_A1_058_093_A_K_Ar_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) % 186.26/24.98 $i(v_a____) & $i(v_qa____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? [v1: % 186.26/24.98 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 186.26/24.98 ? [v7: $i] : ? [v8: $i] : (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.26/24.98 c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v2 & % 186.26/24.98 c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v3 & % 186.26/24.98 c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v4) = v5 & % 186.26/24.98 c_Polynomial_OpCons(tc_Complex_Ocomplex, v2, v5) = v6 & % 186.26/24.98 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/24.98 c_Groups_Ozero__class_Ozero(v0) = v4 & hAPP(v7, v8) = v_qa____ & hAPP(v1, % 186.26/24.98 v6) = v7 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 186.26/24.98 $i(v1) & $i(v0)) % 186.26/24.98 % 186.26/24.98 (fact__096_B_Bthesis_O_A_I_B_Bs_O_Ap_A_061_A_091_058_N_Aa_M_A1_058_093_A_094_Aorder_Aa_Ap_A_K_As_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) % 186.26/24.99 $i(v_a____) & $i(v_pa____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? [v1: % 186.26/24.99 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 186.26/24.99 ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 186.26/24.99 [v12: $i] : (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.26/24.99 c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v3 & % 186.26/24.99 c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & % 186.26/24.99 c_Power_Opower__class_Opower(v0) = v2 & % 186.26/24.99 c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.26/24.99 c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.26/24.99 c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.26/24.99 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/24.99 c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v11, v12) = v_pa____ & hAPP(v8, % 186.26/24.99 v9) = v10 & hAPP(v2, v7) = v8 & hAPP(v1, v10) = v11 & $i(v12) & $i(v11) & % 186.26/24.99 $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 186.26/24.99 $i(v2) & $i(v1) & $i(v0)) % 186.26/24.99 % 186.26/24.99 (fact_ap_I1_J) % 186.26/24.99 $i(v_a____) & $i(v_pa____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? [v1: % 186.26/24.99 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 186.26/24.99 ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 186.26/24.99 [v12: $i] : (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.26/24.99 v3 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & % 186.26/24.99 c_Power_Opower__class_Opower(v0) = v2 & c_Rings_Odvd__class_Odvd(v0) = v1 & % 186.26/24.99 c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.26/24.99 c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.26/24.99 c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.26/24.99 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/24.99 c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v11, v_pa____) = v12 & hAPP(v8, % 186.26/24.99 v9) = v10 & hAPP(v2, v7) = v8 & hAPP(v1, v10) = v11 & $i(v12) & $i(v11) & % 186.26/24.99 $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 186.26/24.99 $i(v2) & $i(v1) & $i(v0) & hBOOL(v12)) % 186.26/24.99 % 186.26/24.99 (fact_ap_I2_J) % 186.26/24.99 $i(v_a____) & $i(v_pa____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? [v1: % 186.26/24.99 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 186.26/24.99 ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? % 186.26/24.99 [v12: $i] : ? [v13: $i] : % 186.26/24.99 (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v3 & % 186.26/24.99 c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & c_Nat_OSuc(v9) = v10 & % 186.26/24.99 c_Power_Opower__class_Opower(v0) = v2 & c_Rings_Odvd__class_Odvd(v0) = v1 & % 186.26/24.99 c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.26/24.99 c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.26/24.99 c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.26/24.99 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/24.99 c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v12, v_pa____) = v13 & hAPP(v8, % 186.26/24.99 v10) = v11 & hAPP(v2, v7) = v8 & hAPP(v1, v11) = v12 & $i(v13) & $i(v12) & % 186.26/24.99 $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 186.26/24.99 $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ hBOOL(v13)) % 186.26/24.99 % 186.26/24.99 (fact_calculation) % 186.26/24.99 $i(v_na____) & $i(v_qa____) & $i(v_pa____) & $i(tc_Complex_Ocomplex) & ? [v0: % 186.26/24.99 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 186.26/24.99 ? [v6: $i] : ? [v7: $i] : (tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/24.99 $i(v0) & (( ~ (v1 = v_qa____) & c_Groups_Ozero__class_Ozero(v0) = v1 & % 186.26/24.99 $i(v1)) | (c_Power_Opower__class_Opower(v0) = v4 & % 186.26/24.99 c_Rings_Odvd__class_Odvd(v0) = v2 & hAPP(v5, v_na____) = v6 & hAPP(v4, % 186.26/24.99 v_qa____) = v5 & hAPP(v3, v6) = v7 & hAPP(v2, v_pa____) = v3 & $i(v7) % 186.26/24.99 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & hBOOL(v7)))) % 186.26/24.99 % 186.26/24.99 (fact_mult__poly__0__right) % 186.26/24.99 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 186.26/24.99 $i] : ! [v6: $i] : (v6 = v5 | ~ (c_Groups_Otimes__class_Otimes(v2) = v3) | % 186.26/24.99 ~ (tc_Polynomial_Opoly(v1) = v2) | ~ (c_Groups_Ozero__class_Ozero(v2) = % 186.26/24.99 v5) | ~ (hAPP(v4, v5) = v6) | ~ (hAPP(v3, v0) = v4) | ~ $i(v1) | ~ % 186.26/24.99 $i(v0) | ~ class_Rings_Ocomm__semiring__0(v1)) % 186.26/24.99 % 186.26/24.99 (fact_oa) % 186.26/25.00 $i(v_a____) & $i(tc_Nat_Onat) & $i(v_pa____) & $i(tc_Complex_Ocomplex) & ? % 186.26/25.00 [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & % 186.26/25.00 c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v0 & % 186.26/25.00 c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = v1 & $i(v1) & $i(v0)) % 186.26/25.00 % 186.26/25.00 (fact_pne) % 186.26/25.00 $i(v_pa____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = % 186.26/25.00 v_pa____) & tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/25.00 c_Groups_Ozero__class_Ozero(v0) = v1 & $i(v1) & $i(v0)) % 186.26/25.00 % 186.26/25.00 (fact_q0) % 186.26/25.00 $i(v_qa____) & $i(tc_Complex_Ocomplex) & ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = % 186.26/25.00 v_qa____) & tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/25.00 c_Groups_Ozero__class_Ozero(v0) = v1 & $i(v1) & $i(v0)) % 186.26/25.00 % 186.26/25.00 (fact_r) % 186.26/25.00 $i(v_r____) & $i(v_a____) & $i(v_qa____) & $i(tc_Complex_Ocomplex) & ? [v0: % 186.26/25.00 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 186.26/25.00 ? [v6: $i] : ? [v7: $i] : (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.26/25.00 c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v2 & % 186.26/25.00 c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v3 & % 186.26/25.00 c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v4) = v5 & % 186.26/25.00 c_Polynomial_OpCons(tc_Complex_Ocomplex, v2, v5) = v6 & % 186.26/25.00 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/25.00 c_Groups_Ozero__class_Ozero(v0) = v4 & hAPP(v7, v_r____) = v_qa____ & % 186.26/25.00 hAPP(v1, v6) = v7 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 186.26/25.00 $i(v1) & $i(v0)) % 186.26/25.00 % 186.26/25.00 (fact_s) % 186.26/25.00 $i(v_s____) & $i(v_a____) & $i(v_pa____) & $i(tc_Complex_Ocomplex) & ? [v0: % 186.26/25.00 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 186.26/25.00 ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: % 186.26/25.00 $i] : (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.26/25.00 c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v3 & % 186.26/25.00 c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & % 186.26/25.00 c_Power_Opower__class_Opower(v0) = v2 & % 186.26/25.00 c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.26/25.00 c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.26/25.00 c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.26/25.00 tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.26/25.00 c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v11, v_s____) = v_pa____ & % 186.26/25.00 hAPP(v8, v9) = v10 & hAPP(v2, v7) = v8 & hAPP(v1, v10) = v11 & $i(v11) & % 186.26/25.00 $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 186.26/25.00 $i(v2) & $i(v1) & $i(v0)) % 186.26/25.00 % 186.26/25.00 (function-axioms) % 186.26/25.01 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 186.26/25.01 $i] : ! [v6: $i] : (v1 = v0 | ~ (c_Polynomial_Opoly__rec(v6, v5, v4, v3, % 186.26/25.01 v2) = v1) | ~ (c_Polynomial_Opoly__rec(v6, v5, v4, v3, v2) = v0)) & ! % 186.26/25.01 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 186.26/25.01 : (v1 = v0 | ~ (c_If(v5, v4, v3, v2) = v1) | ~ (c_If(v5, v4, v3, v2) = v0)) % 186.26/25.01 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = % 186.26/25.01 v0 | ~ (c_Groups_Ominus__class_Ominus(v4, v3, v2) = v1) | ~ % 186.26/25.01 (c_Groups_Ominus__class_Ominus(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 186.26/25.01 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Divides_Odiv__class_Omod(v4, v3, v2) = v1) | ~ % 186.26/25.01 (c_Divides_Odiv__class_Omod(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 186.26/25.01 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Polynomial_Opoly__gcd(v4, v3, v2) = v1) | ~ (c_Polynomial_Opoly__gcd(v4, % 186.26/25.01 v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 186.26/25.01 ! [v4: $i] : (v1 = v0 | ~ (c_Groups_Oplus__class_Oplus(v4, v3, v2) = v1) | % 186.26/25.01 ~ (c_Groups_Oplus__class_Oplus(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 186.26/25.01 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Power_Opower_Opower(v4, v3, v2) = v1) | ~ (c_Power_Opower_Opower(v4, v3, % 186.26/25.01 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 186.26/25.01 [v4: $i] : (v1 = v0 | ~ (c_Nat_Onat_Onat__case(v4, v3, v2) = v1) | ~ % 186.26/25.01 (c_Nat_Onat_Onat__case(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 186.26/25.01 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Polynomial_Osynthetic__div(v4, v3, v2) = v1) | ~ % 186.26/25.01 (c_Polynomial_Osynthetic__div(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 186.26/25.01 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Polynomial_Opcompose(v4, v3, v2) = v1) | ~ (c_Polynomial_Opcompose(v4, % 186.26/25.01 v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 186.26/25.01 ! [v4: $i] : (v1 = v0 | ~ (c_Polynomial_OpCons(v4, v3, v2) = v1) | ~ % 186.26/25.01 (c_Polynomial_OpCons(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 186.26/25.01 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (c_Polynomial_Oorder(v4, % 186.26/25.01 v3, v2) = v1) | ~ (c_Polynomial_Oorder(v4, v3, v2) = v0)) & ! [v0: $i] % 186.26/25.01 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Polynomial_Osmult(v4, v3, v2) = v1) | ~ (c_Polynomial_Osmult(v4, v3, v2) % 186.26/25.01 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 186.26/25.01 $i] : (v1 = v0 | ~ (c_Polynomial_Omonom(v4, v3, v2) = v1) | ~ % 186.26/25.01 (c_Polynomial_Omonom(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 186.26/25.01 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v4, v3, v2) = v1) % 186.26/25.01 | ~ (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v4, v3, v2) = % 186.26/25.01 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 186.26/25.01 ~ (c_Rings_Oinverse__class_Oinverse(v3, v2) = v1) | ~ % 186.26/25.01 (c_Rings_Oinverse__class_Oinverse(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 186.26/25.01 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_Polynomial_OAbs__poly(v3, v2) = % 186.26/25.01 v1) | ~ (c_Polynomial_OAbs__poly(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 186.26/25.01 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (tc_fun(v3, v2) = v1) | ~ % 186.26/25.01 (tc_fun(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 186.26/25.01 $i] : (v1 = v0 | ~ (c_Groups_Ouminus__class_Ouminus(v3, v2) = v1) | ~ % 186.26/25.01 (c_Groups_Ouminus__class_Ouminus(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 186.26/25.01 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_fequal(v3, v2) = v1) | ~ % 186.26/25.01 (c_fequal(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 186.26/25.01 $i] : (v1 = v0 | ~ (c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(v3, % 186.26/25.01 v2) = v1) | ~ (c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(v3, % 186.26/25.01 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 186.26/25.01 = v0 | ~ (c_Polynomial_Odegree(v3, v2) = v1) | ~ (c_Polynomial_Odegree(v3, % 186.26/25.01 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 186.26/25.01 = v0 | ~ (c_Polynomial_Ocoeff(v3, v2) = v1) | ~ (c_Polynomial_Ocoeff(v3, % 186.26/25.01 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 186.26/25.01 = v0 | ~ (c_Polynomial_Opoly(v3, v2) = v1) | ~ (c_Polynomial_Opoly(v3, v2) % 186.26/25.01 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 186.26/25.01 | ~ (hAPP(v3, v2) = v1) | ~ (hAPP(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 186.26/25.01 $i] : ! [v2: $i] : (v1 = v0 | ~ (c_Groups_Otimes__class_Otimes(v2) = v1) | % 186.26/25.01 ~ (c_Groups_Otimes__class_Otimes(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 186.26/25.01 ! [v2: $i] : (v1 = v0 | ~ (c_Groups_Oone__class_Oone(v2) = v1) | ~ % 186.26/25.01 (c_Groups_Oone__class_Oone(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 186.26/25.01 $i] : (v1 = v0 | ~ (c_Nat_OSuc(v2) = v1) | ~ (c_Nat_OSuc(v2) = v0)) & ! % 186.26/25.01 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 186.26/25.01 (c_Power_Opower__class_Opower(v2) = v1) | ~ % 186.26/25.01 (c_Power_Opower__class_Opower(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 186.26/25.01 [v2: $i] : (v1 = v0 | ~ (c_Rings_Odvd__class_Odvd(v2) = v1) | ~ % 186.26/25.01 (c_Rings_Odvd__class_Odvd(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 186.26/25.01 $i] : (v1 = v0 | ~ (tc_Polynomial_Opoly(v2) = v1) | ~ % 186.26/25.01 (tc_Polynomial_Opoly(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 186.26/25.01 (v1 = v0 | ~ (c_Groups_Ozero__class_Ozero(v2) = v1) | ~ % 186.26/25.01 (c_Groups_Ozero__class_Ozero(v2) = v0)) % 186.26/25.01 % 186.26/25.01 Further assumptions not needed in the proof: % 186.26/25.01 -------------------------------------------- % 186.26/25.01 arity_Complex__Ocomplex__Fields_Ofield, % 186.26/25.01 arity_Complex__Ocomplex__Fields_Ofield__inverse__zero, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Oab__group__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Oab__semigroup__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Oab__semigroup__mult, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ocancel__ab__semigroup__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ocancel__comm__monoid__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ocancel__semigroup__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ocomm__monoid__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ocomm__monoid__mult, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ogroup__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ominus, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Omonoid__add, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Omonoid__mult, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Oone, arity_Complex__Ocomplex__Groups_Ouminus, % 186.26/25.01 arity_Complex__Ocomplex__Groups_Ozero, % 186.26/25.01 arity_Complex__Ocomplex__Int_Oring__char__0, % 186.26/25.01 arity_Complex__Ocomplex__Power_Opower, % 186.26/25.01 arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Ocomm__ring, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Ocomm__ring__1, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Ocomm__semiring, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Ocomm__semiring__1, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Odivision__ring, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Odivision__ring__inverse__zero, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Odvd, arity_Complex__Ocomplex__Rings_Oidom, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Omult__zero, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Ono__zero__divisors, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Oring, arity_Complex__Ocomplex__Rings_Oring__1, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Oring__1__no__zero__divisors, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Osemiring, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Osemiring__0, % 186.26/25.01 arity_Complex__Ocomplex__Rings_Ozero__neq__one, % 186.26/25.01 arity_Complex__Ocomplex__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 186.26/25.01 arity_HOL__Obool__Groups_Ominus, arity_HOL__Obool__Groups_Ouminus, % 186.26/25.01 arity_HOL__Obool__Lattices_Oboolean__algebra, arity_HOL__Obool__Orderings_Oord, % 186.26/25.01 arity_HOL__Obool__Orderings_Oorder, arity_HOL__Obool__Orderings_Opreorder, % 186.26/25.01 arity_Int__Oint__Divides_Oring__div, arity_Int__Oint__Divides_Osemiring__div, % 186.26/25.02 arity_Int__Oint__Groups_Oab__group__add, % 186.26/25.02 arity_Int__Oint__Groups_Oab__semigroup__add, % 186.26/25.02 arity_Int__Oint__Groups_Oab__semigroup__mult, % 186.26/25.02 arity_Int__Oint__Groups_Ocancel__ab__semigroup__add, % 186.26/25.02 arity_Int__Oint__Groups_Ocancel__comm__monoid__add, % 186.26/25.02 arity_Int__Oint__Groups_Ocancel__semigroup__add, % 186.26/25.02 arity_Int__Oint__Groups_Ocomm__monoid__add, % 186.26/25.02 arity_Int__Oint__Groups_Ocomm__monoid__mult, % 186.26/25.02 arity_Int__Oint__Groups_Ogroup__add, % 186.26/25.02 arity_Int__Oint__Groups_Olinordered__ab__group__add, % 186.26/25.02 arity_Int__Oint__Groups_Ominus, arity_Int__Oint__Groups_Omonoid__add, % 186.26/25.02 arity_Int__Oint__Groups_Omonoid__mult, arity_Int__Oint__Groups_Oone, % 186.26/25.02 arity_Int__Oint__Groups_Oordered__ab__group__add, % 186.26/25.02 arity_Int__Oint__Groups_Oordered__ab__semigroup__add, % 186.26/25.02 arity_Int__Oint__Groups_Oordered__ab__semigroup__add__imp__le, % 186.26/25.02 arity_Int__Oint__Groups_Oordered__cancel__ab__semigroup__add, % 186.26/25.02 arity_Int__Oint__Groups_Oordered__comm__monoid__add, % 186.26/25.02 arity_Int__Oint__Groups_Ouminus, arity_Int__Oint__Groups_Ozero, % 186.26/25.02 arity_Int__Oint__Int_Oring__char__0, arity_Int__Oint__Orderings_Olinorder, % 186.26/25.02 arity_Int__Oint__Orderings_Oord, arity_Int__Oint__Orderings_Oorder, % 186.26/25.02 arity_Int__Oint__Orderings_Opreorder, arity_Int__Oint__Power_Opower, % 186.26/25.02 arity_Int__Oint__Rings_Ocomm__ring, arity_Int__Oint__Rings_Ocomm__ring__1, % 186.44/25.02 arity_Int__Oint__Rings_Ocomm__semiring, % 186.44/25.02 arity_Int__Oint__Rings_Ocomm__semiring__0, % 186.44/25.02 arity_Int__Oint__Rings_Ocomm__semiring__1, arity_Int__Oint__Rings_Odvd, % 186.44/25.02 arity_Int__Oint__Rings_Oidom, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__comm__semiring__strict, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__idom, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__ring, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__ring__strict, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__semidom, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__semiring, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__semiring__1, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__semiring__1__strict, % 186.44/25.02 arity_Int__Oint__Rings_Olinordered__semiring__strict, % 186.44/25.02 arity_Int__Oint__Rings_Omult__zero, arity_Int__Oint__Rings_Ono__zero__divisors, % 186.44/25.02 arity_Int__Oint__Rings_Oordered__cancel__semiring, % 186.44/25.02 arity_Int__Oint__Rings_Oordered__comm__semiring, % 186.44/25.02 arity_Int__Oint__Rings_Oordered__ring, % 186.44/25.02 arity_Int__Oint__Rings_Oordered__semiring, arity_Int__Oint__Rings_Oring, % 186.44/25.02 arity_Int__Oint__Rings_Oring__1, % 186.44/25.02 arity_Int__Oint__Rings_Oring__1__no__zero__divisors, % 186.44/25.02 arity_Int__Oint__Rings_Oring__no__zero__divisors, % 186.44/25.02 arity_Int__Oint__Rings_Osemiring, arity_Int__Oint__Rings_Osemiring__0, % 186.44/25.02 arity_Int__Oint__Rings_Ozero__neq__one, % 186.44/25.02 arity_Int__Oint__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 186.44/25.02 arity_Nat__Onat__Divides_Osemiring__div, % 186.44/25.02 arity_Nat__Onat__Groups_Oab__semigroup__add, % 186.44/25.02 arity_Nat__Onat__Groups_Oab__semigroup__mult, % 186.44/25.02 arity_Nat__Onat__Groups_Ocancel__ab__semigroup__add, % 186.44/25.02 arity_Nat__Onat__Groups_Ocancel__comm__monoid__add, % 186.44/25.02 arity_Nat__Onat__Groups_Ocancel__semigroup__add, % 186.44/25.02 arity_Nat__Onat__Groups_Ocomm__monoid__add, % 186.44/25.02 arity_Nat__Onat__Groups_Ocomm__monoid__mult, arity_Nat__Onat__Groups_Ominus, % 186.44/25.02 arity_Nat__Onat__Groups_Omonoid__add, arity_Nat__Onat__Groups_Omonoid__mult, % 186.44/25.02 arity_Nat__Onat__Groups_Oone, % 186.44/25.02 arity_Nat__Onat__Groups_Oordered__ab__semigroup__add, % 186.44/25.02 arity_Nat__Onat__Groups_Oordered__ab__semigroup__add__imp__le, % 186.44/25.02 arity_Nat__Onat__Groups_Oordered__cancel__ab__semigroup__add, % 186.44/25.02 arity_Nat__Onat__Groups_Oordered__comm__monoid__add, % 186.44/25.02 arity_Nat__Onat__Groups_Ozero, arity_Nat__Onat__Orderings_Olinorder, % 186.44/25.02 arity_Nat__Onat__Orderings_Oord, arity_Nat__Onat__Orderings_Oorder, % 186.44/25.02 arity_Nat__Onat__Orderings_Opreorder, arity_Nat__Onat__Power_Opower, % 186.44/25.02 arity_Nat__Onat__Rings_Ocomm__semiring, % 186.44/25.02 arity_Nat__Onat__Rings_Ocomm__semiring__0, % 186.44/25.02 arity_Nat__Onat__Rings_Ocomm__semiring__1, arity_Nat__Onat__Rings_Odvd, % 186.44/25.02 arity_Nat__Onat__Rings_Olinordered__comm__semiring__strict, % 186.44/25.02 arity_Nat__Onat__Rings_Olinordered__semidom, % 186.44/25.02 arity_Nat__Onat__Rings_Olinordered__semiring, % 186.44/25.02 arity_Nat__Onat__Rings_Olinordered__semiring__strict, % 186.44/25.02 arity_Nat__Onat__Rings_Omult__zero, arity_Nat__Onat__Rings_Ono__zero__divisors, % 186.44/25.02 arity_Nat__Onat__Rings_Oordered__cancel__semiring, % 186.44/25.02 arity_Nat__Onat__Rings_Oordered__comm__semiring, % 186.44/25.02 arity_Nat__Onat__Rings_Oordered__semiring, arity_Nat__Onat__Rings_Osemiring, % 186.44/25.02 arity_Nat__Onat__Rings_Osemiring__0, arity_Nat__Onat__Rings_Ozero__neq__one, % 186.44/25.02 arity_Nat__Onat__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 186.44/25.02 arity_Polynomial__Opoly__Divides_Oring__div, % 186.44/25.02 arity_Polynomial__Opoly__Divides_Osemiring__div, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oab__group__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oab__semigroup__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oab__semigroup__mult, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ocancel__ab__semigroup__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ocancel__comm__monoid__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ocancel__semigroup__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ocomm__monoid__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ocomm__monoid__mult, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ogroup__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Olinordered__ab__group__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ominus, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Omonoid__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Omonoid__mult, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oone, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oordered__ab__group__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oordered__ab__semigroup__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oordered__ab__semigroup__add__imp__le, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oordered__cancel__ab__semigroup__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Oordered__comm__monoid__add, % 186.44/25.02 arity_Polynomial__Opoly__Groups_Ouminus, arity_Polynomial__Opoly__Groups_Ozero, % 186.44/25.02 arity_Polynomial__Opoly__Int_Oring__char__0, % 186.44/25.02 arity_Polynomial__Opoly__Orderings_Olinorder, % 186.44/25.02 arity_Polynomial__Opoly__Orderings_Oord, % 186.44/25.02 arity_Polynomial__Opoly__Orderings_Oorder, % 186.44/25.02 arity_Polynomial__Opoly__Orderings_Opreorder, % 186.44/25.02 arity_Polynomial__Opoly__Power_Opower, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Ocomm__ring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Ocomm__ring__1, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Ocomm__semiring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Ocomm__semiring__0, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Ocomm__semiring__1, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Odvd, arity_Polynomial__Opoly__Rings_Oidom, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__comm__semiring__strict, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__idom, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__ring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__ring__strict, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__semidom, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__semiring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__semiring__1, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__semiring__1__strict, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Olinordered__semiring__strict, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Omult__zero, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Ono__zero__divisors, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Oordered__cancel__semiring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Oordered__comm__semiring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Oordered__ring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Oordered__semiring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Oring, arity_Polynomial__Opoly__Rings_Oring__1, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Oring__1__no__zero__divisors, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Oring__no__zero__divisors, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Osemiring, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Osemiring__0, % 186.44/25.02 arity_Polynomial__Opoly__Rings_Ozero__neq__one, % 186.44/25.02 arity_Polynomial__Opoly__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct, % 186.44/25.02 arity_fun__Groups_Ominus, arity_fun__Groups_Ouminus, % 186.44/25.02 arity_fun__Lattices_Oboolean__algebra, arity_fun__Orderings_Oord, % 186.44/25.02 arity_fun__Orderings_Oorder, arity_fun__Orderings_Opreorder, % 186.44/25.02 fact_Divides_Otransfer__nat__int__function__closures_I2_J, % 186.44/25.02 fact_Nat_Oadd__0__right, fact_Nat_Odiff__diff__eq, % 186.44/25.02 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J, % 186.44/25.02 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J, % 186.44/25.02 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J, % 186.44/25.02 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J, % 186.44/25.02 fact_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J, % 186.44/25.02 fact_One__nat__def, fact_Suc__diff__diff, fact_Suc__diff__le, % 186.44/25.02 fact_Suc__eq__plus1, fact_Suc__eq__plus1__left, fact_Suc__inject, fact_Suc__leD, % 186.44/25.02 fact_Suc__leI, fact_Suc__le__eq, fact_Suc__le__lessD, fact_Suc__le__mono, % 186.44/25.02 fact_Suc__lessD, fact_Suc__lessI, fact_Suc__less__SucD, fact_Suc__less__eq, % 186.44/25.02 fact_Suc__mono, fact_Suc__mult__cancel1, fact_Suc__mult__le__cancel1, % 186.44/25.02 fact_Suc__mult__less__cancel1, fact_Suc__n__not__le__n, fact_Suc__n__not__n, % 186.44/25.02 fact_Suc__neq__Zero, fact_Suc__not__Zero, fact_Zero__neq__Suc, % 186.44/25.02 fact_Zero__not__Suc, fact_a, fact_ab__left__minus, % 186.44/25.02 fact_ab__semigroup__add__class_Oadd__ac_I1_J, % 186.44/25.02 fact_ab__semigroup__mult__class_Omult__ac_I1_J, fact_add1__zle__eq, % 186.44/25.02 fact_add_Ocomm__neutral, fact_add__0, fact_add__0__iff, fact_add__0__left, % 186.44/25.02 fact_add__0__right, fact_add__Suc, fact_add__Suc__right, fact_add__Suc__shift, % 186.44/25.02 fact_add__diff__assoc, fact_add__diff__inverse, fact_add__eq__0__iff, % 186.44/25.02 fact_add__eq__self__zero, fact_add__gr__0, fact_add__imp__eq, % 186.44/25.02 fact_add__increasing, fact_add__increasing2, fact_add__is__0, fact_add__is__1, % 186.44/25.02 fact_add__leD1, fact_add__leD2, fact_add__leE, fact_add__le__cancel__left, % 186.44/25.02 fact_add__le__cancel__right, fact_add__le__imp__le__left, % 186.44/25.02 fact_add__le__imp__le__right, fact_add__le__less__mono, fact_add__le__mono, % 186.44/25.02 fact_add__le__mono1, fact_add__left__cancel, fact_add__left__imp__eq, % 186.44/25.02 fact_add__left__mono, fact_add__lessD1, fact_add__less__cancel__left, % 186.44/25.02 fact_add__less__cancel__right, fact_add__less__imp__less__left, % 186.44/25.02 fact_add__less__imp__less__right, fact_add__less__le__mono, % 186.44/25.02 fact_add__less__mono, fact_add__less__mono1, fact_add__minus__cancel, % 186.44/25.02 fact_add__mono, fact_add__monom, fact_add__mult__distrib, % 186.44/25.02 fact_add__mult__distrib2, fact_add__neg__neg, fact_add__neg__nonpos, % 186.44/25.02 fact_add__nonneg__eq__0__iff, fact_add__nonneg__nonneg, fact_add__nonneg__pos, % 186.44/25.02 fact_add__nonpos__neg, fact_add__nonpos__nonpos, fact_add__pCons, % 186.44/25.02 fact_add__poly__code_I1_J, fact_add__poly__code_I2_J, fact_add__pos__nonneg, % 186.44/25.02 fact_add__pos__pos, fact_add__right__cancel, fact_add__right__imp__eq, % 186.44/25.02 fact_add__right__mono, fact_add__scale__eq__noteq, fact_add__strict__increasing, % 186.44/25.02 fact_add__strict__increasing2, fact_add__strict__left__mono, % 186.44/25.02 fact_add__strict__mono, fact_add__strict__right__mono, fact_assms_I1_J, % 186.44/25.02 fact_assms_I2_J, fact_assms_I3_J, fact_coeff__0, fact_coeff__1, fact_coeff__add, % 186.44/25.02 fact_coeff__diff, fact_coeff__eq__0, fact_coeff__inject, fact_coeff__inverse, % 186.44/25.02 fact_coeff__linear__power, fact_coeff__minus, fact_coeff__monom, % 186.44/25.02 fact_coeff__mult__degree__sum, fact_coeff__pCons, fact_coeff__pCons__0, % 186.44/25.02 fact_coeff__pCons__Suc, fact_coeff__smult, fact_combine__common__factor, % 186.44/25.02 fact_comm__mult__left__mono, fact_comm__mult__strict__left__mono, % 186.44/25.02 fact_comm__ring__1__class_Onormalizing__ring__rules_I1_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I27_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I8_J, % 186.44/25.02 fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J, % 186.44/25.02 fact_comm__semiring__class_Odistrib, fact_compl__eq__compl__iff, % 186.44/25.02 fact_compl__le__compl__iff, fact_compl__mono, fact_convex__bound__le, % 186.44/25.02 fact_convex__bound__lt, fact_crossproduct__eq, fact_crossproduct__noteq, % 186.44/25.02 fact_degree__0, fact_degree__1, fact_degree__add__eq__left, % 186.44/25.02 fact_degree__add__eq__right, fact_degree__add__le, fact_degree__add__less, % 186.44/25.02 fact_degree__le, fact_degree__linear__power, fact_degree__minus, % 186.44/25.02 fact_degree__mod__less, fact_degree__monom__eq, fact_degree__monom__le, % 186.44/25.02 fact_degree__mult__eq, fact_degree__mult__le, fact_degree__offset__poly, % 186.44/25.02 fact_degree__pCons__0, fact_degree__pCons__eq, fact_degree__pCons__eq__if, % 186.44/25.02 fact_degree__pCons__le, fact_degree__pcompose__le, fact_degree__power__le, % 186.44/25.02 fact_degree__smult__eq, fact_degree__smult__le, fact_diff__0__eq__0, % 186.44/25.02 fact_diff__0__right, fact_diff__Suc__1, fact_diff__Suc__Suc, % 186.44/25.02 fact_diff__Suc__eq__diff__pred, fact_diff__commute, fact_diff__diff__cancel, % 186.44/25.02 fact_diff__diff__right, fact_diff__eq__diff__eq, fact_diff__eq__diff__less, % 186.44/25.02 fact_diff__eq__diff__less__eq, fact_diff__is__0__eq, fact_diff__is__0__eq_H, % 186.44/25.02 fact_diff__le__mono, fact_diff__le__mono2, fact_diff__le__self, fact_diff__less, % 186.44/25.02 fact_diff__less__Suc, fact_diff__less__mono, fact_diff__less__mono2, % 186.44/25.02 fact_diff__monom, fact_diff__mult__distrib, fact_diff__mult__distrib2, % 186.44/25.02 fact_diff__pCons, fact_diff__self, fact_diff__self__eq__0, % 186.44/25.02 fact_diffs0__imp__equal, fact_division__ring__inverse__add, fact_divisors__zero, % 186.44/25.02 fact_double__add__le__zero__iff__single__add__le__zero, % 186.44/25.02 fact_double__add__less__zero__iff__single__add__less__zero, fact_double__compl, % 186.44/25.02 fact_double__eq__0__iff, fact_double__zero__sym, fact_dpn, fact_dvdI, % 186.44/25.02 fact_dvd_Oantisym, fact_dvd_Oantisym__conv, fact_dvd_Oeq__iff, % 186.44/25.02 fact_dvd_Oeq__refl, fact_dvd_Ole__imp__less__or__eq, fact_dvd_Ole__less, % 186.44/25.02 fact_dvd_Ole__less__trans, fact_dvd_Ole__neq__trans, fact_dvd_Oless__asym, % 186.44/25.02 fact_dvd_Oless__asym_H, fact_dvd_Oless__imp__le, fact_dvd_Oless__imp__neq, % 186.44/25.02 fact_dvd_Oless__imp__not__eq, fact_dvd_Oless__imp__not__eq2, % 186.44/25.02 fact_dvd_Oless__imp__not__less, fact_dvd_Oless__le, fact_dvd_Oless__le__trans, % 186.44/25.02 fact_dvd_Oless__not__sym, fact_dvd_Oless__trans, fact_dvd_OmonoD, % 186.44/25.02 fact_dvd_Oneq__le__trans, fact_dvd_Oord__eq__le__trans, % 186.44/25.02 fact_dvd_Oord__eq__less__trans, fact_dvd_Oord__le__eq__trans, % 186.44/25.02 fact_dvd_Oord__less__eq__trans, fact_dvd_Oorder__refl, fact_dvd_Oorder__trans, % 186.44/25.02 fact_dvd__0__left, fact_dvd__0__right, fact_dvd__1__iff__1, fact_dvd__1__left, % 186.44/25.02 fact_dvd__add, fact_dvd__antisym, fact_dvd__diff, fact_dvd__diffD, % 186.44/25.02 fact_dvd__diffD1, fact_dvd__diff__nat, fact_dvd__eq__mod__eq__0, % 186.44/25.02 fact_dvd__iff__poly__eq__0, fact_dvd__imp__degree__le, fact_dvd__imp__le, % 186.44/25.02 fact_dvd__imp__mod__0, fact_dvd__minus__iff, fact_dvd__mod, fact_dvd__mod__iff, % 186.44/25.02 fact_dvd__mod__imp__dvd, fact_dvd__mult, fact_dvd__mult2, % 186.44/25.02 fact_dvd__mult__cancel, fact_dvd__mult__cancel1, fact_dvd__mult__cancel2, % 186.44/25.02 fact_dvd__mult__cancel__left, fact_dvd__mult__cancel__right, % 186.44/25.02 fact_dvd__mult__left, fact_dvd__mult__right, fact_dvd__poly__gcd__iff, % 186.44/25.02 fact_dvd__pos__nat, fact_dvd__power, fact_dvd__power__le, fact_dvd__power__same, % 186.44/25.02 fact_dvd__reduce, fact_dvd__refl, fact_dvd__smult, fact_dvd__smult__cancel, % 186.44/25.02 fact_dvd__smult__iff, fact_dvd__trans, fact_dvd__triv__left, % 186.44/25.02 fact_dvd__triv__right, fact_eq__add__iff1, fact_eq__add__iff2, % 186.44/25.02 fact_eq__diff__iff, fact_eq__iff__diff__eq__0, fact_eq__imp__le, % 186.44/25.02 fact_eq__neg__iff__add__eq__0, fact_eq__zero__or__degree__less, % 186.44/25.02 fact_equal__neg__zero, fact_equation__minus__iff, fact_even__less__0__iff, % 186.44/25.02 fact_ex__least__nat__less, fact_expand__poly__eq, fact_ext, fact_field__inverse, % 186.44/25.02 fact_field__inverse__zero, fact_field__le__mult__one__interval, % 186.44/25.02 fact_field__power__not__zero, fact_gcd__lcm__complete__lattice__nat_Obot__least, % 186.44/25.02 fact_gcd__lcm__complete__lattice__nat_Otop__greatest, fact_gr0I, % 186.44/25.02 fact_gr0__conv__Suc, fact_gr__implies__not0, fact_incr__mult__lemma, % 186.44/25.02 fact_int__0__less__1, fact_int__0__neq__1, fact_int__one__le__iff__zero__less, % 186.44/25.02 fact_inverse__1, fact_inverse__add, fact_inverse__eq__1__iff, % 186.44/25.02 fact_inverse__eq__iff__eq, fact_inverse__eq__imp__eq, fact_inverse__inverse__eq, % 186.44/25.02 fact_inverse__le__1__iff, fact_inverse__le__imp__le, % 186.44/25.02 fact_inverse__le__imp__le__neg, fact_inverse__less__1__iff, % 186.44/25.02 fact_inverse__less__imp__less, fact_inverse__less__imp__less__neg, % 186.44/25.02 fact_inverse__minus__eq, fact_inverse__mult__distrib, % 186.44/25.02 fact_inverse__negative__iff__negative, fact_inverse__negative__imp__negative, % 186.44/25.02 fact_inverse__nonnegative__iff__nonnegative, % 186.44/25.02 fact_inverse__nonpositive__iff__nonpositive, % 186.44/25.02 fact_inverse__nonzero__iff__nonzero, fact_inverse__positive__iff__positive, % 186.44/25.02 fact_inverse__positive__imp__positive, fact_inverse__unique, fact_inverse__zero, % 186.44/25.02 fact_inverse__zero__imp__zero, fact_le0, fact_leD, fact_leI, fact_le__0__eq, % 186.44/25.02 fact_le__SucE, fact_le__SucI, fact_le__Suc__eq, fact_le__Suc__ex__iff, % 186.44/25.02 fact_le__add1, fact_le__add2, fact_le__add__diff, fact_le__add__diff__inverse, % 186.44/25.02 fact_le__add__diff__inverse2, fact_le__add__iff1, fact_le__add__iff2, % 186.44/25.02 fact_le__antisym, fact_le__cube, fact_le__degree, fact_le__diff__conv, % 186.44/25.02 fact_le__diff__conv2, fact_le__diff__iff, fact_le__eq__less__or__eq, % 186.44/25.02 fact_le__funD, fact_le__funE, fact_le__fun__def, fact_le__iff__add, % 186.44/25.02 fact_le__iff__diff__le__0, fact_le__imp__0__less, fact_le__imp__inverse__le, % 186.44/25.02 fact_le__imp__inverse__le__neg, fact_le__imp__less__Suc, fact_le__imp__neg__le, % 186.44/25.02 fact_le__imp__power__dvd, fact_le__less__Suc__eq, fact_le__minus__iff, % 186.44/25.02 fact_le__minus__self__iff, fact_le__mod__geq, fact_le__neq__implies__less, % 186.44/25.02 fact_le__refl, fact_le__square, fact_le__trans, fact_leading__coeff__0__iff, % 186.44/25.02 fact_leading__coeff__neq__0, fact_left__add__mult__distrib, fact_left__inverse, % 186.44/25.02 fact_left__minus, fact_lessI, fact_less__1__mult, fact_less__Suc0, % 186.44/25.02 fact_less__SucE, fact_less__SucI, fact_less__Suc__eq, % 186.44/25.02 fact_less__Suc__eq__0__disj, fact_less__Suc__eq__le, fact_less__add__Suc1, % 186.44/25.02 fact_less__add__Suc2, fact_less__add__eq__less, fact_less__add__one, % 186.44/25.02 fact_less__antisym, fact_less__degree__imp, fact_less__diff__conv, % 186.44/25.02 fact_less__diff__iff, fact_less__eq__Suc__le, fact_less__eq__nat_Osimps_I1_J, % 186.44/25.02 fact_less__fun__def, fact_less__iff__Suc__add, fact_less__iff__diff__less__0, % 186.44/25.02 fact_less__imp__diff__less, fact_less__imp__inverse__less, % 186.44/25.02 fact_less__imp__inverse__less__neg, fact_less__imp__le__nat, % 186.44/25.02 fact_less__imp__neq, fact_less__irrefl__nat, fact_less__le__not__le, % 186.44/25.02 fact_less__minus__iff, fact_less__minus__self__iff, fact_less__nat__zero__code, % 186.44/25.02 fact_less__not__refl, fact_less__not__refl2, fact_less__not__refl3, % 186.44/25.02 fact_less__or__eq__imp__le, fact_less__trans__Suc, fact_less__zeroE, % 186.44/25.02 fact_linorder__antisym__conv1, fact_linorder__antisym__conv2, % 186.44/25.02 fact_linorder__antisym__conv3, fact_linorder__cases, fact_linorder__le__cases, % 186.44/25.02 fact_linorder__le__less__linear, fact_linorder__less__linear, % 186.44/25.02 fact_linorder__linear, fact_linorder__neqE, % 186.44/25.02 fact_linorder__neqE__linordered__idom, fact_linorder__neqE__nat, % 186.44/25.02 fact_linorder__neq__iff, fact_linorder__not__le, fact_linorder__not__less, % 186.44/25.02 fact_minus__add, fact_minus__add__cancel, fact_minus__add__distrib, % 186.44/25.02 fact_minus__apply, fact_minus__dvd__iff, fact_minus__equation__iff, % 186.44/25.02 fact_minus__le__iff, fact_minus__le__self__iff, fact_minus__less__iff, % 186.44/25.02 fact_minus__minus, fact_minus__monom, fact_minus__mult__commute, % 186.44/25.02 fact_minus__mult__left, fact_minus__mult__minus, fact_minus__mult__right, % 186.44/25.02 fact_minus__nat_Odiff__0, fact_minus__pCons, fact_minus__poly__code_I1_J, % 186.44/25.02 fact_minus__poly__code_I2_J, fact_minus__unique, fact_minus__zero, fact_mod__0, % 186.44/25.02 fact_mod__1, fact_mod__Suc, fact_mod__Suc__eq__Suc__mod, fact_mod__add__cong, % 186.44/25.02 fact_mod__add__eq, fact_mod__add__left__eq, fact_mod__add__right__eq, % 186.44/25.02 fact_mod__add__self1, fact_mod__add__self2, fact_mod__by__0, fact_mod__by__1, % 186.44/25.02 fact_mod__diff__cong, fact_mod__diff__eq, fact_mod__diff__left__eq, % 186.44/25.02 fact_mod__diff__right__eq, fact_mod__eq__0__iff, fact_mod__geq, fact_mod__if, % 186.44/25.02 fact_mod__less, fact_mod__less__divisor, fact_mod__less__eq__dividend, % 186.44/25.02 fact_mod__minus__cong, fact_mod__minus__eq, fact_mod__mod__cancel, % 186.44/25.02 fact_mod__mod__trivial, fact_mod__mult__cong, fact_mod__mult__distrib, % 186.44/25.02 fact_mod__mult__distrib2, fact_mod__mult__eq, fact_mod__mult__left__eq, % 186.44/25.02 fact_mod__mult__mult1, fact_mod__mult__mult2, fact_mod__mult__right__eq, % 186.44/25.02 fact_mod__mult__self1, fact_mod__mult__self1__is__0, fact_mod__mult__self2, % 186.44/25.02 fact_mod__mult__self2__is__0, fact_mod__mult__self3, fact_mod__poly__eq, % 186.44/25.02 fact_mod__poly__less, fact_mod__self, fact_mod__smult__left, % 186.44/25.02 fact_mod__smult__right, fact_monom__0, fact_monom__Suc, fact_monom__eq__0, % 186.44/25.02 fact_monom__eq__0__iff, fact_monom__eq__iff, fact_mult_Oadd__left, % 186.44/25.02 fact_mult_Oadd__right, fact_mult_Ocomm__neutral, fact_mult_Odiff__left, % 186.44/25.02 fact_mult_Odiff__right, fact_mult_Ominus__left, fact_mult_Ominus__right, % 186.44/25.02 fact_mult_Ozero__left, fact_mult_Ozero__right, fact_mult__0, % 186.44/25.02 fact_mult__0__right, fact_mult__1, fact_mult__1__left, fact_mult__1__right, % 186.44/25.02 fact_mult__Suc, fact_mult__Suc__right, fact_mult__cancel1, fact_mult__cancel2, % 186.44/25.02 fact_mult__diff__mult, fact_mult__dvd__mono, fact_mult__eq__0__iff, % 186.44/25.02 fact_mult__eq__1__iff, fact_mult__eq__self__implies__10, fact_mult__idem, % 186.44/25.02 fact_mult__is__0, fact_mult__le__0__iff, fact_mult__le__cancel1, % 186.44/25.02 fact_mult__le__cancel2, fact_mult__le__cancel__left__neg, % 186.44/25.02 fact_mult__le__cancel__left__pos, fact_mult__le__less__imp__less, % 186.44/25.02 fact_mult__le__mono, fact_mult__le__mono1, fact_mult__le__mono2, % 186.44/25.02 fact_mult__left_Oadd, fact_mult__left_Odiff, fact_mult__left_Ominus, % 186.44/25.02 fact_mult__left_Ozero, fact_mult__left__idem, fact_mult__left__le__imp__le, % 186.44/25.02 fact_mult__left__le__one__le, fact_mult__left__less__imp__less, % 186.44/25.02 fact_mult__left__mono, fact_mult__left__mono__neg, fact_mult__less__cancel1, % 186.44/25.02 fact_mult__less__cancel2, fact_mult__less__cancel__left__disj, % 186.44/25.02 fact_mult__less__cancel__left__neg, fact_mult__less__cancel__left__pos, % 186.44/25.02 fact_mult__less__cancel__right__disj, fact_mult__less__imp__less__left, % 186.44/25.02 fact_mult__less__imp__less__right, fact_mult__less__le__imp__less, % 186.44/25.02 fact_mult__less__mono1, fact_mult__less__mono2, fact_mult__mono, % 186.44/25.02 fact_mult__mono_H, fact_mult__monom, fact_mult__neg__neg, fact_mult__neg__pos, % 186.44/25.02 fact_mult__nonneg__nonneg, fact_mult__nonneg__nonpos, % 186.44/25.02 fact_mult__nonneg__nonpos2, fact_mult__nonpos__nonneg, % 186.44/25.02 fact_mult__nonpos__nonpos, fact_mult__pCons__left, fact_mult__pCons__right, % 186.44/25.02 fact_mult__poly__0__left, fact_mult__poly__add__left, fact_mult__pos__neg, % 186.44/25.02 fact_mult__pos__neg2, fact_mult__pos__pos, fact_mult__right_Oadd, % 186.44/25.02 fact_mult__right_Odiff, fact_mult__right_Ominus, fact_mult__right_Ozero, % 186.44/25.02 fact_mult__right__le__imp__le, fact_mult__right__le__one__le, % 186.44/25.02 fact_mult__right__less__imp__less, fact_mult__right__mono, % 186.44/25.02 fact_mult__right__mono__neg, fact_mult__smult__left, fact_mult__smult__right, % 186.44/25.02 fact_mult__strict__left__mono, fact_mult__strict__left__mono__neg, % 186.44/25.02 fact_mult__strict__mono, fact_mult__strict__mono_H, % 186.44/25.02 fact_mult__strict__right__mono, fact_mult__strict__right__mono__neg, % 186.44/25.02 fact_mult__zero__left, fact_mult__zero__right, fact_n0, % 186.44/25.02 fact_n__less__m__mult__n, fact_n__less__n__mult__m, fact_n__not__Suc__n, % 186.44/25.02 fact_nat_Oinject, fact_nat_Osimps_I2_J, fact_nat_Osimps_I3_J, % 186.44/25.02 fact_nat__0__less__mult__iff, fact_nat__1__eq__mult__iff, fact_nat__add__assoc, % 186.44/25.02 fact_nat__add__commute, fact_nat__add__left__cancel, % 186.44/25.02 fact_nat__add__left__cancel__le, fact_nat__add__left__cancel__less, % 186.44/25.02 fact_nat__add__left__commute, fact_nat__add__right__cancel, fact_nat__case__0, % 186.44/25.02 fact_nat__case__Suc, fact_nat__dvd__1__iff__1, fact_nat__dvd__not__less, % 186.44/25.02 fact_nat__le__linear, fact_nat__less__cases, fact_nat__less__le, % 186.44/25.02 fact_nat__lt__two__imp__zero__or__one, fact_nat__mult__1, % 186.44/25.02 fact_nat__mult__1__right, fact_nat__mult__assoc, fact_nat__mult__commute, % 186.44/25.02 fact_nat__mult__dvd__cancel1, fact_nat__mult__dvd__cancel__disj, % 186.44/25.02 fact_nat__mult__eq__1__iff, fact_nat__mult__eq__cancel1, % 186.44/25.02 fact_nat__mult__eq__cancel__disj, fact_nat__mult__le__cancel1, % 186.44/25.02 fact_nat__mult__less__cancel1, fact_nat__neq__iff, fact_nat__one__le__power, % 186.44/25.02 fact_nat__power__eq__Suc__0__iff, fact_nat__power__less__imp__less, % 186.44/25.02 fact_nat__zero__less__power__iff, fact_neg__0__equal__iff__equal, % 186.44/25.02 fact_neg__0__le__iff__le, fact_neg__0__less__iff__less, % 186.44/25.02 fact_neg__equal__0__iff__equal, fact_neg__equal__iff__equal, % 186.44/25.02 fact_neg__equal__zero, fact_neg__le__0__iff__le, fact_neg__le__iff__le, % 186.44/25.02 fact_neg__less__0__iff__less, fact_neg__less__iff__less, fact_neg__less__nonneg, % 186.44/25.02 fact_neg__mod__bound, fact_negative__imp__inverse__negative, fact_neq0__conv, % 186.44/25.02 fact_no__zero__divisors, fact_nonzero__imp__inverse__nonzero, % 186.44/25.02 fact_nonzero__inverse__eq__imp__eq, fact_nonzero__inverse__inverse__eq, % 186.44/25.02 fact_nonzero__inverse__minus__eq, fact_nonzero__inverse__mult__distrib, % 186.44/25.02 fact_nonzero__power__inverse, fact_not__add__less1, fact_not__add__less2, % 186.44/25.02 fact_not__leE, fact_not__less0, fact_not__less__eq, fact_not__less__eq__eq, % 186.44/25.02 fact_not__less__iff__gr__or__eq, fact_not__less__less__Suc__eq, % 186.44/25.02 fact_not__one__le__zero, fact_not__one__less__zero, fact_not__pos__poly__0, % 186.44/25.02 fact_not__square__less__zero, fact_not__sum__squares__lt__zero, % 186.44/25.02 fact_odd__less__0, fact_odd__nonzero, fact_offset__poly__0, % 186.44/25.02 fact_offset__poly__eq__0__iff, fact_offset__poly__eq__0__lemma, % 186.44/25.02 fact_offset__poly__pCons, fact_offset__poly__single, fact_one__dvd, % 186.44/25.02 fact_one__is__add, fact_one__le__inverse, fact_one__le__inverse__iff, % 186.44/25.02 fact_one__le__mult__iff, fact_one__le__power, fact_one__less__inverse, % 186.44/25.02 fact_one__less__inverse__iff, fact_one__less__mult, fact_one__less__power, % 186.44/25.02 fact_one__neq__zero, fact_one__poly__def, fact_one__reorient, fact_oop, % 186.44/25.02 fact_ord__eq__le__trans, fact_ord__eq__less__trans, fact_ord__le__eq__trans, % 186.44/25.02 fact_ord__less__eq__trans, fact_order, fact_order__1, fact_order__2, % 186.44/25.02 fact_order__antisym, fact_order__antisym__conv, fact_order__degree, % 186.44/25.02 fact_order__eq__iff, fact_order__eq__refl, fact_order__le__imp__less__or__eq, % 186.44/25.02 fact_order__le__less, fact_order__le__less__trans, fact_order__le__neq__trans, % 186.44/25.02 fact_order__less__asym, fact_order__less__asym_H, fact_order__less__imp__le, % 186.44/25.02 fact_order__less__imp__not__eq, fact_order__less__imp__not__eq2, % 186.44/25.02 fact_order__less__imp__not__less, fact_order__less__irrefl, % 186.44/25.02 fact_order__less__le, fact_order__less__le__trans, fact_order__less__not__sym, % 186.44/25.02 fact_order__less__trans, fact_order__neq__le__trans, fact_order__refl, % 186.44/25.02 fact_order__root, fact_order__trans, fact_pCons__0__0, fact_pCons__def, % 186.44/25.02 fact_pCons__eq__0__iff, fact_pCons__eq__iff, fact_pcompose__0, % 186.44/25.02 fact_pcompose__pCons, fact_pdivmod__rel__0, fact_pdivmod__rel__0__iff, % 186.44/25.02 fact_pdivmod__rel__by__0, fact_pdivmod__rel__by__0__iff, fact_pdivmod__rel__def, % 186.44/25.02 fact_pdivmod__rel__mult, fact_pdivmod__rel__smult__left, % 186.44/25.02 fact_pdivmod__rel__smult__right, fact_pdivmod__rel__unique, % 186.44/25.02 fact_pdivmod__rel__unique__div, fact_pdivmod__rel__unique__mod, % 186.44/25.02 fact_plus__nat_Oadd__0, fact_poly__0, fact_poly__1, fact_poly__add, % 186.44/25.02 fact_poly__diff, fact_poly__dvd__antisym, fact_poly__eq__0__iff__dvd, % 186.44/25.02 fact_poly__eq__iff, fact_poly__gcd_Oassoc, fact_poly__gcd_Ocommute, % 186.44/25.02 fact_poly__gcd_Oleft__commute, fact_poly__gcd_Osimps_I1_J, % 186.44/25.02 fact_poly__gcd_Osimps_I2_J, fact_poly__gcd__0__0, fact_poly__gcd__1__left, % 186.44/25.02 fact_poly__gcd__1__right, fact_poly__gcd__code, fact_poly__gcd__dvd1, % 186.44/25.02 fact_poly__gcd__dvd2, fact_poly__gcd__greatest, fact_poly__gcd__minus__left, % 186.44/25.02 fact_poly__gcd__minus__right, fact_poly__gcd__monic, fact_poly__gcd__unique, % 186.44/25.02 fact_poly__gcd__zero__iff, fact_poly__minus, fact_poly__mod__minus__left, % 186.44/25.02 fact_poly__mod__minus__right, fact_poly__monom, fact_poly__mult, % 186.44/25.02 fact_poly__offset__poly, fact_poly__pCons, fact_poly__pcompose, % 186.44/25.02 fact_poly__power, fact_poly__rec_Osimps, fact_poly__rec__0, % 186.44/25.02 fact_poly__rec__pCons, fact_poly__replicate__append, fact_poly__smult, % 186.44/25.02 fact_poly__zero, fact_pos__add__strict, fact_pos__mod__bound, % 186.44/25.02 fact_pos__poly__add, fact_pos__poly__def, fact_pos__poly__mult, % 186.44/25.02 fact_pos__poly__pCons, fact_pos__poly__total, fact_pos__zmult__eq__1__iff, % 186.44/25.02 fact_positive__imp__inverse__positive, fact_pow__divides__eq__int, % 186.44/25.02 fact_pow__divides__eq__nat, fact_pow__divides__pow__int, % 186.44/25.02 fact_pow__divides__pow__nat, fact_power_Opower_Opower__0, % 186.44/25.02 fact_power_Opower_Opower__Suc, fact_power__0, fact_power__0__Suc, % 186.44/25.02 fact_power__0__left, fact_power__Suc, fact_power__Suc2, fact_power__Suc__0, % 186.44/25.02 fact_power__Suc__less, fact_power__Suc__less__one, fact_power__add, % 186.44/25.02 fact_power__commutes, fact_power__decreasing, fact_power__dvd__imp__le, % 186.44/25.02 fact_power__eq__0__iff, fact_power__eq__imp__eq__base, fact_power__gt1, % 186.44/25.02 fact_power__gt1__lemma, fact_power__increasing, fact_power__increasing__iff, % 186.44/25.02 fact_power__inject__base, fact_power__inject__exp, fact_power__inverse, % 186.44/25.02 fact_power__le__dvd, fact_power__le__imp__le__base, % 186.44/25.02 fact_power__le__imp__le__exp, fact_power__less__imp__less__base, % 186.44/25.02 fact_power__less__imp__less__exp, fact_power__less__power__Suc, % 186.44/25.02 fact_power__minus, fact_power__mono, fact_power__mult, % 186.44/25.02 fact_power__mult__distrib, fact_power__one, fact_power__one__right, % 186.44/25.02 fact_power__power__power, fact_power__strict__decreasing, % 186.44/25.02 fact_power__strict__increasing, fact_power__strict__increasing__iff, % 186.44/25.02 fact_power__strict__mono, fact_pq0, fact_psize__def, fact_psize__eq__0__iff, % 186.44/25.02 fact_q__neg__lemma, fact_q__pos__lemma, fact_realpow__Suc__le__self, % 186.44/25.02 fact_realpow__minus__mult, fact_realpow__two__disj, fact_right__inverse, % 186.44/25.02 fact_right__minus, fact_right__minus__eq, fact_self__quotient__aux1, % 186.44/25.02 fact_self__quotient__aux2, fact_smult__0__left, fact_smult__0__right, % 186.44/25.02 fact_smult__1__left, fact_smult__add__left, fact_smult__add__right, % 186.44/25.02 fact_smult__diff__left, fact_smult__dvd, fact_smult__dvd__cancel, % 186.44/25.02 fact_smult__dvd__iff, fact_smult__eq__0__iff, fact_smult__minus__left, % 186.44/25.02 fact_smult__minus__right, fact_smult__monom, fact_smult__pCons, % 186.44/25.02 fact_smult__smult, fact_split__mult__neg__le, fact_split__mult__pos__le, % 186.44/25.02 fact_square__eq__1__iff, fact_square__eq__iff, fact_sum__squares__eq__zero__iff, % 186.44/25.02 fact_sum__squares__ge__zero, fact_sum__squares__gt__zero__iff, % 186.44/25.02 fact_sum__squares__le__zero__iff, fact_synthetic__div__0, % 186.44/25.02 fact_synthetic__div__correct, fact_synthetic__div__correct_H, % 186.44/25.02 fact_synthetic__div__eq__0__iff, fact_synthetic__div__pCons, % 186.44/25.02 fact_synthetic__div__unique, fact_synthetic__div__unique__lemma, % 186.44/25.02 fact_termination__basic__simps_I1_J, fact_termination__basic__simps_I2_J, % 186.44/25.02 fact_termination__basic__simps_I3_J, fact_termination__basic__simps_I4_J, % 186.44/25.02 fact_termination__basic__simps_I5_J, fact_times_Oidem, fact_trans__le__add1, % 186.44/25.02 fact_trans__le__add2, fact_trans__less__add1, fact_trans__less__add2, % 186.44/25.02 fact_uminus__apply, fact_uminus__dvd__conv_I1_J, fact_uminus__dvd__conv_I2_J, % 186.44/25.02 fact_unique__quotient__lemma, fact_unique__quotient__lemma__neg, % 186.44/25.02 fact_unity__coeff__ex, fact_xt1_I10_J, fact_xt1_I11_J, fact_xt1_I12_J, % 186.44/25.02 fact_xt1_I1_J, fact_xt1_I2_J, fact_xt1_I3_J, fact_xt1_I4_J, fact_xt1_I5_J, % 186.44/25.02 fact_xt1_I6_J, fact_xt1_I7_J, fact_xt1_I8_J, fact_xt1_I9_J, fact_zadd__0, % 186.44/25.02 fact_zadd__0__right, fact_zadd__assoc, fact_zadd__commute, % 186.44/25.02 fact_zadd__left__commute, fact_zadd__left__mono, fact_zadd__strict__right__mono, % 186.44/25.02 fact_zadd__zless__mono, fact_zadd__zminus__inverse2, fact_zadd__zmult__distrib, % 186.44/25.02 fact_zadd__zmult__distrib2, fact_zdiv__mono2__lemma, % 186.44/25.02 fact_zdiv__mono2__neg__lemma, fact_zdvd__antisym__nonneg, fact_zdvd__imp__le, % 186.44/25.02 fact_zdvd__mono, fact_zdvd__mult__cancel, fact_zdvd__not__zless, % 186.44/25.02 fact_zdvd__period, fact_zdvd__reduce, fact_zdvd__zmod, % 186.44/25.02 fact_zdvd__zmod__imp__zdvd, % 186.44/25.02 fact_zero__le__double__add__iff__zero__le__single__add, % 186.44/25.02 fact_zero__le__mult__iff, fact_zero__le__one, fact_zero__le__power, % 186.44/25.02 fact_zero__le__square, fact_zero__less__Suc, fact_zero__less__diff, % 186.44/25.02 fact_zero__less__double__add__iff__zero__less__single__add, % 186.44/25.02 fact_zero__less__mult__pos, fact_zero__less__mult__pos2, fact_zero__less__one, % 186.44/25.02 fact_zero__less__power, fact_zero__less__power__nat__eq, fact_zero__less__two, % 186.44/25.02 fact_zero__neq__one, fact_zero__reorient, fact_zle__add1__eq__le, % 186.44/25.02 fact_zle__antisym, fact_zle__linear, fact_zle__refl, fact_zle__trans, % 186.44/25.02 fact_zless__add1__eq, fact_zless__imp__add1__zle, fact_zless__le, % 186.44/25.02 fact_zless__linear, fact_zminus__0, fact_zminus__zadd__distrib, % 186.44/25.02 fact_zminus__zminus, fact_zminus__zmod, fact_zmod__eq__0__iff, % 186.44/25.02 fact_zmod__le__nonneg__dividend, fact_zmod__self, fact_zmod__simps_I1_J, % 186.44/25.02 fact_zmod__simps_I2_J, fact_zmod__simps_I3_J, fact_zmod__simps_I4_J, % 186.44/25.02 fact_zmod__zero, fact_zmod__zminus1__not__zero, fact_zmod__zminus2, % 186.44/25.02 fact_zmod__zminus2__not__zero, fact_zmod__zminus__zminus, fact_zmod__zmult1__eq, % 186.44/25.02 fact_zmult__1, fact_zmult__1__right, fact_zmult__assoc, fact_zmult__commute, % 186.44/25.02 fact_zmult__zless__mono2, fact_zmult__zminus, fact_zpower__zadd__distrib, % 186.44/25.02 fact_zpower__zmod, fact_zpower__zpower, help_c__fequal__1, help_c__fequal__2 % 186.44/25.02 % 186.44/25.02 Those formulas are unsatisfiable: % 186.44/25.02 --------------------------------- % 186.44/25.02 % 186.44/25.02 Begin of proof % 186.44/25.02 | % 186.44/25.02 | ALPHA: (fact_pne) implies: % 186.44/25.03 | (1) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v_pa____) & % 186.44/25.03 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.44/25.03 | c_Groups_Ozero__class_Ozero(v0) = v1 & $i(v1) & $i(v0)) % 186.44/25.03 | % 186.44/25.03 | ALPHA: (fact_q0) implies: % 186.44/25.03 | (2) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v_qa____) & % 186.44/25.03 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.44/25.03 | c_Groups_Ozero__class_Ozero(v0) = v1 & $i(v1) & $i(v0)) % 186.44/25.03 | % 186.44/25.03 | ALPHA: (fact_oa) implies: % 186.44/25.03 | (3) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & % 186.44/25.03 | c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v0 & % 186.44/25.03 | c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = v1 & $i(v1) & $i(v0)) % 186.44/25.03 | % 186.44/25.03 | ALPHA: (fact_calculation) implies: % 186.44/25.03 | (4) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.44/25.03 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 186.44/25.03 | (tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & $i(v0) & (( ~ (v1 = % 186.44/25.03 | v_qa____) & c_Groups_Ozero__class_Ozero(v0) = v1 & $i(v1)) | % 186.44/25.03 | (c_Power_Opower__class_Opower(v0) = v4 & % 186.44/25.03 | c_Rings_Odvd__class_Odvd(v0) = v2 & hAPP(v5, v_na____) = v6 & % 186.44/25.03 | hAPP(v4, v_qa____) = v5 & hAPP(v3, v6) = v7 & hAPP(v2, v_pa____) % 186.44/25.03 | = v3 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 186.44/25.03 | hBOOL(v7)))) % 186.44/25.03 | % 186.44/25.03 | ALPHA: (fact_s) implies: % 186.44/25.03 | (5) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.44/25.03 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 186.44/25.03 | [v10: $i] : ? [v11: $i] : (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.44/25.03 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v3 & % 186.44/25.03 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & % 186.44/25.03 | c_Power_Opower__class_Opower(v0) = v2 & % 186.44/25.03 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.44/25.03 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.44/25.03 | c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.44/25.03 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.44/25.03 | c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v11, v_s____) = v_pa____ % 186.44/25.03 | & hAPP(v8, v9) = v10 & hAPP(v2, v7) = v8 & hAPP(v1, v10) = v11 & % 186.44/25.03 | $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 186.44/25.03 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 186.44/25.03 | % 186.44/25.03 | ALPHA: (fact_IH) implies: % 186.51/25.03 | (6) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.51/25.03 | (c_Power_Opower__class_Opower(v2) = v4 & c_Rings_Odvd__class_Odvd(v2) = % 186.51/25.03 | v3 & tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v2 & % 186.51/25.03 | c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = v1 & % 186.51/25.03 | c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = v0 & $i(v4) & % 186.51/25.03 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & ! [v5: $i] : ! [v6: $i] : ! % 186.51/25.03 | [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : % 186.51/25.03 | (v5 = v1 | ~ (hAPP(v9, v5) = v10) | ~ (hAPP(v8, v10) = v11) | ~ % 186.51/25.03 | (hAPP(v4, v7) = v9) | ~ (hAPP(v3, v6) = v8) | ~ $i(v7) | ~ % 186.51/25.03 | $i(v6) | ~ $i(v5) | ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat, % 186.51/25.03 | v5, v_na____) | hBOOL(v11) | ? [v12: $i] : ? [v13: $i] : ? % 186.51/25.03 | [v14: $i] : ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ($i(v15) & % 186.51/25.03 | ((v16 = v0 & ~ (v17 = v0) & % 186.51/25.03 | c_Polynomial_Opoly(tc_Complex_Ocomplex, v7) = v13 & % 186.51/25.03 | c_Polynomial_Opoly(tc_Complex_Ocomplex, v6) = v12 & hAPP(v13, % 186.51/25.03 | v15) = v17 & hAPP(v12, v15) = v0 & $i(v17) & $i(v13) & % 186.51/25.03 | $i(v12)) | ( ~ (v14 = v5) & % 186.51/25.03 | c_Polynomial_Odegree(tc_Complex_Ocomplex, v6) = v14 & % 186.51/25.03 | $i(v14)))))) % 186.51/25.03 | % 186.51/25.03 | ALPHA: (fact_r) implies: % 186.51/25.03 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.51/25.03 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 186.51/25.03 | (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.51/25.03 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v2 & % 186.51/25.03 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v3 & % 186.51/25.03 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v4) = v5 & % 186.51/25.03 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v2, v5) = v6 & % 186.51/25.03 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.51/25.03 | c_Groups_Ozero__class_Ozero(v0) = v4 & hAPP(v7, v_r____) = v_qa____ & % 186.51/25.03 | hAPP(v1, v6) = v7 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 186.51/25.03 | $i(v2) & $i(v1) & $i(v0)) % 186.51/25.03 | % 186.51/25.03 | ALPHA: (fact__096_091_058_N_Aa_M_A1_058_093_Advd_Aq_096) implies: % 186.51/25.04 | (8) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.51/25.04 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 186.51/25.04 | (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v2 & % 186.51/25.04 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v3 & % 186.51/25.04 | c_Rings_Odvd__class_Odvd(v0) = v1 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v4) = v5 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v2, v5) = v6 & % 186.51/25.04 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.51/25.04 | c_Groups_Ozero__class_Ozero(v0) = v4 & hAPP(v7, v_qa____) = v8 & % 186.51/25.04 | hAPP(v1, v6) = v7 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 186.51/25.04 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & hBOOL(v8)) % 186.51/25.04 | % 186.51/25.04 | ALPHA: (fact_ap_I1_J) implies: % 186.51/25.04 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.51/25.04 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 186.51/25.04 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : % 186.51/25.04 | (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v3 & % 186.51/25.04 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & % 186.51/25.04 | c_Power_Opower__class_Opower(v0) = v2 & c_Rings_Odvd__class_Odvd(v0) % 186.51/25.04 | = v1 & c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.51/25.04 | c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.51/25.04 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.51/25.04 | c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v11, v_pa____) = v12 & % 186.51/25.04 | hAPP(v8, v9) = v10 & hAPP(v2, v7) = v8 & hAPP(v1, v10) = v11 & % 186.51/25.04 | $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 186.51/25.04 | $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & hBOOL(v12)) % 186.51/25.04 | % 186.51/25.04 | ALPHA: (fact_ap_I2_J) implies: % 186.51/25.04 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.51/25.04 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 186.51/25.04 | ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : % 186.51/25.04 | (c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v3 & % 186.51/25.04 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & c_Nat_OSuc(v9) % 186.51/25.04 | = v10 & c_Power_Opower__class_Opower(v0) = v2 & % 186.51/25.04 | c_Rings_Odvd__class_Odvd(v0) = v1 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.51/25.04 | c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.51/25.04 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.51/25.04 | c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v12, v_pa____) = v13 & % 186.51/25.04 | hAPP(v8, v10) = v11 & hAPP(v2, v7) = v8 & hAPP(v1, v11) = v12 & % 186.51/25.04 | $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & % 186.51/25.04 | $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ % 186.51/25.04 | hBOOL(v13)) % 186.51/25.04 | % 186.51/25.04 | ALPHA: (fact__096_B_Bthesis_O_A_I_B_Bs_O_Ap_A_061_A_091_058_N_Aa_M_A1_058_093_A_094_Aorder_Aa_Ap_A_K_As_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) % 186.51/25.04 | implies: % 186.51/25.04 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.51/25.04 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 186.51/25.04 | ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : % 186.51/25.04 | (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.51/25.04 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v3 & % 186.51/25.04 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v4 & % 186.51/25.04 | c_Power_Opower__class_Opower(v0) = v2 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v4, v5) = v6 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v6) = v7 & % 186.51/25.04 | c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = v9 & % 186.51/25.04 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.51/25.04 | c_Groups_Ozero__class_Ozero(v0) = v5 & hAPP(v11, v12) = v_pa____ & % 186.51/25.04 | hAPP(v8, v9) = v10 & hAPP(v2, v7) = v8 & hAPP(v1, v10) = v11 & % 186.51/25.04 | $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & % 186.51/25.04 | $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 186.51/25.04 | % 186.51/25.04 | ALPHA: (fact__096_B_Bthesis_O_A_I_B_Br_O_Aq_A_061_A_091_058_N_Aa_M_A1_058_093_A_K_Ar_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) % 186.51/25.04 | implies: % 186.51/25.04 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 186.51/25.04 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 186.51/25.04 | (c_Groups_Otimes__class_Otimes(v0) = v1 & % 186.51/25.04 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = v2 & % 186.51/25.04 | c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = v3 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v3, v4) = v5 & % 186.51/25.04 | c_Polynomial_OpCons(tc_Complex_Ocomplex, v2, v5) = v6 & % 186.51/25.04 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.51/25.04 | c_Groups_Ozero__class_Ozero(v0) = v4 & hAPP(v7, v8) = v_qa____ & % 186.51/25.04 | hAPP(v1, v6) = v7 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 186.51/25.04 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 186.51/25.04 | % 186.51/25.04 | ALPHA: (arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) implies: % 186.51/25.04 | (13) class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) % 186.51/25.04 | % 186.51/25.04 | ALPHA: (conj_0) implies: % 186.51/25.04 | (14) $i(tc_Complex_Ocomplex) % 186.51/25.04 | (15) ? [v0: $i] : (tc_Polynomial_Opoly(tc_Complex_Ocomplex) = v0 & % 186.51/25.04 | c_Groups_Ozero__class_Ozero(v0) = v_s____ & $i(v0)) % 186.51/25.04 | % 186.51/25.04 | ALPHA: (function-axioms) implies: % 186.51/25.04 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 186.51/25.04 | (c_Groups_Ozero__class_Ozero(v2) = v1) | ~ % 186.51/25.04 | (c_Groups_Ozero__class_Ozero(v2) = v0)) % 186.51/25.04 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 186.51/25.04 | (tc_Polynomial_Opoly(v2) = v1) | ~ (tc_Polynomial_Opoly(v2) = v0)) % 186.51/25.04 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 186.51/25.04 | (c_Power_Opower__class_Opower(v2) = v1) | ~ % 186.51/25.04 | (c_Power_Opower__class_Opower(v2) = v0)) % 186.51/25.05 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 186.51/25.05 | (c_Groups_Oone__class_Oone(v2) = v1) | ~ % 186.51/25.05 | (c_Groups_Oone__class_Oone(v2) = v0)) % 186.51/25.05 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 186.51/25.05 | (c_Groups_Otimes__class_Otimes(v2) = v1) | ~ % 186.51/25.05 | (c_Groups_Otimes__class_Otimes(v2) = v0)) % 186.51/25.05 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 186.51/25.05 | (hAPP(v3, v2) = v1) | ~ (hAPP(v3, v2) = v0)) % 186.51/25.05 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 186.51/25.05 | (c_Groups_Ouminus__class_Ouminus(v3, v2) = v1) | ~ % 186.51/25.05 | (c_Groups_Ouminus__class_Ouminus(v3, v2) = v0)) % 186.51/25.05 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 186.51/25.05 | (v1 = v0 | ~ (c_Polynomial_Oorder(v4, v3, v2) = v1) | ~ % 186.51/25.05 | (c_Polynomial_Oorder(v4, v3, v2) = v0)) % 186.51/25.05 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 186.51/25.05 | (v1 = v0 | ~ (c_Polynomial_OpCons(v4, v3, v2) = v1) | ~ % 186.51/25.05 | (c_Polynomial_OpCons(v4, v3, v2) = v0)) % 186.51/25.05 | % 186.51/25.05 | DELTA: instantiating (15) with fresh symbol all_796_0 gives: % 186.51/25.05 | (25) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_796_0 & % 186.51/25.05 | c_Groups_Ozero__class_Ozero(all_796_0) = v_s____ & $i(all_796_0) % 186.51/25.05 | % 186.51/25.05 | ALPHA: (25) implies: % 186.51/25.05 | (26) c_Groups_Ozero__class_Ozero(all_796_0) = v_s____ % 186.51/25.05 | (27) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_796_0 % 186.51/25.05 | % 186.51/25.05 | DELTA: instantiating (2) with fresh symbols all_877_0, all_877_1 gives: % 186.51/25.05 | (28) ~ (all_877_0 = v_qa____) & tc_Polynomial_Opoly(tc_Complex_Ocomplex) = % 186.51/25.05 | all_877_1 & c_Groups_Ozero__class_Ozero(all_877_1) = all_877_0 & % 186.51/25.05 | $i(all_877_0) & $i(all_877_1) % 186.51/25.05 | % 186.51/25.05 | ALPHA: (28) implies: % 186.51/25.05 | (29) c_Groups_Ozero__class_Ozero(all_877_1) = all_877_0 % 186.51/25.05 | (30) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_877_1 % 186.51/25.05 | % 186.51/25.05 | DELTA: instantiating (1) with fresh symbols all_885_0, all_885_1 gives: % 186.51/25.05 | (31) ~ (all_885_0 = v_pa____) & tc_Polynomial_Opoly(tc_Complex_Ocomplex) = % 186.51/25.05 | all_885_1 & c_Groups_Ozero__class_Ozero(all_885_1) = all_885_0 & % 186.51/25.05 | $i(all_885_0) & $i(all_885_1) % 186.51/25.05 | % 186.51/25.05 | ALPHA: (31) implies: % 186.51/25.05 | (32) ~ (all_885_0 = v_pa____) % 186.51/25.05 | (33) c_Groups_Ozero__class_Ozero(all_885_1) = all_885_0 % 186.51/25.05 | (34) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_885_1 % 186.51/25.05 | % 186.51/25.05 | DELTA: instantiating (3) with fresh symbols all_894_0, all_894_1 gives: % 186.51/25.05 | (35) ~ (all_894_0 = all_894_1) & c_Polynomial_Oorder(tc_Complex_Ocomplex, % 186.51/25.05 | v_a____, v_pa____) = all_894_1 & % 186.51/25.05 | c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = all_894_0 & $i(all_894_0) & % 186.51/25.05 | $i(all_894_1) % 186.51/25.05 | % 186.51/25.05 | ALPHA: (35) implies: % 186.51/25.05 | (36) c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = % 186.51/25.05 | all_894_1 % 186.51/25.05 | % 186.51/25.05 | DELTA: instantiating (7) with fresh symbols all_1324_0, all_1324_1, % 186.51/25.05 | all_1324_2, all_1324_3, all_1324_4, all_1324_5, all_1324_6, all_1324_7 % 186.51/25.05 | gives: % 186.51/25.05 | (37) c_Groups_Otimes__class_Otimes(all_1324_7) = all_1324_6 & % 186.51/25.05 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.05 | all_1324_5 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = % 186.51/25.05 | all_1324_4 & c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, % 186.51/25.05 | all_1324_3) = all_1324_2 & c_Polynomial_OpCons(tc_Complex_Ocomplex, % 186.51/25.05 | all_1324_5, all_1324_2) = all_1324_1 & % 186.51/25.05 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1324_7 & % 186.51/25.05 | c_Groups_Ozero__class_Ozero(all_1324_7) = all_1324_3 & % 186.51/25.05 | hAPP(all_1324_0, v_r____) = v_qa____ & hAPP(all_1324_6, all_1324_1) = % 186.51/25.05 | all_1324_0 & $i(all_1324_0) & $i(all_1324_1) & $i(all_1324_2) & % 186.51/25.05 | $i(all_1324_3) & $i(all_1324_4) & $i(all_1324_5) & $i(all_1324_6) & % 186.51/25.05 | $i(all_1324_7) % 186.51/25.05 | % 186.51/25.05 | ALPHA: (37) implies: % 186.51/25.05 | (38) c_Groups_Ozero__class_Ozero(all_1324_7) = all_1324_3 % 186.51/25.05 | (39) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1324_7 % 186.51/25.05 | (40) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1324_2) = % 186.51/25.05 | all_1324_1 % 186.51/25.05 | (41) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, all_1324_3) = % 186.51/25.05 | all_1324_2 % 186.51/25.05 | (42) c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1324_4 % 186.51/25.05 | (43) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.05 | all_1324_5 % 186.51/25.05 | (44) c_Groups_Otimes__class_Otimes(all_1324_7) = all_1324_6 % 186.51/25.05 | % 186.51/25.05 | DELTA: instantiating (12) with fresh symbols all_1374_0, all_1374_1, % 186.51/25.05 | all_1374_2, all_1374_3, all_1374_4, all_1374_5, all_1374_6, all_1374_7, % 186.51/25.05 | all_1374_8 gives: % 186.51/25.05 | (45) c_Groups_Otimes__class_Otimes(all_1374_8) = all_1374_7 & % 186.51/25.05 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.05 | all_1374_6 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = % 186.51/25.05 | all_1374_5 & c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1374_5, % 186.51/25.05 | all_1374_4) = all_1374_3 & c_Polynomial_OpCons(tc_Complex_Ocomplex, % 186.51/25.05 | all_1374_6, all_1374_3) = all_1374_2 & % 186.51/25.05 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1374_8 & % 186.51/25.05 | c_Groups_Ozero__class_Ozero(all_1374_8) = all_1374_4 & % 186.51/25.05 | hAPP(all_1374_1, all_1374_0) = v_qa____ & hAPP(all_1374_7, all_1374_2) % 186.51/25.05 | = all_1374_1 & $i(all_1374_0) & $i(all_1374_1) & $i(all_1374_2) & % 186.51/25.05 | $i(all_1374_3) & $i(all_1374_4) & $i(all_1374_5) & $i(all_1374_6) & % 186.51/25.05 | $i(all_1374_7) & $i(all_1374_8) % 186.51/25.05 | % 186.51/25.05 | ALPHA: (45) implies: % 186.51/25.05 | (46) c_Groups_Ozero__class_Ozero(all_1374_8) = all_1374_4 % 186.51/25.05 | (47) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1374_8 % 186.51/25.05 | (48) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1374_6, all_1374_3) = % 186.51/25.05 | all_1374_2 % 186.51/25.05 | (49) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1374_5, all_1374_4) = % 186.51/25.05 | all_1374_3 % 186.51/25.05 | (50) c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1374_5 % 186.51/25.05 | (51) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.05 | all_1374_6 % 186.51/25.05 | (52) c_Groups_Otimes__class_Otimes(all_1374_8) = all_1374_7 % 186.51/25.05 | % 186.51/25.05 | DELTA: instantiating (4) with fresh symbols all_1385_0, all_1385_1, % 186.51/25.05 | all_1385_2, all_1385_3, all_1385_4, all_1385_5, all_1385_6, all_1385_7 % 186.51/25.05 | gives: % 186.51/25.06 | (53) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1385_7 & $i(all_1385_7) % 186.51/25.06 | & (( ~ (all_1385_6 = v_qa____) & % 186.51/25.06 | c_Groups_Ozero__class_Ozero(all_1385_7) = all_1385_6 & % 186.51/25.06 | $i(all_1385_6)) | (c_Power_Opower__class_Opower(all_1385_7) = % 186.51/25.06 | all_1385_3 & c_Rings_Odvd__class_Odvd(all_1385_7) = all_1385_5 & % 186.51/25.06 | hAPP(all_1385_2, v_na____) = all_1385_1 & hAPP(all_1385_3, % 186.51/25.06 | v_qa____) = all_1385_2 & hAPP(all_1385_4, all_1385_1) = % 186.51/25.06 | all_1385_0 & hAPP(all_1385_5, v_pa____) = all_1385_4 & % 186.51/25.06 | $i(all_1385_0) & $i(all_1385_1) & $i(all_1385_2) & $i(all_1385_3) % 186.51/25.06 | & $i(all_1385_4) & $i(all_1385_5) & hBOOL(all_1385_0))) % 186.51/25.06 | % 186.51/25.06 | ALPHA: (53) implies: % 186.51/25.06 | (54) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1385_7 % 186.51/25.06 | % 186.51/25.06 | DELTA: instantiating (8) with fresh symbols all_1395_0, all_1395_1, % 186.51/25.06 | all_1395_2, all_1395_3, all_1395_4, all_1395_5, all_1395_6, all_1395_7, % 186.51/25.06 | all_1395_8 gives: % 186.51/25.06 | (55) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.06 | all_1395_6 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = % 186.51/25.06 | all_1395_5 & c_Rings_Odvd__class_Odvd(all_1395_8) = all_1395_7 & % 186.51/25.06 | c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1395_5, all_1395_4) = % 186.51/25.06 | all_1395_3 & c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1395_6, % 186.51/25.06 | all_1395_3) = all_1395_2 & tc_Polynomial_Opoly(tc_Complex_Ocomplex) % 186.51/25.06 | = all_1395_8 & c_Groups_Ozero__class_Ozero(all_1395_8) = all_1395_4 & % 186.51/25.06 | hAPP(all_1395_1, v_qa____) = all_1395_0 & hAPP(all_1395_7, all_1395_2) % 186.51/25.06 | = all_1395_1 & $i(all_1395_0) & $i(all_1395_1) & $i(all_1395_2) & % 186.51/25.06 | $i(all_1395_3) & $i(all_1395_4) & $i(all_1395_5) & $i(all_1395_6) & % 186.51/25.06 | $i(all_1395_7) & $i(all_1395_8) & hBOOL(all_1395_0) % 186.51/25.06 | % 186.51/25.06 | ALPHA: (55) implies: % 186.51/25.06 | (56) c_Groups_Ozero__class_Ozero(all_1395_8) = all_1395_4 % 186.51/25.06 | (57) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1395_8 % 186.51/25.06 | (58) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1395_6, all_1395_3) = % 186.51/25.06 | all_1395_2 % 186.51/25.06 | (59) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1395_5, all_1395_4) = % 186.51/25.06 | all_1395_3 % 186.51/25.06 | (60) c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1395_5 % 186.51/25.06 | (61) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.06 | all_1395_6 % 186.51/25.06 | % 186.51/25.06 | DELTA: instantiating (5) with fresh symbols all_1511_0, all_1511_1, % 186.51/25.06 | all_1511_2, all_1511_3, all_1511_4, all_1511_5, all_1511_6, all_1511_7, % 186.51/25.06 | all_1511_8, all_1511_9, all_1511_10, all_1511_11 gives: % 186.51/25.06 | (62) c_Groups_Otimes__class_Otimes(all_1511_11) = all_1511_10 & % 186.51/25.06 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.06 | all_1511_8 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = % 186.51/25.06 | all_1511_7 & c_Power_Opower__class_Opower(all_1511_11) = all_1511_9 & % 186.51/25.06 | c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1511_7, all_1511_6) = % 186.51/25.06 | all_1511_5 & c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1511_8, % 186.51/25.06 | all_1511_5) = all_1511_4 & c_Polynomial_Oorder(tc_Complex_Ocomplex, % 186.51/25.06 | v_a____, v_pa____) = all_1511_2 & % 186.51/25.06 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1511_11 & % 186.51/25.06 | c_Groups_Ozero__class_Ozero(all_1511_11) = all_1511_6 & % 186.51/25.06 | hAPP(all_1511_0, v_s____) = v_pa____ & hAPP(all_1511_3, all_1511_2) = % 186.51/25.06 | all_1511_1 & hAPP(all_1511_9, all_1511_4) = all_1511_3 & % 186.51/25.06 | hAPP(all_1511_10, all_1511_1) = all_1511_0 & $i(all_1511_0) & % 186.51/25.06 | $i(all_1511_1) & $i(all_1511_2) & $i(all_1511_3) & $i(all_1511_4) & % 186.51/25.06 | $i(all_1511_5) & $i(all_1511_6) & $i(all_1511_7) & $i(all_1511_8) & % 186.51/25.06 | $i(all_1511_9) & $i(all_1511_10) & $i(all_1511_11) % 186.51/25.06 | % 186.51/25.06 | ALPHA: (62) implies: % 186.51/25.06 | (63) hAPP(all_1511_10, all_1511_1) = all_1511_0 % 186.51/25.06 | (64) hAPP(all_1511_9, all_1511_4) = all_1511_3 % 186.51/25.06 | (65) hAPP(all_1511_3, all_1511_2) = all_1511_1 % 186.51/25.06 | (66) hAPP(all_1511_0, v_s____) = v_pa____ % 186.51/25.06 | (67) c_Groups_Ozero__class_Ozero(all_1511_11) = all_1511_6 % 186.51/25.06 | (68) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1511_11 % 186.51/25.06 | (69) c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = % 186.51/25.06 | all_1511_2 % 186.51/25.06 | (70) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1511_8, all_1511_5) = % 186.51/25.06 | all_1511_4 % 186.51/25.06 | (71) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1511_7, all_1511_6) = % 186.51/25.06 | all_1511_5 % 186.51/25.06 | (72) c_Power_Opower__class_Opower(all_1511_11) = all_1511_9 % 186.51/25.06 | (73) c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1511_7 % 186.51/25.06 | (74) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.06 | all_1511_8 % 186.51/25.06 | (75) c_Groups_Otimes__class_Otimes(all_1511_11) = all_1511_10 % 186.51/25.06 | % 186.51/25.06 | DELTA: instantiating (11) with fresh symbols all_1513_0, all_1513_1, % 186.51/25.06 | all_1513_2, all_1513_3, all_1513_4, all_1513_5, all_1513_6, all_1513_7, % 186.51/25.06 | all_1513_8, all_1513_9, all_1513_10, all_1513_11, all_1513_12 gives: % 186.51/25.06 | (76) c_Groups_Otimes__class_Otimes(all_1513_12) = all_1513_11 & % 186.51/25.06 | c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.06 | all_1513_9 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = % 186.51/25.06 | all_1513_8 & c_Power_Opower__class_Opower(all_1513_12) = all_1513_10 & % 186.51/25.06 | c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1513_8, all_1513_7) = % 186.51/25.06 | all_1513_6 & c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1513_9, % 186.51/25.06 | all_1513_6) = all_1513_5 & c_Polynomial_Oorder(tc_Complex_Ocomplex, % 186.51/25.06 | v_a____, v_pa____) = all_1513_3 & % 186.51/25.06 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1513_12 & % 186.51/25.06 | c_Groups_Ozero__class_Ozero(all_1513_12) = all_1513_7 & % 186.51/25.06 | hAPP(all_1513_1, all_1513_0) = v_pa____ & hAPP(all_1513_4, all_1513_3) % 186.51/25.06 | = all_1513_2 & hAPP(all_1513_10, all_1513_5) = all_1513_4 & % 186.51/25.06 | hAPP(all_1513_11, all_1513_2) = all_1513_1 & $i(all_1513_0) & % 186.51/25.06 | $i(all_1513_1) & $i(all_1513_2) & $i(all_1513_3) & $i(all_1513_4) & % 186.51/25.06 | $i(all_1513_5) & $i(all_1513_6) & $i(all_1513_7) & $i(all_1513_8) & % 186.51/25.06 | $i(all_1513_9) & $i(all_1513_10) & $i(all_1513_11) & $i(all_1513_12) % 186.51/25.06 | % 186.51/25.06 | ALPHA: (76) implies: % 186.51/25.06 | (77) $i(all_1513_2) % 186.51/25.06 | (78) hAPP(all_1513_11, all_1513_2) = all_1513_1 % 186.51/25.06 | (79) hAPP(all_1513_10, all_1513_5) = all_1513_4 % 186.51/25.06 | (80) hAPP(all_1513_4, all_1513_3) = all_1513_2 % 186.51/25.06 | (81) c_Groups_Ozero__class_Ozero(all_1513_12) = all_1513_7 % 186.51/25.06 | (82) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1513_12 % 186.51/25.06 | (83) c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = % 186.51/25.06 | all_1513_3 % 186.51/25.06 | (84) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1513_9, all_1513_6) = % 186.51/25.06 | all_1513_5 % 186.51/25.06 | (85) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1513_8, all_1513_7) = % 186.51/25.06 | all_1513_6 % 186.51/25.06 | (86) c_Power_Opower__class_Opower(all_1513_12) = all_1513_10 % 186.51/25.06 | (87) c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1513_8 % 186.51/25.06 | (88) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.06 | all_1513_9 % 186.51/25.06 | (89) c_Groups_Otimes__class_Otimes(all_1513_12) = all_1513_11 % 186.51/25.06 | % 186.51/25.06 | DELTA: instantiating (9) with fresh symbols all_1518_0, all_1518_1, % 186.51/25.06 | all_1518_2, all_1518_3, all_1518_4, all_1518_5, all_1518_6, all_1518_7, % 186.51/25.06 | all_1518_8, all_1518_9, all_1518_10, all_1518_11, all_1518_12 gives: % 186.51/25.06 | (90) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.06 | all_1518_9 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = % 186.51/25.06 | all_1518_8 & c_Power_Opower__class_Opower(all_1518_12) = all_1518_10 & % 186.51/25.06 | c_Rings_Odvd__class_Odvd(all_1518_12) = all_1518_11 & % 186.51/25.06 | c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1518_8, all_1518_7) = % 186.51/25.06 | all_1518_6 & c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1518_9, % 186.51/25.06 | all_1518_6) = all_1518_5 & c_Polynomial_Oorder(tc_Complex_Ocomplex, % 186.51/25.06 | v_a____, v_pa____) = all_1518_3 & % 186.51/25.06 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1518_12 & % 186.51/25.06 | c_Groups_Ozero__class_Ozero(all_1518_12) = all_1518_7 & % 186.51/25.06 | hAPP(all_1518_1, v_pa____) = all_1518_0 & hAPP(all_1518_4, all_1518_3) % 186.51/25.06 | = all_1518_2 & hAPP(all_1518_10, all_1518_5) = all_1518_4 & % 186.51/25.06 | hAPP(all_1518_11, all_1518_2) = all_1518_1 & $i(all_1518_0) & % 186.51/25.06 | $i(all_1518_1) & $i(all_1518_2) & $i(all_1518_3) & $i(all_1518_4) & % 186.51/25.06 | $i(all_1518_5) & $i(all_1518_6) & $i(all_1518_7) & $i(all_1518_8) & % 186.51/25.06 | $i(all_1518_9) & $i(all_1518_10) & $i(all_1518_11) & $i(all_1518_12) & % 186.51/25.06 | hBOOL(all_1518_0) % 186.51/25.06 | % 186.51/25.06 | ALPHA: (90) implies: % 186.51/25.06 | (91) hAPP(all_1518_10, all_1518_5) = all_1518_4 % 186.51/25.06 | (92) hAPP(all_1518_4, all_1518_3) = all_1518_2 % 186.51/25.06 | (93) c_Groups_Ozero__class_Ozero(all_1518_12) = all_1518_7 % 186.51/25.06 | (94) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1518_12 % 186.51/25.06 | (95) c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = % 186.51/25.06 | all_1518_3 % 186.51/25.06 | (96) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1518_9, all_1518_6) = % 186.51/25.06 | all_1518_5 % 186.51/25.06 | (97) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1518_8, all_1518_7) = % 186.51/25.06 | all_1518_6 % 186.51/25.07 | (98) c_Power_Opower__class_Opower(all_1518_12) = all_1518_10 % 186.51/25.07 | (99) c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1518_8 % 186.51/25.07 | (100) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.07 | all_1518_9 % 186.51/25.07 | % 186.51/25.07 | DELTA: instantiating (10) with fresh symbols all_1559_0, all_1559_1, % 186.51/25.07 | all_1559_2, all_1559_3, all_1559_4, all_1559_5, all_1559_6, all_1559_7, % 186.51/25.07 | all_1559_8, all_1559_9, all_1559_10, all_1559_11, all_1559_12, % 186.51/25.07 | all_1559_13 gives: % 186.51/25.07 | (101) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.07 | all_1559_10 & c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = % 186.51/25.07 | all_1559_9 & c_Nat_OSuc(all_1559_4) = all_1559_3 & % 186.51/25.07 | c_Power_Opower__class_Opower(all_1559_13) = all_1559_11 & % 186.51/25.07 | c_Rings_Odvd__class_Odvd(all_1559_13) = all_1559_12 & % 186.51/25.07 | c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1559_9, all_1559_8) = % 186.51/25.07 | all_1559_7 & c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1559_10, % 186.51/25.07 | all_1559_7) = all_1559_6 & c_Polynomial_Oorder(tc_Complex_Ocomplex, % 186.51/25.07 | v_a____, v_pa____) = all_1559_4 & % 186.51/25.07 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1559_13 & % 186.51/25.07 | c_Groups_Ozero__class_Ozero(all_1559_13) = all_1559_8 & % 186.51/25.07 | hAPP(all_1559_1, v_pa____) = all_1559_0 & hAPP(all_1559_5, % 186.51/25.07 | all_1559_3) = all_1559_2 & hAPP(all_1559_11, all_1559_6) = % 186.51/25.07 | all_1559_5 & hAPP(all_1559_12, all_1559_2) = all_1559_1 & % 186.51/25.07 | $i(all_1559_0) & $i(all_1559_1) & $i(all_1559_2) & $i(all_1559_3) & % 186.51/25.07 | $i(all_1559_4) & $i(all_1559_5) & $i(all_1559_6) & $i(all_1559_7) & % 186.51/25.07 | $i(all_1559_8) & $i(all_1559_9) & $i(all_1559_10) & $i(all_1559_11) & % 186.51/25.07 | $i(all_1559_12) & $i(all_1559_13) & ~ hBOOL(all_1559_0) % 186.51/25.07 | % 186.51/25.07 | ALPHA: (101) implies: % 186.51/25.07 | (102) hAPP(all_1559_11, all_1559_6) = all_1559_5 % 186.51/25.07 | (103) c_Groups_Ozero__class_Ozero(all_1559_13) = all_1559_8 % 186.51/25.07 | (104) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1559_13 % 186.51/25.07 | (105) c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____) = % 186.51/25.07 | all_1559_4 % 186.51/25.07 | (106) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1559_10, all_1559_7) = % 186.51/25.07 | all_1559_6 % 186.51/25.07 | (107) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1559_9, all_1559_8) = % 186.51/25.07 | all_1559_7 % 186.51/25.07 | (108) c_Power_Opower__class_Opower(all_1559_13) = all_1559_11 % 186.51/25.07 | (109) c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = all_1559_9 % 186.51/25.07 | (110) c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____) = % 186.51/25.07 | all_1559_10 % 186.51/25.07 | % 186.51/25.07 | DELTA: instantiating (6) with fresh symbols all_1573_0, all_1573_1, % 186.51/25.07 | all_1573_2, all_1573_3, all_1573_4 gives: % 186.51/25.07 | (111) c_Power_Opower__class_Opower(all_1573_2) = all_1573_0 & % 186.51/25.07 | c_Rings_Odvd__class_Odvd(all_1573_2) = all_1573_1 & % 186.51/25.07 | tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1573_2 & % 186.51/25.07 | c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = all_1573_3 & % 186.51/25.07 | c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = all_1573_4 & % 186.51/25.07 | $i(all_1573_0) & $i(all_1573_1) & $i(all_1573_2) & $i(all_1573_3) & % 186.51/25.07 | $i(all_1573_4) & ! [v0: any] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 186.51/25.07 | $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v0 = all_1573_3 | % 186.51/25.07 | ~ (hAPP(v4, v0) = v5) | ~ (hAPP(v3, v5) = v6) | ~ % 186.51/25.07 | (hAPP(all_1573_0, v2) = v4) | ~ (hAPP(all_1573_1, v1) = v3) | ~ % 186.51/25.07 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 186.51/25.07 | c_Orderings_Oord__class_Oless(tc_Nat_Onat, v0, v_na____) | % 186.51/25.07 | hBOOL(v6) | ? [v7: $i] : ? [v8: $i] : ? [v9: any] : ? [v10: $i] % 186.51/25.07 | : ? [v11: int] : ? [v12: any] : ($i(v10) & ((v11 = all_1573_4 & % 186.51/25.07 | ~ (v12 = all_1573_4) & % 186.51/25.07 | c_Polynomial_Opoly(tc_Complex_Ocomplex, v2) = v8 & % 186.51/25.07 | c_Polynomial_Opoly(tc_Complex_Ocomplex, v1) = v7 & hAPP(v8, % 186.51/25.07 | v10) = v12 & hAPP(v7, v10) = all_1573_4 & $i(v12) & $i(v8) % 186.51/25.07 | & $i(v7)) | ( ~ (v9 = v0) & % 186.51/25.07 | c_Polynomial_Odegree(tc_Complex_Ocomplex, v1) = v9 & % 186.51/25.07 | $i(v9))))) % 186.51/25.07 | % 186.51/25.07 | ALPHA: (111) implies: % 186.51/25.07 | (112) tc_Polynomial_Opoly(tc_Complex_Ocomplex) = all_1573_2 % 186.51/25.07 | (113) c_Power_Opower__class_Opower(all_1573_2) = all_1573_0 % 186.51/25.07 | % 186.51/25.07 | GROUND_INST: instantiating (17) with all_877_1, all_885_1, % 186.51/25.07 | tc_Complex_Ocomplex, simplifying with (30), (34) gives: % 186.51/25.07 | (114) all_885_1 = all_877_1 % 186.51/25.07 | % 186.51/25.07 | GROUND_INST: instantiating (17) with all_1324_7, all_1385_7, % 186.51/25.07 | tc_Complex_Ocomplex, simplifying with (39), (54) gives: % 186.51/25.07 | (115) all_1385_7 = all_1324_7 % 186.51/25.07 | % 186.51/25.07 | GROUND_INST: instantiating (17) with all_885_1, all_1385_7, % 186.51/25.07 | tc_Complex_Ocomplex, simplifying with (34), (54) gives: % 186.51/25.07 | (116) all_1385_7 = all_885_1 % 186.51/25.07 | % 186.51/25.07 | GROUND_INST: instantiating (17) with all_796_0, all_1385_7, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (27), (54) gives: % 186.51/25.09 | (117) all_1385_7 = all_796_0 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (17) with all_1385_7, all_1395_8, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (54), (57) gives: % 186.51/25.09 | (118) all_1395_8 = all_1385_7 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (17) with all_1395_8, all_1511_11, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (57), (68) gives: % 186.51/25.09 | (119) all_1511_11 = all_1395_8 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (17) with all_1511_11, all_1513_12, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (68), (82) gives: % 186.51/25.09 | (120) all_1513_12 = all_1511_11 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (17) with all_1513_12, all_1518_12, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (82), (94) gives: % 186.51/25.09 | (121) all_1518_12 = all_1513_12 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (17) with all_1518_12, all_1559_13, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (94), (104) gives: % 186.51/25.09 | (122) all_1559_13 = all_1518_12 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (17) with all_1559_13, all_1573_2, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (104), (112) gives: % 186.51/25.09 | (123) all_1573_2 = all_1559_13 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (17) with all_1374_8, all_1573_2, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (47), (112) gives: % 186.51/25.09 | (124) all_1573_2 = all_1374_8 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (23) with all_1513_3, all_1518_3, v_pa____, % 186.51/25.09 | v_a____, tc_Complex_Ocomplex, simplifying with (83), (95) gives: % 186.51/25.09 | (125) all_1518_3 = all_1513_3 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (23) with all_894_1, all_1518_3, v_pa____, v_a____, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (36), (95) gives: % 186.51/25.09 | (126) all_1518_3 = all_894_1 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (23) with all_1518_3, all_1559_4, v_pa____, % 186.51/25.09 | v_a____, tc_Complex_Ocomplex, simplifying with (95), (105) gives: % 186.51/25.09 | (127) all_1559_4 = all_1518_3 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (23) with all_1511_2, all_1559_4, v_pa____, % 186.51/25.09 | v_a____, tc_Complex_Ocomplex, simplifying with (69), (105) gives: % 186.51/25.09 | (128) all_1559_4 = all_1511_2 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (19) with all_1374_5, all_1511_7, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (50), (73) gives: % 186.51/25.09 | (129) all_1511_7 = all_1374_5 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (19) with all_1324_4, all_1511_7, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (42), (73) gives: % 186.51/25.09 | (130) all_1511_7 = all_1324_4 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (19) with all_1511_7, all_1513_8, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (73), (87) gives: % 186.51/25.09 | (131) all_1513_8 = all_1511_7 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (19) with all_1518_8, all_1559_9, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (99), (109) gives: % 186.51/25.09 | (132) all_1559_9 = all_1518_8 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (19) with all_1513_8, all_1559_9, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (87), (109) gives: % 186.51/25.09 | (133) all_1559_9 = all_1513_8 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (19) with all_1395_5, all_1559_9, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (60), (109) gives: % 186.51/25.09 | (134) all_1559_9 = all_1395_5 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (22) with all_1324_5, all_1395_6, v_a____, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (43), (61) gives: % 186.51/25.09 | (135) all_1395_6 = all_1324_5 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (22) with all_1395_6, all_1511_8, v_a____, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (61), (74) gives: % 186.51/25.09 | (136) all_1511_8 = all_1395_6 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (22) with all_1511_8, all_1513_9, v_a____, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (74), (88) gives: % 186.51/25.09 | (137) all_1513_9 = all_1511_8 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (22) with all_1513_9, all_1518_9, v_a____, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (88), (100) gives: % 186.51/25.09 | (138) all_1518_9 = all_1513_9 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (22) with all_1518_9, all_1559_10, v_a____, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (100), (110) gives: % 186.51/25.09 | (139) all_1559_10 = all_1518_9 % 186.51/25.09 | % 186.51/25.09 | GROUND_INST: instantiating (22) with all_1374_6, all_1559_10, v_a____, % 186.51/25.09 | tc_Complex_Ocomplex, simplifying with (51), (110) gives: % 186.51/25.09 | (140) all_1559_10 = all_1374_6 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (123), (124) imply: % 186.51/25.09 | (141) all_1559_13 = all_1374_8 % 186.51/25.09 | % 186.51/25.09 | SIMP: (141) implies: % 186.51/25.09 | (142) all_1559_13 = all_1374_8 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (127), (128) imply: % 186.51/25.09 | (143) all_1518_3 = all_1511_2 % 186.51/25.09 | % 186.51/25.09 | SIMP: (143) implies: % 186.51/25.09 | (144) all_1518_3 = all_1511_2 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (132), (133) imply: % 186.51/25.09 | (145) all_1518_8 = all_1513_8 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (132), (134) imply: % 186.51/25.09 | (146) all_1518_8 = all_1395_5 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (139), (140) imply: % 186.51/25.09 | (147) all_1518_9 = all_1374_6 % 186.51/25.09 | % 186.51/25.09 | SIMP: (147) implies: % 186.51/25.09 | (148) all_1518_9 = all_1374_6 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (122), (142) imply: % 186.51/25.09 | (149) all_1518_12 = all_1374_8 % 186.51/25.09 | % 186.51/25.09 | SIMP: (149) implies: % 186.51/25.09 | (150) all_1518_12 = all_1374_8 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (125), (144) imply: % 186.51/25.09 | (151) all_1513_3 = all_1511_2 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (125), (126) imply: % 186.51/25.09 | (152) all_1513_3 = all_894_1 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (145), (146) imply: % 186.51/25.09 | (153) all_1513_8 = all_1395_5 % 186.51/25.09 | % 186.51/25.09 | SIMP: (153) implies: % 186.51/25.09 | (154) all_1513_8 = all_1395_5 % 186.51/25.09 | % 186.51/25.09 | COMBINE_EQS: (138), (148) imply: % 186.51/25.09 | (155) all_1513_9 = all_1374_6 % 186.51/25.09 | % 186.51/25.09 | SIMP: (155) implies: % 186.51/25.10 | (156) all_1513_9 = all_1374_6 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (121), (150) imply: % 186.51/25.10 | (157) all_1513_12 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | SIMP: (157) implies: % 186.51/25.10 | (158) all_1513_12 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (151), (152) imply: % 186.51/25.10 | (159) all_1511_2 = all_894_1 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (131), (154) imply: % 186.51/25.10 | (160) all_1511_7 = all_1395_5 % 186.51/25.10 | % 186.51/25.10 | SIMP: (160) implies: % 186.51/25.10 | (161) all_1511_7 = all_1395_5 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (137), (156) imply: % 186.51/25.10 | (162) all_1511_8 = all_1374_6 % 186.51/25.10 | % 186.51/25.10 | SIMP: (162) implies: % 186.51/25.10 | (163) all_1511_8 = all_1374_6 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (120), (158) imply: % 186.51/25.10 | (164) all_1511_11 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | SIMP: (164) implies: % 186.51/25.10 | (165) all_1511_11 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (130), (161) imply: % 186.51/25.10 | (166) all_1395_5 = all_1324_4 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (129), (161) imply: % 186.51/25.10 | (167) all_1395_5 = all_1374_5 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (136), (163) imply: % 186.51/25.10 | (168) all_1395_6 = all_1374_6 % 186.51/25.10 | % 186.51/25.10 | SIMP: (168) implies: % 186.51/25.10 | (169) all_1395_6 = all_1374_6 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (119), (165) imply: % 186.51/25.10 | (170) all_1395_8 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | SIMP: (170) implies: % 186.51/25.10 | (171) all_1395_8 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (166), (167) imply: % 186.51/25.10 | (172) all_1374_5 = all_1324_4 % 186.51/25.10 | % 186.51/25.10 | SIMP: (172) implies: % 186.51/25.10 | (173) all_1374_5 = all_1324_4 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (135), (169) imply: % 186.51/25.10 | (174) all_1374_6 = all_1324_5 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (118), (171) imply: % 186.51/25.10 | (175) all_1385_7 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | SIMP: (175) implies: % 186.51/25.10 | (176) all_1385_7 = all_1374_8 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (117), (176) imply: % 186.51/25.10 | (177) all_1374_8 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (116), (176) imply: % 186.51/25.10 | (178) all_1374_8 = all_885_1 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (115), (176) imply: % 186.51/25.10 | (179) all_1374_8 = all_1324_7 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (177), (179) imply: % 186.51/25.10 | (180) all_1324_7 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (178), (179) imply: % 186.51/25.10 | (181) all_1324_7 = all_885_1 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (180), (181) imply: % 186.51/25.10 | (182) all_885_1 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | SIMP: (182) implies: % 186.51/25.10 | (183) all_885_1 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (114), (183) imply: % 186.51/25.10 | (184) all_877_1 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | SIMP: (184) implies: % 186.51/25.10 | (185) all_877_1 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (171), (177) imply: % 186.51/25.10 | (186) all_1395_8 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (165), (177) imply: % 186.51/25.10 | (187) all_1511_11 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (163), (174) imply: % 186.51/25.10 | (188) all_1511_8 = all_1324_5 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (158), (177) imply: % 186.51/25.10 | (189) all_1513_12 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (156), (174) imply: % 186.51/25.10 | (190) all_1513_9 = all_1324_5 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (154), (166) imply: % 186.51/25.10 | (191) all_1513_8 = all_1324_4 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (150), (177) imply: % 186.51/25.10 | (192) all_1518_12 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (148), (174) imply: % 186.51/25.10 | (193) all_1518_9 = all_1324_5 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (146), (166) imply: % 186.51/25.10 | (194) all_1518_8 = all_1324_4 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (142), (177) imply: % 186.51/25.10 | (195) all_1559_13 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (140), (174) imply: % 186.51/25.10 | (196) all_1559_10 = all_1324_5 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (132), (194) imply: % 186.51/25.10 | (197) all_1559_9 = all_1324_4 % 186.51/25.10 | % 186.51/25.10 | COMBINE_EQS: (124), (177) imply: % 186.51/25.10 | (198) all_1573_2 = all_796_0 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (89), (189) imply: % 186.51/25.10 | (199) c_Groups_Otimes__class_Otimes(all_796_0) = all_1513_11 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (75), (187) imply: % 186.51/25.10 | (200) c_Groups_Otimes__class_Otimes(all_796_0) = all_1511_10 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (52), (177) imply: % 186.51/25.10 | (201) c_Groups_Otimes__class_Otimes(all_796_0) = all_1374_7 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (44), (180) imply: % 186.51/25.10 | (202) c_Groups_Otimes__class_Otimes(all_796_0) = all_1324_6 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (113), (198) imply: % 186.51/25.10 | (203) c_Power_Opower__class_Opower(all_796_0) = all_1573_0 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (108), (195) imply: % 186.51/25.10 | (204) c_Power_Opower__class_Opower(all_796_0) = all_1559_11 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (98), (192) imply: % 186.51/25.10 | (205) c_Power_Opower__class_Opower(all_796_0) = all_1518_10 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (86), (189) imply: % 186.51/25.10 | (206) c_Power_Opower__class_Opower(all_796_0) = all_1513_10 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (72), (187) imply: % 186.51/25.10 | (207) c_Power_Opower__class_Opower(all_796_0) = all_1511_9 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (107), (197) imply: % 186.51/25.10 | (208) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, all_1559_8) = % 186.51/25.10 | all_1559_7 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (106), (196) imply: % 186.51/25.10 | (209) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1559_7) = % 186.51/25.10 | all_1559_6 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (97), (194) imply: % 186.51/25.10 | (210) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, all_1518_7) = % 186.51/25.10 | all_1518_6 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (96), (193) imply: % 186.51/25.10 | (211) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1518_6) = % 186.51/25.10 | all_1518_5 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (85), (191) imply: % 186.51/25.10 | (212) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, all_1513_7) = % 186.51/25.10 | all_1513_6 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (84), (190) imply: % 186.51/25.10 | (213) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1513_6) = % 186.51/25.10 | all_1513_5 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (71), (130) imply: % 186.51/25.10 | (214) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, all_1511_6) = % 186.51/25.10 | all_1511_5 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (70), (188) imply: % 186.51/25.10 | (215) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1511_5) = % 186.51/25.10 | all_1511_4 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (59), (166) imply: % 186.51/25.10 | (216) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, all_1395_4) = % 186.51/25.10 | all_1395_3 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (58), (135) imply: % 186.51/25.10 | (217) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1395_3) = % 186.51/25.10 | all_1395_2 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (49), (173) imply: % 186.51/25.10 | (218) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, all_1374_4) = % 186.51/25.10 | all_1374_3 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (48), (174) imply: % 186.51/25.10 | (219) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1374_3) = % 186.51/25.10 | all_1374_2 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (103), (195) imply: % 186.51/25.10 | (220) c_Groups_Ozero__class_Ozero(all_796_0) = all_1559_8 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (93), (192) imply: % 186.51/25.10 | (221) c_Groups_Ozero__class_Ozero(all_796_0) = all_1518_7 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (81), (189) imply: % 186.51/25.10 | (222) c_Groups_Ozero__class_Ozero(all_796_0) = all_1513_7 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (67), (187) imply: % 186.51/25.10 | (223) c_Groups_Ozero__class_Ozero(all_796_0) = all_1511_6 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (56), (186) imply: % 186.51/25.10 | (224) c_Groups_Ozero__class_Ozero(all_796_0) = all_1395_4 % 186.51/25.10 | % 186.51/25.10 | REDUCE: (46), (177) imply: % 186.51/25.11 | (225) c_Groups_Ozero__class_Ozero(all_796_0) = all_1374_4 % 186.51/25.11 | % 186.51/25.11 | REDUCE: (38), (180) imply: % 186.51/25.11 | (226) c_Groups_Ozero__class_Ozero(all_796_0) = all_1324_3 % 186.51/25.11 | % 186.51/25.11 | REDUCE: (33), (183) imply: % 186.51/25.11 | (227) c_Groups_Ozero__class_Ozero(all_796_0) = all_885_0 % 186.51/25.11 | % 186.51/25.11 | REDUCE: (29), (185) imply: % 186.51/25.11 | (228) c_Groups_Ozero__class_Ozero(all_796_0) = all_877_0 % 186.51/25.11 | % 186.51/25.11 | REDUCE: (92), (126) imply: % 186.51/25.11 | (229) hAPP(all_1518_4, all_894_1) = all_1518_2 % 186.51/25.11 | % 186.51/25.11 | REDUCE: (80), (152) imply: % 186.51/25.11 | (230) hAPP(all_1513_4, all_894_1) = all_1513_2 % 186.51/25.11 | % 186.51/25.11 | REDUCE: (65), (159) imply: % 186.51/25.11 | (231) hAPP(all_1511_3, all_894_1) = all_1511_1 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_885_0, all_1324_3, all_796_0, % 186.51/25.11 | simplifying with (226), (227) gives: % 186.51/25.11 | (232) all_1324_3 = all_885_0 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_885_0, all_1395_4, all_796_0, % 186.51/25.11 | simplifying with (224), (227) gives: % 186.51/25.11 | (233) all_1395_4 = all_885_0 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_1395_4, all_1511_6, all_796_0, % 186.51/25.11 | simplifying with (223), (224) gives: % 186.51/25.11 | (234) all_1511_6 = all_1395_4 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_1511_6, all_1513_7, all_796_0, % 186.51/25.11 | simplifying with (222), (223) gives: % 186.51/25.11 | (235) all_1513_7 = all_1511_6 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_1513_7, all_1518_7, all_796_0, % 186.51/25.11 | simplifying with (221), (222) gives: % 186.51/25.11 | (236) all_1518_7 = all_1513_7 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_877_0, all_1518_7, all_796_0, % 186.51/25.11 | simplifying with (221), (228) gives: % 186.51/25.11 | (237) all_1518_7 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with v_s____, all_1559_8, all_796_0, % 186.51/25.11 | simplifying with (26), (220) gives: % 186.51/25.11 | (238) all_1559_8 = v_s____ % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_1374_4, all_1559_8, all_796_0, % 186.51/25.11 | simplifying with (220), (225) gives: % 186.51/25.11 | (239) all_1559_8 = all_1374_4 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (16) with all_1324_3, all_1559_8, all_796_0, % 186.51/25.11 | simplifying with (220), (226) gives: % 186.51/25.11 | (240) all_1559_8 = all_1324_3 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (18) with all_1513_10, all_1518_10, all_796_0, % 186.51/25.11 | simplifying with (205), (206) gives: % 186.51/25.11 | (241) all_1518_10 = all_1513_10 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (18) with all_1559_11, all_1573_0, all_796_0, % 186.51/25.11 | simplifying with (203), (204) gives: % 186.51/25.11 | (242) all_1573_0 = all_1559_11 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (18) with all_1518_10, all_1573_0, all_796_0, % 186.51/25.11 | simplifying with (203), (205) gives: % 186.51/25.11 | (243) all_1573_0 = all_1518_10 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (18) with all_1511_9, all_1573_0, all_796_0, % 186.51/25.11 | simplifying with (203), (207) gives: % 186.51/25.11 | (244) all_1573_0 = all_1511_9 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (20) with all_1374_7, all_1511_10, all_796_0, % 186.51/25.11 | simplifying with (200), (201) gives: % 186.51/25.11 | (245) all_1511_10 = all_1374_7 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (20) with all_1511_10, all_1513_11, all_796_0, % 186.51/25.11 | simplifying with (199), (200) gives: % 186.51/25.11 | (246) all_1513_11 = all_1511_10 % 186.51/25.11 | % 186.51/25.11 | GROUND_INST: instantiating (20) with all_1324_6, all_1513_11, all_796_0, % 186.51/25.11 | simplifying with (199), (202) gives: % 186.51/25.11 | (247) all_1513_11 = all_1324_6 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (242), (244) imply: % 186.51/25.11 | (248) all_1559_11 = all_1511_9 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (242), (243) imply: % 186.51/25.11 | (249) all_1559_11 = all_1518_10 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (238), (239) imply: % 186.51/25.11 | (250) all_1374_4 = v_s____ % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (239), (240) imply: % 186.51/25.11 | (251) all_1374_4 = all_1324_3 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (248), (249) imply: % 186.51/25.11 | (252) all_1518_10 = all_1511_9 % 186.51/25.11 | % 186.51/25.11 | SIMP: (252) implies: % 186.51/25.11 | (253) all_1518_10 = all_1511_9 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (236), (237) imply: % 186.51/25.11 | (254) all_1513_7 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | SIMP: (254) implies: % 186.51/25.11 | (255) all_1513_7 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (241), (253) imply: % 186.51/25.11 | (256) all_1513_10 = all_1511_9 % 186.51/25.11 | % 186.51/25.11 | SIMP: (256) implies: % 186.51/25.11 | (257) all_1513_10 = all_1511_9 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (235), (255) imply: % 186.51/25.11 | (258) all_1511_6 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | SIMP: (258) implies: % 186.51/25.11 | (259) all_1511_6 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (246), (247) imply: % 186.51/25.11 | (260) all_1511_10 = all_1324_6 % 186.51/25.11 | % 186.51/25.11 | SIMP: (260) implies: % 186.51/25.11 | (261) all_1511_10 = all_1324_6 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (234), (259) imply: % 186.51/25.11 | (262) all_1395_4 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | SIMP: (262) implies: % 186.51/25.11 | (263) all_1395_4 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (245), (261) imply: % 186.51/25.11 | (264) all_1374_7 = all_1324_6 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (233), (263) imply: % 186.51/25.11 | (265) all_885_0 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | SIMP: (265) implies: % 186.51/25.11 | (266) all_885_0 = all_877_0 % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (250), (251) imply: % 186.51/25.11 | (267) all_1324_3 = v_s____ % 186.51/25.11 | % 186.51/25.11 | SIMP: (267) implies: % 186.51/25.11 | (268) all_1324_3 = v_s____ % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (232), (268) imply: % 186.51/25.11 | (269) all_885_0 = v_s____ % 186.51/25.11 | % 186.51/25.11 | SIMP: (269) implies: % 186.51/25.11 | (270) all_885_0 = v_s____ % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (266), (270) imply: % 186.51/25.11 | (271) all_877_0 = v_s____ % 186.51/25.11 | % 186.51/25.11 | COMBINE_EQS: (263), (271) imply: % 186.94/25.11 | (272) all_1395_4 = v_s____ % 186.94/25.11 | % 186.94/25.11 | COMBINE_EQS: (259), (271) imply: % 186.94/25.11 | (273) all_1511_6 = v_s____ % 186.94/25.11 | % 186.94/25.11 | COMBINE_EQS: (255), (271) imply: % 186.94/25.11 | (274) all_1513_7 = v_s____ % 186.94/25.11 | % 186.94/25.11 | COMBINE_EQS: (237), (271) imply: % 186.94/25.11 | (275) all_1518_7 = v_s____ % 186.94/25.11 | % 186.94/25.11 | REDUCE: (32), (270) imply: % 186.94/25.11 | (276) ~ (v_s____ = v_pa____) % 186.94/25.11 | % 186.94/25.11 | REDUCE: (208), (238) imply: % 186.94/25.11 | (277) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, v_s____) = % 186.94/25.11 | all_1559_7 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (210), (275) imply: % 186.94/25.11 | (278) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, v_s____) = % 186.94/25.11 | all_1518_6 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (212), (274) imply: % 186.94/25.11 | (279) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, v_s____) = % 186.94/25.11 | all_1513_6 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (214), (273) imply: % 186.94/25.11 | (280) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, v_s____) = % 186.94/25.11 | all_1511_5 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (216), (272) imply: % 186.94/25.11 | (281) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, v_s____) = % 186.94/25.11 | all_1395_3 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (218), (250) imply: % 186.94/25.11 | (282) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, v_s____) = % 186.94/25.11 | all_1374_3 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (41), (268) imply: % 186.94/25.11 | (283) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_4, v_s____) = % 186.94/25.11 | all_1324_2 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (102), (248) imply: % 186.94/25.11 | (284) hAPP(all_1511_9, all_1559_6) = all_1559_5 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (91), (253) imply: % 186.94/25.11 | (285) hAPP(all_1511_9, all_1518_5) = all_1518_4 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (79), (257) imply: % 186.94/25.11 | (286) hAPP(all_1511_9, all_1513_5) = all_1513_4 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (78), (247) imply: % 186.94/25.11 | (287) hAPP(all_1324_6, all_1513_2) = all_1513_1 % 186.94/25.11 | % 186.94/25.11 | REDUCE: (63), (261) imply: % 186.94/25.11 | (288) hAPP(all_1324_6, all_1511_1) = all_1511_0 % 186.94/25.11 | % 186.94/25.11 | GROUND_INST: instantiating (24) with all_1374_3, all_1511_5, v_s____, % 186.94/25.11 | all_1324_4, tc_Complex_Ocomplex, simplifying with (280), (282) % 186.94/25.11 | gives: % 186.94/25.11 | (289) all_1511_5 = all_1374_3 % 186.94/25.11 | % 186.94/25.11 | GROUND_INST: instantiating (24) with all_1511_5, all_1513_6, v_s____, % 186.94/25.11 | all_1324_4, tc_Complex_Ocomplex, simplifying with (279), (280) % 186.94/25.11 | gives: % 186.94/25.12 | (290) all_1513_6 = all_1511_5 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1513_6, all_1518_6, v_s____, % 186.94/25.12 | all_1324_4, tc_Complex_Ocomplex, simplifying with (278), (279) % 186.94/25.12 | gives: % 186.94/25.12 | (291) all_1518_6 = all_1513_6 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1324_2, all_1518_6, v_s____, % 186.94/25.12 | all_1324_4, tc_Complex_Ocomplex, simplifying with (278), (283) % 186.94/25.12 | gives: % 186.94/25.12 | (292) all_1518_6 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1511_5, all_1559_7, v_s____, % 186.94/25.12 | all_1324_4, tc_Complex_Ocomplex, simplifying with (277), (280) % 186.94/25.12 | gives: % 186.94/25.12 | (293) all_1559_7 = all_1511_5 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1395_3, all_1559_7, v_s____, % 186.94/25.12 | all_1324_4, tc_Complex_Ocomplex, simplifying with (277), (281) % 186.94/25.12 | gives: % 186.94/25.12 | (294) all_1559_7 = all_1395_3 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (293), (294) imply: % 186.94/25.12 | (295) all_1511_5 = all_1395_3 % 186.94/25.12 | % 186.94/25.12 | SIMP: (295) implies: % 186.94/25.12 | (296) all_1511_5 = all_1395_3 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (291), (292) imply: % 186.94/25.12 | (297) all_1513_6 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | SIMP: (297) implies: % 186.94/25.12 | (298) all_1513_6 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (290), (298) imply: % 186.94/25.12 | (299) all_1511_5 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | SIMP: (299) implies: % 186.94/25.12 | (300) all_1511_5 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (289), (296) imply: % 186.94/25.12 | (301) all_1395_3 = all_1374_3 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (296), (300) imply: % 186.94/25.12 | (302) all_1395_3 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (301), (302) imply: % 186.94/25.12 | (303) all_1374_3 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | SIMP: (303) implies: % 186.94/25.12 | (304) all_1374_3 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (294), (302) imply: % 186.94/25.12 | (305) all_1559_7 = all_1324_2 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (209), (305) imply: % 186.94/25.12 | (306) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1324_2) = % 186.94/25.12 | all_1559_6 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (211), (292) imply: % 186.94/25.12 | (307) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1324_2) = % 186.94/25.12 | all_1518_5 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (213), (298) imply: % 186.94/25.12 | (308) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1324_2) = % 186.94/25.12 | all_1513_5 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (215), (300) imply: % 186.94/25.12 | (309) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1324_2) = % 186.94/25.12 | all_1511_4 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (217), (302) imply: % 186.94/25.12 | (310) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1324_2) = % 186.94/25.12 | all_1395_2 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (219), (304) imply: % 186.94/25.12 | (311) c_Polynomial_OpCons(tc_Complex_Ocomplex, all_1324_5, all_1324_2) = % 186.94/25.12 | all_1374_2 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1324_1, all_1395_2, all_1324_2, % 186.94/25.12 | all_1324_5, tc_Complex_Ocomplex, simplifying with (40), (310) % 186.94/25.12 | gives: % 186.94/25.12 | (312) all_1395_2 = all_1324_1 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1395_2, all_1511_4, all_1324_2, % 186.94/25.12 | all_1324_5, tc_Complex_Ocomplex, simplifying with (309), (310) % 186.94/25.12 | gives: % 186.94/25.12 | (313) all_1511_4 = all_1395_2 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1511_4, all_1513_5, all_1324_2, % 186.94/25.12 | all_1324_5, tc_Complex_Ocomplex, simplifying with (308), (309) % 186.94/25.12 | gives: % 186.94/25.12 | (314) all_1513_5 = all_1511_4 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1513_5, all_1518_5, all_1324_2, % 186.94/25.12 | all_1324_5, tc_Complex_Ocomplex, simplifying with (307), (308) % 186.94/25.12 | gives: % 186.94/25.12 | (315) all_1518_5 = all_1513_5 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1518_5, all_1559_6, all_1324_2, % 186.94/25.12 | all_1324_5, tc_Complex_Ocomplex, simplifying with (306), (307) % 186.94/25.12 | gives: % 186.94/25.12 | (316) all_1559_6 = all_1518_5 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (24) with all_1374_2, all_1559_6, all_1324_2, % 186.94/25.12 | all_1324_5, tc_Complex_Ocomplex, simplifying with (306), (311) % 186.94/25.12 | gives: % 186.94/25.12 | (317) all_1559_6 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (316), (317) imply: % 186.94/25.12 | (318) all_1518_5 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | SIMP: (318) implies: % 186.94/25.12 | (319) all_1518_5 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (315), (319) imply: % 186.94/25.12 | (320) all_1513_5 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | SIMP: (320) implies: % 186.94/25.12 | (321) all_1513_5 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (314), (321) imply: % 186.94/25.12 | (322) all_1511_4 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | SIMP: (322) implies: % 186.94/25.12 | (323) all_1511_4 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (313), (323) imply: % 186.94/25.12 | (324) all_1395_2 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | SIMP: (324) implies: % 186.94/25.12 | (325) all_1395_2 = all_1374_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (312), (325) imply: % 186.94/25.12 | (326) all_1374_2 = all_1324_1 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (323), (326) imply: % 186.94/25.12 | (327) all_1511_4 = all_1324_1 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (321), (326) imply: % 186.94/25.12 | (328) all_1513_5 = all_1324_1 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (319), (326) imply: % 186.94/25.12 | (329) all_1518_5 = all_1324_1 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (317), (326) imply: % 186.94/25.12 | (330) all_1559_6 = all_1324_1 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (284), (330) imply: % 186.94/25.12 | (331) hAPP(all_1511_9, all_1324_1) = all_1559_5 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (285), (329) imply: % 186.94/25.12 | (332) hAPP(all_1511_9, all_1324_1) = all_1518_4 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (286), (328) imply: % 186.94/25.12 | (333) hAPP(all_1511_9, all_1324_1) = all_1513_4 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (64), (327) imply: % 186.94/25.12 | (334) hAPP(all_1511_9, all_1324_1) = all_1511_3 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (21) with all_1513_4, all_1518_4, all_1324_1, % 186.94/25.12 | all_1511_9, simplifying with (332), (333) gives: % 186.94/25.12 | (335) all_1518_4 = all_1513_4 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (21) with all_1518_4, all_1559_5, all_1324_1, % 186.94/25.12 | all_1511_9, simplifying with (331), (332) gives: % 186.94/25.12 | (336) all_1559_5 = all_1518_4 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (21) with all_1511_3, all_1559_5, all_1324_1, % 186.94/25.12 | all_1511_9, simplifying with (331), (334) gives: % 186.94/25.12 | (337) all_1559_5 = all_1511_3 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (336), (337) imply: % 186.94/25.12 | (338) all_1518_4 = all_1511_3 % 186.94/25.12 | % 186.94/25.12 | SIMP: (338) implies: % 186.94/25.12 | (339) all_1518_4 = all_1511_3 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (335), (339) imply: % 186.94/25.12 | (340) all_1513_4 = all_1511_3 % 186.94/25.12 | % 186.94/25.12 | SIMP: (340) implies: % 186.94/25.12 | (341) all_1513_4 = all_1511_3 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (229), (339) imply: % 186.94/25.12 | (342) hAPP(all_1511_3, all_894_1) = all_1518_2 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (230), (341) imply: % 186.94/25.12 | (343) hAPP(all_1511_3, all_894_1) = all_1513_2 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (21) with all_1511_1, all_1518_2, all_894_1, % 186.94/25.12 | all_1511_3, simplifying with (231), (342) gives: % 186.94/25.12 | (344) all_1518_2 = all_1511_1 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (21) with all_1513_2, all_1518_2, all_894_1, % 186.94/25.12 | all_1511_3, simplifying with (342), (343) gives: % 186.94/25.12 | (345) all_1518_2 = all_1513_2 % 186.94/25.12 | % 186.94/25.12 | COMBINE_EQS: (344), (345) imply: % 186.94/25.12 | (346) all_1513_2 = all_1511_1 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (287), (346) imply: % 186.94/25.12 | (347) hAPP(all_1324_6, all_1511_1) = all_1513_1 % 186.94/25.12 | % 186.94/25.12 | REDUCE: (77), (346) imply: % 186.94/25.12 | (348) $i(all_1511_1) % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (21) with all_1511_0, all_1513_1, all_1511_1, % 186.94/25.12 | all_1324_6, simplifying with (288), (347) gives: % 186.94/25.12 | (349) all_1513_1 = all_1511_0 % 186.94/25.12 | % 186.94/25.12 | GROUND_INST: instantiating (fact_mult__poly__0__right) with all_1511_1, % 186.94/25.12 | tc_Complex_Ocomplex, all_796_0, all_1324_6, all_1511_0, v_s____, % 186.94/25.12 | v_pa____, simplifying with (13), (14), (26), (27), (66), (202), % 186.94/25.12 | (288), (348) gives: % 186.94/25.12 | (350) v_s____ = v_pa____ % 186.94/25.12 | % 186.94/25.12 | REDUCE: (276), (350) imply: % 186.94/25.12 | (351) $false % 186.94/25.13 | % 186.94/25.13 | CLOSE: (351) is inconsistent. % 186.94/25.13 | % 186.94/25.13 End of proof % 186.94/25.13 % SZS output end Proof for theBenchmark % 186.94/25.13 % 186.94/25.13 24608ms %------------------------------------------------------------------------------