%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n015.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 : Tue May 5 06:54:43 PM UTC 2026 % Result : Theorem 110.31s 15.22s % Output : Proof 267.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.33 % Computer : n015.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 05:22:31 EDT 2026 % 0.16/0.33 % CPUTime : % 0.57/0.58 ________ _____ % 0.57/0.58 ___ __ \_________(_)________________________________ % 0.57/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.57/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.57/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.57/0.58 % 0.57/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.57/0.58 (2023-06-19) % 0.57/0.58 % 0.57/0.58 (c) Philipp Rümmer, 2009-2023 % 0.57/0.58 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.57/0.58 Amanda Stjerna. % 0.57/0.58 Free software under BSD-3-Clause. % 0.57/0.58 % 0.57/0.58 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.57/0.58 % 0.57/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.57/0.60 Running up to 7 provers in parallel. % 0.57/0.61 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.57/0.61 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.57/0.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.57/0.61 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.57/0.61 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.57/0.61 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.57/0.61 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 25.50/4.20 Prover 6: Preprocessing ... % 25.50/4.22 Prover 3: Preprocessing ... % 25.50/4.25 Prover 5: Preprocessing ... % 25.50/4.25 Prover 1: Preprocessing ... % 26.25/4.36 Prover 2: Preprocessing ... % 26.25/4.39 Prover 4: Preprocessing ... % 26.25/4.39 Prover 0: Preprocessing ... % 78.89/11.16 Prover 1: Warning: ignoring some quantifiers % 86.58/12.18 Prover 1: Constructing countermodel ... % 86.58/12.18 Prover 3: Warning: ignoring some quantifiers % 87.08/12.27 Prover 3: Constructing countermodel ... % 99.47/13.90 Prover 6: Proving ... % 102.57/14.29 Prover 5: Proving ... % 110.31/15.21 Prover 3: proved (14607ms) % 110.31/15.21 % 110.31/15.22 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 110.31/15.22 % 110.31/15.22 Prover 6: stopped % 110.31/15.23 Prover 5: stopped % 110.31/15.23 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 110.31/15.23 Prover 0: stopped % 110.31/15.25 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 110.31/15.25 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 110.31/15.25 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 111.06/15.32 Prover 2: stopped % 111.06/15.34 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 115.69/15.95 Prover 1: stopped % 115.69/15.95 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 133.07/18.33 Prover 7: Preprocessing ... % 133.85/18.42 Prover 8: Preprocessing ... % 133.85/18.45 Prover 10: Preprocessing ... % 133.85/18.48 Prover 11: Preprocessing ... % 134.61/18.55 Prover 13: Preprocessing ... % 136.91/18.83 Prover 16: Preprocessing ... % 154.08/21.05 Prover 13: Warning: ignoring some quantifiers % 156.23/21.32 Prover 10: Warning: ignoring some quantifiers % 156.23/21.34 Prover 16: Warning: ignoring some quantifiers % 157.72/21.50 Prover 13: Constructing countermodel ... % 157.72/21.59 Prover 16: Constructing countermodel ... % 158.52/21.61 Prover 10: Constructing countermodel ... % 159.25/21.79 Prover 8: Warning: ignoring some quantifiers % 160.80/21.98 Prover 8: Constructing countermodel ... % 168.40/23.01 Prover 7: Warning: ignoring some quantifiers % 172.23/23.42 Prover 7: Constructing countermodel ... % 177.02/24.04 Prover 13: stopped % 177.02/24.06 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 193.73/26.35 Prover 19: Preprocessing ... % 200.61/27.25 Prover 16: stopped % 205.48/27.94 Prover 4: stopped % 212.12/28.94 Prover 19: Warning: ignoring some quantifiers % 213.61/29.16 Prover 19: Constructing countermodel ... % 249.44/34.13 Prover 7: stopped % 249.82/34.29 Prover 19: stopped % 266.56/37.80 Prover 10: Found proof (size 27) % 266.56/37.80 Prover 10: proved (22554ms) % 266.56/37.80 Prover 8: stopped % 266.56/37.86 Prover 11: stopped % 266.56/37.86 % 266.56/37.86 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 266.56/37.86 % 266.56/37.86 % SZS output start Proof for theBenchmark % 266.82/37.90 Assumptions after simplification: % 266.82/37.90 --------------------------------- % 266.82/37.90 % 266.82/37.90 (Coq.ZArith.BinInt.Z.pow_le_mono_l_iff) % 266.82/37.93 $i(cCoq_2eNumbers_2eBinNums_2eZ0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 266.82/37.93 ! [v3: $i] : ( ~ % 266.82/37.93 (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, v2) = % 266.82/37.93 v3) | ~ % 266.82/37.93 (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, v0) = % 266.82/37.93 v1) | ~ $i(v2) | ~ $i(v0) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v2) | % 266.82/37.93 ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) | ? [v4: $i] : % 266.82/37.93 (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v0, v2) = v4 & $i(v4) & ! [v5: $i] % 266.82/37.93 : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 266.82/37.93 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v2, v5) = v7) | ~ % 266.82/37.93 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v0, v5) = v6) | ~ % 266.82/37.93 (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v6, v7) = v8) | ~ $i(v5) | ~ % 266.82/37.93 cCoq_2eNumbers_2eBinNums_2eZ___24t(v5) | ~ p(v8) | ~ p(v3) | ~ p(v1) % 266.82/37.93 | p(v4) | ? [v9: $i] : % 266.82/37.93 (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 266.82/37.93 v5) = v9 & $i(v9) & ~ p(v9))) & ! [v5: $i] : ! [v6: $i] : ! [v7: % 266.82/37.93 $i] : ! [v8: $i] : ( ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v2, % 266.82/37.93 v5) = v7) | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v0, v5) = % 266.82/37.93 v6) | ~ (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v6, v7) = v8) | ~ % 266.82/37.93 $i(v5) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v5) | ~ p(v4) | ~ p(v3) % 266.82/37.93 | ~ p(v1) | p(v8) | ? [v9: $i] : % 266.82/37.93 (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 266.82/37.93 v5) = v9 & $i(v9) & ~ p(v9))))) % 266.82/37.93 % 266.82/37.93 (Coq.ZArith.BinInt.Z.square_le_simpl_nonneg) % 266.82/37.93 $i(cCoq_2eNumbers_2eBinNums_2eZ0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 266.82/37.93 ! [v3: $i] : ! [v4: $i] : ( ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v2, % 266.82/37.93 v2) = v3) | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v0, v0) = v1) % 266.82/37.93 | ~ (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v1, v3) = v4) | ~ $i(v2) | ~ % 266.82/37.93 $i(v0) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v2) | ~ % 266.82/37.93 cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) | ~ p(v4) | ? [v5: $i] : ? [v6: % 266.82/37.93 $i] : ((cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v0, v2) = v6 & $i(v6) & % 266.82/37.93 p(v6)) | % 266.82/37.93 (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, v2) % 266.82/37.93 = v5 & $i(v5) & ~ p(v5)))) % 266.82/37.93 % 266.82/37.93 (_HAMMER_GOAL) % 266.82/37.94 $i(cCoq_2eNumbers_2eBinNums_2eZ0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 266.82/37.94 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 266.82/37.94 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v3, v3) = v5 & % 266.82/37.94 cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v0, v0) = v2 & % 266.82/37.94 cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v5, v2) = v6 & % 266.82/37.94 cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v3, v0) = v7 & % 266.82/37.94 cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, v3) = % 266.82/37.94 v4 & cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 266.82/37.94 v0) = v1 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 266.82/37.94 $i(v0) & cCoq_2eNumbers_2eBinNums_2eZ___24t(v3) & % 266.82/37.94 cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) & p(v6) & p(v4) & p(v1) & ~ p(v7)) % 266.82/37.94 % 266.82/37.94 (function-axioms) % 267.42/38.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 267.42/38.03 $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : % 267.42/38.03 ! [v11: $i] : ! [v12: $i] : ! [v13: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__lam__14596___24a12(v13, v12, v11, v10, v9, v8, v7, v6, v5, v4, v3, % 267.42/38.03 v2) = v1) | ~ (c_24__lam__14596___24a12(v13, v12, v11, v10, v9, v8, v7, % 267.42/38.03 v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 267.42/38.03 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: % 267.42/38.03 $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : ! [v13: % 267.42/38.03 $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2enorm__subst___24a12(v13, v12, v11, % 267.42/38.03 v10, v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2enorm__subst___24a12(v13, v12, v11, % 267.42/38.03 v10, v9, v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 267.42/38.03 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! % 267.42/38.03 [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! [v12: % 267.42/38.03 $i] : (v1 = v0 | ~ (c_24__lam__14596___24a11(v12, v11, v10, v9, v8, v7, v6, % 267.42/38.03 v5, v4, v3, v2) = v1) | ~ (c_24__lam__14596___24a11(v12, v11, v10, v9, % 267.42/38.03 v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.03 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 267.42/38.03 ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : (v1 = % 267.42/38.03 v0 | ~ (cCoq_2esetoid__ring_2eRing__polynom_2enorm__subst___24a11(v12, v11, % 267.42/38.03 v10, v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2enorm__subst___24a11(v12, v11, v10, % 267.42/38.03 v9, v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 267.42/38.03 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] % 267.42/38.03 : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : (v1 % 267.42/38.03 = v0 | ~ (cCoq_2esetoid__ring_2eRing__polynom_2ePNSubstL___24a11(v12, v11, % 267.42/38.03 v10, v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePNSubstL___24a11(v12, v11, v10, v9, % 267.42/38.03 v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.03 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 267.42/38.03 ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2emk__monpol__list___24a10(v11, v10, % 267.42/38.03 v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2emk__monpol__list___24a10(v11, v10, % 267.42/38.03 v9, v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 267.42/38.03 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] % 267.42/38.03 : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__let__11__subst__l__14524___24a10(v11, v10, v9, v8, v7, v6, v5, v4, % 267.42/38.03 v3, v2) = v1) | ~ (c_24__let__11__subst__l__14524___24a10(v11, v10, v9, % 267.42/38.03 v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.03 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 267.42/38.03 ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2enorm__aux___24a9(v10, v9, v8, v7, v6, % 267.42/38.03 v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2enorm__aux___24a9(v10, v9, v8, v7, v6, % 267.42/38.03 v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 267.42/38.03 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | % 267.42/38.03 ~ (c_24__lam__59478___24a6(v7, v6, v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (c_24__lam__59478___24a6(v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] % 267.42/38.03 : (v1 = v0 | ~ (cCoq_2eZArith_2eZnumtheory_2eEuclid__intro___24a5(v6, v5, v4, % 267.42/38.03 v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eZnumtheory_2eEuclid__intro___24a5(v6, v5, v4, v3, v2) = % 267.42/38.03 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 267.42/38.03 : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eZdiv__rest__proofs__rect___24a5(v6, v5, v4, v3, % 267.42/38.03 v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eZdiv__rest__proofs__rect___24a5(v6, v5, v4, v3, % 267.42/38.03 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 267.42/38.03 [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eWf_2eAcc__rect___24a5(v6, v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eWf_2eAcc__rect___24a5(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 267.42/38.03 ! [v6: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eWf_2ewell__founded__induction__type___24a5(v6, v5, v4, v3, % 267.42/38.03 v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eWf_2ewell__founded__induction__type___24a5(v6, v5, v4, v3, % 267.42/38.03 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 267.42/38.03 [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (c_24__type__59565___24a4(v5, v4, v3, % 267.42/38.03 v2) = v1) | ~ (c_24__type__59565___24a4(v5, v4, v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 267.42/38.03 : (v1 = v0 | ~ (cCoq_2eClasses_2eMorphisms_2erespectful___24a4(v5, v4, v3, % 267.42/38.03 v2) = v1) | ~ (cCoq_2eClasses_2eMorphisms_2erespectful___24a4(v5, v4, % 267.42/38.03 v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 267.42/38.03 ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2emon__of__pol___24a4(v5, v4, v3, v2) = % 267.42/38.03 v1) | ~ (cCoq_2esetoid__ring_2eRing__polynom_2emon__of__pol___24a4(v5, % 267.42/38.03 v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 267.42/38.03 $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePeq___24a4(v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePeq___24a4(v5, v4, v3, v2) = v0)) & % 267.42/38.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 267.42/38.03 $i] : (v1 = v0 | ~ (cCoq_2esetoid__ring_2eRing__polynom_2ePX___24a4(v5, v4, % 267.42/38.03 v3, v2) = v1) | ~ (cCoq_2esetoid__ring_2eRing__polynom_2ePX___24a4(v5, % 267.42/38.03 v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 267.42/38.03 $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eZdiv__rest__proof___24a4(v5, v4, v3, v2) = v1) | % 267.42/38.03 ~ (cCoq_2eZArith_2eZpower_2eZdiv__rest__proof___24a4(v5, v4, v3, v2) = v0)) % 267.42/38.03 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 267.42/38.03 [v5: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2ePArith_2eBinPosDef_2ePos_2eiter__op___24a4(v5, v4, v3, v2) = v1) | % 267.42/38.03 ~ (cCoq_2ePArith_2eBinPosDef_2ePos_2eiter__op___24a4(v5, v4, v3, v2) = v0)) % 267.42/38.03 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 267.42/38.03 [v5: $i] : (v1 = v0 | ~ (cCoq_2ePArith_2eBinPosDef_2ePos_2eiter___24a4(v5, % 267.42/38.03 v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2ePArith_2eBinPosDef_2ePos_2eiter___24a4(v5, v4, v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 267.42/38.03 : (v1 = v0 | ~ (c_24__lam__59478___24a4(v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (c_24__lam__59478___24a4(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 267.42/38.03 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2enat__rect___24a4(v5, v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2enat__rect___24a4(v5, v4, v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 267.42/38.03 (v1 = v0 | ~ (cCoq_2eInit_2eDatatypes_2epair___24a4(v5, v4, v3, v2) = v1) | % 267.42/38.03 ~ (cCoq_2eInit_2eDatatypes_2epair___24a4(v5, v4, v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__type__59550___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (c_24__type__59550___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__type__18982___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (c_24__type__18982___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__type__18888___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (c_24__type__18888___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__type__59662___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (c_24__type__59662___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEsub___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEsub___24a3(v4, v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 267.42/38.03 ~ (cCoq_2esetoid__ring_2eRing__polynom_2ePEpow___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEpow___24a3(v4, v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 267.42/38.03 ~ (cCoq_2esetoid__ring_2eRing__polynom_2ePEmul___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEmul___24a3(v4, v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 267.42/38.03 ~ (cCoq_2esetoid__ring_2eRing__polynom_2ePEadd___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEadd___24a3(v4, v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 267.42/38.03 ~ (cCoq_2eInit_2eSpecif_2eexist___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2eexist___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2econs___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2econs___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePinj___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePinj___24a3(v4, v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 267.42/38.03 ~ (cCoq_2eInit_2eDatatypes_2enat__rect___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2enat__rect___24a3(v4, v3, v2) = v0)) & ! [v0: $i] % 267.42/38.03 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2ePArith_2eBinPosDef_2ePos_2eiter___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2ePArith_2eBinPosDef_2ePos_2eiter___24a3(v4, v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2efst___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2efst___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2esnd___24a3(v4, v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2esnd___24a3(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__case__Coq_2eNumbers_2eBinNums_2eZ_2432085___24a3(v4, v3, v2) = v1) | % 267.42/38.03 ~ (c_24__case__Coq_2eNumbers_2eBinNums_2eZ_2432085___24a3(v4, v3, v2) = v0)) % 267.42/38.03 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = % 267.42/38.03 v0 | ~ (c_24__case__Coq_2eInit_2eDatatypes_2enat_2432068___24a3(v4, v3, v2) % 267.42/38.03 = v1) | ~ (c_24__case__Coq_2eInit_2eDatatypes_2enat_2432068___24a3(v4, % 267.42/38.03 v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 267.42/38.03 (v1 = v0 | ~ (c_24__type__18997___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (c_24__type__18997___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 267.42/38.03 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__type__60515___24a2(v3, v2) = v1) % 267.42/38.03 | ~ (c_24__type__60515___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__type__60511___24a2(v3, v2) = % 267.42/38.03 v1) | ~ (c_24__type__60511___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.03 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__type__34421___24a2(v3, v2) = v1) | ~ (c_24__type__34421___24a2(v3, % 267.42/38.03 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 267.42/38.03 = v0 | ~ (c_24__type__59653___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (c_24__type__59653___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 267.42/38.03 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__type__14048___24a2(v3, v2) = v1) % 267.42/38.03 | ~ (c_24__type__14048___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__type__90___24a2(v3, v2) = v1) % 267.42/38.03 | ~ (c_24__type__90___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 267.42/38.03 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__type__18953___24a2(v3, v2) = v1) % 267.42/38.03 | ~ (c_24__type__18953___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__type__65103___24a2(v3, v2) = % 267.42/38.03 v1) | ~ (c_24__type__65103___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.03 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eZdiv__rest__proofs___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eZdiv__rest__proofs___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eZnumtheory_2eEuclid___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eZnumtheory_2eEuclid___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eReals_2eRfunctions_2eZ__spec___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eReals_2eRfunctions_2eZ__spec___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2esumbool___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2esumbool___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2esig___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2esig___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.03 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2emax___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2emax___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2emodulo___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2emodulo___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.03 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2epow___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2epow___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2ediv___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2ediv___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinInt_2eZ_2esetbit___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinInt_2eZ_2esetbit___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2elxor___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2elxor___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2elor___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2elor___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2eldiff___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2eldiff___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2eland___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2eland___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eZpower__nat___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eZpower__nat___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (c_24__lam__300___24a2(v3, v2) = v1) | ~ (c_24__lam__300___24a2(v3, v2) = % 267.42/38.03 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 267.42/38.03 ~ (c_24__lam__259___24a2(v3, v2) = v1) | ~ (c_24__lam__259___24a2(v3, v2) = % 267.42/38.03 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 267.42/38.03 ~ (c_24__prop__35229___24a2(v3, v2) = v1) | ~ (c_24__prop__35229___24a2(v3, % 267.42/38.03 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 267.42/38.03 = v0 | ~ (c_24__prop__19713___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (c_24__prop__19713___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 267.42/38.03 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__prop__13363___24a2(v3, v2) = v1) % 267.42/38.03 | ~ (c_24__prop__13363___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.03 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c_24__lam__18639___24a2(v3, v2) = % 267.42/38.03 v1) | ~ (c_24__lam__18639___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.03 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2evmon___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2evmon___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEopp___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEopp___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEc___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEc___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEX___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePEX___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eReals_2eRfunctions_2eZintNeg___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eReals_2eRfunctions_2eZintNeg___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ezmon___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ezmon___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eReals_2eRfunctions_2eZintPos___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eReals_2eRfunctions_2eZintPos___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2eleft___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2eleft___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.03 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2eright___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eSpecif_2eright___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.03 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2eprod___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2eprod___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2eSome___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eInit_2eDatatypes_2eSome___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePc___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2esetoid__ring_2eRing__polynom_2ePc___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eshift__pos___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eZpower_2eshift__pos___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eZbool_2eZeq__bool___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eZbool_2eZeq__bool___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.03 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinInt_2eZ_2eeq__dec___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinInt_2eZ_2eeq__dec___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2etestbit___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2etestbit___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.03 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2esub___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2esub___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2eshiftr___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2eshiftr___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.03 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2erem___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2erem___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2epos__div__eucl___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eNArith_2eBinNatDef_2eN_2epos__div__eucl___24a2(v3, v2) = v0)) & ! % 267.42/38.03 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2equotrem___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2equotrem___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.03 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2equot___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2equot___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.03 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow__pos___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow__pos___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.03 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2emodulo___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2emodulo___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.03 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2emin___24a2(v3, v2) = v1) | ~ % 267.42/38.03 (cCoq_2eZArith_2eBinIntDef_2eZ_2emin___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2emax___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2emax___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eltb___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eltb___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eleb___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eleb___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2egcd___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2egcd___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eeqb___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eeqb___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eeqb___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eeqb___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epos__sub___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epos__sub___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eshiftl___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eshiftl___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2egcd___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2egcd___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ediv___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ediv___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elcm___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elcm___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2egt___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2egt___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ecompare___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ecompare___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eReals_2eRpow__def_2epow___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eReals_2eRpow__def_2epow___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eRmult___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eRmult___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eQArith_2eQArith__base_2eQmake___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eQArith_2eQArith__base_2eQmake___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esub___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esub___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (c_24__fix__413__1__add__carry___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (c_24__fix__413__1__add__carry___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2etestbit___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2etestbit___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2etestbit___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2etestbit___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2esub___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2esub___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esub__mask___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esub__mask___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2emul___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2emul___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2emul___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2emul___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2emin___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2emin___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ecompare___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ecompare___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2eadd___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2eadd___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eadd___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eadd___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2ecompare___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2ecompare___24a2(v3, v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2esub___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2esub___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.04 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (cCoq_2eInit_2eNat_2emul___24a2(v3, % 267.42/38.04 v2) = v1) | ~ (cCoq_2eInit_2eNat_2emul___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2emax___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2emax___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.04 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2ecompare___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2ecompare___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2eadd___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eNat_2eadd___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.04 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2exorb___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2exorb___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2eorb___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2eorb___24a2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (happ(v3, v2) = v1) | ~ % 267.42/38.04 (happ(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 267.42/38.04 : (v1 = v0 | ~ (cCoq_2eInit_2eDatatypes_2eandb___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2eandb___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ediv__eucl___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ediv__eucl___24a2(v3, v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epos__div__eucl___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epos__div__eucl___24a2(v3, v2) = v0)) & ! % 267.42/38.04 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eadd___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eadd___24a2(v3, v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(v3, v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(v3, v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (c_24__type__14243___24a1(v2) = v1) | % 267.42/38.04 ~ (c_24__type__14243___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__97___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__97___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 267.42/38.04 : (v1 = v0 | ~ (c_24__type__59528___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__59528___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__13234___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__13234___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__59578___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__59578___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__13636___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__13636___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__13214___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__13214___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__16422___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__16422___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__68539___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__68539___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__68565___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__68565___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__13657___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__13657___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (c_24__type__14746___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__type__14746___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (cCoq_2eInit_2eDatatypes_2elist___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2elist___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2etestbit___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2etestbit___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (c_3d___24a1(v2) = v1) | ~ % 267.42/38.04 (c_3d___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 267.42/38.04 | ~ (c_24__lam__68508___24a1(v2) = v1) | ~ (c_24__lam__68508___24a1(v2) = % 267.42/38.04 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (c_24__prop__34426___24a1(v2) = v1) | ~ (c_24__prop__34426___24a1(v2) = % 267.42/38.04 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (c_24__prop__34425___24a1(v2) = v1) | ~ (c_24__prop__34425___24a1(v2) = % 267.42/38.04 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (c_24__lam__18637___24a1(v2) = v1) | ~ (c_24__lam__18637___24a1(v2) = v0)) % 267.42/38.04 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePEO___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePEO___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePEI___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePEI___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eReals_2eRfunctions_2eZintNull___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eReals_2eRfunctions_2eZintNull___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePExpr___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePExpr___24a1(v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePol___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2esetoid__ring_2eRing__polynom_2ePol___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2enil___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2enil___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 267.42/38.04 : ! [v2: $i] : (v1 = v0 | ~ (cCoq_2eInit_2eDatatypes_2eNone___24a1(v2) = v1) % 267.42/38.04 | ~ (cCoq_2eInit_2eDatatypes_2eNone___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eZpower_2etwo__p___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eZpower_2etwo__p___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ (c_24__lam__18639___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__lam__18639___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 267.42/38.04 $i] : (v1 = v0 | ~ (cCoq_2eZArith_2eZpower_2eZpower__nat___24a1(v2) = v1) | % 267.42/38.04 ~ (cCoq_2eZArith_2eZpower_2eZpower__nat___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eZpower_2etwo__power__pos___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eZpower_2etwo__power__pos___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eZArith__dec_2eZ__zerop___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eZArith__dec_2eZ__zerop___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eto__pos___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eto__pos___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eto__nat___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eto__nat___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eto__N___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eto__N___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esgn___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esgn___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow__pos___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epow__pos___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epred__double___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epred__double___24a1(v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esucc__double___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esucc__double___24a1(v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2edouble___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2edouble___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eof__nat___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eof__nat___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eof__N___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eof__N___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eodd___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eodd___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esize___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esize___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ediv2___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2ediv2___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ediv2__up___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ediv2__up___24a1(v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ediv2___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ediv2___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eabs__nat___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eabs__nat___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eabs__N___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eabs__N___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2esqrt__up___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2esqrt__up___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2eones___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2eones___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elog2__up___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elog2__up___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2elog2___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2elog2___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esucc___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esucc___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elnot___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2elnot___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eopp___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eopp___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epred___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2epred___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eabs___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2eabs___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2eb2z___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinInt_2eZ_2eb2z___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eRelations_2eRelation__Definitions_2erelation___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eRelations_2eRelation__Definitions_2erelation___24a1(v2) = v0)) & ! % 267.42/38.04 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (c_24__type__399___24a1(v2) = v1) | ~ (c_24__type__399___24a1(v2) = v0)) & % 267.42/38.04 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eIZR___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eIZR___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eRopp___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eRopp___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eIPR___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eReals_2eRdefinitions_2eIPR___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eQArith_2eQArith__base_2eQnum___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eQArith_2eQArith__base_2eQnum___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eQArith_2eQArith__base_2eQden___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eQArith_2eQArith__base_2eQden___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esqrtrem___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esqrtrem___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2epred__N___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2epred__N___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2epred__double___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2epred__double___24a1(v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ecompare__cont___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2ecompare__cont___24a1(v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2exI___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2exI___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 267.42/38.04 : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2eto__nat___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2eto__nat___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eto__nat___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eto__nat___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2esucc___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2esucc___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esucc___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esucc___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eIsPos___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eIsPos___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2eof__nat___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNArith_2eBinNatDef_2eN_2eof__nat___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2eNpos___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2eNpos___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ (cCoq_2eInit_2eDatatypes_2enegb___24a1(v2) % 267.42/38.04 = v1) | ~ (cCoq_2eInit_2eDatatypes_2enegb___24a1(v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2enat__rect___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2enat__rect___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2enat__rec___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2enat__rec___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2eCompOpp___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2eCompOpp___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ (c_24__let__2__s__19729___24a1(v2) = v1) | % 267.42/38.04 ~ (c_24__let__2__s__19729___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.04 ! [v2: $i] : (v1 = v0 | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2esqrt___24a1(v2) = % 267.42/38.04 v1) | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2esqrt___24a1(v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esqrt___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2esqrt___24a1(v2) = v0)) & ! [v0: $i] : ! % 267.42/38.04 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (c_24__let__1__s__19231___24a1(v2) = % 267.42/38.04 v1) | ~ (c_24__let__1__s__19231___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2eZneg___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2eZneg___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: % 267.42/38.04 $i] : ! [v2: $i] : (v1 = v0 | ~ (cCoq_2eNumbers_2eBinNums_2exO___24a1(v2) % 267.42/38.04 = v1) | ~ (cCoq_2eNumbers_2eBinNums_2exO___24a1(v2) = v0)) & ! [v0: $i] % 267.42/38.04 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esqrtrem___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eZArith_2eBinIntDef_2eZ_2esqrtrem___24a1(v2) = v0)) & ! [v0: $i] : % 267.42/38.04 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (c_24__case__Coq_2eInit_2eDatatypes_2enat_2432090___24a1(v2) = v1) | ~ % 267.42/38.04 (c_24__case__Coq_2eInit_2eDatatypes_2enat_2432090___24a1(v2) = v0)) & ! % 267.42/38.04 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2eS___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eInit_2eDatatypes_2eS___24a1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 267.42/38.04 ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eof__succ__nat___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2ePArith_2eBinPosDef_2ePos_2eof__succ__nat___24a1(v2) = v0)) & ! [v0: % 267.42/38.04 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2eZpos___24a1(v2) = v1) | ~ % 267.42/38.04 (cCoq_2eNumbers_2eBinNums_2eZpos___24a1(v2) = v0)) % 267.42/38.04 % 267.42/38.04 Further assumptions not needed in the proof: % 267.42/38.04 -------------------------------------------- % 267.42/38.05 $_case_Coq.Init.Datatypes.nat$32068, $_case_Coq.Init.Datatypes.nat$32090, % 267.42/38.05 $_case_Coq.Init.Datatypes.prod$16639, $_case_Coq.Init.Datatypes.prod$16654, % 267.42/38.05 $_case_Coq.Init.Datatypes.prod$964, $_case_Coq.Numbers.BinNums.Z$32085, % 267.42/38.05 $_def_$_let_11_subst_l_14524, $_def_$_let_1_s_19231, $_def_$_let_2_s_19729, % 267.42/38.05 $_def_Coq.Init.Datatypes.CompOpp, $_def_Coq.Init.Datatypes.andb, % 267.42/38.05 $_def_Coq.Init.Datatypes.nat_rec, $_def_Coq.Init.Datatypes.nat_rect, % 267.42/38.05 $_def_Coq.Init.Datatypes.negb, $_def_Coq.Init.Datatypes.orb, % 267.42/38.05 $_def_Coq.Init.Datatypes.snd, $_def_Coq.Init.Datatypes.xorb, % 267.42/38.05 $_def_Coq.Init.Nat.add, $_def_Coq.Init.Nat.compare, $_def_Coq.Init.Nat.max, % 267.42/38.05 $_def_Coq.Init.Nat.mul, $_def_Coq.Init.Nat.sub, $_def_Coq.Init.Peano.lt, % 267.42/38.05 $_def_Coq.Init.Wf.well_founded, $_def_Coq.Init.Wf.well_founded_induction_type, % 267.42/38.05 $_def_Coq.Logic.Decidable.decidable, $_def_Coq.NArith.BinNat.N.le, % 267.42/38.05 $_def_Coq.NArith.BinNat.N.lt, $_def_Coq.NArith.BinNatDef.N.add, % 267.42/38.05 $_def_Coq.NArith.BinNatDef.N.compare, $_def_Coq.NArith.BinNatDef.N.min, % 267.42/38.05 $_def_Coq.NArith.BinNatDef.N.mul, $_def_Coq.NArith.BinNatDef.N.of_nat, % 267.42/38.05 $_def_Coq.NArith.BinNatDef.N.sub, $_def_Coq.NArith.BinNatDef.N.succ, % 267.42/38.05 $_def_Coq.NArith.BinNatDef.N.testbit, $_def_Coq.NArith.BinNatDef.N.to_nat, % 267.42/38.05 $_def_Coq.PArith.BinPos.Pos.le, $_def_Coq.PArith.BinPos.Pos.lt, % 267.42/38.05 $_def_Coq.PArith.BinPosDef.Pos.add, $_def_Coq.PArith.BinPosDef.Pos.compare, % 267.42/38.05 $_def_Coq.PArith.BinPosDef.Pos.iter, $_def_Coq.PArith.BinPosDef.Pos.mul, % 267.42/38.05 $_def_Coq.PArith.BinPosDef.Pos.pred_N, % 267.42/38.05 $_def_Coq.PArith.BinPosDef.Pos.pred_double, $_def_Coq.PArith.BinPosDef.Pos.sqrt, % 267.42/38.05 $_def_Coq.PArith.BinPosDef.Pos.sub, $_def_Coq.PArith.BinPosDef.Pos.succ, % 267.42/38.05 $_def_Coq.PArith.BinPosDef.Pos.testbit, $_def_Coq.PArith.BinPosDef.Pos.to_nat, % 267.42/38.05 $_def_Coq.QArith.QArith_base.Qden, $_def_Coq.QArith.QArith_base.Qle, % 267.42/38.05 $_def_Coq.QArith.QArith_base.Qnum, $_def_Coq.Reals.Rdefinitions.IZR, % 267.42/38.05 $_def_Coq.Reals.Rdefinitions.Rle, $_def_Coq.Reals.Rpow_def.pow, % 267.42/38.05 $_def_Coq.Relations.Relation_Definitions.relation, % 267.42/38.05 $_def_Coq.ZArith.BinInt.Z.Odd, $_def_Coq.ZArith.BinInt.Z.b2z, % 267.42/38.05 $_def_Coq.ZArith.BinInt.Z.divide, $_def_Coq.ZArith.BinInt.Z.eqf, % 267.42/38.05 $_def_Coq.ZArith.BinInt.Z.ge, $_def_Coq.ZArith.BinInt.Z.gt, % 267.42/38.05 $_def_Coq.ZArith.BinInt.Z.lcm, $_def_Coq.ZArith.BinInt.Z.le, % 267.42/38.05 $_def_Coq.ZArith.BinInt.Z.lnot, $_def_Coq.ZArith.BinInt.Z.log2_up, % 267.42/38.05 $_def_Coq.ZArith.BinInt.Z.lt, $_def_Coq.ZArith.BinInt.Z.ones, % 267.42/38.05 $_def_Coq.ZArith.BinInt.Z.sqrt_up, $_def_Coq.ZArith.BinInt.Zne, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.abs, $_def_Coq.ZArith.BinIntDef.Z.abs_N, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.abs_nat, $_def_Coq.ZArith.BinIntDef.Z.add, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.compare, $_def_Coq.ZArith.BinIntDef.Z.div, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.div2, $_def_Coq.ZArith.BinIntDef.Z.eqb, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.gcd, $_def_Coq.ZArith.BinIntDef.Z.leb, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.log2, $_def_Coq.ZArith.BinIntDef.Z.ltb, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.max, $_def_Coq.ZArith.BinIntDef.Z.min, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.modulo, $_def_Coq.ZArith.BinIntDef.Z.mul, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.odd, $_def_Coq.ZArith.BinIntDef.Z.of_N, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.of_nat, $_def_Coq.ZArith.BinIntDef.Z.opp, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.pos_sub, $_def_Coq.ZArith.BinIntDef.Z.pow, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.pow_pos, $_def_Coq.ZArith.BinIntDef.Z.pred, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.quot, $_def_Coq.ZArith.BinIntDef.Z.quotrem, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.rem, $_def_Coq.ZArith.BinIntDef.Z.sgn, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.shiftl, $_def_Coq.ZArith.BinIntDef.Z.shiftr, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.sqrt, $_def_Coq.ZArith.BinIntDef.Z.sqrtrem, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.sub, $_def_Coq.ZArith.BinIntDef.Z.succ, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.testbit, $_def_Coq.ZArith.BinIntDef.Z.to_N, % 267.42/38.05 $_def_Coq.ZArith.BinIntDef.Z.to_nat, $_def_Coq.ZArith.BinIntDef.Z.to_pos, % 267.42/38.05 $_def_Coq.ZArith.ZArith_dec.Z_zerop, $_def_Coq.ZArith.Zbool.Zeq_bool, % 267.42/38.05 $_def_Coq.ZArith.Zdiv.Remainder, $_def_Coq.ZArith.Zeven.Zodd, % 267.42/38.05 $_def_Coq.ZArith.Znumtheory.rel_prime, % 267.42/38.05 $_def_Coq.ZArith.Zpower.Zdiv_rest_proofs_rect, % 267.42/38.05 $_def_Coq.ZArith.Zpower.Zpower_nat, $_def_Coq.ZArith.Zpower.two_p, % 267.42/38.05 $_def_Coq.ZArith.Zpower.two_power_pos, $_def_Coq.setoid_ring.Ring_polynom.Peq, % 267.42/38.05 $_def_Coq.setoid_ring.Ring_polynom.mk_monpol_list, % 267.42/38.05 $_def_Coq.setoid_ring.Ring_polynom.norm_subst, % 267.42/38.05 $_def_Coq.setoid_ring.Ring_tac.ring_subst_niter, % 267.42/38.05 $_discrim_Coq.Init.Datatypes.Eq$Coq.Init.Datatypes.Lt, % 267.42/38.05 $_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S, % 267.42/38.05 $_discrim_Coq.Init.Datatypes.nil$Coq.Init.Datatypes.cons, % 267.42/38.05 $_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false, % 267.42/38.05 $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right, % 267.42/38.05 $_discrim_Coq.Numbers.BinNums.N0$Coq.Numbers.BinNums.Npos, % 267.42/38.05 $_discrim_Coq.Numbers.BinNums.Z0$Coq.Numbers.BinNums.Zpos, % 267.42/38.05 $_discrim_Coq.Numbers.BinNums.xI$Coq.Numbers.BinNums.xO, % 267.42/38.05 $_discrim_Coq.PArith.BinPosDef.Pos.IsNul$Coq.PArith.BinPosDef.Pos.IsPos, % 267.42/38.05 $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos, % 267.42/38.05 $_discrim_Coq.Structures.OrdersTac.OEQ$Coq.Structures.OrdersTac.OLT, % 267.42/38.05 $_discrim_Coq.setoid_ring.Ring_polynom.PEO$Coq.setoid_ring.Ring_polynom.PEI, % 267.42/38.05 $_discrim_Coq.setoid_ring.Ring_polynom.Pc$Coq.setoid_ring.Ring_polynom.Pinj, % 267.42/38.05 $_discrim_Coq.setoid_ring.Ring_polynom.mon0$Coq.setoid_ring.Ring_polynom.zmon, % 267.42/38.05 $_fix_413_1_add_carry, $_inj_Coq.Init.Datatypes.S, % 267.42/38.05 $_inj_Coq.Init.Datatypes.cons, $_inj_Coq.Init.Datatypes.nil, % 267.42/38.05 $_inj_Coq.Init.Datatypes.pair, $_inj_Coq.Init.Specif.exist, % 267.42/38.05 $_inj_Coq.Init.Specif.left, $_inj_Coq.Init.Specif.right, % 267.42/38.05 $_inj_Coq.Numbers.BinNums.Npos, $_inj_Coq.Numbers.BinNums.Zneg, % 267.42/38.05 $_inj_Coq.Numbers.BinNums.Zpos, $_inj_Coq.Numbers.BinNums.xI, % 267.42/38.05 $_inj_Coq.Numbers.BinNums.xO, $_inj_Coq.PArith.BinPosDef.Pos.IsPos, % 267.42/38.05 $_inj_Coq.QArith.QArith_base.Qmake, $_inj_Coq.Reals.Rfunctions.ZintNeg, % 267.42/38.05 $_inj_Coq.Reals.Rfunctions.ZintNull, $_inj_Coq.Reals.Rfunctions.ZintPos, % 267.42/38.05 $_inj_Coq.ZArith.Znumtheory.Euclid_intro, % 267.42/38.05 $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof, $_inj_Coq.setoid_ring.Ring_polynom.PEI, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.PEO, $_inj_Coq.setoid_ring.Ring_polynom.PEX, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.PEadd, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.PEc, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.PEmul, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.PEopp, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.PEpow, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.PEsub, $_inj_Coq.setoid_ring.Ring_polynom.PX, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.Pc, $_inj_Coq.setoid_ring.Ring_polynom.Pinj, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.vmon, % 267.42/38.05 $_inj_Coq.setoid_ring.Ring_polynom.zmon, % 267.42/38.05 $_inversion_Coq.Init.Datatypes.BoolSpec, % 267.42/38.05 $_inversion_Coq.Init.Datatypes.CompareSpec, $_inversion_Coq.Init.Datatypes.bool, % 267.42/38.05 $_inversion_Coq.Init.Datatypes.comparison, $_inversion_Coq.Init.Datatypes.list, % 267.42/38.05 $_inversion_Coq.Init.Datatypes.nat, $_inversion_Coq.Init.Datatypes.prod, % 267.42/38.05 $_inversion_Coq.Init.Datatypes.unit, $_inversion_Coq.Init.Peano.le, % 267.42/38.05 $_inversion_Coq.Init.Specif.sig, $_inversion_Coq.Init.Specif.sumbool, % 267.42/38.05 $_inversion_Coq.Numbers.BinNums.N, $_inversion_Coq.Numbers.BinNums.Z, % 267.42/38.05 $_inversion_Coq.Numbers.BinNums.positive, % 267.42/38.05 $_inversion_Coq.PArith.BinPos.Pos.SqrtSpec, % 267.42/38.05 $_inversion_Coq.PArith.BinPosDef.Pos.mask, $_inversion_Coq.QArith.QArith_base.Q, % 267.42/38.05 $_inversion_Coq.Reals.Rfunctions.Z_spec, % 267.42/38.05 $_inversion_Coq.Structures.OrdersTac.ord, % 267.42/38.05 $_inversion_Coq.ZArith.Znumtheory.Bezout, % 267.42/38.05 $_inversion_Coq.ZArith.Znumtheory.Euclid, % 267.42/38.05 $_inversion_Coq.ZArith.Znumtheory.Zis_gcd, % 267.42/38.05 $_inversion_Coq.ZArith.Znumtheory.prime, % 267.42/38.05 $_inversion_Coq.ZArith.Zpower.Zdiv_rest_proofs, % 267.42/38.05 $_inversion_Coq.setoid_ring.Ring_polynom.Mon, % 267.42/38.05 $_inversion_Coq.setoid_ring.Ring_polynom.PExpr, % 267.42/38.05 $_inversion_Coq.setoid_ring.Ring_polynom.Pol, $_lam_14596, $_lam_18637, % 267.42/38.05 $_lam_18639, $_lam_259, $_lam_300, $_lam_59478, $_lam_68508, $_prop_13363, % 267.42/38.05 $_prop_19713, $_prop_34425, $_prop_34426, $_prop_35229, $_type_117, $_type_12, % 267.42/38.05 $_type_13186, $_type_13189, $_type_13192, $_type_13209, $_type_13214, % 267.42/38.05 $_type_13227, $_type_13229, $_type_13234, $_type_13315, $_type_13335, % 267.42/38.05 $_type_13340, $_type_13342, $_type_13361, $_type_13636, $_type_13657, % 267.42/38.05 $_type_13849, $_type_13869, $_type_13871, $_type_13874, $_type_13885, % 267.42/38.05 $_type_14048, $_type_14243, $_type_14254, $_type_14503, $_type_14506, % 267.42/38.05 $_type_14511, $_type_14728, $_type_14746, $_type_14906, $_type_16386, % 267.42/38.05 $_type_16391, $_type_16412, $_type_16414, $_type_16422, $_type_16816, % 267.42/38.05 $_type_16853, $_type_18641, $_type_18835, $_type_18872, $_type_18888, % 267.42/38.05 $_type_18949, $_type_18953, $_type_18982, $_type_18997, $_type_19090, % 267.42/38.05 $_type_19157, $_type_19160, $_type_19197, $_type_19204, $_type_19220, % 267.42/38.05 $_type_19222, $_type_19295, $_type_19298, $_type_19307, $_type_19311, % 267.42/38.05 $_type_19318, $_type_19321, $_type_19325, $_type_19459, $_type_19818, % 267.42/38.05 $_type_19822, $_type_21994, $_type_22003, $_type_22008, $_type_22011, % 267.42/38.05 $_type_245, $_type_25, $_type_286, $_type_30, $_type_31256, $_type_31347, % 267.42/38.05 $_type_31442, $_type_323, $_type_34421, $_type_34423, $_type_35232, $_type_376, % 267.42/38.05 $_type_392, $_type_399, $_type_401, $_type_410, $_type_443, $_type_45, % 267.42/38.05 $_type_471, $_type_515, $_type_525, $_type_57851, $_type_59295, $_type_59418, % 267.42/38.05 $_type_59522, $_type_59528, $_type_59550, $_type_59565, $_type_59575, % 267.42/38.05 $_type_59578, $_type_59635, $_type_59653, $_type_59662, $_type_60221, % 267.42/38.05 $_type_60500, $_type_60503, $_type_60511, $_type_60515, $_type_61, $_type_65103, % 267.42/38.05 $_type_68505, $_type_68531, $_type_68539, $_type_68555, $_type_68565, $_type_74, % 267.42/38.05 $_type_90, $_type_94, $_type_956, $_type_97, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.CompOpp, $_typeof_Coq.Init.Datatypes.Eq, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.Gt, $_typeof_Coq.Init.Datatypes.Lt, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.O, $_typeof_Coq.Init.Datatypes.S, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.andb, $_typeof_Coq.Init.Datatypes.bool, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.comparison, $_typeof_Coq.Init.Datatypes.cons, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.false, $_typeof_Coq.Init.Datatypes.list, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.nat, $_typeof_Coq.Init.Datatypes.nat_rec, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.nat_rect, $_typeof_Coq.Init.Datatypes.negb, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.nil, $_typeof_Coq.Init.Datatypes.orb, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.pair, $_typeof_Coq.Init.Datatypes.prod, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.snd, $_typeof_Coq.Init.Datatypes.true, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.tt, $_typeof_Coq.Init.Datatypes.unit, % 267.42/38.05 $_typeof_Coq.Init.Datatypes.xorb, $_typeof_Coq.Init.Nat.add, % 267.42/38.05 $_typeof_Coq.Init.Nat.compare, $_typeof_Coq.Init.Nat.max, % 267.42/38.05 $_typeof_Coq.Init.Nat.mul, $_typeof_Coq.Init.Nat.sub, % 267.42/38.05 $_typeof_Coq.Init.Peano.lt, $_typeof_Coq.Init.Specif.exist, % 267.42/38.05 $_typeof_Coq.Init.Specif.left, $_typeof_Coq.Init.Specif.right, % 267.42/38.05 $_typeof_Coq.Init.Specif.sig, $_typeof_Coq.Init.Specif.sumbool, % 267.42/38.05 $_typeof_Coq.Init.Wf.well_founded, % 267.42/38.05 $_typeof_Coq.Init.Wf.well_founded_induction_type, % 267.42/38.05 $_typeof_Coq.Logic.Decidable.decidable, $_typeof_Coq.NArith.BinNat.N.le, % 267.42/38.05 $_typeof_Coq.NArith.BinNat.N.lt, $_typeof_Coq.NArith.BinNatDef.N.add, % 267.42/38.05 $_typeof_Coq.NArith.BinNatDef.N.compare, $_typeof_Coq.NArith.BinNatDef.N.min, % 267.42/38.05 $_typeof_Coq.NArith.BinNatDef.N.mul, $_typeof_Coq.NArith.BinNatDef.N.of_nat, % 267.42/38.05 $_typeof_Coq.NArith.BinNatDef.N.sub, $_typeof_Coq.NArith.BinNatDef.N.succ, % 267.42/38.05 $_typeof_Coq.NArith.BinNatDef.N.testbit, $_typeof_Coq.NArith.BinNatDef.N.to_nat, % 267.42/38.05 $_typeof_Coq.Numbers.BinNums.N, $_typeof_Coq.Numbers.BinNums.N0, % 267.42/38.05 $_typeof_Coq.Numbers.BinNums.Npos, $_typeof_Coq.Numbers.BinNums.Z, % 267.42/38.05 $_typeof_Coq.Numbers.BinNums.Z0, $_typeof_Coq.Numbers.BinNums.Zneg, % 267.42/38.05 $_typeof_Coq.Numbers.BinNums.Zpos, $_typeof_Coq.Numbers.BinNums.positive, % 267.42/38.05 $_typeof_Coq.Numbers.BinNums.xH, $_typeof_Coq.Numbers.BinNums.xI, % 267.42/38.05 $_typeof_Coq.Numbers.BinNums.xO, $_typeof_Coq.PArith.BinPos.Pos.le, % 267.42/38.05 $_typeof_Coq.PArith.BinPos.Pos.lt, $_typeof_Coq.PArith.BinPosDef.Pos.add, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.compare, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.iter, $_typeof_Coq.PArith.BinPosDef.Pos.mask, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.mul, $_typeof_Coq.PArith.BinPosDef.Pos.pred_N, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.pred_double, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.sqrt, $_typeof_Coq.PArith.BinPosDef.Pos.sub, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.succ, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.testbit, % 267.42/38.05 $_typeof_Coq.PArith.BinPosDef.Pos.to_nat, $_typeof_Coq.QArith.QArith_base.Q, % 267.42/38.05 $_typeof_Coq.QArith.QArith_base.Qden, $_typeof_Coq.QArith.QArith_base.Qle, % 267.42/38.05 $_typeof_Coq.QArith.QArith_base.Qnum, $_typeof_Coq.Reals.Rdefinitions.IZR, % 267.42/38.05 $_typeof_Coq.Reals.Rdefinitions.R, $_typeof_Coq.Reals.Rdefinitions.Rinv, % 267.42/38.05 $_typeof_Coq.Reals.Rdefinitions.Rle, $_typeof_Coq.Reals.Rdefinitions.Rlt, % 267.42/38.05 $_typeof_Coq.Reals.Rdefinitions.Rmult, $_typeof_Coq.Reals.Rfunctions.Z_spec, % 267.42/38.05 $_typeof_Coq.Reals.RiemannInt_SF.IZN_var, $_typeof_Coq.Reals.Rpow_def.pow, % 267.42/38.05 $_typeof_Coq.Relations.Relation_Definitions.relation, % 267.42/38.05 $_typeof_Coq.Structures.OrdersTac.ord, $_typeof_Coq.ZArith.BinInt.Z.Odd, % 267.42/38.05 $_typeof_Coq.ZArith.BinInt.Z.b2z, $_typeof_Coq.ZArith.BinInt.Z.divide, % 267.42/38.05 $_typeof_Coq.ZArith.BinInt.Z.eqf, $_typeof_Coq.ZArith.BinInt.Z.ge, % 267.42/38.05 $_typeof_Coq.ZArith.BinInt.Z.gt, $_typeof_Coq.ZArith.BinInt.Z.lcm, % 267.42/38.05 $_typeof_Coq.ZArith.BinInt.Z.le, $_typeof_Coq.ZArith.BinInt.Z.lnot, % 267.42/38.05 $_typeof_Coq.ZArith.BinInt.Z.log2_up, $_typeof_Coq.ZArith.BinInt.Z.lt, % 267.42/38.05 $_typeof_Coq.ZArith.BinInt.Z.ones, $_typeof_Coq.ZArith.BinInt.Z.sqrt_up, % 267.42/38.05 $_typeof_Coq.ZArith.BinInt.Zne, $_typeof_Coq.ZArith.BinIntDef.Z.abs, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.abs_N, $_typeof_Coq.ZArith.BinIntDef.Z.abs_nat, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.add, $_typeof_Coq.ZArith.BinIntDef.Z.compare, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.div, $_typeof_Coq.ZArith.BinIntDef.Z.div2, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.eqb, $_typeof_Coq.ZArith.BinIntDef.Z.gcd, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.leb, $_typeof_Coq.ZArith.BinIntDef.Z.log2, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.ltb, $_typeof_Coq.ZArith.BinIntDef.Z.max, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.min, $_typeof_Coq.ZArith.BinIntDef.Z.modulo, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.mul, $_typeof_Coq.ZArith.BinIntDef.Z.odd, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.of_N, $_typeof_Coq.ZArith.BinIntDef.Z.of_nat, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.opp, $_typeof_Coq.ZArith.BinIntDef.Z.pos_sub, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.pow, $_typeof_Coq.ZArith.BinIntDef.Z.pow_pos, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.pred, $_typeof_Coq.ZArith.BinIntDef.Z.quot, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.quotrem, $_typeof_Coq.ZArith.BinIntDef.Z.rem, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.sgn, $_typeof_Coq.ZArith.BinIntDef.Z.shiftl, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.shiftr, $_typeof_Coq.ZArith.BinIntDef.Z.sqrt, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.sqrtrem, $_typeof_Coq.ZArith.BinIntDef.Z.sub, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.succ, $_typeof_Coq.ZArith.BinIntDef.Z.testbit, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.to_N, $_typeof_Coq.ZArith.BinIntDef.Z.to_nat, % 267.42/38.05 $_typeof_Coq.ZArith.BinIntDef.Z.to_pos, $_typeof_Coq.ZArith.Wf_Z.Z_lt_rec, % 267.42/38.05 $_typeof_Coq.ZArith.Wf_Z.Z_of_nat_complete_inf, % 267.42/38.05 $_typeof_Coq.ZArith.Wf_Z.Z_of_nat_set, % 267.42/38.05 $_typeof_Coq.ZArith.Wf_Z.Zlt_lower_bound_rec, % 267.42/38.05 $_typeof_Coq.ZArith.Wf_Z.natlike_rec, $_typeof_Coq.ZArith.Wf_Z.natlike_rec2, % 267.42/38.05 $_typeof_Coq.ZArith.Wf_Z.natlike_rec3, $_typeof_Coq.ZArith.ZArith_dec.Z_zerop, % 267.42/38.05 $_typeof_Coq.ZArith.Zbool.Zeq_bool, $_typeof_Coq.ZArith.Zdiv.Remainder, % 267.42/38.05 $_typeof_Coq.ZArith.Zdiv.Zdiv_eucl_exist, % 267.42/38.05 $_typeof_Coq.ZArith.Zdiv.Zdiv_eucl_extended, $_typeof_Coq.ZArith.Zeven.Zodd, % 267.42/38.05 $_typeof_Coq.ZArith.Zmin.Zmin_le_prime_inf, % 267.42/38.05 $_typeof_Coq.ZArith.Znumtheory.Euclid, % 267.42/38.05 $_typeof_Coq.ZArith.Znumtheory.Euclid_intro, % 267.42/38.05 $_typeof_Coq.ZArith.Znumtheory.euclid_rec, % 267.42/38.05 $_typeof_Coq.ZArith.Znumtheory.rel_prime, % 267.42/38.05 $_typeof_Coq.ZArith.Zpower.Zdiv_rest_proof, % 267.42/38.05 $_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs, % 267.42/38.05 $_typeof_Coq.ZArith.Zpower.Zdiv_rest_proofs_rect, % 267.42/38.05 $_typeof_Coq.ZArith.Zpower.Zpower_nat, $_typeof_Coq.ZArith.Zpower.two_p, % 267.42/38.05 $_typeof_Coq.ZArith.Zpower.two_power_pos, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.Mon, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.PEX, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.PEadd, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.PEc, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.PEmul, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.PEsub, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.PExpr, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.Peq, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.Pol, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.mk_monpol_list, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_polynom.norm_subst, % 267.42/38.05 $_typeof_Coq.setoid_ring.Ring_tac.ring_subst_niter, % 267.42/38.05 $adef_$_case_Coq.Init.Datatypes.nat$32068_$a3, % 267.42/38.05 $adef_$_case_Coq.Init.Datatypes.nat$32090_$a1, % 267.42/38.05 $adef_$_case_Coq.Init.Datatypes.prod$16639_$a2, % 267.42/38.05 $adef_$_case_Coq.Init.Datatypes.prod$16654_$a2, % 267.42/38.05 $adef_$_case_Coq.Init.Datatypes.prod$964_$a1, % 267.42/38.05 $adef_$_case_Coq.Numbers.BinNums.Z$32085_$a3, $adef_$_fix_413_1_add_carry_$a2, % 267.42/38.05 $adef_$_lam_14596_$a11, $adef_$_lam_14596_$a12, $adef_$_lam_18637_$a1, % 267.42/38.05 $adef_$_lam_18639_$a1, $adef_$_lam_18639_$a2, $adef_$_lam_259_$a2, % 267.42/38.05 $adef_$_lam_259_$a3, $adef_$_lam_300_$a2, $adef_$_lam_300_$a3, % 267.42/38.05 $adef_$_lam_59478_$a4, $adef_$_lam_59478_$a6, $adef_$_lam_68508_$a1, % 267.42/38.05 $adef_$_lam_68508_$a2, $adef_$_let_11_subst_l_14524_$a10, % 267.42/38.05 $adef_$_let_1_s_19231_$a1, $adef_$_let_2_s_19729_$a1, $adef_$_prop_13363_$a2, % 267.42/38.05 $adef_$_prop_19713_$a2, $adef_$_prop_34425_$a1, $adef_$_prop_34426_$a1, % 267.42/38.05 $adef_$_prop_35229_$a2, $adef_Coq.Classes.Morphisms.Proper_$a3, % 267.42/38.05 $adef_Coq.Classes.Morphisms.respectful_$a4, % 267.42/38.05 $adef_Coq.Classes.RelationClasses.Equivalence_$a2, % 267.42/38.05 $adef_Coq.Classes.RelationClasses.PreOrder_$a2, % 267.42/38.05 $adef_Coq.Classes.RelationClasses.Symmetric_$a2, % 267.42/38.05 $adef_Coq.Init.Datatypes.BoolSpec_$a3, $adef_Coq.Init.Datatypes.CompOpp_$a1, % 267.42/38.05 $adef_Coq.Init.Datatypes.CompareSpec_$a4, $adef_Coq.Init.Datatypes.None_$a1, % 267.42/38.05 $adef_Coq.Init.Datatypes.S_$a1, $adef_Coq.Init.Datatypes.Some_$a2, % 267.42/38.05 $adef_Coq.Init.Datatypes.andb_$a2, $adef_Coq.Init.Datatypes.cons_$a3, % 267.42/38.05 $adef_Coq.Init.Datatypes.fst_$a3, $adef_Coq.Init.Datatypes.list_$a1, % 267.42/38.05 $adef_Coq.Init.Datatypes.nat_rec_$a1, $adef_Coq.Init.Datatypes.nat_rect_$a1, % 267.42/38.05 $adef_Coq.Init.Datatypes.nat_rect_$a3, $adef_Coq.Init.Datatypes.nat_rect_$a4, % 267.42/38.05 $adef_Coq.Init.Datatypes.negb_$a1, $adef_Coq.Init.Datatypes.nil_$a1, % 267.42/38.05 $adef_Coq.Init.Datatypes.orb_$a2, $adef_Coq.Init.Datatypes.pair_$a4, % 267.42/38.05 $adef_Coq.Init.Datatypes.prod_$a2, $adef_Coq.Init.Datatypes.snd_$a3, % 267.42/38.05 $adef_Coq.Init.Datatypes.xorb_$a2, $adef_Coq.Init.Nat.add_$a2, % 267.42/38.05 $adef_Coq.Init.Nat.compare_$a2, $adef_Coq.Init.Nat.max_$a2, % 267.42/38.05 $adef_Coq.Init.Nat.mul_$a2, $adef_Coq.Init.Nat.sub_$a2, % 267.42/38.05 $adef_Coq.Init.Peano.le_$a2, $adef_Coq.Init.Peano.lt_$a2, % 267.42/38.05 $adef_Coq.Init.Specif.exist_$a3, $adef_Coq.Init.Specif.left_$a2, % 267.42/38.05 $adef_Coq.Init.Specif.right_$a2, $adef_Coq.Init.Specif.sig_$a2, % 267.42/38.05 $adef_Coq.Init.Specif.sumbool_$a2, $adef_Coq.Init.Wf.Acc_$a3, % 267.42/38.05 $adef_Coq.Init.Wf.Acc_rect_$a5, $adef_Coq.Init.Wf.well_founded_$a2, % 267.42/38.05 $adef_Coq.Init.Wf.well_founded_induction_type_$a5, % 267.42/38.05 $adef_Coq.Logic.Decidable.decidable_$a1, $adef_Coq.NArith.BinNat.N.le_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNat.N.lt_$a2, $adef_Coq.NArith.BinNatDef.N.add_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.compare_$a2, $adef_Coq.NArith.BinNatDef.N.div_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.max_$a2, $adef_Coq.NArith.BinNatDef.N.min_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.modulo_$a2, $adef_Coq.NArith.BinNatDef.N.mul_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.of_nat_$a1, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.pos_div_eucl_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.pow_$a2, $adef_Coq.NArith.BinNatDef.N.sub_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.succ_$a1, $adef_Coq.NArith.BinNatDef.N.testbit_$a2, % 267.42/38.05 $adef_Coq.NArith.BinNatDef.N.to_nat_$a1, $adef_Coq.Numbers.BinNums.Npos_$a1, % 267.42/38.05 $adef_Coq.Numbers.BinNums.Zneg_$a1, $adef_Coq.Numbers.BinNums.Zpos_$a1, % 267.42/38.05 $adef_Coq.Numbers.BinNums.xI_$a1, $adef_Coq.Numbers.BinNums.xO_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPos.Pos.SqrtSpec_$a2, $adef_Coq.PArith.BinPos.Pos.le_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPos.Pos.lt_$a2, $adef_Coq.PArith.BinPosDef.Pos.IsPos_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.add_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.compare_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.compare_cont_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.div2_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.div2_up_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.eqb_$a2, $adef_Coq.PArith.BinPosDef.Pos.gcd_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.iter_$a3, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.iter_$a4, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.iter_op_$a4, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.mul_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.of_succ_nat_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.pred_N_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.pred_double_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.size_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.sqrt_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.sqrtrem_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.sub_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.sub_mask_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.succ_$a1, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.testbit_$a2, % 267.42/38.05 $adef_Coq.PArith.BinPosDef.Pos.to_nat_$a1, % 267.42/38.05 $adef_Coq.QArith.QArith_base.Qden_$a1, $adef_Coq.QArith.QArith_base.Qle_$a2, % 267.42/38.05 $adef_Coq.QArith.QArith_base.Qmake_$a2, $adef_Coq.QArith.QArith_base.Qnum_$a1, % 267.42/38.05 $adef_Coq.Reals.Rdefinitions.IPR_$a1, $adef_Coq.Reals.Rdefinitions.IZR_$a1, % 267.42/38.05 $adef_Coq.Reals.Rdefinitions.Rle_$a2, $adef_Coq.Reals.Rdefinitions.Rlt_$a2, % 267.42/38.05 $adef_Coq.Reals.Rdefinitions.Rmult_$a2, $adef_Coq.Reals.Rdefinitions.Ropp_$a1, % 267.42/38.05 $adef_Coq.Reals.Rfunctions.Z_spec_$a2, $adef_Coq.Reals.Rfunctions.ZintNeg_$a2, % 267.42/38.05 $adef_Coq.Reals.Rfunctions.ZintNull_$a1, $adef_Coq.Reals.Rfunctions.ZintPos_$a2, % 267.42/38.05 $adef_Coq.Reals.Rpow_def.pow_$a2, % 267.42/38.05 $adef_Coq.Relations.Relation_Definitions.relation_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.Odd_$a1, $adef_Coq.ZArith.BinInt.Z.b2z_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.divide_$a2, $adef_Coq.ZArith.BinInt.Z.eq_dec_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.eqf_$a2, $adef_Coq.ZArith.BinInt.Z.ge_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.gt_$a2, $adef_Coq.ZArith.BinInt.Z.lcm_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.le_$a2, $adef_Coq.ZArith.BinInt.Z.lnot_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.log2_up_$a1, $adef_Coq.ZArith.BinInt.Z.lt_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.ones_$a1, $adef_Coq.ZArith.BinInt.Z.setbit_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinInt.Z.sqrt_up_$a1, $adef_Coq.ZArith.BinInt.Zne_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.abs_$a1, $adef_Coq.ZArith.BinIntDef.Z.abs_N_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.abs_nat_$a1, $adef_Coq.ZArith.BinIntDef.Z.add_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.compare_$a2, $adef_Coq.ZArith.BinIntDef.Z.div2_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.div_$a2, $adef_Coq.ZArith.BinIntDef.Z.div_eucl_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.double_$a1, $adef_Coq.ZArith.BinIntDef.Z.eqb_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.gcd_$a2, $adef_Coq.ZArith.BinIntDef.Z.land_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.ldiff_$a2, $adef_Coq.ZArith.BinIntDef.Z.leb_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.log2_$a1, $adef_Coq.ZArith.BinIntDef.Z.lor_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.ltb_$a2, $adef_Coq.ZArith.BinIntDef.Z.lxor_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.max_$a2, $adef_Coq.ZArith.BinIntDef.Z.min_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.modulo_$a2, $adef_Coq.ZArith.BinIntDef.Z.mul_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.mul_$a2, $adef_Coq.ZArith.BinIntDef.Z.odd_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.of_N_$a1, $adef_Coq.ZArith.BinIntDef.Z.of_nat_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.opp_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.pos_div_eucl_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.pos_sub_$a2, $adef_Coq.ZArith.BinIntDef.Z.pow_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.pow_pos_$a2, $adef_Coq.ZArith.BinIntDef.Z.pred_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.pred_double_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.quot_$a2, $adef_Coq.ZArith.BinIntDef.Z.quotrem_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.rem_$a2, $adef_Coq.ZArith.BinIntDef.Z.sgn_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.shiftl_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.shiftr_$a2, $adef_Coq.ZArith.BinIntDef.Z.sqrt_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.sqrtrem_$a1, $adef_Coq.ZArith.BinIntDef.Z.sub_$a2, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.succ_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.succ_double_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.testbit_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.testbit_$a2, $adef_Coq.ZArith.BinIntDef.Z.to_N_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.to_nat_$a1, % 267.42/38.05 $adef_Coq.ZArith.BinIntDef.Z.to_pos_$a1, % 267.42/38.05 $adef_Coq.ZArith.ZArith_dec.Z_zerop_$a1, $adef_Coq.ZArith.Zbool.Zeq_bool_$a2, % 267.42/38.05 $adef_Coq.ZArith.Zdiv.Remainder_$a2, $adef_Coq.ZArith.Zeven.Zodd_$a1, % 267.42/38.05 $adef_Coq.ZArith.Znumtheory.Bezout_$a3, $adef_Coq.ZArith.Znumtheory.Euclid_$a2, % 267.42/38.05 $adef_Coq.ZArith.Znumtheory.Euclid_intro_$a5, % 267.42/38.05 $adef_Coq.ZArith.Znumtheory.Zis_gcd_$a3, $adef_Coq.ZArith.Znumtheory.prime_$a1, % 267.42/38.05 $adef_Coq.ZArith.Znumtheory.rel_prime_$a2, % 267.42/38.05 $adef_Coq.ZArith.Zpower.Zdiv_rest_proof_$a4, % 267.42/38.05 $adef_Coq.ZArith.Zpower.Zdiv_rest_proofs_$a2, % 267.42/38.05 $adef_Coq.ZArith.Zpower.Zdiv_rest_proofs_rect_$a5, % 267.42/38.05 $adef_Coq.ZArith.Zpower.Zpower_nat_$a1, $adef_Coq.ZArith.Zpower.Zpower_nat_$a2, % 267.42/38.05 $adef_Coq.ZArith.Zpower.shift_pos_$a2, $adef_Coq.ZArith.Zpower.two_p_$a1, % 267.42/38.05 $adef_Coq.ZArith.Zpower.two_power_pos_$a1, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEI_$a1, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEO_$a1, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEX_$a2, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEadd_$a3, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEc_$a2, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEmul_$a3, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEopp_$a2, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEpow_$a3, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PEsub_$a3, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PExpr_$a1, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PNSubstL_$a11, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.PX_$a4, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.Pc_$a2, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.Peq_$a4, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.Pinj_$a3, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.Pol_$a1, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.mk_monpol_list_$a10, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.mon_of_pol_$a4, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.norm_aux_$a9, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a11, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.norm_subst_$a12, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.vmon_$a2, % 267.42/38.05 $adef_Coq.setoid_ring.Ring_polynom.zmon_$a2, $tdef_$_type_117, $tdef_$_type_12, % 267.42/38.05 $tdef_$_type_13186, $tdef_$_type_13189, $tdef_$_type_13192, $tdef_$_type_13209, % 267.42/38.05 $tdef_$_type_13214, $tdef_$_type_13227, $tdef_$_type_13229, $tdef_$_type_13234, % 267.42/38.05 $tdef_$_type_13315, $tdef_$_type_13335, $tdef_$_type_13340, $tdef_$_type_13342, % 267.42/38.05 $tdef_$_type_13361, $tdef_$_type_13636, $tdef_$_type_13657, $tdef_$_type_13849, % 267.42/38.05 $tdef_$_type_13869, $tdef_$_type_13871, $tdef_$_type_13874, $tdef_$_type_13885, % 267.42/38.05 $tdef_$_type_14048, $tdef_$_type_14243, $tdef_$_type_14254, $tdef_$_type_14503, % 267.42/38.05 $tdef_$_type_14506, $tdef_$_type_14511, $tdef_$_type_14728, $tdef_$_type_14746, % 267.42/38.05 $tdef_$_type_14906, $tdef_$_type_16386, $tdef_$_type_16391, $tdef_$_type_16412, % 267.42/38.05 $tdef_$_type_16414, $tdef_$_type_16422, $tdef_$_type_16816, $tdef_$_type_16853, % 267.42/38.05 $tdef_$_type_18641, $tdef_$_type_18835, $tdef_$_type_18872, $tdef_$_type_18888, % 267.42/38.05 $tdef_$_type_18949, $tdef_$_type_18953, $tdef_$_type_18982, $tdef_$_type_18997, % 267.42/38.05 $tdef_$_type_19090, $tdef_$_type_19157, $tdef_$_type_19160, $tdef_$_type_19197, % 267.42/38.05 $tdef_$_type_19204, $tdef_$_type_19220, $tdef_$_type_19222, $tdef_$_type_19295, % 267.42/38.05 $tdef_$_type_19298, $tdef_$_type_19307, $tdef_$_type_19311, $tdef_$_type_19318, % 267.42/38.05 $tdef_$_type_19321, $tdef_$_type_19325, $tdef_$_type_19459, $tdef_$_type_19818, % 267.42/38.05 $tdef_$_type_19822, $tdef_$_type_21994, $tdef_$_type_22003, $tdef_$_type_22008, % 267.42/38.05 $tdef_$_type_22011, $tdef_$_type_245, $tdef_$_type_25, $tdef_$_type_286, % 267.42/38.05 $tdef_$_type_30, $tdef_$_type_31256, $tdef_$_type_31347, $tdef_$_type_31442, % 267.42/38.05 $tdef_$_type_323, $tdef_$_type_34421, $tdef_$_type_34423, $tdef_$_type_35232, % 267.42/38.05 $tdef_$_type_376, $tdef_$_type_392, $tdef_$_type_399, $tdef_$_type_401, % 267.42/38.05 $tdef_$_type_410, $tdef_$_type_443, $tdef_$_type_45, $tdef_$_type_471, % 267.42/38.05 $tdef_$_type_515, $tdef_$_type_525, $tdef_$_type_57851, $tdef_$_type_59295, % 267.42/38.05 $tdef_$_type_59418, $tdef_$_type_59522, $tdef_$_type_59528, $tdef_$_type_59550, % 267.42/38.05 $tdef_$_type_59565, $tdef_$_type_59575, $tdef_$_type_59578, $tdef_$_type_59635, % 267.42/38.05 $tdef_$_type_59653, $tdef_$_type_59662, $tdef_$_type_60221, $tdef_$_type_60500, % 267.42/38.05 $tdef_$_type_60503, $tdef_$_type_60511, $tdef_$_type_60515, $tdef_$_type_61, % 267.42/38.05 $tdef_$_type_65103, $tdef_$_type_68505, $tdef_$_type_68531, $tdef_$_type_68539, % 267.42/38.05 $tdef_$_type_68555, $tdef_$_type_68565, $tdef_$_type_74, $tdef_$_type_90, % 267.42/38.05 $tdef_$_type_94, $tdef_$_type_956, $tdef_$_type_97, % 267.42/38.05 $tdef_Coq.Init.Datatypes.bool, $tdef_Coq.Init.Datatypes.comparison, % 267.42/38.05 $tdef_Coq.Init.Datatypes.list, $tdef_Coq.Init.Datatypes.nat, % 267.42/38.05 $tdef_Coq.Init.Datatypes.prod, $tdef_Coq.Init.Datatypes.unit, % 267.42/38.05 $tdef_Coq.Init.Specif.sig, $tdef_Coq.Init.Specif.sumbool, % 267.42/38.05 $tdef_Coq.Numbers.BinNums.N, $tdef_Coq.Numbers.BinNums.Z, % 267.42/38.05 $tdef_Coq.Numbers.BinNums.positive, $tdef_Coq.PArith.BinPosDef.Pos.mask, % 267.42/38.05 $tdef_Coq.QArith.QArith_base.Q, $tdef_Coq.Reals.Rdefinitions.R, % 267.42/38.05 $tdef_Coq.Reals.Rfunctions.Z_spec, $tdef_Coq.Structures.OrdersTac.ord, % 267.42/38.05 $tdef_Coq.ZArith.Znumtheory.Euclid, $tdef_Coq.ZArith.Zpower.Zdiv_rest_proofs, % 267.42/38.05 $tdef_Coq.setoid_ring.Ring_polynom.Mon, % 267.42/38.05 $tdef_Coq.setoid_ring.Ring_polynom.PExpr, % 267.42/38.05 $tdef_Coq.setoid_ring.Ring_polynom.Pol, $tdef_Prop, $tdef_Type, % 267.42/38.05 ArithCompl.sqr_0, ArithCompl.sqr_2, ArithCompl.sqr_ge, ArithCompl.sqr_le, % 267.42/38.05 ArithCompl.sqr_poss, ArithCompl.sqr_sub1, ArithCompl.sqr_sub2, % 267.42/38.05 ArithCompl.sqr_sub3, ArithCompl.sqr_sum2, ArithCompl.sqr_sum4, % 267.42/38.05 Coq.Init.Datatypes.nat_ind, Coq.Init.Specif.sumbool_ind, % 267.42/38.05 Coq.Logic.Decidable.dec_and, Coq.Logic.Decidable.dec_not_not, % 267.42/38.05 Coq.Logic.Decidable.not_and, Coq.PArith.BinPos.Pos.add_1_r, % 267.42/38.05 Coq.PArith.BinPos.Pos.add_comm, Coq.PArith.BinPos.Pos.iter_invariant, % 267.42/38.05 Coq.PArith.BinPos.Pos.iter_swap_gen, Coq.PArith.BinPos.Pos.sqrt_spec, % 267.42/38.05 Coq.PArith.BinPos.Pos.sqrtrem_spec, Coq.Reals.RIneq.IZN, % 267.42/38.05 Coq.Reals.RIneq.Rmult_0_l, Coq.Reals.RIneq.Rmult_0_r, Coq.Reals.RIneq.le_0_IZR, % 267.42/38.05 Coq.Reals.RIneq.le_IZR, Coq.Reals.RIneq.mult_IZR, Coq.Reals.Raxioms.Rmult_1_l, % 267.42/38.05 Coq.Reals.Rfunctions.Zpower_NR0, Coq.ZArith.BinInt.Pos2Z.is_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.A'A_left, Coq.ZArith.BinInt.Z.A'A_right, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.add_mod, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.add_mod_idemp_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.add_mod_idemp_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_1_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_add, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_add_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_div, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_exact, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_compat_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_lower_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_le_upper_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_lt_upper_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mod_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul_cancel_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul_cancel_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_mul_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_small, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_small_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_str_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_str_pos_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_unique_exact, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_1_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_add, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_divides, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_mod, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_mul_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_small, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_small_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mod_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_div_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_distr_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_distr_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_idemp_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_mod_idemp_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.NZQuot.mul_succ_div_gt, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.div_mod, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.div_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.mod_bound_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Div.Quot2Div.mod_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.add_mod, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.add_mod_idemp_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.add_mod_idemp_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_1_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_add, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_add_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_div, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_exact, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_compat_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_lower_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_le_upper_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_lt_upper_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_mod_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul_cancel_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul_cancel_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_mul_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_small, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_small_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_str_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_str_pos_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.div_unique_exact, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_1_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_add, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_divides, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_mod, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_mul_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_small, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_small_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mod_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mul_div_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_distr_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_distr_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_idemp_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mul_mod_idemp_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_NZDiv.mul_succ_div_gt, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_neq, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_refl, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_sym, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.eq_trans, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_antisym, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_eq, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_lt_trans, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_neq_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_refl, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.le_trans, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_eq, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_irrefl, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.lt_trans, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_eq, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.neq_sym, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_ge_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_gt_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_OrderTac.Tac.not_neq_eq, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Tac.eq_le, Coq.ZArith.BinInt.Z.Private_Tac.eq_sym, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Tac.le_antisym, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Tac.le_eq, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Tac.le_neq_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Tac.le_trans, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Tac.lt_irrefl, % 267.42/38.05 Coq.ZArith.BinInt.Z.Private_Tac.not_gt_le, Coq.ZArith.BinInt.Z.abs_0_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.abs_eq, Coq.ZArith.BinInt.Z.abs_neq, % 267.42/38.05 Coq.ZArith.BinInt.Z.abs_nonneg, Coq.ZArith.BinInt.Z.abs_sgn, % 267.42/38.05 Coq.ZArith.BinInt.Z.abs_spec, Coq.ZArith.BinInt.Z.add_0_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_0_r, Coq.ZArith.BinInt.Z.add_1_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_1_r, Coq.ZArith.BinInt.Z.add_assoc, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_cancel_l, Coq.ZArith.BinInt.Z.add_cancel_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_comm, Coq.ZArith.BinInt.Z.add_le_cases, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_le_lt_mono, Coq.ZArith.BinInt.Z.add_le_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_le_mono_l, Coq.ZArith.BinInt.Z.add_le_mono_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_lt_le_mono, Coq.ZArith.BinInt.Z.add_lt_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_lt_mono_l, Coq.ZArith.BinInt.Z.add_lt_mono_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_neg_nonpos, Coq.ZArith.BinInt.Z.add_nonneg_cases, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_nonneg_nonneg, Coq.ZArith.BinInt.Z.add_nonneg_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_nonpos_cases, Coq.ZArith.BinInt.Z.add_nonpos_neg, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_nonpos_nonpos, Coq.ZArith.BinInt.Z.add_opp_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_pos_nonneg, Coq.ZArith.BinInt.Z.add_pos_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_rem, Coq.ZArith.BinInt.Z.add_rem_idemp_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_rem_idemp_r, Coq.ZArith.BinInt.Z.add_shuffle0, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_simpl_r, Coq.ZArith.BinInt.Z.add_sqrt_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_sqrt_up_le, Coq.ZArith.BinInt.Z.add_square_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_sub_assoc, Coq.ZArith.BinInt.Z.add_sub_swap, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_succ_l, Coq.ZArith.BinInt.Z.add_succ_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.add_wd, Coq.ZArith.BinInt.Z.b2z_inj, % 267.42/38.05 Coq.ZArith.BinInt.Z.bit0_odd, Coq.ZArith.BinInt.Z.bits_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.bits_above_log2, Coq.ZArith.BinInt.Z.bits_inj', % 267.42/38.05 Coq.ZArith.BinInt.Z.bits_inj_iff, Coq.ZArith.BinInt.Z.bits_inj_iff', % 267.42/38.05 Coq.ZArith.BinInt.Z.bits_m1, Coq.ZArith.BinInt.Z.bits_opp, % 267.42/38.05 Coq.ZArith.BinInt.Z.compare_antisym, Coq.ZArith.BinInt.Z.compare_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.compare_sub, Coq.ZArith.BinInt.Z.crossmul_le_addsquare, % 267.42/38.05 Coq.ZArith.BinInt.Z.div2_bits, Coq.ZArith.BinInt.Z.div_0_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_1_r, Coq.ZArith.BinInt.Z.div_add, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_div, Coq.ZArith.BinInt.Z.div_le_compat_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_le_lower_bound, Coq.ZArith.BinInt.Z.div_le_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_le_upper_bound, Coq.ZArith.BinInt.Z.div_lt_upper_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_mod, Coq.ZArith.BinInt.Z.div_mod_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_mul, Coq.ZArith.BinInt.Z.div_mul_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_opp_opp, Coq.ZArith.BinInt.Z.div_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_small, Coq.ZArith.BinInt.Z.div_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_unique_exact, Coq.ZArith.BinInt.Z.div_unique_neg, % 267.42/38.05 Coq.ZArith.BinInt.Z.div_unique_pos, Coq.ZArith.BinInt.Z.div_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.divide_1_l, Coq.ZArith.BinInt.Z.divide_1_r_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.divide_antisym_nonneg, Coq.ZArith.BinInt.Z.divide_gcd_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.divide_lcm_eq_r, Coq.ZArith.BinInt.Z.divide_lcm_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.divide_mul_l, Coq.ZArith.BinInt.Z.divide_pos_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.divide_refl, Coq.ZArith.BinInt.Z.divide_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.eq_decidable, Coq.ZArith.BinInt.Z.eq_equiv, % 267.42/38.05 Coq.ZArith.BinInt.Z.eq_le_incl, Coq.ZArith.BinInt.Z.eq_mul_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.eq_mul_0_l, Coq.ZArith.BinInt.Z.eq_mul_0_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.eq_mul_1_nonneg, Coq.ZArith.BinInt.Z.eq_mul_1_nonneg', % 267.42/38.05 Coq.ZArith.BinInt.Z.eq_sym, Coq.ZArith.BinInt.Z.gcd_0_l_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.gcd_0_r_nonneg, Coq.ZArith.BinInt.Z.gcd_diag_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.gcd_divide_l, Coq.ZArith.BinInt.Z.gcd_divide_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.gcd_mul_diag_l, Coq.ZArith.BinInt.Z.gcd_mul_mono_l_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.gcd_mul_mono_r_nonneg, Coq.ZArith.BinInt.Z.gcd_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.gcd_unique, Coq.ZArith.BinInt.Z.gcd_unique_alt, % 267.42/38.05 Coq.ZArith.BinInt.Z.gcd_wd, Coq.ZArith.BinInt.Z.ge_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.ge_le_iff, Coq.ZArith.BinInt.Z.gt_lt_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.land_comm, Coq.ZArith.BinInt.Z.land_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.lbase, Coq.ZArith.BinInt.Z.lcm_1_l_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.lcm_1_r_nonneg, Coq.ZArith.BinInt.Z.lcm_diag_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.lcm_mul_mono_l_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.lcm_mul_mono_r_nonneg, Coq.ZArith.BinInt.Z.lcm_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.lcm_unique, Coq.ZArith.BinInt.Z.lcm_unique_alt, % 267.42/38.05 Coq.ZArith.BinInt.Z.ldiff_le, Coq.ZArith.BinInt.Z.ldiff_neg, % 267.42/38.05 Coq.ZArith.BinInt.Z.ldiff_spec, Coq.ZArith.BinInt.Z.ldiff_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_0_1, Coq.ZArith.BinInt.Z.le_0_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_0_sub, Coq.ZArith.BinInt.Z.le_add_le_sub_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_antisymm, Coq.ZArith.BinInt.Z.le_decidable, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_exists_sub, Coq.ZArith.BinInt.Z.le_ge, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_ge_cases, Coq.ZArith.BinInt.Z.le_gt_cases, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_ind, Coq.ZArith.BinInt.Z.le_le_add_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_le_pred, Coq.ZArith.BinInt.Z.le_le_sub_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_le_succ_r, Coq.ZArith.BinInt.Z.le_lt_add_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_lt_trans, Coq.ZArith.BinInt.Z.le_lteq, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_max_l, Coq.ZArith.BinInt.Z.le_mul_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_mul_diag_l, Coq.ZArith.BinInt.Z.le_mul_diag_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_ngt, Coq.ZArith.BinInt.Z.le_pred_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_pred_lt, Coq.ZArith.BinInt.Z.le_preorder, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_refl, Coq.ZArith.BinInt.Z.le_stepl, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_stepr, Coq.ZArith.BinInt.Z.le_sub_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_sub_le_add_r, Coq.ZArith.BinInt.Z.le_sub_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_succ_diag_r, Coq.ZArith.BinInt.Z.le_succ_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.le_trans, Coq.ZArith.BinInt.Z.le_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.leb_le, Coq.ZArith.BinInt.Z.leb_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.lnot_shiftr, Coq.ZArith.BinInt.Z.lnot_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_land, Coq.ZArith.BinInt.Z.log2_le_lin, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_le_mono, Coq.ZArith.BinInt.Z.log2_log2_up_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_lor, Coq.ZArith.BinInt.Z.log2_lt_cancel, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_lt_lin, Coq.ZArith.BinInt.Z.log2_lt_pow2, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_lxor, Coq.ZArith.BinInt.Z.log2_mul_above, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_mul_pow2, Coq.ZArith.BinInt.Z.log2_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_nonpos, Coq.ZArith.BinInt.Z.log2_pow2, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_spec, Coq.ZArith.BinInt.Z.log2_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_1, Coq.ZArith.BinInt.Z.log2_up_eqn, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_eqn0, Coq.ZArith.BinInt.Z.log2_up_le_lin, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_le_mono, Coq.ZArith.BinInt.Z.log2_up_le_pow2, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_lt_lin, Coq.ZArith.BinInt.Z.log2_up_mul_above, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_mul_pow2, Coq.ZArith.BinInt.Z.log2_up_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_nonpos, Coq.ZArith.BinInt.Z.log2_up_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_pow2, Coq.ZArith.BinInt.Z.log2_up_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.log2_up_wd, Coq.ZArith.BinInt.Z.log2_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.lor_spec, Coq.ZArith.BinInt.Z.lt_0_1, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_0_mul, Coq.ZArith.BinInt.Z.lt_0_sub, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_1_2, Coq.ZArith.BinInt.Z.lt_1_mul_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_decidable, Coq.ZArith.BinInt.Z.lt_eq_cases, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_exists_pred, Coq.ZArith.BinInt.Z.lt_exists_pred_strong, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_ge_cases, Coq.ZArith.BinInt.Z.lt_ind, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_irrefl, Coq.ZArith.BinInt.Z.lt_le_incl, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_le_pred, Coq.ZArith.BinInt.Z.lt_le_trans, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_lt_succ_r, Coq.ZArith.BinInt.Z.lt_mul_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_neq, Coq.ZArith.BinInt.Z.lt_nge, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_pred_l, Coq.ZArith.BinInt.Z.lt_sub_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_succ_diag_r, Coq.ZArith.BinInt.Z.lt_succ_pred, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_succ_r, Coq.ZArith.BinInt.Z.lt_trans, % 267.42/38.05 Coq.ZArith.BinInt.Z.lt_trichotomy, Coq.ZArith.BinInt.Z.lt_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.ltb_spec, Coq.ZArith.BinInt.Z.lxor_comm, % 267.42/38.05 Coq.ZArith.BinInt.Z.lxor_nonneg, Coq.ZArith.BinInt.Z.lxor_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.max_l, Coq.ZArith.BinInt.Z.max_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.max_lub, Coq.ZArith.BinInt.Z.max_lub_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.max_lub_r, Coq.ZArith.BinInt.Z.max_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.max_spec, Coq.ZArith.BinInt.Z.min_glb, % 267.42/38.05 Coq.ZArith.BinInt.Z.min_glb_l, Coq.ZArith.BinInt.Z.min_glb_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.min_l, Coq.ZArith.BinInt.Z.min_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.min_r, Coq.ZArith.BinInt.Z.min_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.mod_bound_or, Coq.ZArith.BinInt.Z.mod_bound_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.mod_le, Coq.ZArith.BinInt.Z.mod_neg_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.mod_pos_bound, Coq.ZArith.BinInt.Z.mod_sign_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.mod_small, Coq.ZArith.BinInt.Z.mod_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.mod_unique_neg, Coq.ZArith.BinInt.Z.mod_unique_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_0_l, Coq.ZArith.BinInt.Z.mul_0_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_1_l, Coq.ZArith.BinInt.Z.mul_1_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_add_distr_l, Coq.ZArith.BinInt.Z.mul_add_distr_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_assoc, Coq.ZArith.BinInt.Z.mul_cancel_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_comm, Coq.ZArith.BinInt.Z.mul_div_ge, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_div_le, Coq.ZArith.BinInt.Z.mul_eq_0_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_eq_0_r, Coq.ZArith.BinInt.Z.mul_id_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_neg_l, Coq.ZArith.BinInt.Z.mul_le_mono_neg_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_nonneg_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_nonneg_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_nonpos, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_nonpos_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_nonpos_r, Coq.ZArith.BinInt.Z.mul_le_mono_pos_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_le_mono_pos_r, Coq.ZArith.BinInt.Z.mul_lt_mono_neg_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_lt_mono_neg_r, Coq.ZArith.BinInt.Z.mul_lt_mono_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_lt_mono_nonpos, Coq.ZArith.BinInt.Z.mul_lt_mono_pos_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_lt_mono_pos_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_max_distr_nonneg_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_max_distr_nonneg_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_max_distr_nonpos_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_max_distr_nonpos_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_min_distr_nonneg_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_min_distr_nonneg_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_min_distr_nonpos_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_min_distr_nonpos_r, Coq.ZArith.BinInt.Z.mul_neg_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_nonneg_cancel_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_nonneg_cancel_r, Coq.ZArith.BinInt.Z.mul_nonneg_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_nonneg_nonpos, Coq.ZArith.BinInt.Z.mul_nonpos_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_nonpos_nonpos, Coq.ZArith.BinInt.Z.mul_opp_comm, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_opp_l, Coq.ZArith.BinInt.Z.mul_opp_opp, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_opp_r, Coq.ZArith.BinInt.Z.mul_pos_cancel_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_pos_neg, Coq.ZArith.BinInt.Z.mul_pos_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_pow2_bits, Coq.ZArith.BinInt.Z.mul_pow2_bits_add, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_pred_quot_gt, Coq.ZArith.BinInt.Z.mul_pred_quot_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_quot_ge, Coq.ZArith.BinInt.Z.mul_quot_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_reg_l, Coq.ZArith.BinInt.Z.mul_reg_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_shuffle0, Coq.ZArith.BinInt.Z.mul_shuffle1, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_shuffle3, Coq.ZArith.BinInt.Z.mul_sub_distr_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_sub_distr_r, Coq.ZArith.BinInt.Z.mul_succ_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_succ_quot_gt, Coq.ZArith.BinInt.Z.mul_succ_quot_lt, % 267.42/38.05 Coq.ZArith.BinInt.Z.mul_succ_r, Coq.ZArith.BinInt.Z.mul_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.neg_nonneg_cases, Coq.ZArith.BinInt.Z.neq_mul_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.nle_gt, Coq.ZArith.BinInt.Z.nonpos_nonneg_cases, % 267.42/38.05 Coq.ZArith.BinInt.Z.nonpos_pos_cases, Coq.ZArith.BinInt.Z.one_succ, % 267.42/38.05 Coq.ZArith.BinInt.Z.ones_spec_high, Coq.ZArith.BinInt.Z.ones_spec_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.ones_spec_low, Coq.ZArith.BinInt.Z.opp_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.opp_add_distr, Coq.ZArith.BinInt.Z.opp_inj, % 267.42/38.05 Coq.ZArith.BinInt.Z.opp_inj_wd, Coq.ZArith.BinInt.Z.opp_involutive, % 267.42/38.05 Coq.ZArith.BinInt.Z.opp_le_mono, Coq.ZArith.BinInt.Z.opp_lt_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.opp_neg_pos, Coq.ZArith.BinInt.Z.opp_nonneg_nonpos, % 267.42/38.05 Coq.ZArith.BinInt.Z.opp_nonpos_nonneg, Coq.ZArith.BinInt.Z.opp_pos_neg, % 267.42/38.05 Coq.ZArith.BinInt.Z.opp_wd, Coq.ZArith.BinInt.Z.order_induction_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_0_r, Coq.ZArith.BinInt.Z.pow_1_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_1_r, Coq.ZArith.BinInt.Z.pow_add_lower, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_add_r, Coq.ZArith.BinInt.Z.pow_add_upper, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_eq_0, Coq.ZArith.BinInt.Z.pow_gt_lin_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_inj_l, Coq.ZArith.BinInt.Z.pow_inj_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_le_mono, Coq.ZArith.BinInt.Z.pow_le_mono_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_le_mono_r, Coq.ZArith.BinInt.Z.pow_le_mono_r_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_lt_mono_l, Coq.ZArith.BinInt.Z.pow_lt_mono_l_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_lt_mono_r, Coq.ZArith.BinInt.Z.pow_lt_mono_r_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_mul_l, Coq.ZArith.BinInt.Z.pow_mul_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_neg_r, Coq.ZArith.BinInt.Z.pow_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_nonzero, Coq.ZArith.BinInt.Z.pow_odd_sgn, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_pos_nonneg, Coq.ZArith.BinInt.Z.pow_succ_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.pow_wd, Coq.ZArith.BinInt.Z.pred_succ, % 267.42/38.05 Coq.ZArith.BinInt.Z.pred_wd, Coq.ZArith.BinInt.Z.quadmul_le_squareadd, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_add, Coq.ZArith.BinInt.Z.quot_add_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_div_nonneg, Coq.ZArith.BinInt.Z.quot_le_compat_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_le_lower_bound, Coq.ZArith.BinInt.Z.quot_le_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_le_upper_bound, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_lt_upper_bound, Coq.ZArith.BinInt.Z.quot_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_mul_le, Coq.ZArith.BinInt.Z.quot_opp_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_opp_opp, Coq.ZArith.BinInt.Z.quot_opp_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_pos, Coq.ZArith.BinInt.Z.quot_rem, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_rem_unique, Coq.ZArith.BinInt.Z.quot_small, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_unique, Coq.ZArith.BinInt.Z.quot_unique_exact, % 267.42/38.05 Coq.ZArith.BinInt.Z.quot_wd, Coq.ZArith.BinInt.Z.rbase, % 267.42/38.05 Coq.ZArith.BinInt.Z.rem_0_l, Coq.ZArith.BinInt.Z.rem_add, % 267.42/38.05 Coq.ZArith.BinInt.Z.rem_bound_pos, Coq.ZArith.BinInt.Z.rem_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.rem_mod_nonneg, Coq.ZArith.BinInt.Z.rem_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.rem_nonpos, Coq.ZArith.BinInt.Z.rem_opp_l, % 267.42/38.05 Coq.ZArith.BinInt.Z.rem_opp_r, Coq.ZArith.BinInt.Z.rem_sign_mul, % 267.42/38.05 Coq.ZArith.BinInt.Z.rem_small, Coq.ZArith.BinInt.Z.rem_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.rem_wd, Coq.ZArith.BinInt.Z.setbit_eq, % 267.42/38.05 Coq.ZArith.BinInt.Z.setbit_neq, Coq.ZArith.BinInt.Z.sgn_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.sgn_neg, Coq.ZArith.BinInt.Z.sgn_null, % 267.42/38.05 Coq.ZArith.BinInt.Z.sgn_null_iff, Coq.ZArith.BinInt.Z.sgn_pos, % 267.42/38.05 Coq.ZArith.BinInt.Z.sgn_spec, Coq.ZArith.BinInt.Z.shiftl_eq_0_iff, % 267.42/38.05 Coq.ZArith.BinInt.Z.shiftl_mul_pow2, Coq.ZArith.BinInt.Z.shiftl_shiftl, % 267.42/38.05 Coq.ZArith.BinInt.Z.shiftl_spec, Coq.ZArith.BinInt.Z.shiftl_spec_alt, % 267.42/38.05 Coq.ZArith.BinInt.Z.shiftl_spec_high, Coq.ZArith.BinInt.Z.shiftr_div_pow2, % 267.42/38.05 Coq.ZArith.BinInt.Z.shiftr_eq_0, Coq.ZArith.BinInt.Z.shiftr_mul_pow2, % 267.42/38.05 Coq.ZArith.BinInt.Z.shiftr_shiftl_r, Coq.ZArith.BinInt.Z.shiftr_shiftr, % 267.42/38.05 Coq.ZArith.BinInt.Z.shiftr_spec, Coq.ZArith.BinInt.Z.shiftr_spec_aux, % 267.42/38.05 Coq.ZArith.BinInt.Z.shiftr_wd, Coq.ZArith.BinInt.Z.sqrt_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_1, Coq.ZArith.BinInt.Z.sqrt_eq_succ_iff_square, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_le_lin, Coq.ZArith.BinInt.Z.sqrt_le_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_le_square, Coq.ZArith.BinInt.Z.sqrt_lt_cancel, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_lt_square, Coq.ZArith.BinInt.Z.sqrt_mul_above, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_neg, Coq.ZArith.BinInt.Z.sqrt_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_pred_square, Coq.ZArith.BinInt.Z.sqrt_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_spec_alt, Coq.ZArith.BinInt.Z.sqrt_spec_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_sqrt_up_exact, Coq.ZArith.BinInt.Z.sqrt_sqrt_up_spec, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_square, Coq.ZArith.BinInt.Z.sqrt_succ_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_succ_or, Coq.ZArith.BinInt.Z.sqrt_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_unique', Coq.ZArith.BinInt.Z.sqrt_up_0, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_eq_succ_iff_square, Coq.ZArith.BinInt.Z.sqrt_up_eqn, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_eqn0, Coq.ZArith.BinInt.Z.sqrt_up_le_lin, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_le_mono, Coq.ZArith.BinInt.Z.sqrt_up_le_square, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_lt_cancel, Coq.ZArith.BinInt.Z.sqrt_up_lt_square, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_mul_above, Coq.ZArith.BinInt.Z.sqrt_up_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_spec, Coq.ZArith.BinInt.Z.sqrt_up_square, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_succ_le, Coq.ZArith.BinInt.Z.sqrt_up_succ_or, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_succ_square, Coq.ZArith.BinInt.Z.sqrt_up_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrt_up_wd, Coq.ZArith.BinInt.Z.sqrt_wd, % 267.42/38.05 Coq.ZArith.BinInt.Z.sqrtrem_spec, Coq.ZArith.BinInt.Z.square_add_le, % 267.42/38.05 Coq.ZArith.BinInt.Z.square_le_mono_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.square_le_mono_nonpos, % 267.42/38.05 Coq.ZArith.BinInt.Z.square_le_simpl_nonpos, % 267.42/38.05 Coq.ZArith.BinInt.Z.square_lt_mono_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.square_lt_mono_nonpos, % 267.42/38.05 Coq.ZArith.BinInt.Z.square_lt_simpl_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.square_lt_simpl_nonpos, Coq.ZArith.BinInt.Z.square_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.strong_right_induction, Coq.ZArith.BinInt.Z.sub_0_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.sub_add, Coq.ZArith.BinInt.Z.sub_diag, % 267.42/38.05 Coq.ZArith.BinInt.Z.sub_le_mono_l, Coq.ZArith.BinInt.Z.sub_le_mono_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.sub_nonneg_cases, Coq.ZArith.BinInt.Z.sub_nonpos_cases, % 267.42/38.05 Coq.ZArith.BinInt.Z.sub_opp_r, Coq.ZArith.BinInt.Z.sub_simpl_r, % 267.42/38.05 Coq.ZArith.BinInt.Z.succ_inj, Coq.ZArith.BinInt.Z.succ_le_mono, % 267.42/38.05 Coq.ZArith.BinInt.Z.succ_lt_mono, Coq.ZArith.BinInt.Z.succ_pred, % 267.42/38.05 Coq.ZArith.BinInt.Z.succ_wd, Coq.ZArith.BinInt.Z.testbit_even_succ, % 267.42/38.05 Coq.ZArith.BinInt.Z.testbit_neg_r, Coq.ZArith.BinInt.Z.testbit_odd_succ, % 267.42/38.05 Coq.ZArith.BinInt.Z.testbit_of_N', Coq.ZArith.BinInt.Z.testbit_ones_nonneg, % 267.42/38.05 Coq.ZArith.BinInt.Z.testbit_spec, Coq.ZArith.BinInt.Z.testbit_spec', % 267.42/38.05 Coq.ZArith.BinInt.Z.testbit_succ_r, Coq.ZArith.BinInt.Z.testbit_unique, % 267.42/38.05 Coq.ZArith.BinInt.Z.testbit_wd, Coq.ZArith.BinInt.Z.two_succ, % 267.42/38.05 Coq.ZArith.BinInt.Z2Pos.to_pos_nonpos, Coq.ZArith.BinInt.Zmult_integral, % 267.42/38.05 Coq.ZArith.BinInt.Zmult_integral_l, Coq.ZArith.Wf_Z.Z_lt_induction, % 267.42/38.05 Coq.ZArith.Wf_Z.Z_of_nat_complete, Coq.ZArith.Wf_Z.Z_of_nat_prop, % 267.42/38.05 Coq.ZArith.Wf_Z.Zlt_0_ind, Coq.ZArith.Wf_Z.Zlt_lower_bound_ind, % 267.42/38.05 Coq.ZArith.Wf_Z.natlike_ind, Coq.ZArith.Zabs.Zabs_nat_le, % 267.42/38.05 Coq.ZArith.Zabs.Zabs_nat_lt, Coq.ZArith.Zbool.Zle_bool_imp_le, % 267.42/38.05 Coq.ZArith.Zcomplements.sqr_pos, Coq.ZArith.Zdiv.Z_div_le, % 267.42/38.05 Coq.ZArith.Zdiv.Z_div_mod, Coq.ZArith.Zdiv.Z_div_mod_POS, % 267.42/38.05 Coq.ZArith.Zdiv.Z_div_mod_eq, Coq.ZArith.Zdiv.Z_div_pos, % 267.42/38.05 Coq.ZArith.Zdiv.Z_mod_lt, Coq.ZArith.Zdiv.Z_mult_div_ge, % 267.42/38.05 Coq.ZArith.Zdiv.Zdiv_0_r, Coq.ZArith.Zdiv.Zdiv_Zdiv, % 267.42/38.05 Coq.ZArith.Zdiv.Zdiv_le_compat_l, Coq.ZArith.Zdiv.Zdiv_le_lower_bound, % 267.42/38.05 Coq.ZArith.Zdiv.Zdiv_le_upper_bound, Coq.ZArith.Zdiv.Zdiv_lt_upper_bound, % 267.42/38.05 Coq.ZArith.Zdiv.Zdiv_mod_unique, Coq.ZArith.Zdiv.Zdiv_mult_le, % 267.42/38.05 Coq.ZArith.Zdiv.Zdiv_small, Coq.ZArith.Zdiv.Zdiv_unique, % 267.42/38.05 Coq.ZArith.Zdiv.Zdiv_unique_full, Coq.ZArith.Zdiv.Zmod_le, % 267.42/38.05 Coq.ZArith.Zdiv.Zmod_small, Coq.ZArith.Zdiv.Zmod_unique, % 267.42/38.05 Coq.ZArith.Zdiv.Zmod_unique_full, Coq.ZArith.Znat.Nat2Z.inj_succ, % 267.42/38.05 Coq.ZArith.Znat.Nat2Z.is_nonneg, Coq.ZArith.Znat.Z2N.id, % 267.42/38.05 Coq.ZArith.Znat.Z2N.inj, Coq.ZArith.Znat.Z2N.inj_add, % 267.42/38.05 Coq.ZArith.Znat.Z2N.inj_compare, Coq.ZArith.Znat.Z2N.inj_div, % 267.42/38.05 Coq.ZArith.Znat.Z2N.inj_iff, Coq.ZArith.Znat.Z2N.inj_le, % 267.42/38.05 Coq.ZArith.Znat.Z2N.inj_lt, Coq.ZArith.Znat.Z2N.inj_mul, % 267.42/38.05 Coq.ZArith.Znat.Z2N.inj_pow, Coq.ZArith.Znat.Z2N.inj_quot, % 267.42/38.05 Coq.ZArith.Znat.Z2N.inj_rem, Coq.ZArith.Znat.Z2N.inj_sub, % 267.42/38.05 Coq.ZArith.Znat.Z2N.inj_succ, Coq.ZArith.Znat.Z2Nat.id, % 267.42/38.05 Coq.ZArith.Znat.Z2Nat.inj, Coq.ZArith.Znat.Z2Nat.inj_add, % 267.42/38.05 Coq.ZArith.Znat.Z2Nat.inj_compare, Coq.ZArith.Znat.Z2Nat.inj_iff, % 267.42/38.05 Coq.ZArith.Znat.Z2Nat.inj_le, Coq.ZArith.Znat.Z2Nat.inj_lt, % 267.42/38.05 Coq.ZArith.Znat.Z2Nat.inj_mul, Coq.ZArith.Znat.Z2Nat.inj_sub, % 267.42/38.05 Coq.ZArith.Znat.Z2Nat.inj_succ, Coq.ZArith.Znat.Z_N_nat, % 267.42/38.05 Coq.ZArith.Znat.Zabs2N.abs_N_nonneg, Coq.ZArith.Znat.Zabs2N.inj_add, % 267.42/38.05 Coq.ZArith.Znat.Zabs2N.inj_compare, Coq.ZArith.Znat.Zabs2N.inj_le, % 267.42/38.05 Coq.ZArith.Znat.Zabs2N.inj_lt, Coq.ZArith.Znat.Zabs2N.inj_max, % 267.42/38.05 Coq.ZArith.Znat.Zabs2N.inj_min, Coq.ZArith.Znat.Zabs2N.inj_pow, % 267.42/38.05 Coq.ZArith.Znat.Zabs2N.inj_sub, Coq.ZArith.Znat.Zabs2N.inj_succ, % 267.42/38.05 Coq.ZArith.Znat.Zabs2Nat.abs_nat_nonneg, Coq.ZArith.Znat.Zabs2Nat.inj_add, % 267.42/38.05 Coq.ZArith.Znat.Zabs2Nat.inj_compare, Coq.ZArith.Znat.Zabs2Nat.inj_le, % 267.42/38.05 Coq.ZArith.Znat.Zabs2Nat.inj_lt, Coq.ZArith.Znat.Zabs2Nat.inj_sub, % 267.42/38.05 Coq.ZArith.Znat.Zabs2Nat.inj_succ, Coq.ZArith.Znumtheory.Bezout_intro, % 267.42/38.05 Coq.ZArith.Znumtheory.Z_0_1_more, Coq.ZArith.Znumtheory.Zdivide_le, % 267.42/38.05 Coq.ZArith.Znumtheory.Zdivide_mod, Coq.ZArith.Znumtheory.Zdivide_mod_minus, % 267.42/38.05 Coq.ZArith.Znumtheory.Zgcd_is_gcd, Coq.ZArith.Znumtheory.Zis_gcd_0, % 267.42/38.05 Coq.ZArith.Znumtheory.Zis_gcd_for_euclid, Coq.ZArith.Znumtheory.Zis_gcd_gcd, % 267.42/38.05 Coq.ZArith.Znumtheory.Zis_gcd_intro, % 267.42/38.05 Coq.ZArith.Znumtheory.prime_dec_aux_subproof, % 267.42/38.05 Coq.ZArith.Znumtheory.prime_dec_aux_subproof0, % 267.42/38.05 Coq.ZArith.Znumtheory.prime_dec_aux_subproof1, Coq.ZArith.Znumtheory.prime_ind, % 267.42/38.05 Coq.ZArith.Znumtheory.rel_prime_cross_prod, Coq.ZArith.Zorder.Zgt_square_simpl, % 267.42/38.05 Coq.ZArith.Zorder.Zle_0_minus_le, Coq.ZArith.Zorder.Zle_lt_or_eq, % 267.42/38.05 Coq.ZArith.Zorder.Zle_minus_le_0, Coq.ZArith.Zorder.Zle_succ_le, % 267.42/38.05 Coq.ZArith.Zorder.Zlt_square_simpl, Coq.ZArith.Zorder.Zmult_ge_reg_r, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_gt_0_le_0_compat, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_gt_0_le_compat_r, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_gt_0_lt_0_reg_r, Coq.ZArith.Zorder.Zmult_gt_0_lt_reg_r, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_gt_0_reg_l, Coq.ZArith.Zorder.Zmult_gt_reg_r, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_le_0_reg_r, Coq.ZArith.Zorder.Zmult_le_compat, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_le_compat_l, Coq.ZArith.Zorder.Zmult_le_compat_r, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_le_reg_r, Coq.ZArith.Zorder.Zmult_lt_0_le_compat_r, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_lt_0_le_reg_r, Coq.ZArith.Zorder.Zmult_lt_0_reg_r, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_lt_compat, Coq.ZArith.Zorder.Zmult_lt_compat2, % 267.42/38.05 Coq.ZArith.Zorder.Zmult_lt_reg_r, Coq.ZArith.Zorder.Znot_gt_le, % 267.42/38.05 Coq.ZArith.Zorder.Znot_le_gt, Coq.ZArith.Zorder.Znot_lt_ge, % 267.42/38.05 Coq.ZArith.Zorder.Zplus_le_compat_l, Coq.ZArith.Zorder.Zplus_le_reg_l, % 267.42/38.05 Coq.ZArith.Zorder.Zplus_le_reg_r, Coq.ZArith.Zorder.dec_Zgt, % 267.42/38.05 Coq.ZArith.Zpower.Zdiv_rest_proofs_ind, Coq.ZArith.Zpower.Zdiv_rest_proofs_sind, % 267.42/38.05 Coq.ZArith.Zpower.Zpower_nat_Zpower, Coq.ZArith.Zpower.two_p_S, % 267.42/38.05 Coq.ZArith.Zpower.two_p_gt_ZERO, Coq.ZArith.Zpower.two_p_is_exp, % 267.42/38.05 Coq.ZArith.Zpower.two_p_pred, Coq.ZArith.auxiliary.Zegal_left, % 267.42/38.05 Coq.ZArith.auxiliary.Zge_left, Coq.ZArith.auxiliary.Zgt_left, % 267.42/38.05 Coq.ZArith.auxiliary.Zle_left, Coq.ZArith.auxiliary.Zle_left_rev, % 267.42/38.05 Coq.ZArith.auxiliary.Zle_mult_approx, Coq.ZArith.auxiliary.Zlt_left, % 267.42/38.05 Coq.ZArith.auxiliary.Zmult_le_approx, Coq.ZArith.auxiliary.Zne_left, % 267.42/38.05 Coq.omega.OmegaLemmas.OMEGA1, Coq.omega.OmegaLemmas.OMEGA17, % 267.42/38.05 Coq.omega.OmegaLemmas.OMEGA2, Coq.omega.OmegaLemmas.OMEGA3, % 267.42/38.05 Coq.omega.OmegaLemmas.OMEGA6, Coq.omega.OmegaLemmas.OMEGA7, % 267.42/38.05 Coq.omega.OmegaLemmas.OMEGA8, Coq.omega.OmegaLemmas.fast_OMEGA10, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_OMEGA11, Coq.omega.OmegaLemmas.fast_OMEGA12, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_OMEGA13, Coq.omega.OmegaLemmas.fast_OMEGA14, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_OMEGA15, Coq.omega.OmegaLemmas.fast_OMEGA16, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zmult_assoc_reverse, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zmult_comm, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zopp_eq_mult_neg_1, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zopp_mult_distr_r, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zopp_plus_distr, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zplus_assoc, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zplus_assoc_reverse, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zplus_comm, Coq.omega.OmegaLemmas.fast_Zplus_permute, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zred_factor0, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zred_factor2, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zred_factor3, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zred_factor4, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zred_factor5, % 267.42/38.05 Coq.omega.OmegaLemmas.fast_Zred_factor6, Coq.omega.OmegaLemmas.intro_Z, % 267.42/38.05 Coq.omega.OmegaLemmas.new_var, Coq.omega.PreOmega.Z.rem_bound_neg_neg, % 267.42/38.05 Coq.omega.PreOmega.Z.rem_bound_neg_pos, Coq.omega.PreOmega.Z.rem_bound_pos_neg, % 267.42/38.05 Coq.omega.PreOmega.Z.rem_bound_pos_pos, _HAMMER_COQ_FALSE, _HAMMER_COQ_TRUE, % 267.42/38.05 _HAMMER_COQ_TYPE_TYPE % 267.42/38.05 % 267.42/38.05 Those formulas are unsatisfiable: % 267.42/38.05 --------------------------------- % 267.42/38.05 % 267.42/38.05 Begin of proof % 267.42/38.06 | % 267.42/38.06 | ALPHA: (Coq.ZArith.BinInt.Z.pow_le_mono_l_iff) implies: % 267.42/38.06 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | v2) = v3) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | v0) = v1) | ~ $i(v2) | ~ $i(v0) | ~ % 267.42/38.06 | cCoq_2eNumbers_2eBinNums_2eZ___24t(v2) | ~ % 267.42/38.06 | cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) | ? [v4: $i] : % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v0, v2) = v4 & $i(v4) & ! % 267.42/38.06 | [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v2, v5) = v7) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v0, v5) = v6) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v6, v7) = v8) | ~ $i(v5) % 267.42/38.06 | | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v5) | ~ p(v8) | ~ p(v3) % 267.42/38.06 | | ~ p(v1) | p(v4) | ? [v9: $i] : % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | v5) = v9 & $i(v9) & ~ p(v9))) & ! [v5: $i] : ! [v6: $i] : % 267.42/38.06 | ! [v7: $i] : ! [v8: $i] : ( ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v2, v5) = v7) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(v0, v5) = v6) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v6, v7) = v8) | ~ $i(v5) % 267.42/38.06 | | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v5) | ~ p(v4) | ~ p(v3) % 267.42/38.06 | | ~ p(v1) | p(v8) | ? [v9: $i] : % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | v5) = v9 & $i(v9) & ~ p(v9))))) % 267.42/38.06 | % 267.42/38.06 | ALPHA: (Coq.ZArith.BinInt.Z.square_le_simpl_nonneg) implies: % 267.42/38.06 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 267.42/38.06 | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v2, v2) = v3) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v0, v0) = v1) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v1, v3) = v4) | ~ $i(v2) | % 267.42/38.06 | ~ $i(v0) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v2) | ~ % 267.42/38.06 | cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) | ~ p(v4) | ? [v5: $i] : ? % 267.42/38.06 | [v6: $i] : ((cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v0, v2) = v6 & % 267.42/38.06 | $i(v6) & p(v6)) | % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | v2) = v5 & $i(v5) & ~ p(v5)))) % 267.42/38.06 | % 267.42/38.06 | ALPHA: (_HAMMER_GOAL) implies: % 267.42/38.06 | (3) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 267.42/38.06 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 267.42/38.06 | (cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v3, v3) = v5 & % 267.42/38.06 | cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(v0, v0) = v2 & % 267.42/38.06 | cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v5, v2) = v6 & % 267.42/38.06 | cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v3, v0) = v7 & % 267.42/38.06 | cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | v3) = v4 & % 267.42/38.06 | cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | v0) = v1 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & % 267.42/38.06 | $i(v1) & $i(v0) & cCoq_2eNumbers_2eBinNums_2eZ___24t(v3) & % 267.42/38.06 | cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) & p(v6) & p(v4) & p(v1) & ~ % 267.42/38.06 | p(v7)) % 267.42/38.06 | % 267.42/38.06 | ALPHA: (function-axioms) implies: % 267.42/38.06 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v3, v2) = v1) | ~ % 267.42/38.06 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v3, v2) = v0)) % 267.42/38.06 | % 267.42/38.06 | DELTA: instantiating (3) with fresh symbols all_1731_0, all_1731_1, % 267.42/38.06 | all_1731_2, all_1731_3, all_1731_4, all_1731_5, all_1731_6, all_1731_7 % 267.42/38.06 | gives: % 267.42/38.06 | (5) cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(all_1731_4, all_1731_4) = % 267.42/38.06 | all_1731_2 & cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(all_1731_7, % 267.42/38.06 | all_1731_7) = all_1731_5 & % 267.42/38.06 | cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_2, all_1731_5) = % 267.42/38.06 | all_1731_1 & cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, % 267.42/38.06 | all_1731_7) = all_1731_0 & % 267.42/38.06 | cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | all_1731_4) = all_1731_3 & % 267.42/38.06 | cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | all_1731_7) = all_1731_6 & $i(all_1731_0) & $i(all_1731_1) & % 267.42/38.06 | $i(all_1731_2) & $i(all_1731_3) & $i(all_1731_4) & $i(all_1731_5) & % 267.42/38.06 | $i(all_1731_6) & $i(all_1731_7) & % 267.42/38.06 | cCoq_2eNumbers_2eBinNums_2eZ___24t(all_1731_4) & % 267.42/38.06 | cCoq_2eNumbers_2eBinNums_2eZ___24t(all_1731_7) & p(all_1731_1) & % 267.42/38.06 | p(all_1731_3) & p(all_1731_6) & ~ p(all_1731_0) % 267.42/38.06 | % 267.42/38.06 | ALPHA: (5) implies: % 267.42/38.06 | (6) ~ p(all_1731_0) % 267.42/38.06 | (7) p(all_1731_6) % 267.42/38.06 | (8) p(all_1731_1) % 267.42/38.06 | (9) cCoq_2eNumbers_2eBinNums_2eZ___24t(all_1731_7) % 267.42/38.06 | (10) cCoq_2eNumbers_2eBinNums_2eZ___24t(all_1731_4) % 267.42/38.06 | (11) $i(all_1731_7) % 267.42/38.06 | (12) $i(all_1731_4) % 267.42/38.06 | (13) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | all_1731_7) = all_1731_6 % 267.42/38.06 | (14) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.06 | all_1731_4) = all_1731_3 % 267.42/38.06 | (15) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, all_1731_7) = % 267.42/38.06 | all_1731_0 % 267.42/38.06 | (16) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_2, all_1731_5) = % 267.42/38.06 | all_1731_1 % 267.42/38.06 | (17) cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(all_1731_7, all_1731_7) = % 267.42/38.06 | all_1731_5 % 267.42/38.06 | (18) cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(all_1731_4, all_1731_4) = % 267.42/38.06 | all_1731_2 % 267.42/38.06 | % 267.42/38.07 | GROUND_INST: instantiating (1) with all_1731_4, all_1731_3, all_1731_7, % 267.42/38.07 | all_1731_6, simplifying with (9), (10), (11), (12), (13), (14) % 267.42/38.07 | gives: % 267.42/38.07 | (19) ? [v0: $i] : (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, % 267.42/38.07 | all_1731_7) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ! [v3: % 267.42/38.07 | $i] : ! [v4: $i] : ( ~ % 267.42/38.07 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_4, v1) = v2) % 267.42/38.07 | | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_7, v1) = % 267.42/38.07 | v3) | ~ (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v2, v3) = v4) | % 267.42/38.07 | ~ $i(v1) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v1) | ~ p(v4) | % 267.42/38.07 | ~ p(all_1731_3) | ~ p(all_1731_6) | p(v0) | ? [v5: $i] : % 267.42/38.07 | (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | v1) = v5 & $i(v5) & ~ p(v5))) & ! [v1: $i] : ! [v2: $i] : % 267.42/38.07 | ! [v3: $i] : ! [v4: $i] : ( ~ % 267.42/38.07 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_4, v1) = v2) % 267.42/38.07 | | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_7, v1) = % 267.42/38.07 | v3) | ~ (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v2, v3) = v4) | % 267.42/38.07 | ~ $i(v1) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v1) | ~ p(v0) | % 267.42/38.07 | ~ p(all_1731_3) | ~ p(all_1731_6) | p(v4) | ? [v5: $i] : % 267.42/38.07 | (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | v1) = v5 & $i(v5) & ~ p(v5)))) % 267.42/38.07 | % 267.42/38.07 | GROUND_INST: instantiating (2) with all_1731_4, all_1731_2, all_1731_7, % 267.42/38.07 | all_1731_5, all_1731_1, simplifying with (8), (9), (10), (11), % 267.42/38.07 | (12), (16), (17), (18) gives: % 267.42/38.07 | (20) ? [v0: $i] : ? [v1: $i] : % 267.42/38.07 | ((cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, all_1731_7) = v1 % 267.42/38.07 | & $i(v1) & p(v1)) | % 267.42/38.07 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | all_1731_7) = v0 & $i(v0) & ~ p(v0))) % 267.42/38.07 | % 267.42/38.07 | DELTA: instantiating (20) with fresh symbols all_2011_0, all_2011_1 gives: % 267.42/38.07 | (21) (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, all_1731_7) = % 267.42/38.07 | all_2011_0 & $i(all_2011_0) & p(all_2011_0)) | % 267.42/38.07 | (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | all_1731_7) = all_2011_1 & $i(all_2011_1) & ~ p(all_2011_1)) % 267.42/38.07 | % 267.42/38.07 | DELTA: instantiating (19) with fresh symbol all_2819_0 gives: % 267.42/38.07 | (22) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, all_1731_7) = % 267.42/38.07 | all_2819_0 & $i(all_2819_0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 267.42/38.07 | : ! [v3: $i] : ( ~ % 267.42/38.07 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_4, v0) = v1) | % 267.42/38.07 | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_7, v0) = v2) % 267.42/38.07 | | ~ (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v1, v2) = v3) | ~ % 267.42/38.07 | $i(v0) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) | ~ p(v3) | ~ % 267.42/38.07 | p(all_1731_3) | ~ p(all_1731_6) | p(all_2819_0) | ? [v4: $i] : % 267.42/38.07 | (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | v0) = v4 & $i(v4) & ~ p(v4))) & ! [v0: $i] : ! [v1: $i] : ! % 267.42/38.07 | [v2: $i] : ! [v3: $i] : ( ~ % 267.42/38.07 | (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_4, v0) = v1) | % 267.42/38.07 | ~ (cCoq_2eZArith_2eBinIntDef_2eZ_2epow___24a2(all_1731_7, v0) = v2) % 267.42/38.07 | | ~ (cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(v1, v2) = v3) | ~ % 267.42/38.07 | $i(v0) | ~ cCoq_2eNumbers_2eBinNums_2eZ___24t(v0) | ~ % 267.42/38.07 | p(all_2819_0) | ~ p(all_1731_3) | ~ p(all_1731_6) | p(v3) | ? % 267.42/38.07 | [v4: $i] : % 267.42/38.07 | (cCoq_2eZArith_2eBinInt_2eZ_2elt___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | v0) = v4 & $i(v4) & ~ p(v4))) % 267.42/38.07 | % 267.42/38.07 | ALPHA: (22) implies: % 267.42/38.07 | (23) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, all_1731_7) = % 267.42/38.07 | all_2819_0 % 267.42/38.07 | % 267.42/38.07 | BETA: splitting (21) gives: % 267.42/38.07 | % 267.42/38.07 | Case 1: % 267.42/38.07 | | % 267.42/38.07 | | (24) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, all_1731_7) = % 267.42/38.07 | | all_2011_0 & $i(all_2011_0) & p(all_2011_0) % 267.42/38.07 | | % 267.42/38.07 | | ALPHA: (24) implies: % 267.42/38.07 | | (25) p(all_2011_0) % 267.42/38.07 | | (26) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(all_1731_4, all_1731_7) = % 267.42/38.07 | | all_2011_0 % 267.42/38.07 | | % 267.42/38.07 | | GROUND_INST: instantiating (4) with all_1731_0, all_2819_0, all_1731_7, % 267.42/38.07 | | all_1731_4, simplifying with (15), (23) gives: % 267.42/38.07 | | (27) all_2819_0 = all_1731_0 % 267.42/38.07 | | % 267.42/38.07 | | GROUND_INST: instantiating (4) with all_2011_0, all_2819_0, all_1731_7, % 267.42/38.07 | | all_1731_4, simplifying with (23), (26) gives: % 267.42/38.07 | | (28) all_2819_0 = all_2011_0 % 267.42/38.07 | | % 267.42/38.07 | | COMBINE_EQS: (27), (28) imply: % 267.42/38.07 | | (29) all_2011_0 = all_1731_0 % 267.42/38.07 | | % 267.42/38.07 | | REDUCE: (25), (29) imply: % 267.42/38.07 | | (30) p(all_1731_0) % 267.42/38.07 | | % 267.42/38.07 | | PRED_UNIFY: (6), (30) imply: % 267.42/38.07 | | (31) $false % 267.42/38.07 | | % 267.42/38.07 | | CLOSE: (31) is inconsistent. % 267.42/38.07 | | % 267.42/38.07 | Case 2: % 267.42/38.07 | | % 267.42/38.07 | | (32) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | | all_1731_7) = all_2011_1 & $i(all_2011_1) & ~ p(all_2011_1) % 267.42/38.07 | | % 267.42/38.07 | | ALPHA: (32) implies: % 267.42/38.07 | | (33) ~ p(all_2011_1) % 267.42/38.07 | | (34) cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, % 267.42/38.07 | | all_1731_7) = all_2011_1 % 267.42/38.07 | | % 267.42/38.07 | | GROUND_INST: instantiating (4) with all_1731_6, all_2011_1, all_1731_7, % 267.42/38.07 | | cCoq_2eNumbers_2eBinNums_2eZ0, simplifying with (13), (34) % 267.42/38.07 | | gives: % 267.42/38.07 | | (35) all_2011_1 = all_1731_6 % 267.42/38.07 | | % 267.42/38.07 | | REDUCE: (33), (35) imply: % 267.42/38.07 | | (36) ~ p(all_1731_6) % 267.42/38.07 | | % 267.42/38.07 | | PRED_UNIFY: (7), (36) imply: % 267.42/38.07 | | (37) $false % 267.42/38.07 | | % 267.42/38.07 | | CLOSE: (37) is inconsistent. % 267.42/38.07 | | % 267.42/38.07 | End of split % 267.42/38.07 | % 267.42/38.07 End of proof % 267.42/38.07 % SZS output end Proof for theBenchmark % 267.42/38.08 % 267.42/38.08 37490ms %------------------------------------------------------------------------------