%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP004_1 : TPTP v8.1.2. Bugfixed v7.5.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 04:08:22 EDT 2023 % Result : Theorem 28.74s 4.63s % Output : Proof 46.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : ITP004_1 : TPTP v8.1.2. Bugfixed v7.5.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n025.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Sun Aug 27 13:42:39 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.62 ________ _____ % 0.20/0.62 ___ __ \_________(_)________________________________ % 0.20/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.62 % 0.20/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.62 (2023-06-19) % 0.20/0.62 % 0.20/0.62 (c) Philipp Rümmer, 2009-2023 % 0.20/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.62 Amanda Stjerna. % 0.20/0.62 Free software under BSD-3-Clause. % 0.20/0.62 % 0.20/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.62 % 0.20/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.62/1.21 Prover 4: Preprocessing ... % 3.62/1.21 Prover 1: Preprocessing ... % 3.74/1.25 Prover 6: Preprocessing ... % 3.74/1.25 Prover 0: Preprocessing ... % 3.74/1.25 Prover 3: Preprocessing ... % 3.74/1.25 Prover 2: Preprocessing ... % 3.74/1.25 Prover 5: Preprocessing ... % 9.34/2.01 Prover 1: Warning: ignoring some quantifiers % 9.88/2.08 Prover 4: Warning: ignoring some quantifiers % 9.88/2.09 Prover 3: Warning: ignoring some quantifiers % 9.88/2.12 Prover 1: Constructing countermodel ... % 9.88/2.13 Prover 6: Proving ... % 9.88/2.15 Prover 0: Proving ... % 9.88/2.15 Prover 4: Constructing countermodel ... % 9.88/2.16 Prover 3: Constructing countermodel ... % 11.77/2.34 Prover 5: Proving ... % 11.77/2.37 Prover 2: Proving ... % 17.82/3.14 Prover 3: gave up % 17.82/3.14 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.31/3.22 Prover 7: Preprocessing ... % 20.57/3.51 Prover 7: Warning: ignoring some quantifiers % 20.57/3.52 Prover 7: Constructing countermodel ... % 21.19/3.74 Prover 1: gave up % 21.19/3.76 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 23.03/3.84 Prover 8: Preprocessing ... % 24.66/4.07 Prover 8: Warning: ignoring some quantifiers % 24.85/4.10 Prover 8: Constructing countermodel ... % 28.74/4.62 Prover 0: proved (3986ms) % 28.74/4.62 % 28.74/4.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.74/4.63 % 28.74/4.65 Prover 2: stopped % 28.74/4.65 Prover 5: stopped % 28.74/4.66 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 28.74/4.66 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 28.74/4.66 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 29.29/4.71 Prover 6: stopped % 29.29/4.72 Prover 10: Preprocessing ... % 29.29/4.72 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 29.29/4.74 Prover 13: Preprocessing ... % 29.29/4.75 Prover 11: Preprocessing ... % 30.22/4.81 Prover 16: Preprocessing ... % 30.45/4.87 Prover 10: Warning: ignoring some quantifiers % 30.45/4.89 Prover 10: Constructing countermodel ... % 30.45/4.97 Prover 11: Warning: ignoring some quantifiers % 30.45/4.99 Prover 11: Constructing countermodel ... % 31.20/5.06 Prover 16: Warning: ignoring some quantifiers % 31.20/5.07 Prover 16: Constructing countermodel ... % 32.26/5.10 Prover 13: Warning: ignoring some quantifiers % 32.26/5.14 Prover 13: Constructing countermodel ... % 33.36/5.28 Prover 8: gave up % 33.36/5.29 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 34.57/5.41 Prover 19: Preprocessing ... % 35.67/5.59 Prover 19: Warning: ignoring some quantifiers % 35.86/5.64 Prover 19: Constructing countermodel ... % 35.86/5.66 Prover 10: gave up % 45.43/6.80 Prover 4: Found proof (size 313) % 45.43/6.80 Prover 4: proved (6157ms) % 45.43/6.80 Prover 7: stopped % 45.43/6.80 Prover 11: stopped % 45.43/6.80 Prover 13: stopped % 45.43/6.80 Prover 16: stopped % 45.43/6.80 Prover 19: stopped % 45.43/6.80 % 45.43/6.80 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 45.43/6.80 % 45.43/6.84 % SZS output start Proof for theBenchmark % 45.43/6.84 Assumptions after simplification: % 45.43/6.84 --------------------------------- % 45.43/6.84 % 45.43/6.84 (arityeq1_2Ec_2Ebool_2E_7E_2E1) % 45.75/6.87 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Ebool_2E_7E_2E0) % 45.75/6.87 & ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: int] : (v1 = 0 | ~ (p(v0) = v1) % 45.75/6.87 | ~ mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.87 (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.87 v0) = v2 & p(v2) = 0 & mono_2Etyop_2Emin_2Ebool(v2))) & ! [v0: % 45.75/6.87 mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : ( ~ % 45.75/6.87 (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.87 v0) = v1) | ~ mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: any] : ? [v3: % 45.75/6.87 any] : (p(v1) = v3 & p(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0: % 45.75/6.87 mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : ( ~ % 45.75/6.87 (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.87 v0) = v1) | ~ mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: any] : ? [v3: % 45.75/6.87 any] : (p(v1) = v2 & p(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0: % 45.75/6.87 mono_2Etyop_2Emin_2Ebool] : ( ~ (p(v0) = 0) | ~ % 45.75/6.87 mono_2Etyop_2Emin_2Ebool(v0) | ? [v1: mono_2Etyop_2Emin_2Ebool] : ? [v2: % 45.75/6.87 int] : ( ~ (v2 = 0) & % 45.75/6.87 mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.87 v0) = v1 & p(v1) = v2 & mono_2Etyop_2Emin_2Ebool(v1))) % 45.75/6.87 % 45.75/6.87 (arityeq1_2Ec_2Epred__set_2ECHOICE_2E1_2Emono_2EA_27a) % 45.75/6.87 d(tyop_2Emin_2Ebool) & u(c_2Epred__set_2ECHOICE_2E0) & ! [v0: d] : ! [v1: u] % 45.75/6.87 : ! [v2: d] : ! [v3: du] : ( ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = % 45.75/6.87 v2) | ~ (s(v2, v1) = v3) | ~ d(v0) | ~ u(v1) | ? [v4: u] : ? [v5: du] % 45.75/6.87 : ? [v6: d] : ? [v7: du] : ? [v8: u] : (c_2Epred__set_2ECHOICE_2E1(v3) = % 45.75/6.87 v4 & tyop_2Emin_2Efun(v2, v0) = v6 & app_2E2(v7, v3) = v8 & s(v6, % 45.75/6.87 c_2Epred__set_2ECHOICE_2E0) = v7 & s(v0, v8) = v5 & s(v0, v4) = v5 & % 45.75/6.87 du(v7) & du(v5) & d(v6) & u(v8) & u(v4))) % 45.75/6.87 % 45.75/6.87 (arityeq1_2Ec_2Epred__set_2EREST_2E1_2Emono_2EA_27a) % 45.75/6.88 d(tyop_2Emin_2Ebool) & u(c_2Epred__set_2EREST_2E0) & ! [v0: d] : ! [v1: u] : % 45.75/6.88 ! [v2: d] : ! [v3: du] : ( ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v2) % 45.75/6.88 | ~ (s(v2, v1) = v3) | ~ d(v0) | ~ u(v1) | ? [v4: u] : ? [v5: du] : ? % 45.75/6.88 [v6: d] : ? [v7: du] : ? [v8: u] : (c_2Epred__set_2EREST_2E1(v3) = v4 & % 45.75/6.88 tyop_2Emin_2Efun(v2, v2) = v6 & app_2E2(v7, v3) = v8 & s(v6, % 45.75/6.88 c_2Epred__set_2EREST_2E0) = v7 & s(v2, v8) = v5 & s(v2, v4) = v5 & % 45.75/6.88 du(v7) & du(v5) & d(v6) & u(v8) & u(v4))) % 45.75/6.88 % 45.75/6.88 (arityeq2_2Ec_2Ebool_2EIN_2E2_2Emono_2EA_27a) % 45.75/6.88 d(tyop_2Emin_2Ebool) & u(c_2Ebool_2EIN_2E0) & ! [v0: d] : ! [v1: u] : ! % 45.75/6.88 [v2: u] : ! [v3: du] : ! [v4: d] : ! [v5: du] : ! [v6: d] : ! [v7: d] : % 45.75/6.88 ! [v8: du] : ! [v9: u] : ! [v10: du] : ! [v11: u] : ( ~ % 45.75/6.88 (tyop_2Emin_2Efun(v4, tyop_2Emin_2Ebool) = v6) | ~ (tyop_2Emin_2Efun(v0, % 45.75/6.88 v6) = v7) | ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v4) | ~ % 45.75/6.88 (app_2E2(v10, v5) = v11) | ~ (app_2E2(v8, v3) = v9) | ~ (s(v7, % 45.75/6.88 c_2Ebool_2EIN_2E0) = v8) | ~ (s(v6, v9) = v10) | ~ (s(v4, v2) = v5) | % 45.75/6.88 ~ (s(v0, v1) = v3) | ~ d(v0) | ~ u(v2) | ~ u(v1) | ? [v12: u] : ? [v13: % 45.75/6.88 du] : ? [v14: mono_2Etyop_2Emin_2Ebool] : ? [v15: du] : % 45.75/6.88 (c_2Ebool_2EIN_2E2(v3, v5) = v12 & j_mono_2Etyop_2Emin_2Ebool(v15) = v14 & % 45.75/6.88 j_mono_2Etyop_2Emin_2Ebool(v13) = v14 & s(tyop_2Emin_2Ebool, v12) = v13 & % 45.75/6.88 s(tyop_2Emin_2Ebool, v11) = v15 & mono_2Etyop_2Emin_2Ebool(v14) & du(v15) % 45.75/6.88 & du(v13) & u(v12))) & ! [v0: d] : ! [v1: u] : ! [v2: u] : ! [v3: du] % 45.75/6.88 : ! [v4: d] : ! [v5: du] : ! [v6: u] : ( ~ (c_2Ebool_2EIN_2E2(v3, v5) = v6) % 45.75/6.88 | ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v4) | ~ (s(v4, v2) = v5) | % 45.75/6.88 ~ (s(v0, v1) = v3) | ~ d(v0) | ~ u(v2) | ~ u(v1) | ? [v7: du] : ? [v8: % 45.75/6.88 mono_2Etyop_2Emin_2Ebool] : ? [v9: d] : ? [v10: d] : ? [v11: du] : ? % 45.75/6.88 [v12: u] : ? [v13: du] : ? [v14: u] : ? [v15: du] : % 45.75/6.88 (j_mono_2Etyop_2Emin_2Ebool(v15) = v8 & j_mono_2Etyop_2Emin_2Ebool(v7) = v8 % 45.75/6.88 & tyop_2Emin_2Efun(v4, tyop_2Emin_2Ebool) = v9 & tyop_2Emin_2Efun(v0, v9) % 45.75/6.88 = v10 & app_2E2(v13, v5) = v14 & app_2E2(v11, v3) = v12 & s(v10, % 45.75/6.88 c_2Ebool_2EIN_2E0) = v11 & s(v9, v12) = v13 & s(tyop_2Emin_2Ebool, v14) % 45.75/6.88 = v15 & s(tyop_2Emin_2Ebool, v6) = v7 & mono_2Etyop_2Emin_2Ebool(v8) & % 45.75/6.88 du(v15) & du(v13) & du(v11) & du(v7) & d(v10) & d(v9) & u(v14) & u(v12))) % 45.75/6.88 % 45.75/6.88 (arityeq2_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2EA_27a) % 45.75/6.88 d(tyop_2Emin_2Ebool) & u(c_2Epred__set_2ESUBSET_2E0) & ! [v0: d] : ! [v1: u] % 45.75/6.88 : ! [v2: u] : ! [v3: d] : ! [v4: du] : ! [v5: du] : ! [v6: d] : ! [v7: % 45.75/6.88 d] : ! [v8: du] : ! [v9: u] : ! [v10: du] : ! [v11: u] : ( ~ % 45.75/6.88 (tyop_2Emin_2Efun(v3, v6) = v7) | ~ (tyop_2Emin_2Efun(v3, % 45.75/6.88 tyop_2Emin_2Ebool) = v6) | ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = % 45.75/6.88 v3) | ~ (app_2E2(v10, v5) = v11) | ~ (app_2E2(v8, v4) = v9) | ~ (s(v7, % 45.75/6.88 c_2Epred__set_2ESUBSET_2E0) = v8) | ~ (s(v6, v9) = v10) | ~ (s(v3, v2) % 45.75/6.89 = v5) | ~ (s(v3, v1) = v4) | ~ d(v0) | ~ u(v2) | ~ u(v1) | ? [v12: u] % 45.75/6.89 : ? [v13: du] : ? [v14: mono_2Etyop_2Emin_2Ebool] : ? [v15: du] : % 45.75/6.89 (c_2Epred__set_2ESUBSET_2E2(v4, v5) = v12 & j_mono_2Etyop_2Emin_2Ebool(v15) % 45.75/6.89 = v14 & j_mono_2Etyop_2Emin_2Ebool(v13) = v14 & s(tyop_2Emin_2Ebool, v12) % 45.75/6.89 = v13 & s(tyop_2Emin_2Ebool, v11) = v15 & mono_2Etyop_2Emin_2Ebool(v14) & % 45.75/6.89 du(v15) & du(v13) & u(v12))) & ! [v0: d] : ! [v1: u] : ! [v2: u] : ! % 45.75/6.89 [v3: d] : ! [v4: du] : ! [v5: du] : ! [v6: u] : ( ~ % 45.75/6.89 (c_2Epred__set_2ESUBSET_2E2(v4, v5) = v6) | ~ (tyop_2Emin_2Efun(v0, % 45.75/6.89 tyop_2Emin_2Ebool) = v3) | ~ (s(v3, v2) = v5) | ~ (s(v3, v1) = v4) | % 45.75/6.89 ~ d(v0) | ~ u(v2) | ~ u(v1) | ? [v7: du] : ? [v8: % 45.75/6.89 mono_2Etyop_2Emin_2Ebool] : ? [v9: d] : ? [v10: d] : ? [v11: du] : ? % 45.75/6.89 [v12: u] : ? [v13: du] : ? [v14: u] : ? [v15: du] : % 45.75/6.89 (j_mono_2Etyop_2Emin_2Ebool(v15) = v8 & j_mono_2Etyop_2Emin_2Ebool(v7) = v8 % 45.75/6.89 & tyop_2Emin_2Efun(v3, v9) = v10 & tyop_2Emin_2Efun(v3, tyop_2Emin_2Ebool) % 45.75/6.89 = v9 & app_2E2(v13, v5) = v14 & app_2E2(v11, v4) = v12 & s(v10, % 45.75/6.89 c_2Epred__set_2ESUBSET_2E0) = v11 & s(v9, v12) = v13 & % 45.75/6.89 s(tyop_2Emin_2Ebool, v14) = v15 & s(tyop_2Emin_2Ebool, v6) = v7 & % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v8) & du(v15) & du(v13) & du(v11) & du(v7) & % 45.75/6.89 d(v10) & d(v9) & u(v14) & u(v12))) % 45.75/6.89 % 45.75/6.89 (ij_2Emono_2Etyop_2Emin_2Ebool) % 45.75/6.89 d(tyop_2Emin_2Ebool) & ! [v0: u] : ! [v1: du] : ( ~ (s(tyop_2Emin_2Ebool, % 45.75/6.89 v0) = v1) | ~ u(v0) | ? [v2: mono_2Etyop_2Emin_2Ebool] : ? [v3: u] : % 45.75/6.89 (i_mono_2Etyop_2Emin_2Ebool(v2) = v3 & j_mono_2Etyop_2Emin_2Ebool(v1) = v2 & % 45.75/6.89 s(tyop_2Emin_2Ebool, v3) = v1 & mono_2Etyop_2Emin_2Ebool(v2) & du(v1) & % 45.75/6.89 u(v3))) % 45.75/6.89 % 45.75/6.89 (reserved_2Eho_2Ebool__cases__ax) % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) & % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) & ? [v0: % 45.75/6.89 mono_2Etyop_2Emin_2Ebool] : (v0 = mono_2Ec_2Ebool_2ET_2E0 | v0 = % 45.75/6.89 mono_2Ec_2Ebool_2EF_2E0 | ~ mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.89 % 45.75/6.89 (reserved_2Eho_2Eboolext) % 45.75/6.89 ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : ! % 45.75/6.89 [v2: int] : ! [v3: int] : (v3 = 0 | v2 = 0 | v1 = v0 | ~ (p(v1) = v3) | ~ % 45.75/6.89 (p(v0) = v2) | ~ mono_2Etyop_2Emin_2Ebool(v1) | ~ % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v0)) & ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: % 45.75/6.89 mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | ~ (p(v1) = 0) | ~ (p(v0) = 0) | ~ % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v1) | ~ mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.89 % 45.75/6.89 (reserved_2Eho_2Ei__thm) % 45.75/6.89 u(combin_i_2E0) & ! [v0: d] : ! [v1: u] : ! [v2: du] : ( ~ (s(v0, v1) = v2) % 45.75/6.89 | ~ d(v0) | ~ u(v1) | ? [v3: d] : ? [v4: du] : ? [v5: u] : % 45.75/6.89 (tyop_2Emin_2Efun(v0, v0) = v3 & app_2E2(v4, v2) = v5 & s(v3, combin_i_2E0) % 45.75/6.89 = v4 & s(v0, v5) = v2 & du(v4) & du(v2) & d(v3) & u(v5))) % 45.75/6.89 % 45.75/6.89 (reserved_2Eho_2Enotfalse) % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) & ? [v0: int] : ( ~ (v0 = % 45.75/6.89 0) & p(mono_2Ec_2Ebool_2EF_2E0) = v0) % 45.75/6.89 % 45.75/6.89 (reserved_2Eho_2Etruth) % 45.75/6.89 p(mono_2Ec_2Ebool_2ET_2E0) = 0 & % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) % 45.75/6.89 % 45.75/6.89 (reserved_2Elogic_2E_7E) % 45.75/6.89 ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: int] : (v1 = 0 | ~ (p(v0) = v1) | % 45.75/6.89 ~ mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.89 (mono_2Ec_2Ebool_2E_7E_2E1(v0) = v2 & p(v2) = 0 & % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v2))) & ! [v0: mono_2Etyop_2Emin_2Ebool] : ! % 45.75/6.89 [v1: mono_2Etyop_2Emin_2Ebool] : ( ~ (mono_2Ec_2Ebool_2E_7E_2E1(v0) = v1) | ~ % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: any] : ? [v3: any] : (p(v1) = v3 & % 45.75/6.89 p(v0) = v2 & (v3 = 0 | v2 = 0))) & ! [v0: mono_2Etyop_2Emin_2Ebool] : ! % 45.75/6.89 [v1: mono_2Etyop_2Emin_2Ebool] : ( ~ (mono_2Ec_2Ebool_2E_7E_2E1(v0) = v1) | ~ % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: any] : ? [v3: any] : (p(v1) = v2 & % 45.75/6.89 p(v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0: % 45.75/6.89 mono_2Etyop_2Emin_2Ebool] : ( ~ (p(v0) = 0) | ~ % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v0) | ? [v1: mono_2Etyop_2Emin_2Ebool] : ? [v2: % 45.75/6.89 int] : ( ~ (v2 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(v0) = v1 & p(v1) = v2 & % 45.75/6.89 mono_2Etyop_2Emin_2Ebool(v1))) % 45.75/6.89 % 45.75/6.89 (thm_2Epred__set_2EIN__DELETE) % 45.75/6.90 d(tyop_2Emin_2Ebool) & ! [v0: d] : ! [v1: u] : ! [v2: u] : ! [v3: u] : ! % 45.75/6.90 [v4: du] : ! [v5: d] : ! [v6: du] : ! [v7: du] : ! [v8: u] : ! [v9: du] : % 45.75/6.90 ! [v10: u] : (v7 = v4 | ~ (c_2Ebool_2EIN_2E2(v4, v9) = v10) | ~ % 45.75/6.90 (c_2Epred__set_2EDELETE_2E2(v6, v7) = v8) | ~ (tyop_2Emin_2Efun(v0, % 45.75/6.90 tyop_2Emin_2Ebool) = v5) | ~ (s(v5, v8) = v9) | ~ (s(v5, v1) = v6) | % 45.75/6.90 ~ (s(v0, v3) = v7) | ~ (s(v0, v2) = v4) | ~ d(v0) | ~ u(v3) | ~ u(v2) | % 45.75/6.90 ~ u(v1) | ? [v11: u] : ? [v12: du] : ? [v13: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.90 ? [v14: any] : ? [v15: du] : ? [v16: mono_2Etyop_2Emin_2Ebool] : ? [v17: % 45.75/6.90 any] : (c_2Ebool_2EIN_2E2(v4, v6) = v11 & j_mono_2Etyop_2Emin_2Ebool(v15) % 45.75/6.90 = v16 & j_mono_2Etyop_2Emin_2Ebool(v12) = v13 & p(v16) = v17 & p(v13) = % 45.75/6.90 v14 & s(tyop_2Emin_2Ebool, v11) = v12 & s(tyop_2Emin_2Ebool, v10) = v15 & % 45.75/6.90 mono_2Etyop_2Emin_2Ebool(v16) & mono_2Etyop_2Emin_2Ebool(v13) & du(v15) & % 45.75/6.90 du(v12) & u(v11) & ( ~ (v14 = 0) | v17 = 0))) & ! [v0: d] : ! [v1: u] : % 45.75/6.90 ! [v2: u] : ! [v3: u] : ! [v4: du] : ! [v5: d] : ! [v6: du] : ! [v7: du] % 45.75/6.90 : ! [v8: u] : ! [v9: du] : ! [v10: u] : ( ~ (c_2Ebool_2EIN_2E2(v4, v9) = % 45.75/6.90 v10) | ~ (c_2Epred__set_2EDELETE_2E2(v6, v7) = v8) | ~ % 45.75/6.90 (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v5) | ~ (s(v5, v8) = v9) | ~ % 45.75/6.90 (s(v5, v1) = v6) | ~ (s(v0, v3) = v7) | ~ (s(v0, v2) = v4) | ~ d(v0) | ~ % 45.75/6.90 u(v3) | ~ u(v2) | ~ u(v1) | ? [v11: du] : ? [v12: % 45.75/6.90 mono_2Etyop_2Emin_2Ebool] : ? [v13: any] : ? [v14: u] : ? [v15: du] : % 45.75/6.90 ? [v16: mono_2Etyop_2Emin_2Ebool] : ? [v17: any] : (c_2Ebool_2EIN_2E2(v4, % 45.75/6.90 v6) = v14 & j_mono_2Etyop_2Emin_2Ebool(v15) = v16 & % 45.75/6.90 j_mono_2Etyop_2Emin_2Ebool(v11) = v12 & p(v16) = v17 & p(v12) = v13 & % 45.75/6.90 s(tyop_2Emin_2Ebool, v14) = v15 & s(tyop_2Emin_2Ebool, v10) = v11 & % 45.75/6.90 mono_2Etyop_2Emin_2Ebool(v16) & mono_2Etyop_2Emin_2Ebool(v12) & du(v15) & % 45.75/6.90 du(v11) & u(v14) & ( ~ (v13 = 0) | (v17 = 0 & ~ (v7 = v4))))) % 45.75/6.90 % 45.75/6.90 (thm_2Epred__set_2EREST__DEF) % 45.75/6.90 d(tyop_2Emin_2Ebool) & ! [v0: d] : ! [v1: u] : ! [v2: d] : ! [v3: du] : ( % 45.75/6.90 ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v2) | ~ (s(v2, v1) = v3) | ~ % 45.75/6.90 d(v0) | ~ u(v1) | ? [v4: u] : ? [v5: du] : ? [v6: u] : ? [v7: du] : ? % 45.75/6.90 [v8: u] : (c_2Epred__set_2EREST_2E1(v3) = v4 & % 45.75/6.90 c_2Epred__set_2EDELETE_2E2(v3, v7) = v8 & c_2Epred__set_2ECHOICE_2E1(v3) = % 45.75/6.90 v6 & s(v2, v8) = v5 & s(v2, v4) = v5 & s(v0, v6) = v7 & du(v7) & du(v5) & % 45.75/6.90 u(v8) & u(v6) & u(v4))) % 45.75/6.90 % 45.75/6.90 (thm_2Epred__set_2EREST__SUBSET) % 45.75/6.90 d(tyop_2Emin_2Ebool) & ? [v0: d] : ? [v1: u] : ? [v2: d] : ? [v3: du] : ? % 45.75/6.90 [v4: u] : ? [v5: du] : ? [v6: u] : ? [v7: du] : ? [v8: % 45.75/6.90 mono_2Etyop_2Emin_2Ebool] : ? [v9: int] : ( ~ (v9 = 0) & % 45.75/6.90 c_2Epred__set_2ESUBSET_2E2(v5, v3) = v6 & c_2Epred__set_2EREST_2E1(v3) = v4 % 45.75/6.90 & j_mono_2Etyop_2Emin_2Ebool(v7) = v8 & p(v8) = v9 & tyop_2Emin_2Efun(v0, % 45.75/6.90 tyop_2Emin_2Ebool) = v2 & s(v2, v4) = v5 & s(v2, v1) = v3 & % 45.75/6.90 s(tyop_2Emin_2Ebool, v6) = v7 & mono_2Etyop_2Emin_2Ebool(v8) & du(v7) & % 45.75/6.90 du(v5) & du(v3) & d(v2) & d(v0) & u(v6) & u(v4) & u(v1)) % 45.75/6.90 % 45.75/6.90 (thm_2Epred__set_2ESUBSET__DEF) % 45.75/6.90 d(tyop_2Emin_2Ebool) & ! [v0: d] : ! [v1: u] : ! [v2: u] : ! [v3: d] : ! % 45.75/6.90 [v4: du] : ! [v5: du] : ! [v6: u] : ! [v7: u] : ! [v8: du] : ( ~ % 45.75/6.90 (c_2Epred__set_2ESUBSET_2E2(v4, v5) = v6) | ~ (tyop_2Emin_2Efun(v0, % 45.75/6.90 tyop_2Emin_2Ebool) = v3) | ~ (s(v3, v2) = v5) | ~ (s(v3, v1) = v4) | % 45.75/6.90 ~ (s(v0, v7) = v8) | ~ d(v0) | ~ u(v7) | ~ u(v2) | ~ u(v1) | ? [v9: % 45.75/6.90 any] : ? [v10: any] : ? [v11: any] : ? [v12: any] : ? [v13: u] : ? % 45.75/6.90 [v14: du] : ? [v15: mono_2Etyop_2Emin_2Ebool] : ? [v16: any] : (( ~ (v11 = % 45.75/6.90 0) & j_mono_2Etyop_2Emin_2Ebool(v9) = v10 & p(v10) = v11 & % 45.75/6.90 s(tyop_2Emin_2Ebool, v6) = v9 & mono_2Etyop_2Emin_2Ebool(v10) & du(v9)) % 45.75/6.90 | (c_2Ebool_2EIN_2E2(v8, v5) = v13 & c_2Ebool_2EIN_2E2(v8, v4) = v9 & % 45.75/6.90 j_mono_2Etyop_2Emin_2Ebool(v14) = v15 & j_mono_2Etyop_2Emin_2Ebool(v10) % 45.75/6.90 = v11 & p(v15) = v16 & p(v11) = v12 & s(tyop_2Emin_2Ebool, v13) = v14 & % 45.75/6.91 s(tyop_2Emin_2Ebool, v9) = v10 & mono_2Etyop_2Emin_2Ebool(v15) & % 45.75/6.91 mono_2Etyop_2Emin_2Ebool(v11) & du(v14) & du(v10) & u(v13) & u(v9) & ( ~ % 45.75/6.91 (v12 = 0) | v16 = 0)))) & ! [v0: d] : ! [v1: u] : ! [v2: u] : ! % 45.75/6.91 [v3: d] : ! [v4: du] : ! [v5: du] : ! [v6: u] : ( ~ % 45.75/6.91 (c_2Epred__set_2ESUBSET_2E2(v4, v5) = v6) | ~ (tyop_2Emin_2Efun(v0, % 45.75/6.91 tyop_2Emin_2Ebool) = v3) | ~ (s(v3, v2) = v5) | ~ (s(v3, v1) = v4) | % 45.75/6.91 ~ d(v0) | ~ u(v2) | ~ u(v1) | ? [v7: du] : ? [v8: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : ? [v9: int] : ? [v10: u] : ? [v11: du] : ? % 45.75/6.91 [v12: u] : ? [v13: du] : ? [v14: mono_2Etyop_2Emin_2Ebool] : ? [v15: int] % 45.75/6.91 : ? [v16: u] : ? [v17: du] : ? [v18: mono_2Etyop_2Emin_2Ebool] : ? [v19: % 45.75/6.91 int] : (u(v10) & ((v15 = 0 & ~ (v19 = 0) & c_2Ebool_2EIN_2E2(v11, v5) = % 45.75/6.91 v16 & c_2Ebool_2EIN_2E2(v11, v4) = v12 & % 45.75/6.91 j_mono_2Etyop_2Emin_2Ebool(v17) = v18 & % 45.75/6.91 j_mono_2Etyop_2Emin_2Ebool(v13) = v14 & p(v18) = v19 & p(v14) = 0 & % 45.75/6.91 s(v0, v10) = v11 & s(tyop_2Emin_2Ebool, v16) = v17 & % 45.75/6.91 s(tyop_2Emin_2Ebool, v12) = v13 & mono_2Etyop_2Emin_2Ebool(v18) & % 45.75/6.91 mono_2Etyop_2Emin_2Ebool(v14) & du(v17) & du(v13) & du(v11) & u(v16) & % 45.75/6.91 u(v12)) | (v9 = 0 & j_mono_2Etyop_2Emin_2Ebool(v7) = v8 & p(v8) = 0 & % 45.75/6.91 s(tyop_2Emin_2Ebool, v6) = v7 & mono_2Etyop_2Emin_2Ebool(v8) & % 45.75/6.91 du(v7))))) % 45.75/6.91 % 45.75/6.91 (function-axioms) % 45.75/6.91 ! [v0: u] : ! [v1: u] : ! [v2: du] : ! [v3: du] : (v1 = v0 | ~ % 45.75/6.91 (c_2Epred__set_2ESUBSET_2E2(v3, v2) = v1) | ~ % 45.75/6.91 (c_2Epred__set_2ESUBSET_2E2(v3, v2) = v0)) & ! [v0: u] : ! [v1: u] : ! % 45.75/6.91 [v2: du] : ! [v3: du] : (v1 = v0 | ~ (c_2Ebool_2EIN_2E2(v3, v2) = v1) | ~ % 45.75/6.91 (c_2Ebool_2EIN_2E2(v3, v2) = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: du] : % 45.75/6.91 ! [v3: du] : (v1 = v0 | ~ (c_2Epred__set_2EDELETE_2E2(v3, v2) = v1) | ~ % 45.75/6.91 (c_2Epred__set_2EDELETE_2E2(v3, v2) = v0)) & ! [v0: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29] : ! % 45.75/6.91 [v1: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29] : ! % 45.75/6.91 [v2: mono_2Etyop_2Emin_2Ebool] : ! [v3: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29] % 45.75/6.91 : (v1 = v0 | ~ % 45.75/6.91 (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29(v3, % 45.75/6.91 v2) = v1) | ~ % 45.75/6.91 (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29(v3, % 45.75/6.91 v2) = v0)) & ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : ! [v2: mono_2Etyop_2Emin_2Ebool] : ! [v3: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29] : (v1 = % 45.75/6.91 v0 | ~ % 45.75/6.91 (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(v3, % 45.75/6.91 v2) = v1) | ~ % 45.75/6.91 (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(v3, % 45.75/6.91 v2) = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: du] : ! [v3: du] : (v1 = % 45.75/6.91 v0 | ~ (c_2Emin_2E_3D_2E2(v3, v2) = v1) | ~ (c_2Emin_2E_3D_2E2(v3, v2) = % 45.75/6.91 v0)) & ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : ! [v2: mono_2Etyop_2Emin_2Ebool] : ! [v3: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | ~ % 45.75/6.91 (mono_2Ec_2Emin_2E_3D_3D_3E_2E2(v3, v2) = v1) | ~ % 45.75/6.91 (mono_2Ec_2Emin_2E_3D_3D_3E_2E2(v3, v2) = v0)) & ! [v0: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : ! [v2: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : ! [v3: mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | % 45.75/6.91 ~ (mono_2Ec_2Ebool_2E_5C_2F_2E2(v3, v2) = v1) | ~ % 45.75/6.91 (mono_2Ec_2Ebool_2E_5C_2F_2E2(v3, v2) = v0)) & ! [v0: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : ! [v2: % 45.75/6.91 mono_2Etyop_2Emin_2Ebool] : ! [v3: mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | % 45.75/6.91 ~ (mono_2Ec_2Ebool_2E_2F_5C_2E2(v3, v2) = v1) | ~ % 45.75/6.91 (mono_2Ec_2Ebool_2E_2F_5C_2E2(v3, v2) = v0)) & ! [v0: d] : ! [v1: d] : ! % 45.75/6.91 [v2: d] : ! [v3: d] : (v1 = v0 | ~ (tyop_2Emin_2Efun(v3, v2) = v1) | ~ % 45.75/6.91 (tyop_2Emin_2Efun(v3, v2) = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: du] : % 45.75/6.91 ! [v3: du] : (v1 = v0 | ~ (app_2E2(v3, v2) = v1) | ~ (app_2E2(v3, v2) = v0)) % 45.75/6.91 & ! [v0: du] : ! [v1: du] : ! [v2: u] : ! [v3: d] : (v1 = v0 | ~ (s(v3, % 45.75/6.91 v2) = v1) | ~ (s(v3, v2) = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: du] % 45.75/6.91 : (v1 = v0 | ~ (c_2Epred__set_2EREST_2E1(v2) = v1) | ~ % 45.75/6.91 (c_2Epred__set_2EREST_2E1(v2) = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: du] % 45.75/6.91 : (v1 = v0 | ~ (c_2Epred__set_2ECHOICE_2E1(v2) = v1) | ~ % 45.75/6.91 (c_2Epred__set_2ECHOICE_2E1(v2) = v0)) & ! [v0: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29] % 45.75/6.91 : ! [v1: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29] % 45.75/6.91 : ! [v2: du] : (v1 = v0 | ~ % 45.75/6.91 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29(v2) % 45.75/6.91 = v1) | ~ % 45.75/6.91 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29(v2) % 45.75/6.91 = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29] % 45.75/6.91 : (v1 = v0 | ~ % 45.75/6.91 (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29(v2) % 45.75/6.91 = v1) | ~ % 45.75/6.91 (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29(v2) % 45.75/6.91 = v0)) & ! [v0: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29] : ! % 45.75/6.91 [v1: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29] : ! % 45.75/6.91 [v2: du] : (v1 = v0 | ~ % 45.75/6.91 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29(v2) = % 45.75/6.91 v1) | ~ % 45.75/6.91 (j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29(v2) = % 45.75/6.91 v0)) & ! [v0: u] : ! [v1: u] : ! [v2: % 45.75/6.91 mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29] : (v1 = % 45.75/6.91 v0 | ~ % 45.75/6.91 (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29(v2) = % 45.75/6.91 v1) | ~ % 45.75/6.91 (i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29(v2) = % 45.75/6.91 v0)) & ! [v0: u] : ! [v1: u] : ! [v2: mono_2Etyop_2Emin_2Ebool] : (v1 = % 45.75/6.91 v0 | ~ (i_mono_2Etyop_2Emin_2Ebool(v2) = v1) | ~ % 45.75/6.91 (i_mono_2Etyop_2Emin_2Ebool(v2) = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: % 45.75/6.91 du] : (v1 = v0 | ~ (c_2Ebool_2E_3F_2E1(v2) = v1) | ~ % 45.75/6.91 (c_2Ebool_2E_3F_2E1(v2) = v0)) & ! [v0: u] : ! [v1: u] : ! [v2: du] : (v1 % 45.75/6.91 = v0 | ~ (c_2Ebool_2E_21_2E1(v2) = v1) | ~ (c_2Ebool_2E_21_2E1(v2) = v0)) % 45.75/6.91 & ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : ! % 45.75/6.91 [v2: du] : (v1 = v0 | ~ (j_mono_2Etyop_2Emin_2Ebool(v2) = v1) | ~ % 45.75/6.91 (j_mono_2Etyop_2Emin_2Ebool(v2) = v0)) & ! [v0: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.91 ! [v1: mono_2Etyop_2Emin_2Ebool] : ! [v2: mono_2Etyop_2Emin_2Ebool] : (v1 = % 45.75/6.91 v0 | ~ (mono_2Ec_2Ebool_2E_7E_2E1(v2) = v1) | ~ % 45.75/6.91 (mono_2Ec_2Ebool_2E_7E_2E1(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 45.75/6.91 MultipleValueBool] : ! [v2: mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | ~ % 45.75/6.91 (p(v2) = v1) | ~ (p(v2) = v0)) % 45.75/6.91 % 45.75/6.91 Further assumptions not needed in the proof: % 45.75/6.91 -------------------------------------------- % 45.75/6.91 arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a, % 45.75/6.91 arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a, arityeq2_2Ec_2Ebool_2E_2F_5C_2E2, % 45.75/6.91 arityeq2_2Ec_2Ebool_2E_5C_2F_2E2, arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a, % 45.75/6.91 arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2, % 45.75/6.91 arityeq2_2Ec_2Epred__set_2EDELETE_2E2_2Emono_2EA_27a, % 45.75/6.91 ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29, % 45.75/6.91 ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29, % 45.75/6.91 ji_2Emono_2Etyop_2Emin_2Ebool, % 45.75/6.91 ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29, % 45.75/6.91 ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29, % 45.75/6.91 monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool, % 45.75/6.91 monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29, % 45.75/6.91 reserved_2Eho_2Eeq__ext, reserved_2Eho_2Ek__thm, reserved_2Eho_2Es__thm, % 45.75/6.91 reserved_2Elogic_2E_2F_5C, reserved_2Elogic_2E_3D, reserved_2Elogic_2E_3D_3D_3E, % 45.75/6.91 reserved_2Elogic_2E_5C_2F, reserved_2Equant_2E_21, reserved_2Equant_2E_3F % 45.75/6.91 % 45.75/6.91 Those formulas are unsatisfiable: % 45.75/6.91 --------------------------------- % 45.75/6.91 % 45.75/6.91 Begin of proof % 45.75/6.92 | % 45.75/6.92 | ALPHA: (reserved_2Eho_2Eboolext) implies: % 45.75/6.92 | (1) ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.92 | (v1 = v0 | ~ (p(v1) = 0) | ~ (p(v0) = 0) | ~ % 45.75/6.92 | mono_2Etyop_2Emin_2Ebool(v1) | ~ mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.92 | (2) ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.92 | ! [v2: int] : ! [v3: int] : (v3 = 0 | v2 = 0 | v1 = v0 | ~ (p(v1) = % 45.75/6.92 | v3) | ~ (p(v0) = v2) | ~ mono_2Etyop_2Emin_2Ebool(v1) | ~ % 45.75/6.92 | mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.92 | % 45.75/6.92 | ALPHA: (reserved_2Eho_2Etruth) implies: % 45.75/6.92 | (3) p(mono_2Ec_2Ebool_2ET_2E0) = 0 % 45.75/6.92 | % 45.75/6.92 | ALPHA: (reserved_2Eho_2Enotfalse) implies: % 45.75/6.92 | (4) ? [v0: int] : ( ~ (v0 = 0) & p(mono_2Ec_2Ebool_2EF_2E0) = v0) % 45.75/6.92 | % 45.75/6.92 | ALPHA: (reserved_2Eho_2Ebool__cases__ax) implies: % 45.75/6.92 | (5) mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) % 45.75/6.92 | (6) mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) % 45.75/6.92 | % 45.75/6.92 | ALPHA: (reserved_2Eho_2Ei__thm) implies: % 45.75/6.92 | (7) ! [v0: d] : ! [v1: u] : ! [v2: du] : ( ~ (s(v0, v1) = v2) | ~ d(v0) % 45.75/6.92 | | ~ u(v1) | ? [v3: d] : ? [v4: du] : ? [v5: u] : % 45.75/6.92 | (tyop_2Emin_2Efun(v0, v0) = v3 & app_2E2(v4, v2) = v5 & s(v3, % 45.75/6.92 | combin_i_2E0) = v4 & s(v0, v5) = v2 & du(v4) & du(v2) & d(v3) & % 45.75/6.92 | u(v5))) % 45.75/6.92 | % 45.75/6.92 | ALPHA: (reserved_2Elogic_2E_7E) implies: % 45.75/6.92 | (8) ! [v0: mono_2Etyop_2Emin_2Ebool] : ( ~ (p(v0) = 0) | ~ % 45.75/6.92 | mono_2Etyop_2Emin_2Ebool(v0) | ? [v1: mono_2Etyop_2Emin_2Ebool] : ? % 45.75/6.92 | [v2: int] : ( ~ (v2 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(v0) = v1 & p(v1) % 45.75/6.92 | = v2 & mono_2Etyop_2Emin_2Ebool(v1))) % 45.75/6.92 | (9) ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: int] : (v1 = 0 | ~ (p(v0) % 45.75/6.92 | = v1) | ~ mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: % 45.75/6.92 | mono_2Etyop_2Emin_2Ebool] : (mono_2Ec_2Ebool_2E_7E_2E1(v0) = v2 & % 45.75/6.92 | p(v2) = 0 & mono_2Etyop_2Emin_2Ebool(v2))) % 45.75/6.92 | % 45.75/6.92 | ALPHA: (ij_2Emono_2Etyop_2Emin_2Ebool) implies: % 45.75/6.92 | (10) ! [v0: u] : ! [v1: du] : ( ~ (s(tyop_2Emin_2Ebool, v0) = v1) | ~ % 45.75/6.92 | u(v0) | ? [v2: mono_2Etyop_2Emin_2Ebool] : ? [v3: u] : % 45.75/6.92 | (i_mono_2Etyop_2Emin_2Ebool(v2) = v3 & % 45.75/6.92 | j_mono_2Etyop_2Emin_2Ebool(v1) = v2 & s(tyop_2Emin_2Ebool, v3) = % 45.75/6.92 | v1 & mono_2Etyop_2Emin_2Ebool(v2) & du(v1) & u(v3))) % 45.75/6.92 | % 45.75/6.92 | ALPHA: (arityeq1_2Ec_2Epred__set_2ECHOICE_2E1_2Emono_2EA_27a) implies: % 45.75/6.93 | (11) ! [v0: d] : ! [v1: u] : ! [v2: d] : ! [v3: du] : ( ~ % 45.75/6.93 | (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v2) | ~ (s(v2, v1) = v3) % 45.75/6.93 | | ~ d(v0) | ~ u(v1) | ? [v4: u] : ? [v5: du] : ? [v6: d] : ? % 45.75/6.93 | [v7: du] : ? [v8: u] : (c_2Epred__set_2ECHOICE_2E1(v3) = v4 & % 45.75/6.93 | tyop_2Emin_2Efun(v2, v0) = v6 & app_2E2(v7, v3) = v8 & s(v6, % 45.75/6.93 | c_2Epred__set_2ECHOICE_2E0) = v7 & s(v0, v8) = v5 & s(v0, v4) = % 45.75/6.93 | v5 & du(v7) & du(v5) & d(v6) & u(v8) & u(v4))) % 45.75/6.93 | % 45.75/6.93 | ALPHA: (arityeq2_2Ec_2Ebool_2EIN_2E2_2Emono_2EA_27a) implies: % 45.75/6.93 | (12) ! [v0: d] : ! [v1: u] : ! [v2: u] : ! [v3: du] : ! [v4: d] : ! % 45.75/6.93 | [v5: du] : ! [v6: u] : ( ~ (c_2Ebool_2EIN_2E2(v3, v5) = v6) | ~ % 45.75/6.93 | (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v4) | ~ (s(v4, v2) = v5) % 45.75/6.93 | | ~ (s(v0, v1) = v3) | ~ d(v0) | ~ u(v2) | ~ u(v1) | ? [v7: du] % 45.75/6.93 | : ? [v8: mono_2Etyop_2Emin_2Ebool] : ? [v9: d] : ? [v10: d] : ? % 45.75/6.93 | [v11: du] : ? [v12: u] : ? [v13: du] : ? [v14: u] : ? [v15: du] % 45.75/6.93 | : (j_mono_2Etyop_2Emin_2Ebool(v15) = v8 & % 45.75/6.93 | j_mono_2Etyop_2Emin_2Ebool(v7) = v8 & tyop_2Emin_2Efun(v4, % 45.75/6.93 | tyop_2Emin_2Ebool) = v9 & tyop_2Emin_2Efun(v0, v9) = v10 & % 45.75/6.93 | app_2E2(v13, v5) = v14 & app_2E2(v11, v3) = v12 & s(v10, % 45.75/6.93 | c_2Ebool_2EIN_2E0) = v11 & s(v9, v12) = v13 & % 45.75/6.93 | s(tyop_2Emin_2Ebool, v14) = v15 & s(tyop_2Emin_2Ebool, v6) = v7 & % 45.75/6.93 | mono_2Etyop_2Emin_2Ebool(v8) & du(v15) & du(v13) & du(v11) & % 45.75/6.93 | du(v7) & d(v10) & d(v9) & u(v14) & u(v12))) % 45.75/6.93 | % 45.75/6.93 | ALPHA: (arityeq1_2Ec_2Epred__set_2EREST_2E1_2Emono_2EA_27a) implies: % 45.75/6.93 | (13) ! [v0: d] : ! [v1: u] : ! [v2: d] : ! [v3: du] : ( ~ % 45.75/6.93 | (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v2) | ~ (s(v2, v1) = v3) % 45.75/6.93 | | ~ d(v0) | ~ u(v1) | ? [v4: u] : ? [v5: du] : ? [v6: d] : ? % 45.75/6.93 | [v7: du] : ? [v8: u] : (c_2Epred__set_2EREST_2E1(v3) = v4 & % 45.75/6.93 | tyop_2Emin_2Efun(v2, v2) = v6 & app_2E2(v7, v3) = v8 & s(v6, % 45.75/6.93 | c_2Epred__set_2EREST_2E0) = v7 & s(v2, v8) = v5 & s(v2, v4) = v5 % 45.75/6.93 | & du(v7) & du(v5) & d(v6) & u(v8) & u(v4))) % 45.75/6.93 | % 45.75/6.93 | ALPHA: (arityeq2_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2EA_27a) implies: % 45.75/6.93 | (14) ! [v0: d] : ! [v1: u] : ! [v2: u] : ! [v3: d] : ! [v4: du] : ! % 45.75/6.93 | [v5: du] : ! [v6: u] : ( ~ (c_2Epred__set_2ESUBSET_2E2(v4, v5) = v6) % 45.75/6.93 | | ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v3) | ~ (s(v3, v2) % 45.75/6.93 | = v5) | ~ (s(v3, v1) = v4) | ~ d(v0) | ~ u(v2) | ~ u(v1) | ? % 45.75/6.93 | [v7: du] : ? [v8: mono_2Etyop_2Emin_2Ebool] : ? [v9: d] : ? [v10: % 45.75/6.93 | d] : ? [v11: du] : ? [v12: u] : ? [v13: du] : ? [v14: u] : ? % 45.75/6.93 | [v15: du] : (j_mono_2Etyop_2Emin_2Ebool(v15) = v8 & % 45.75/6.93 | j_mono_2Etyop_2Emin_2Ebool(v7) = v8 & tyop_2Emin_2Efun(v3, v9) = % 45.75/6.93 | v10 & tyop_2Emin_2Efun(v3, tyop_2Emin_2Ebool) = v9 & app_2E2(v13, % 45.75/6.93 | v5) = v14 & app_2E2(v11, v4) = v12 & s(v10, % 45.75/6.93 | c_2Epred__set_2ESUBSET_2E0) = v11 & s(v9, v12) = v13 & % 45.75/6.93 | s(tyop_2Emin_2Ebool, v14) = v15 & s(tyop_2Emin_2Ebool, v6) = v7 & % 45.75/6.93 | mono_2Etyop_2Emin_2Ebool(v8) & du(v15) & du(v13) & du(v11) & % 45.75/6.93 | du(v7) & d(v10) & d(v9) & u(v14) & u(v12))) % 45.75/6.93 | % 45.75/6.93 | ALPHA: (arityeq1_2Ec_2Ebool_2E_7E_2E1) implies: % 45.75/6.93 | (15) ! [v0: mono_2Etyop_2Emin_2Ebool] : ( ~ (p(v0) = 0) | ~ % 45.75/6.93 | mono_2Etyop_2Emin_2Ebool(v0) | ? [v1: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.93 | ? [v2: int] : ( ~ (v2 = 0) & % 45.75/6.93 | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.93 | v0) = v1 & p(v1) = v2 & mono_2Etyop_2Emin_2Ebool(v1))) % 45.75/6.93 | (16) ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: int] : (v1 = 0 | ~ (p(v0) % 45.75/6.93 | = v1) | ~ mono_2Etyop_2Emin_2Ebool(v0) | ? [v2: % 45.75/6.93 | mono_2Etyop_2Emin_2Ebool] : % 45.75/6.93 | (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.93 | v0) = v2 & p(v2) = 0 & mono_2Etyop_2Emin_2Ebool(v2))) % 45.75/6.93 | % 45.75/6.93 | ALPHA: (thm_2Epred__set_2ESUBSET__DEF) implies: % 45.75/6.93 | (17) ! [v0: d] : ! [v1: u] : ! [v2: u] : ! [v3: d] : ! [v4: du] : ! % 45.75/6.93 | [v5: du] : ! [v6: u] : ( ~ (c_2Epred__set_2ESUBSET_2E2(v4, v5) = v6) % 45.75/6.93 | | ~ (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v3) | ~ (s(v3, v2) % 45.75/6.93 | = v5) | ~ (s(v3, v1) = v4) | ~ d(v0) | ~ u(v2) | ~ u(v1) | ? % 45.75/6.93 | [v7: du] : ? [v8: mono_2Etyop_2Emin_2Ebool] : ? [v9: int] : ? % 45.75/6.93 | [v10: u] : ? [v11: du] : ? [v12: u] : ? [v13: du] : ? [v14: % 45.75/6.93 | mono_2Etyop_2Emin_2Ebool] : ? [v15: int] : ? [v16: u] : ? [v17: % 45.75/6.93 | du] : ? [v18: mono_2Etyop_2Emin_2Ebool] : ? [v19: int] : (u(v10) % 45.75/6.93 | & ((v15 = 0 & ~ (v19 = 0) & c_2Ebool_2EIN_2E2(v11, v5) = v16 & % 45.75/6.93 | c_2Ebool_2EIN_2E2(v11, v4) = v12 & % 45.75/6.93 | j_mono_2Etyop_2Emin_2Ebool(v17) = v18 & % 45.75/6.93 | j_mono_2Etyop_2Emin_2Ebool(v13) = v14 & p(v18) = v19 & p(v14) % 45.75/6.93 | = 0 & s(v0, v10) = v11 & s(tyop_2Emin_2Ebool, v16) = v17 & % 45.75/6.93 | s(tyop_2Emin_2Ebool, v12) = v13 & % 45.75/6.93 | mono_2Etyop_2Emin_2Ebool(v18) & mono_2Etyop_2Emin_2Ebool(v14) % 45.75/6.93 | & du(v17) & du(v13) & du(v11) & u(v16) & u(v12)) | (v9 = 0 & % 45.75/6.93 | j_mono_2Etyop_2Emin_2Ebool(v7) = v8 & p(v8) = 0 & % 45.75/6.93 | s(tyop_2Emin_2Ebool, v6) = v7 & mono_2Etyop_2Emin_2Ebool(v8) & % 45.75/6.93 | du(v7))))) % 45.75/6.93 | % 45.75/6.93 | ALPHA: (thm_2Epred__set_2EIN__DELETE) implies: % 45.75/6.94 | (18) ! [v0: d] : ! [v1: u] : ! [v2: u] : ! [v3: u] : ! [v4: du] : ! % 45.75/6.94 | [v5: d] : ! [v6: du] : ! [v7: du] : ! [v8: u] : ! [v9: du] : ! % 45.75/6.94 | [v10: u] : ( ~ (c_2Ebool_2EIN_2E2(v4, v9) = v10) | ~ % 45.75/6.94 | (c_2Epred__set_2EDELETE_2E2(v6, v7) = v8) | ~ (tyop_2Emin_2Efun(v0, % 45.75/6.94 | tyop_2Emin_2Ebool) = v5) | ~ (s(v5, v8) = v9) | ~ (s(v5, v1) = % 45.75/6.94 | v6) | ~ (s(v0, v3) = v7) | ~ (s(v0, v2) = v4) | ~ d(v0) | ~ % 45.75/6.94 | u(v3) | ~ u(v2) | ~ u(v1) | ? [v11: du] : ? [v12: % 45.75/6.94 | mono_2Etyop_2Emin_2Ebool] : ? [v13: any] : ? [v14: u] : ? [v15: % 45.75/6.94 | du] : ? [v16: mono_2Etyop_2Emin_2Ebool] : ? [v17: any] : % 45.75/6.94 | (c_2Ebool_2EIN_2E2(v4, v6) = v14 & j_mono_2Etyop_2Emin_2Ebool(v15) = % 45.75/6.94 | v16 & j_mono_2Etyop_2Emin_2Ebool(v11) = v12 & p(v16) = v17 & % 45.75/6.94 | p(v12) = v13 & s(tyop_2Emin_2Ebool, v14) = v15 & % 45.75/6.94 | s(tyop_2Emin_2Ebool, v10) = v11 & mono_2Etyop_2Emin_2Ebool(v16) & % 45.75/6.94 | mono_2Etyop_2Emin_2Ebool(v12) & du(v15) & du(v11) & u(v14) & ( ~ % 45.75/6.94 | (v13 = 0) | (v17 = 0 & ~ (v7 = v4))))) % 45.75/6.94 | % 45.75/6.94 | ALPHA: (thm_2Epred__set_2EREST__DEF) implies: % 45.75/6.94 | (19) ! [v0: d] : ! [v1: u] : ! [v2: d] : ! [v3: du] : ( ~ % 45.75/6.94 | (tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v2) | ~ (s(v2, v1) = v3) % 45.75/6.94 | | ~ d(v0) | ~ u(v1) | ? [v4: u] : ? [v5: du] : ? [v6: u] : ? % 45.75/6.94 | [v7: du] : ? [v8: u] : (c_2Epred__set_2EREST_2E1(v3) = v4 & % 45.75/6.94 | c_2Epred__set_2EDELETE_2E2(v3, v7) = v8 & % 45.75/6.94 | c_2Epred__set_2ECHOICE_2E1(v3) = v6 & s(v2, v8) = v5 & s(v2, v4) = % 45.75/6.94 | v5 & s(v0, v6) = v7 & du(v7) & du(v5) & u(v8) & u(v6) & u(v4))) % 45.75/6.94 | % 45.75/6.94 | ALPHA: (thm_2Epred__set_2EREST__SUBSET) implies: % 45.75/6.94 | (20) ? [v0: d] : ? [v1: u] : ? [v2: d] : ? [v3: du] : ? [v4: u] : ? % 45.75/6.94 | [v5: du] : ? [v6: u] : ? [v7: du] : ? [v8: % 45.75/6.94 | mono_2Etyop_2Emin_2Ebool] : ? [v9: int] : ( ~ (v9 = 0) & % 45.75/6.94 | c_2Epred__set_2ESUBSET_2E2(v5, v3) = v6 & % 45.75/6.94 | c_2Epred__set_2EREST_2E1(v3) = v4 & j_mono_2Etyop_2Emin_2Ebool(v7) = % 45.75/6.94 | v8 & p(v8) = v9 & tyop_2Emin_2Efun(v0, tyop_2Emin_2Ebool) = v2 & % 45.75/6.94 | s(v2, v4) = v5 & s(v2, v1) = v3 & s(tyop_2Emin_2Ebool, v6) = v7 & % 45.75/6.94 | mono_2Etyop_2Emin_2Ebool(v8) & du(v7) & du(v5) & du(v3) & d(v2) & % 45.75/6.94 | d(v0) & u(v6) & u(v4) & u(v1)) % 45.75/6.94 | % 45.75/6.94 | ALPHA: (function-axioms) implies: % 45.75/6.94 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 45.75/6.94 | mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = % 45.75/6.94 | v0)) % 45.75/6.94 | (22) ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] % 45.75/6.94 | : ! [v2: mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | ~ % 45.75/6.94 | (mono_2Ec_2Ebool_2E_7E_2E1(v2) = v1) | ~ % 45.75/6.94 | (mono_2Ec_2Ebool_2E_7E_2E1(v2) = v0)) % 45.75/6.94 | (23) ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] % 45.75/6.94 | : ! [v2: du] : (v1 = v0 | ~ (j_mono_2Etyop_2Emin_2Ebool(v2) = v1) | % 45.75/6.94 | ~ (j_mono_2Etyop_2Emin_2Ebool(v2) = v0)) % 45.75/6.94 | (24) ! [v0: u] : ! [v1: u] : ! [v2: du] : (v1 = v0 | ~ % 45.75/6.94 | (c_2Epred__set_2ECHOICE_2E1(v2) = v1) | ~ % 45.75/6.94 | (c_2Epred__set_2ECHOICE_2E1(v2) = v0)) % 45.75/6.94 | (25) ! [v0: u] : ! [v1: u] : ! [v2: du] : (v1 = v0 | ~ % 45.75/6.94 | (c_2Epred__set_2EREST_2E1(v2) = v1) | ~ % 45.75/6.94 | (c_2Epred__set_2EREST_2E1(v2) = v0)) % 45.75/6.94 | (26) ! [v0: du] : ! [v1: du] : ! [v2: u] : ! [v3: d] : (v1 = v0 | ~ % 45.75/6.94 | (s(v3, v2) = v1) | ~ (s(v3, v2) = v0)) % 45.75/6.94 | (27) ! [v0: mono_2Etyop_2Emin_2Ebool] : ! [v1: mono_2Etyop_2Emin_2Ebool] % 45.75/6.94 | : ! [v2: mono_2Etyop_2Emin_2Ebool] : ! [v3: % 45.75/6.94 | mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29] % 45.75/6.94 | : (v1 = v0 | ~ % 45.75/6.94 | (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(v3, % 45.75/6.94 | v2) = v1) | ~ % 45.75/6.94 | (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(v3, % 45.75/6.94 | v2) = v0)) % 45.75/6.94 | (28) ! [v0: u] : ! [v1: u] : ! [v2: du] : ! [v3: du] : (v1 = v0 | ~ % 45.75/6.94 | (c_2Ebool_2EIN_2E2(v3, v2) = v1) | ~ (c_2Ebool_2EIN_2E2(v3, v2) = % 45.75/6.94 | v0)) % 45.75/6.94 | % 45.75/6.94 | DELTA: instantiating (4) with fresh symbol all_45_0 gives: % 45.75/6.94 | (29) ~ (all_45_0 = 0) & p(mono_2Ec_2Ebool_2EF_2E0) = all_45_0 % 45.75/6.94 | % 45.75/6.94 | ALPHA: (29) implies: % 45.75/6.94 | (30) ~ (all_45_0 = 0) % 45.75/6.94 | (31) p(mono_2Ec_2Ebool_2EF_2E0) = all_45_0 % 45.75/6.94 | % 45.75/6.94 | DELTA: instantiating (20) with fresh symbols all_60_0, all_60_1, all_60_2, % 45.75/6.94 | all_60_3, all_60_4, all_60_5, all_60_6, all_60_7, all_60_8, all_60_9 % 45.75/6.94 | gives: % 45.75/6.94 | (32) ~ (all_60_0 = 0) & c_2Epred__set_2ESUBSET_2E2(all_60_4, all_60_6) = % 45.75/6.94 | all_60_3 & c_2Epred__set_2EREST_2E1(all_60_6) = all_60_5 & % 45.75/6.94 | j_mono_2Etyop_2Emin_2Ebool(all_60_2) = all_60_1 & p(all_60_1) = % 45.75/6.94 | all_60_0 & tyop_2Emin_2Efun(all_60_9, tyop_2Emin_2Ebool) = all_60_7 & % 45.75/6.94 | s(all_60_7, all_60_5) = all_60_4 & s(all_60_7, all_60_8) = all_60_6 & % 45.75/6.94 | s(tyop_2Emin_2Ebool, all_60_3) = all_60_2 & % 45.75/6.94 | mono_2Etyop_2Emin_2Ebool(all_60_1) & du(all_60_2) & du(all_60_4) & % 45.75/6.94 | du(all_60_6) & d(all_60_7) & d(all_60_9) & u(all_60_3) & u(all_60_5) & % 45.75/6.94 | u(all_60_8) % 45.75/6.94 | % 45.75/6.94 | ALPHA: (32) implies: % 45.75/6.95 | (33) ~ (all_60_0 = 0) % 45.75/6.95 | (34) u(all_60_8) % 45.75/6.95 | (35) u(all_60_5) % 45.75/6.95 | (36) u(all_60_3) % 45.75/6.95 | (37) d(all_60_9) % 45.75/6.95 | (38) d(all_60_7) % 45.75/6.95 | (39) mono_2Etyop_2Emin_2Ebool(all_60_1) % 45.75/6.95 | (40) s(tyop_2Emin_2Ebool, all_60_3) = all_60_2 % 45.75/6.95 | (41) s(all_60_7, all_60_8) = all_60_6 % 45.75/6.95 | (42) s(all_60_7, all_60_5) = all_60_4 % 45.75/6.95 | (43) tyop_2Emin_2Efun(all_60_9, tyop_2Emin_2Ebool) = all_60_7 % 45.75/6.95 | (44) p(all_60_1) = all_60_0 % 45.75/6.95 | (45) j_mono_2Etyop_2Emin_2Ebool(all_60_2) = all_60_1 % 45.75/6.95 | (46) c_2Epred__set_2EREST_2E1(all_60_6) = all_60_5 % 45.75/6.95 | (47) c_2Epred__set_2ESUBSET_2E2(all_60_4, all_60_6) = all_60_3 % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (10) with all_60_3, all_60_2, simplifying with % 45.75/6.95 | (36), (40) gives: % 45.75/6.95 | (48) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: u] : % 45.75/6.95 | (i_mono_2Etyop_2Emin_2Ebool(v0) = v1 & % 45.75/6.95 | j_mono_2Etyop_2Emin_2Ebool(all_60_2) = v0 & s(tyop_2Emin_2Ebool, v1) % 45.75/6.95 | = all_60_2 & mono_2Etyop_2Emin_2Ebool(v0) & du(all_60_2) & u(v1)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (7) with all_60_7, all_60_8, all_60_6, simplifying % 45.75/6.95 | with (34), (38), (41) gives: % 45.75/6.95 | (49) ? [v0: d] : ? [v1: du] : ? [v2: u] : (tyop_2Emin_2Efun(all_60_7, % 45.75/6.95 | all_60_7) = v0 & app_2E2(v1, all_60_6) = v2 & s(v0, combin_i_2E0) % 45.75/6.95 | = v1 & s(all_60_7, v2) = all_60_6 & du(v1) & du(all_60_6) & d(v0) & % 45.75/6.95 | u(v2)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (7) with all_60_7, all_60_5, all_60_4, simplifying % 45.75/6.95 | with (35), (38), (42) gives: % 45.75/6.95 | (50) ? [v0: d] : ? [v1: du] : ? [v2: u] : (tyop_2Emin_2Efun(all_60_7, % 45.75/6.95 | all_60_7) = v0 & app_2E2(v1, all_60_4) = v2 & s(v0, combin_i_2E0) % 45.75/6.95 | = v1 & s(all_60_7, v2) = all_60_4 & du(v1) & du(all_60_4) & d(v0) & % 45.75/6.95 | u(v2)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (19) with all_60_9, all_60_8, all_60_7, all_60_6, % 45.75/6.95 | simplifying with (34), (37), (41), (43) gives: % 45.75/6.95 | (51) ? [v0: u] : ? [v1: du] : ? [v2: u] : ? [v3: du] : ? [v4: u] : % 45.75/6.95 | (c_2Epred__set_2EREST_2E1(all_60_6) = v0 & % 45.75/6.95 | c_2Epred__set_2EDELETE_2E2(all_60_6, v3) = v4 & % 45.75/6.95 | c_2Epred__set_2ECHOICE_2E1(all_60_6) = v2 & s(all_60_7, v4) = v1 & % 45.75/6.95 | s(all_60_7, v0) = v1 & s(all_60_9, v2) = v3 & du(v3) & du(v1) & % 45.75/6.95 | u(v4) & u(v2) & u(v0)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (13) with all_60_9, all_60_8, all_60_7, all_60_6, % 45.75/6.95 | simplifying with (34), (37), (41), (43) gives: % 45.75/6.95 | (52) ? [v0: u] : ? [v1: du] : ? [v2: d] : ? [v3: du] : ? [v4: u] : % 45.75/6.95 | (c_2Epred__set_2EREST_2E1(all_60_6) = v0 & tyop_2Emin_2Efun(all_60_7, % 45.75/6.95 | all_60_7) = v2 & app_2E2(v3, all_60_6) = v4 & s(v2, % 45.75/6.95 | c_2Epred__set_2EREST_2E0) = v3 & s(all_60_7, v4) = v1 & % 45.75/6.95 | s(all_60_7, v0) = v1 & du(v3) & du(v1) & d(v2) & u(v4) & u(v0)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (11) with all_60_9, all_60_8, all_60_7, all_60_6, % 45.75/6.95 | simplifying with (34), (37), (41), (43) gives: % 45.75/6.95 | (53) ? [v0: u] : ? [v1: du] : ? [v2: d] : ? [v3: du] : ? [v4: u] : % 45.75/6.95 | (c_2Epred__set_2ECHOICE_2E1(all_60_6) = v0 & % 45.75/6.95 | tyop_2Emin_2Efun(all_60_7, all_60_9) = v2 & app_2E2(v3, all_60_6) = % 45.75/6.95 | v4 & s(v2, c_2Epred__set_2ECHOICE_2E0) = v3 & s(all_60_9, v4) = v1 & % 45.75/6.95 | s(all_60_9, v0) = v1 & du(v3) & du(v1) & d(v2) & u(v4) & u(v0)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (16) with mono_2Ec_2Ebool_2EF_2E0, all_45_0, % 45.75/6.95 | simplifying with (5), (31) gives: % 45.75/6.95 | (54) all_45_0 = 0 | ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.95 | (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.95 | mono_2Ec_2Ebool_2EF_2E0) = v0 & p(v0) = 0 & % 45.75/6.95 | mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (15) with mono_2Ec_2Ebool_2ET_2E0, simplifying with % 45.75/6.95 | (3), (6) gives: % 45.75/6.95 | (55) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ (v1 = 0) & % 45.75/6.95 | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.95 | mono_2Ec_2Ebool_2ET_2E0) = v0 & p(v0) = v1 & % 45.75/6.95 | mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (8) with mono_2Ec_2Ebool_2ET_2E0, simplifying with % 45.75/6.95 | (3), (6) gives: % 45.75/6.95 | (56) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ (v1 = 0) & % 45.75/6.95 | mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0) = v0 & p(v0) = v1 % 45.75/6.95 | & mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.95 | % 45.75/6.95 | GROUND_INST: instantiating (2) with mono_2Ec_2Ebool_2EF_2E0, all_60_1, % 45.75/6.95 | all_45_0, all_60_0, simplifying with (5), (31), (39), (44) gives: % 45.75/6.95 | (57) all_60_0 = 0 | all_60_1 = mono_2Ec_2Ebool_2EF_2E0 | all_45_0 = 0 % 45.75/6.95 | % 45.75/6.96 | GROUND_INST: instantiating (16) with all_60_1, all_60_0, simplifying with % 45.75/6.96 | (39), (44) gives: % 45.75/6.96 | (58) all_60_0 = 0 | ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.96 | (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.96 | all_60_1) = v0 & p(v0) = 0 & mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.96 | % 45.75/6.96 | GROUND_INST: instantiating (9) with all_60_1, all_60_0, simplifying with (39), % 45.75/6.96 | (44) gives: % 45.75/6.96 | (59) all_60_0 = 0 | ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.75/6.96 | (mono_2Ec_2Ebool_2E_7E_2E1(all_60_1) = v0 & p(v0) = 0 & % 45.75/6.96 | mono_2Etyop_2Emin_2Ebool(v0)) % 45.75/6.96 | % 45.75/6.96 | GROUND_INST: instantiating (17) with all_60_9, all_60_5, all_60_8, all_60_7, % 45.75/6.96 | all_60_4, all_60_6, all_60_3, simplifying with (34), (35), (37), % 45.75/6.96 | (41), (42), (43), (47) gives: % 45.75/6.96 | (60) ? [v0: du] : ? [v1: mono_2Etyop_2Emin_2Ebool] : ? [v2: int] : ? % 45.75/6.96 | [v3: u] : ? [v4: du] : ? [v5: u] : ? [v6: du] : ? [v7: % 45.75/6.96 | mono_2Etyop_2Emin_2Ebool] : ? [v8: int] : ? [v9: u] : ? [v10: du] % 45.75/6.96 | : ? [v11: mono_2Etyop_2Emin_2Ebool] : ? [v12: int] : (u(v3) & ((v8 = % 45.75/6.96 | 0 & ~ (v12 = 0) & c_2Ebool_2EIN_2E2(v4, all_60_4) = v5 & % 45.75/6.96 | c_2Ebool_2EIN_2E2(v4, all_60_6) = v9 & % 45.75/6.96 | j_mono_2Etyop_2Emin_2Ebool(v10) = v11 & % 45.75/6.96 | j_mono_2Etyop_2Emin_2Ebool(v6) = v7 & p(v11) = v12 & p(v7) = 0 & % 45.75/6.96 | s(all_60_9, v3) = v4 & s(tyop_2Emin_2Ebool, v9) = v10 & % 45.75/6.96 | s(tyop_2Emin_2Ebool, v5) = v6 & mono_2Etyop_2Emin_2Ebool(v11) & % 45.75/6.96 | mono_2Etyop_2Emin_2Ebool(v7) & du(v10) & du(v6) & du(v4) & u(v9) % 45.75/6.96 | & u(v5)) | (v2 = 0 & j_mono_2Etyop_2Emin_2Ebool(v0) = v1 & p(v1) % 45.75/6.96 | = 0 & s(tyop_2Emin_2Ebool, all_60_3) = v0 & % 45.75/6.96 | mono_2Etyop_2Emin_2Ebool(v1) & du(v0)))) % 45.75/6.96 | % 45.75/6.96 | GROUND_INST: instantiating (14) with all_60_9, all_60_5, all_60_8, all_60_7, % 45.75/6.96 | all_60_4, all_60_6, all_60_3, simplifying with (34), (35), (37), % 45.75/6.96 | (41), (42), (43), (47) gives: % 45.75/6.96 | (61) ? [v0: du] : ? [v1: mono_2Etyop_2Emin_2Ebool] : ? [v2: d] : ? [v3: % 45.75/6.96 | d] : ? [v4: du] : ? [v5: u] : ? [v6: du] : ? [v7: u] : ? [v8: % 45.75/6.96 | du] : (j_mono_2Etyop_2Emin_2Ebool(v8) = v1 & % 45.75/6.96 | j_mono_2Etyop_2Emin_2Ebool(v0) = v1 & tyop_2Emin_2Efun(all_60_7, v2) % 45.75/6.96 | = v3 & tyop_2Emin_2Efun(all_60_7, tyop_2Emin_2Ebool) = v2 & % 45.75/6.96 | app_2E2(v6, all_60_6) = v7 & app_2E2(v4, all_60_4) = v5 & s(v3, % 45.75/6.96 | c_2Epred__set_2ESUBSET_2E0) = v4 & s(v2, v5) = v6 & % 45.75/6.96 | s(tyop_2Emin_2Ebool, v7) = v8 & s(tyop_2Emin_2Ebool, all_60_3) = v0 % 45.75/6.96 | & mono_2Etyop_2Emin_2Ebool(v1) & du(v8) & du(v6) & du(v4) & du(v0) & % 45.75/6.96 | d(v3) & d(v2) & u(v7) & u(v5)) % 45.75/6.96 | % 45.75/6.96 | DELTA: instantiating (56) with fresh symbols all_81_0, all_81_1 gives: % 45.75/6.96 | (62) ~ (all_81_0 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0) % 45.75/6.96 | = all_81_1 & p(all_81_1) = all_81_0 & % 45.75/6.96 | mono_2Etyop_2Emin_2Ebool(all_81_1) % 45.75/6.96 | % 45.75/6.96 | ALPHA: (62) implies: % 45.75/6.96 | (63) ~ (all_81_0 = 0) % 45.75/6.96 | (64) mono_2Etyop_2Emin_2Ebool(all_81_1) % 45.75/6.96 | (65) p(all_81_1) = all_81_0 % 45.75/6.96 | (66) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0) = all_81_1 % 45.75/6.96 | % 45.75/6.96 | DELTA: instantiating (55) with fresh symbols all_83_0, all_83_1 gives: % 45.75/6.96 | (67) ~ (all_83_0 = 0) & % 45.75/6.96 | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.96 | mono_2Ec_2Ebool_2ET_2E0) = all_83_1 & p(all_83_1) = all_83_0 & % 45.75/6.96 | mono_2Etyop_2Emin_2Ebool(all_83_1) % 45.75/6.96 | % 45.75/6.96 | ALPHA: (67) implies: % 45.75/6.96 | (68) ~ (all_83_0 = 0) % 45.75/6.96 | (69) mono_2Etyop_2Emin_2Ebool(all_83_1) % 45.75/6.96 | (70) p(all_83_1) = all_83_0 % 45.75/6.96 | (71) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.75/6.96 | mono_2Ec_2Ebool_2ET_2E0) = all_83_1 % 45.75/6.96 | % 45.75/6.96 | DELTA: instantiating (48) with fresh symbols all_85_0, all_85_1 gives: % 45.75/6.96 | (72) i_mono_2Etyop_2Emin_2Ebool(all_85_1) = all_85_0 & % 45.75/6.96 | j_mono_2Etyop_2Emin_2Ebool(all_60_2) = all_85_1 & s(tyop_2Emin_2Ebool, % 45.75/6.96 | all_85_0) = all_60_2 & mono_2Etyop_2Emin_2Ebool(all_85_1) & % 45.75/6.96 | du(all_60_2) & u(all_85_0) % 45.75/6.96 | % 45.75/6.96 | ALPHA: (72) implies: % 45.75/6.96 | (73) j_mono_2Etyop_2Emin_2Ebool(all_60_2) = all_85_1 % 45.75/6.96 | % 45.75/6.96 | DELTA: instantiating (50) with fresh symbols all_87_0, all_87_1, all_87_2 % 45.75/6.96 | gives: % 45.75/6.96 | (74) tyop_2Emin_2Efun(all_60_7, all_60_7) = all_87_2 & app_2E2(all_87_1, % 45.75/6.96 | all_60_4) = all_87_0 & s(all_87_2, combin_i_2E0) = all_87_1 & % 45.75/6.96 | s(all_60_7, all_87_0) = all_60_4 & du(all_87_1) & du(all_60_4) & % 45.75/6.96 | d(all_87_2) & u(all_87_0) % 45.75/6.96 | % 45.75/6.96 | ALPHA: (74) implies: % 45.75/6.96 | (75) u(all_87_0) % 45.75/6.96 | (76) s(all_60_7, all_87_0) = all_60_4 % 45.75/6.96 | % 45.75/6.96 | DELTA: instantiating (49) with fresh symbols all_89_0, all_89_1, all_89_2 % 45.75/6.96 | gives: % 45.75/6.96 | (77) tyop_2Emin_2Efun(all_60_7, all_60_7) = all_89_2 & app_2E2(all_89_1, % 45.75/6.96 | all_60_6) = all_89_0 & s(all_89_2, combin_i_2E0) = all_89_1 & % 45.75/6.96 | s(all_60_7, all_89_0) = all_60_6 & du(all_89_1) & du(all_60_6) & % 45.75/6.96 | d(all_89_2) & u(all_89_0) % 45.75/6.96 | % 45.75/6.96 | ALPHA: (77) implies: % 45.75/6.96 | (78) u(all_89_0) % 45.75/6.96 | (79) s(all_60_7, all_89_0) = all_60_6 % 45.75/6.96 | % 45.75/6.96 | DELTA: instantiating (52) with fresh symbols all_93_0, all_93_1, all_93_2, % 45.75/6.96 | all_93_3, all_93_4 gives: % 45.75/6.96 | (80) c_2Epred__set_2EREST_2E1(all_60_6) = all_93_4 & % 45.75/6.96 | tyop_2Emin_2Efun(all_60_7, all_60_7) = all_93_2 & app_2E2(all_93_1, % 45.75/6.96 | all_60_6) = all_93_0 & s(all_93_2, c_2Epred__set_2EREST_2E0) = % 45.75/6.96 | all_93_1 & s(all_60_7, all_93_0) = all_93_3 & s(all_60_7, all_93_4) = % 45.75/6.96 | all_93_3 & du(all_93_1) & du(all_93_3) & d(all_93_2) & u(all_93_0) & % 45.75/6.96 | u(all_93_4) % 45.75/6.96 | % 45.75/6.96 | ALPHA: (80) implies: % 45.75/6.96 | (81) c_2Epred__set_2EREST_2E1(all_60_6) = all_93_4 % 45.75/6.96 | % 45.75/6.96 | DELTA: instantiating (51) with fresh symbols all_99_0, all_99_1, all_99_2, % 45.75/6.96 | all_99_3, all_99_4 gives: % 45.75/6.97 | (82) c_2Epred__set_2EREST_2E1(all_60_6) = all_99_4 & % 45.75/6.97 | c_2Epred__set_2EDELETE_2E2(all_60_6, all_99_1) = all_99_0 & % 45.75/6.97 | c_2Epred__set_2ECHOICE_2E1(all_60_6) = all_99_2 & s(all_60_7, % 45.75/6.97 | all_99_0) = all_99_3 & s(all_60_7, all_99_4) = all_99_3 & % 45.75/6.97 | s(all_60_9, all_99_2) = all_99_1 & du(all_99_1) & du(all_99_3) & % 45.75/6.97 | u(all_99_0) & u(all_99_2) & u(all_99_4) % 45.75/6.97 | % 45.75/6.97 | ALPHA: (82) implies: % 45.75/6.97 | (83) s(all_60_9, all_99_2) = all_99_1 % 45.75/6.97 | (84) s(all_60_7, all_99_4) = all_99_3 % 45.75/6.97 | (85) s(all_60_7, all_99_0) = all_99_3 % 45.75/6.97 | (86) c_2Epred__set_2ECHOICE_2E1(all_60_6) = all_99_2 % 45.75/6.97 | (87) c_2Epred__set_2EDELETE_2E2(all_60_6, all_99_1) = all_99_0 % 45.75/6.97 | (88) c_2Epred__set_2EREST_2E1(all_60_6) = all_99_4 % 45.75/6.97 | % 45.75/6.97 | DELTA: instantiating (53) with fresh symbols all_103_0, all_103_1, all_103_2, % 45.75/6.97 | all_103_3, all_103_4 gives: % 45.75/6.97 | (89) c_2Epred__set_2ECHOICE_2E1(all_60_6) = all_103_4 & % 45.75/6.97 | tyop_2Emin_2Efun(all_60_7, all_60_9) = all_103_2 & app_2E2(all_103_1, % 45.75/6.97 | all_60_6) = all_103_0 & s(all_103_2, c_2Epred__set_2ECHOICE_2E0) = % 45.75/6.97 | all_103_1 & s(all_60_9, all_103_0) = all_103_3 & s(all_60_9, % 45.75/6.97 | all_103_4) = all_103_3 & du(all_103_1) & du(all_103_3) & % 45.75/6.97 | d(all_103_2) & u(all_103_0) & u(all_103_4) % 45.75/6.97 | % 45.75/6.97 | ALPHA: (89) implies: % 45.75/6.97 | (90) u(all_103_4) % 45.75/6.97 | (91) s(all_60_9, all_103_4) = all_103_3 % 45.75/6.97 | (92) c_2Epred__set_2ECHOICE_2E1(all_60_6) = all_103_4 % 45.75/6.97 | % 45.75/6.97 | DELTA: instantiating (61) with fresh symbols all_113_0, all_113_1, all_113_2, % 45.75/6.97 | all_113_3, all_113_4, all_113_5, all_113_6, all_113_7, all_113_8 gives: % 45.75/6.97 | (93) j_mono_2Etyop_2Emin_2Ebool(all_113_0) = all_113_7 & % 45.75/6.97 | j_mono_2Etyop_2Emin_2Ebool(all_113_8) = all_113_7 & % 45.75/6.97 | tyop_2Emin_2Efun(all_60_7, all_113_6) = all_113_5 & % 45.75/6.97 | tyop_2Emin_2Efun(all_60_7, tyop_2Emin_2Ebool) = all_113_6 & % 45.75/6.97 | app_2E2(all_113_2, all_60_6) = all_113_1 & app_2E2(all_113_4, % 45.75/6.97 | all_60_4) = all_113_3 & s(all_113_5, c_2Epred__set_2ESUBSET_2E0) = % 45.75/6.97 | all_113_4 & s(all_113_6, all_113_3) = all_113_2 & s(tyop_2Emin_2Ebool, % 45.75/6.97 | all_113_1) = all_113_0 & s(tyop_2Emin_2Ebool, all_60_3) = all_113_8 % 45.75/6.97 | & mono_2Etyop_2Emin_2Ebool(all_113_7) & du(all_113_0) & du(all_113_2) % 45.75/6.97 | & du(all_113_4) & du(all_113_8) & d(all_113_5) & d(all_113_6) & % 45.75/6.97 | u(all_113_1) & u(all_113_3) % 45.75/6.97 | % 45.75/6.97 | ALPHA: (93) implies: % 45.75/6.97 | (94) mono_2Etyop_2Emin_2Ebool(all_113_7) % 45.75/6.97 | (95) s(tyop_2Emin_2Ebool, all_60_3) = all_113_8 % 45.75/6.97 | (96) j_mono_2Etyop_2Emin_2Ebool(all_113_8) = all_113_7 % 45.75/6.97 | % 45.75/6.97 | DELTA: instantiating (60) with fresh symbols all_123_0, all_123_1, all_123_2, % 45.75/6.97 | all_123_3, all_123_4, all_123_5, all_123_6, all_123_7, all_123_8, % 45.75/6.97 | all_123_9, all_123_10, all_123_11, all_123_12 gives: % 45.75/6.97 | (97) u(all_123_9) & ((all_123_4 = 0 & ~ (all_123_0 = 0) & % 45.75/6.97 | c_2Ebool_2EIN_2E2(all_123_8, all_60_4) = all_123_7 & % 45.75/6.97 | c_2Ebool_2EIN_2E2(all_123_8, all_60_6) = all_123_3 & % 45.75/6.97 | j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_123_1 & % 45.75/6.97 | j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_123_5 & p(all_123_1) = % 45.75/6.97 | all_123_0 & p(all_123_5) = 0 & s(all_60_9, all_123_9) = all_123_8 % 45.75/6.97 | & s(tyop_2Emin_2Ebool, all_123_3) = all_123_2 & % 45.75/6.97 | s(tyop_2Emin_2Ebool, all_123_7) = all_123_6 & % 45.75/6.97 | mono_2Etyop_2Emin_2Ebool(all_123_1) & % 45.75/6.97 | mono_2Etyop_2Emin_2Ebool(all_123_5) & du(all_123_2) & % 45.75/6.97 | du(all_123_6) & du(all_123_8) & u(all_123_3) & u(all_123_7)) | % 45.75/6.97 | (all_123_10 = 0 & j_mono_2Etyop_2Emin_2Ebool(all_123_12) = % 45.75/6.97 | all_123_11 & p(all_123_11) = 0 & s(tyop_2Emin_2Ebool, all_60_3) = % 45.75/6.97 | all_123_12 & mono_2Etyop_2Emin_2Ebool(all_123_11) & % 45.75/6.97 | du(all_123_12))) % 45.75/6.97 | % 45.75/6.97 | ALPHA: (97) implies: % 45.75/6.97 | (98) u(all_123_9) % 45.75/6.98 | (99) (all_123_4 = 0 & ~ (all_123_0 = 0) & c_2Ebool_2EIN_2E2(all_123_8, % 45.75/6.98 | all_60_4) = all_123_7 & c_2Ebool_2EIN_2E2(all_123_8, all_60_6) = % 45.75/6.98 | all_123_3 & j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_123_1 & % 45.75/6.98 | j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_123_5 & p(all_123_1) = % 45.75/6.98 | all_123_0 & p(all_123_5) = 0 & s(all_60_9, all_123_9) = all_123_8 & % 45.75/6.98 | s(tyop_2Emin_2Ebool, all_123_3) = all_123_2 & s(tyop_2Emin_2Ebool, % 45.75/6.98 | all_123_7) = all_123_6 & mono_2Etyop_2Emin_2Ebool(all_123_1) & % 45.75/6.98 | mono_2Etyop_2Emin_2Ebool(all_123_5) & du(all_123_2) & du(all_123_6) % 45.75/6.98 | & du(all_123_8) & u(all_123_3) & u(all_123_7)) | (all_123_10 = 0 & % 45.75/6.98 | j_mono_2Etyop_2Emin_2Ebool(all_123_12) = all_123_11 & p(all_123_11) % 45.75/6.98 | = 0 & s(tyop_2Emin_2Ebool, all_60_3) = all_123_12 & % 45.75/6.98 | mono_2Etyop_2Emin_2Ebool(all_123_11) & du(all_123_12)) % 45.75/6.98 | % 45.75/6.98 | BETA: splitting (57) gives: % 45.75/6.98 | % 45.89/6.98 | Case 1: % 45.89/6.98 | | % 45.89/6.98 | | (100) all_60_0 = 0 % 45.89/6.98 | | % 45.89/6.98 | | REDUCE: (33), (100) imply: % 45.89/6.98 | | (101) $false % 45.89/6.98 | | % 45.89/6.98 | | CLOSE: (101) is inconsistent. % 45.89/6.98 | | % 45.89/6.98 | Case 2: % 45.89/6.98 | | % 45.89/6.98 | | (102) all_60_1 = mono_2Ec_2Ebool_2EF_2E0 | all_45_0 = 0 % 45.89/6.98 | | % 45.89/6.98 | | BETA: splitting (102) gives: % 45.89/6.98 | | % 45.89/6.98 | | Case 1: % 45.89/6.98 | | | % 45.89/6.98 | | | (103) all_45_0 = 0 % 45.89/6.98 | | | % 45.89/6.98 | | | REDUCE: (30), (103) imply: % 45.89/6.98 | | | (104) $false % 45.89/6.98 | | | % 45.89/6.98 | | | CLOSE: (104) is inconsistent. % 45.89/6.98 | | | % 45.89/6.98 | | Case 2: % 45.89/6.98 | | | % 45.89/6.98 | | | (105) all_60_1 = mono_2Ec_2Ebool_2EF_2E0 % 45.89/6.98 | | | % 45.89/6.98 | | | REDUCE: (45), (105) imply: % 45.89/6.98 | | | (106) j_mono_2Etyop_2Emin_2Ebool(all_60_2) = mono_2Ec_2Ebool_2EF_2E0 % 45.89/6.98 | | | % 45.89/6.98 | | | REDUCE: (44), (105) imply: % 45.89/6.98 | | | (107) p(mono_2Ec_2Ebool_2EF_2E0) = all_60_0 % 45.89/6.98 | | | % 45.89/6.98 | | | BETA: splitting (59) gives: % 45.89/6.98 | | | % 45.89/6.98 | | | Case 1: % 45.89/6.98 | | | | % 45.89/6.98 | | | | (108) all_60_0 = 0 % 45.89/6.98 | | | | % 45.89/6.98 | | | | REDUCE: (33), (108) imply: % 45.89/6.98 | | | | (109) $false % 45.89/6.98 | | | | % 45.89/6.98 | | | | CLOSE: (109) is inconsistent. % 45.89/6.98 | | | | % 45.89/6.98 | | | Case 2: % 45.89/6.98 | | | | % 45.89/6.98 | | | | (110) ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.89/6.98 | | | | (mono_2Ec_2Ebool_2E_7E_2E1(all_60_1) = v0 & p(v0) = 0 & % 45.89/6.98 | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.98 | | | | % 45.89/6.98 | | | | DELTA: instantiating (110) with fresh symbol all_136_0 gives: % 45.89/6.98 | | | | (111) mono_2Ec_2Ebool_2E_7E_2E1(all_60_1) = all_136_0 & p(all_136_0) % 45.89/6.98 | | | | = 0 & mono_2Etyop_2Emin_2Ebool(all_136_0) % 45.89/6.98 | | | | % 45.89/6.98 | | | | ALPHA: (111) implies: % 45.89/6.98 | | | | (112) mono_2Etyop_2Emin_2Ebool(all_136_0) % 45.89/6.98 | | | | (113) p(all_136_0) = 0 % 45.89/6.98 | | | | (114) mono_2Ec_2Ebool_2E_7E_2E1(all_60_1) = all_136_0 % 45.89/6.98 | | | | % 45.89/6.98 | | | | REDUCE: (105), (114) imply: % 45.89/6.98 | | | | (115) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2EF_2E0) = all_136_0 % 45.89/6.98 | | | | % 45.89/6.98 | | | | BETA: splitting (58) gives: % 45.89/6.98 | | | | % 45.89/6.98 | | | | Case 1: % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | (116) all_60_0 = 0 % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | REDUCE: (33), (116) imply: % 45.89/6.98 | | | | | (117) $false % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | CLOSE: (117) is inconsistent. % 45.89/6.98 | | | | | % 45.89/6.98 | | | | Case 2: % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | (118) ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.89/6.98 | | | | | (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | all_60_1) = v0 & p(v0) = 0 & % 45.89/6.98 | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | DELTA: instantiating (118) with fresh symbol all_142_0 gives: % 45.89/6.98 | | | | | (119) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | all_60_1) = all_142_0 & p(all_142_0) = 0 & % 45.89/6.98 | | | | | mono_2Etyop_2Emin_2Ebool(all_142_0) % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | ALPHA: (119) implies: % 45.89/6.98 | | | | | (120) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | all_60_1) = all_142_0 % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | REDUCE: (105), (120) imply: % 45.89/6.98 | | | | | (121) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | mono_2Ec_2Ebool_2EF_2E0) = all_142_0 % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | BETA: splitting (54) gives: % 45.89/6.98 | | | | | % 45.89/6.98 | | | | | Case 1: % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | (122) all_45_0 = 0 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | REDUCE: (30), (122) imply: % 45.89/6.98 | | | | | | (123) $false % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | CLOSE: (123) is inconsistent. % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | Case 2: % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | (124) ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.89/6.98 | | | | | | (mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | | mono_2Ec_2Ebool_2EF_2E0) = v0 & p(v0) = 0 & % 45.89/6.98 | | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | DELTA: instantiating (124) with fresh symbol all_147_0 gives: % 45.89/6.98 | | | | | | (125) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | | mono_2Ec_2Ebool_2EF_2E0) = all_147_0 & p(all_147_0) = 0 & % 45.89/6.98 | | | | | | mono_2Etyop_2Emin_2Ebool(all_147_0) % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | ALPHA: (125) implies: % 45.89/6.98 | | | | | | (126) mono_2Etyop_2Emin_2Ebool(all_147_0) % 45.89/6.98 | | | | | | (127) p(all_147_0) = 0 % 45.89/6.98 | | | | | | (128) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | | mono_2Ec_2Ebool_2EF_2E0) = all_147_0 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | GROUND_INST: instantiating (26) with all_60_2, all_113_8, all_60_3, % 45.89/6.98 | | | | | | tyop_2Emin_2Ebool, simplifying with (40), (95) gives: % 45.89/6.98 | | | | | | (129) all_113_8 = all_60_2 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | GROUND_INST: instantiating (21) with all_45_0, all_60_0, % 45.89/6.98 | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (31), (107) % 45.89/6.98 | | | | | | gives: % 45.89/6.98 | | | | | | (130) all_60_0 = all_45_0 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2EF_2E0, % 45.89/6.98 | | | | | | all_85_1, all_60_2, simplifying with (73), (106) gives: % 45.89/6.98 | | | | | | (131) all_85_1 = mono_2Ec_2Ebool_2EF_2E0 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | GROUND_INST: instantiating (27) with all_142_0, all_147_0, % 45.89/6.98 | | | | | | mono_2Ec_2Ebool_2EF_2E0, mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.98 | | | | | | simplifying with (121), (128) gives: % 45.89/6.98 | | | | | | (132) all_147_0 = all_142_0 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | GROUND_INST: instantiating (24) with all_99_2, all_103_4, all_60_6, % 45.89/6.98 | | | | | | simplifying with (86), (92) gives: % 45.89/6.98 | | | | | | (133) all_103_4 = all_99_2 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | GROUND_INST: instantiating (25) with all_60_5, all_99_4, all_60_6, % 45.89/6.98 | | | | | | simplifying with (46), (88) gives: % 45.89/6.98 | | | | | | (134) all_99_4 = all_60_5 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | GROUND_INST: instantiating (25) with all_93_4, all_99_4, all_60_6, % 45.89/6.98 | | | | | | simplifying with (81), (88) gives: % 45.89/6.98 | | | | | | (135) all_99_4 = all_93_4 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | COMBINE_EQS: (134), (135) imply: % 45.89/6.98 | | | | | | (136) all_93_4 = all_60_5 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | REDUCE: (96), (129) imply: % 45.89/6.98 | | | | | | (137) j_mono_2Etyop_2Emin_2Ebool(all_60_2) = all_113_7 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | REDUCE: (127), (132) imply: % 45.89/6.98 | | | | | | (138) p(all_142_0) = 0 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | REDUCE: (84), (134) imply: % 45.89/6.98 | | | | | | (139) s(all_60_7, all_60_5) = all_99_3 % 45.89/6.98 | | | | | | % 45.89/6.98 | | | | | | REDUCE: (91), (133) imply: % 45.89/6.99 | | | | | | (140) s(all_60_9, all_99_2) = all_103_3 % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | REDUCE: (126), (132) imply: % 45.89/6.99 | | | | | | (141) mono_2Etyop_2Emin_2Ebool(all_142_0) % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | REDUCE: (90), (133) imply: % 45.89/6.99 | | | | | | (142) u(all_99_2) % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | GROUND_INST: instantiating (26) with all_99_1, all_103_3, all_99_2, % 45.89/6.99 | | | | | | all_60_9, simplifying with (83), (140) gives: % 45.89/6.99 | | | | | | (143) all_103_3 = all_99_1 % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | GROUND_INST: instantiating (26) with all_60_4, all_99_3, all_60_5, % 45.89/6.99 | | | | | | all_60_7, simplifying with (42), (139) gives: % 45.89/6.99 | | | | | | (144) all_99_3 = all_60_4 % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2EF_2E0, % 45.89/6.99 | | | | | | all_113_7, all_60_2, simplifying with (106), (137) % 45.89/6.99 | | | | | | gives: % 45.89/6.99 | | | | | | (145) all_113_7 = mono_2Ec_2Ebool_2EF_2E0 % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | REDUCE: (85), (144) imply: % 45.89/6.99 | | | | | | (146) s(all_60_7, all_99_0) = all_60_4 % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | BETA: splitting (99) gives: % 45.89/6.99 | | | | | | % 45.89/6.99 | | | | | | Case 1: % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | (147) all_123_4 = 0 & ~ (all_123_0 = 0) & % 45.89/6.99 | | | | | | | c_2Ebool_2EIN_2E2(all_123_8, all_60_4) = all_123_7 & % 45.89/6.99 | | | | | | | c_2Ebool_2EIN_2E2(all_123_8, all_60_6) = all_123_3 & % 45.89/6.99 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_123_1 & % 45.89/6.99 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_123_5 & % 45.89/6.99 | | | | | | | p(all_123_1) = all_123_0 & p(all_123_5) = 0 & s(all_60_9, % 45.89/6.99 | | | | | | | all_123_9) = all_123_8 & s(tyop_2Emin_2Ebool, % 45.89/6.99 | | | | | | | all_123_3) = all_123_2 & s(tyop_2Emin_2Ebool, % 45.89/6.99 | | | | | | | all_123_7) = all_123_6 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_123_1) & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_123_5) & du(all_123_2) & % 45.89/6.99 | | | | | | | du(all_123_6) & du(all_123_8) & u(all_123_3) & % 45.89/6.99 | | | | | | | u(all_123_7) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | ALPHA: (147) implies: % 45.89/6.99 | | | | | | | (148) ~ (all_123_0 = 0) % 45.89/6.99 | | | | | | | (149) u(all_123_7) % 45.89/6.99 | | | | | | | (150) u(all_123_3) % 45.89/6.99 | | | | | | | (151) mono_2Etyop_2Emin_2Ebool(all_123_5) % 45.89/6.99 | | | | | | | (152) mono_2Etyop_2Emin_2Ebool(all_123_1) % 45.89/6.99 | | | | | | | (153) s(tyop_2Emin_2Ebool, all_123_7) = all_123_6 % 45.89/6.99 | | | | | | | (154) s(tyop_2Emin_2Ebool, all_123_3) = all_123_2 % 45.89/6.99 | | | | | | | (155) s(all_60_9, all_123_9) = all_123_8 % 45.89/6.99 | | | | | | | (156) p(all_123_5) = 0 % 45.89/6.99 | | | | | | | (157) p(all_123_1) = all_123_0 % 45.89/6.99 | | | | | | | (158) j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_123_5 % 45.89/6.99 | | | | | | | (159) j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_123_1 % 45.89/6.99 | | | | | | | (160) c_2Ebool_2EIN_2E2(all_123_8, all_60_6) = all_123_3 % 45.89/6.99 | | | | | | | (161) c_2Ebool_2EIN_2E2(all_123_8, all_60_4) = all_123_7 % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (10) with all_123_7, all_123_6, % 45.89/6.99 | | | | | | | simplifying with (149), (153) gives: % 45.89/6.99 | | | | | | | (162) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: u] : % 45.89/6.99 | | | | | | | (i_mono_2Etyop_2Emin_2Ebool(v0) = v1 & % 45.89/6.99 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_123_6) = v0 & % 45.89/6.99 | | | | | | | s(tyop_2Emin_2Ebool, v1) = all_123_6 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0) & du(all_123_6) & u(v1)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (10) with all_123_3, all_123_2, % 45.89/6.99 | | | | | | | simplifying with (150), (154) gives: % 45.89/6.99 | | | | | | | (163) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: u] : % 45.89/6.99 | | | | | | | (i_mono_2Etyop_2Emin_2Ebool(v0) = v1 & % 45.89/6.99 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_123_2) = v0 & % 45.89/6.99 | | | | | | | s(tyop_2Emin_2Ebool, v1) = all_123_2 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0) & du(all_123_2) & u(v1)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (2) with mono_2Ec_2Ebool_2EF_2E0, % 45.89/6.99 | | | | | | | all_81_1, all_45_0, all_81_0, simplifying with (5), % 45.89/6.99 | | | | | | | (31), (64), (65) gives: % 45.89/6.99 | | | | | | | (164) all_81_0 = 0 | all_81_1 = mono_2Ec_2Ebool_2EF_2E0 | % 45.89/6.99 | | | | | | | all_45_0 = 0 % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (9) with all_81_1, all_81_0, % 45.89/6.99 | | | | | | | simplifying with (64), (65) gives: % 45.89/6.99 | | | | | | | (165) all_81_0 = 0 | ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.89/6.99 | | | | | | | (mono_2Ec_2Ebool_2E_7E_2E1(all_81_1) = v0 & p(v0) = 0 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (2) with all_81_1, all_83_1, all_81_0, % 45.89/6.99 | | | | | | | all_83_0, simplifying with (64), (65), (69), (70) % 45.89/6.99 | | | | | | | gives: % 45.89/6.99 | | | | | | | (166) all_83_0 = 0 | all_83_1 = all_81_1 | all_81_0 = 0 % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (9) with all_83_1, all_83_0, % 45.89/6.99 | | | | | | | simplifying with (69), (70) gives: % 45.89/6.99 | | | | | | | (167) all_83_0 = 0 | ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.89/6.99 | | | | | | | (mono_2Ec_2Ebool_2E_7E_2E1(all_83_1) = v0 & p(v0) = 0 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (15) with all_123_5, simplifying with % 45.89/6.99 | | | | | | | (151), (156) gives: % 45.89/6.99 | | | | | | | (168) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ % 45.89/6.99 | | | | | | | (v1 = 0) & % 45.89/6.99 | | | | | | | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.99 | | | | | | | all_123_5) = v0 & p(v0) = v1 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (8) with all_123_5, simplifying with % 45.89/6.99 | | | | | | | (151), (156) gives: % 45.89/6.99 | | | | | | | (169) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ % 45.89/6.99 | | | | | | | (v1 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(all_123_5) = v0 & % 45.89/6.99 | | | | | | | p(v0) = v1 & mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (2) with all_81_1, all_123_1, all_81_0, % 45.89/6.99 | | | | | | | all_123_0, simplifying with (64), (65), (152), (157) % 45.89/6.99 | | | | | | | gives: % 45.89/6.99 | | | | | | | (170) all_123_0 = 0 | all_123_1 = all_81_1 | all_81_0 = 0 % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (9) with all_123_1, all_123_0, % 45.89/6.99 | | | | | | | simplifying with (152), (157) gives: % 45.89/6.99 | | | | | | | (171) all_123_0 = 0 | ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.89/6.99 | | | | | | | (mono_2Ec_2Ebool_2E_7E_2E1(all_123_1) = v0 & p(v0) = 0 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (1) with mono_2Ec_2Ebool_2ET_2E0, % 45.89/6.99 | | | | | | | all_136_0, simplifying with (3), (6), (112), (113) % 45.89/6.99 | | | | | | | gives: % 45.89/6.99 | | | | | | | (172) all_136_0 = mono_2Ec_2Ebool_2ET_2E0 % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (15) with all_136_0, simplifying with % 45.89/6.99 | | | | | | | (112), (113) gives: % 45.89/6.99 | | | | | | | (173) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ % 45.89/6.99 | | | | | | | (v1 = 0) & % 45.89/6.99 | | | | | | | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/6.99 | | | | | | | all_136_0) = v0 & p(v0) = v1 & % 45.89/6.99 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (8) with all_136_0, simplifying with % 45.89/6.99 | | | | | | | (112), (113) gives: % 45.89/6.99 | | | | | | | (174) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ % 45.89/6.99 | | | | | | | (v1 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(all_136_0) = v0 & % 45.89/6.99 | | | | | | | p(v0) = v1 & mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (1) with all_136_0, all_142_0, % 45.89/6.99 | | | | | | | simplifying with (112), (113), (138), (141) gives: % 45.89/6.99 | | | | | | | (175) all_142_0 = all_136_0 % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (1) with all_123_5, all_142_0, % 45.89/6.99 | | | | | | | simplifying with (138), (141), (151), (156) gives: % 45.89/6.99 | | | | | | | (176) all_142_0 = all_123_5 % 45.89/6.99 | | | | | | | % 45.89/6.99 | | | | | | | GROUND_INST: instantiating (15) with all_142_0, simplifying with % 45.89/6.99 | | | | | | | (138), (141) gives: % 45.89/7.00 | | | | | | | (177) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ % 45.89/7.00 | | | | | | | (v1 = 0) & % 45.89/7.00 | | | | | | | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.00 | | | | | | | all_142_0) = v0 & p(v0) = v1 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | GROUND_INST: instantiating (8) with all_142_0, simplifying with % 45.89/7.00 | | | | | | | (138), (141) gives: % 45.89/7.00 | | | | | | | (178) ? [v0: mono_2Etyop_2Emin_2Ebool] : ? [v1: int] : ( ~ % 45.89/7.00 | | | | | | | (v1 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(all_142_0) = v0 & % 45.89/7.00 | | | | | | | p(v0) = v1 & mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | GROUND_INST: instantiating (12) with all_60_9, all_123_9, % 45.89/7.00 | | | | | | | all_89_0, all_123_8, all_60_7, all_60_6, all_123_3, % 45.89/7.00 | | | | | | | simplifying with (37), (43), (78), (79), (98), (155), % 45.89/7.00 | | | | | | | (160) gives: % 45.89/7.00 | | | | | | | (179) ? [v0: du] : ? [v1: mono_2Etyop_2Emin_2Ebool] : ? [v2: % 45.89/7.00 | | | | | | | d] : ? [v3: d] : ? [v4: du] : ? [v5: u] : ? [v6: % 45.89/7.00 | | | | | | | du] : ? [v7: u] : ? [v8: du] : % 45.89/7.00 | | | | | | | (j_mono_2Etyop_2Emin_2Ebool(v8) = v1 & % 45.89/7.00 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(v0) = v1 & % 45.89/7.00 | | | | | | | tyop_2Emin_2Efun(all_60_7, tyop_2Emin_2Ebool) = v2 & % 45.89/7.00 | | | | | | | tyop_2Emin_2Efun(all_60_9, v2) = v3 & app_2E2(v6, % 45.89/7.00 | | | | | | | all_60_6) = v7 & app_2E2(v4, all_123_8) = v5 & s(v3, % 45.89/7.00 | | | | | | | c_2Ebool_2EIN_2E0) = v4 & s(v2, v5) = v6 & % 45.89/7.00 | | | | | | | s(tyop_2Emin_2Ebool, v7) = v8 & s(tyop_2Emin_2Ebool, % 45.89/7.00 | | | | | | | all_123_3) = v0 & mono_2Etyop_2Emin_2Ebool(v1) & % 45.89/7.00 | | | | | | | du(v8) & du(v6) & du(v4) & du(v0) & d(v3) & d(v2) & % 45.89/7.00 | | | | | | | u(v7) & u(v5)) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | GROUND_INST: instantiating (18) with all_60_9, all_89_0, % 45.89/7.00 | | | | | | | all_123_9, all_99_2, all_123_8, all_60_7, all_60_6, % 45.89/7.00 | | | | | | | all_99_1, all_99_0, all_60_4, all_123_7, simplifying % 45.89/7.00 | | | | | | | with (37), (43), (78), (79), (83), (87), (98), (142), % 45.89/7.00 | | | | | | | (146), (155), (161) gives: % 45.89/7.00 | | | | | | | (180) ? [v0: du] : ? [v1: mono_2Etyop_2Emin_2Ebool] : ? [v2: % 45.89/7.00 | | | | | | | any] : ? [v3: u] : ? [v4: du] : ? [v5: % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool] : ? [v6: any] : % 45.89/7.00 | | | | | | | (c_2Ebool_2EIN_2E2(all_123_8, all_60_6) = v3 & % 45.89/7.00 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(v4) = v5 & % 45.89/7.00 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(v0) = v1 & p(v5) = v6 & % 45.89/7.00 | | | | | | | p(v1) = v2 & s(tyop_2Emin_2Ebool, v3) = v4 & % 45.89/7.00 | | | | | | | s(tyop_2Emin_2Ebool, all_123_7) = v0 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(v5) & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(v1) & du(v4) & du(v0) & u(v3) % 45.89/7.00 | | | | | | | & ( ~ (v2 = 0) | (v6 = 0 & ~ (all_123_8 = all_99_1)))) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | GROUND_INST: instantiating (12) with all_60_9, all_123_9, % 45.89/7.00 | | | | | | | all_87_0, all_123_8, all_60_7, all_60_4, all_123_7, % 45.89/7.00 | | | | | | | simplifying with (37), (43), (75), (76), (98), (155), % 45.89/7.00 | | | | | | | (161) gives: % 45.89/7.00 | | | | | | | (181) ? [v0: du] : ? [v1: mono_2Etyop_2Emin_2Ebool] : ? [v2: % 45.89/7.00 | | | | | | | d] : ? [v3: d] : ? [v4: du] : ? [v5: u] : ? [v6: % 45.89/7.00 | | | | | | | du] : ? [v7: u] : ? [v8: du] : % 45.89/7.00 | | | | | | | (j_mono_2Etyop_2Emin_2Ebool(v8) = v1 & % 45.89/7.00 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(v0) = v1 & % 45.89/7.00 | | | | | | | tyop_2Emin_2Efun(all_60_7, tyop_2Emin_2Ebool) = v2 & % 45.89/7.00 | | | | | | | tyop_2Emin_2Efun(all_60_9, v2) = v3 & app_2E2(v6, % 45.89/7.00 | | | | | | | all_60_4) = v7 & app_2E2(v4, all_123_8) = v5 & s(v3, % 45.89/7.00 | | | | | | | c_2Ebool_2EIN_2E0) = v4 & s(v2, v5) = v6 & % 45.89/7.00 | | | | | | | s(tyop_2Emin_2Ebool, v7) = v8 & s(tyop_2Emin_2Ebool, % 45.89/7.00 | | | | | | | all_123_7) = v0 & mono_2Etyop_2Emin_2Ebool(v1) & % 45.89/7.00 | | | | | | | du(v8) & du(v6) & du(v4) & du(v0) & d(v3) & d(v2) & % 45.89/7.00 | | | | | | | u(v7) & u(v5)) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | COMBINE_EQS: (175), (176) imply: % 45.89/7.00 | | | | | | | (182) all_136_0 = all_123_5 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | SIMP: (182) implies: % 45.89/7.00 | | | | | | | (183) all_136_0 = all_123_5 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | COMBINE_EQS: (172), (183) imply: % 45.89/7.00 | | | | | | | (184) all_123_5 = mono_2Ec_2Ebool_2ET_2E0 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | COMBINE_EQS: (176), (184) imply: % 45.89/7.00 | | | | | | | (185) all_142_0 = mono_2Ec_2Ebool_2ET_2E0 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (174) with fresh symbols all_167_0, all_167_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (186) ~ (all_167_0 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(all_136_0) % 45.89/7.00 | | | | | | | = all_167_1 & p(all_167_1) = all_167_0 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_167_1) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (186) implies: % 45.89/7.00 | | | | | | | (187) ~ (all_167_0 = 0) % 45.89/7.00 | | | | | | | (188) p(all_167_1) = all_167_0 % 45.89/7.00 | | | | | | | (189) mono_2Ec_2Ebool_2E_7E_2E1(all_136_0) = all_167_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (173) with fresh symbols all_169_0, all_169_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (190) ~ (all_169_0 = 0) & % 45.89/7.00 | | | | | | | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.00 | | | | | | | all_136_0) = all_169_1 & p(all_169_1) = all_169_0 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_169_1) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (190) implies: % 45.89/7.00 | | | | | | | (191) p(all_169_1) = all_169_0 % 45.89/7.00 | | | | | | | (192) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.00 | | | | | | | all_136_0) = all_169_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (169) with fresh symbols all_171_0, all_171_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (193) ~ (all_171_0 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(all_123_5) % 45.89/7.00 | | | | | | | = all_171_1 & p(all_171_1) = all_171_0 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_171_1) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (193) implies: % 45.89/7.00 | | | | | | | (194) p(all_171_1) = all_171_0 % 45.89/7.00 | | | | | | | (195) mono_2Ec_2Ebool_2E_7E_2E1(all_123_5) = all_171_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (168) with fresh symbols all_173_0, all_173_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (196) ~ (all_173_0 = 0) & % 45.89/7.00 | | | | | | | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.00 | | | | | | | all_123_5) = all_173_1 & p(all_173_1) = all_173_0 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_173_1) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (196) implies: % 45.89/7.00 | | | | | | | (197) p(all_173_1) = all_173_0 % 45.89/7.00 | | | | | | | (198) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.00 | | | | | | | all_123_5) = all_173_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (178) with fresh symbols all_175_0, all_175_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (199) ~ (all_175_0 = 0) & mono_2Ec_2Ebool_2E_7E_2E1(all_142_0) % 45.89/7.00 | | | | | | | = all_175_1 & p(all_175_1) = all_175_0 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_175_1) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (199) implies: % 45.89/7.00 | | | | | | | (200) p(all_175_1) = all_175_0 % 45.89/7.00 | | | | | | | (201) mono_2Ec_2Ebool_2E_7E_2E1(all_142_0) = all_175_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (177) with fresh symbols all_177_0, all_177_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (202) ~ (all_177_0 = 0) & % 45.89/7.00 | | | | | | | mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.00 | | | | | | | all_142_0) = all_177_1 & p(all_177_1) = all_177_0 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_177_1) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (202) implies: % 45.89/7.00 | | | | | | | (203) p(all_177_1) = all_177_0 % 45.89/7.00 | | | | | | | (204) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.00 | | | | | | | all_142_0) = all_177_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (163) with fresh symbols all_179_0, all_179_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (205) i_mono_2Etyop_2Emin_2Ebool(all_179_1) = all_179_0 & % 45.89/7.00 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_179_1 & % 45.89/7.00 | | | | | | | s(tyop_2Emin_2Ebool, all_179_0) = all_123_2 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_179_1) & du(all_123_2) & % 45.89/7.00 | | | | | | | u(all_179_0) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (205) implies: % 45.89/7.00 | | | | | | | (206) j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_179_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (162) with fresh symbols all_189_0, all_189_1 % 45.89/7.00 | | | | | | | gives: % 45.89/7.00 | | | | | | | (207) i_mono_2Etyop_2Emin_2Ebool(all_189_1) = all_189_0 & % 45.89/7.00 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_189_1 & % 45.89/7.00 | | | | | | | s(tyop_2Emin_2Ebool, all_189_0) = all_123_6 & % 45.89/7.00 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_189_1) & du(all_123_6) & % 45.89/7.00 | | | | | | | u(all_189_0) % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | ALPHA: (207) implies: % 45.89/7.00 | | | | | | | (208) j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_189_1 % 45.89/7.00 | | | | | | | % 45.89/7.00 | | | | | | | DELTA: instantiating (180) with fresh symbols all_293_0, % 45.89/7.00 | | | | | | | all_293_1, all_293_2, all_293_3, all_293_4, all_293_5, % 45.89/7.00 | | | | | | | all_293_6 gives: % 45.89/7.01 | | | | | | | (209) c_2Ebool_2EIN_2E2(all_123_8, all_60_6) = all_293_3 & % 45.89/7.01 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_293_2) = all_293_1 & % 45.89/7.01 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_293_6) = all_293_5 & % 45.89/7.01 | | | | | | | p(all_293_1) = all_293_0 & p(all_293_5) = all_293_4 & % 45.89/7.01 | | | | | | | s(tyop_2Emin_2Ebool, all_293_3) = all_293_2 & % 45.89/7.01 | | | | | | | s(tyop_2Emin_2Ebool, all_123_7) = all_293_6 & % 45.89/7.01 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_293_1) & % 45.89/7.01 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_293_5) & du(all_293_2) & % 45.89/7.01 | | | | | | | du(all_293_6) & u(all_293_3) & ( ~ (all_293_4 = 0) | % 45.89/7.01 | | | | | | | (all_293_0 = 0 & ~ (all_123_8 = all_99_1))) % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | ALPHA: (209) implies: % 45.89/7.01 | | | | | | | (210) s(tyop_2Emin_2Ebool, all_123_7) = all_293_6 % 45.89/7.01 | | | | | | | (211) s(tyop_2Emin_2Ebool, all_293_3) = all_293_2 % 45.89/7.01 | | | | | | | (212) p(all_293_5) = all_293_4 % 45.89/7.01 | | | | | | | (213) p(all_293_1) = all_293_0 % 45.89/7.01 | | | | | | | (214) j_mono_2Etyop_2Emin_2Ebool(all_293_6) = all_293_5 % 45.89/7.01 | | | | | | | (215) j_mono_2Etyop_2Emin_2Ebool(all_293_2) = all_293_1 % 45.89/7.01 | | | | | | | (216) c_2Ebool_2EIN_2E2(all_123_8, all_60_6) = all_293_3 % 45.89/7.01 | | | | | | | (217) ~ (all_293_4 = 0) | (all_293_0 = 0 & ~ (all_123_8 = % 45.89/7.01 | | | | | | | all_99_1)) % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | DELTA: instantiating (181) with fresh symbols all_379_0, % 45.89/7.01 | | | | | | | all_379_1, all_379_2, all_379_3, all_379_4, all_379_5, % 45.89/7.01 | | | | | | | all_379_6, all_379_7, all_379_8 gives: % 45.89/7.01 | | | | | | | (218) j_mono_2Etyop_2Emin_2Ebool(all_379_0) = all_379_7 & % 45.89/7.01 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_379_8) = all_379_7 & % 45.89/7.01 | | | | | | | tyop_2Emin_2Efun(all_60_7, tyop_2Emin_2Ebool) = all_379_6 % 45.89/7.01 | | | | | | | & tyop_2Emin_2Efun(all_60_9, all_379_6) = all_379_5 & % 45.89/7.01 | | | | | | | app_2E2(all_379_2, all_60_4) = all_379_1 & % 45.89/7.01 | | | | | | | app_2E2(all_379_4, all_123_8) = all_379_3 & s(all_379_5, % 45.89/7.01 | | | | | | | c_2Ebool_2EIN_2E0) = all_379_4 & s(all_379_6, % 45.89/7.01 | | | | | | | all_379_3) = all_379_2 & s(tyop_2Emin_2Ebool, % 45.89/7.01 | | | | | | | all_379_1) = all_379_0 & s(tyop_2Emin_2Ebool, % 45.89/7.01 | | | | | | | all_123_7) = all_379_8 & % 45.89/7.01 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_379_7) & du(all_379_0) & % 45.89/7.01 | | | | | | | du(all_379_2) & du(all_379_4) & du(all_379_8) & % 45.89/7.01 | | | | | | | d(all_379_5) & d(all_379_6) & u(all_379_1) & u(all_379_3) % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | ALPHA: (218) implies: % 45.89/7.01 | | | | | | | (219) s(tyop_2Emin_2Ebool, all_123_7) = all_379_8 % 45.89/7.01 | | | | | | | (220) j_mono_2Etyop_2Emin_2Ebool(all_379_8) = all_379_7 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | DELTA: instantiating (179) with fresh symbols all_381_0, % 45.89/7.01 | | | | | | | all_381_1, all_381_2, all_381_3, all_381_4, all_381_5, % 45.89/7.01 | | | | | | | all_381_6, all_381_7, all_381_8 gives: % 45.89/7.01 | | | | | | | (221) j_mono_2Etyop_2Emin_2Ebool(all_381_0) = all_381_7 & % 45.89/7.01 | | | | | | | j_mono_2Etyop_2Emin_2Ebool(all_381_8) = all_381_7 & % 45.89/7.01 | | | | | | | tyop_2Emin_2Efun(all_60_7, tyop_2Emin_2Ebool) = all_381_6 % 45.89/7.01 | | | | | | | & tyop_2Emin_2Efun(all_60_9, all_381_6) = all_381_5 & % 45.89/7.01 | | | | | | | app_2E2(all_381_2, all_60_6) = all_381_1 & % 45.89/7.01 | | | | | | | app_2E2(all_381_4, all_123_8) = all_381_3 & s(all_381_5, % 45.89/7.01 | | | | | | | c_2Ebool_2EIN_2E0) = all_381_4 & s(all_381_6, % 45.89/7.01 | | | | | | | all_381_3) = all_381_2 & s(tyop_2Emin_2Ebool, % 45.89/7.01 | | | | | | | all_381_1) = all_381_0 & s(tyop_2Emin_2Ebool, % 45.89/7.01 | | | | | | | all_123_3) = all_381_8 & % 45.89/7.01 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_381_7) & du(all_381_0) & % 45.89/7.01 | | | | | | | du(all_381_2) & du(all_381_4) & du(all_381_8) & % 45.89/7.01 | | | | | | | d(all_381_5) & d(all_381_6) & u(all_381_1) & u(all_381_3) % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | ALPHA: (221) implies: % 45.89/7.01 | | | | | | | (222) s(tyop_2Emin_2Ebool, all_123_3) = all_381_8 % 45.89/7.01 | | | | | | | (223) j_mono_2Etyop_2Emin_2Ebool(all_381_8) = all_381_7 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (185), (204) imply: % 45.89/7.01 | | | | | | | (224) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.01 | | | | | | | mono_2Ec_2Ebool_2ET_2E0) = all_177_1 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (172), (192) imply: % 45.89/7.01 | | | | | | | (225) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.01 | | | | | | | mono_2Ec_2Ebool_2ET_2E0) = all_169_1 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (184), (198) imply: % 45.89/7.01 | | | | | | | (226) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 45.89/7.01 | | | | | | | mono_2Ec_2Ebool_2ET_2E0) = all_173_1 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (158), (184) imply: % 45.89/7.01 | | | | | | | (227) j_mono_2Etyop_2Emin_2Ebool(all_123_6) = % 45.89/7.01 | | | | | | | mono_2Ec_2Ebool_2ET_2E0 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (185), (201) imply: % 45.89/7.01 | | | | | | | (228) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0) = % 45.89/7.01 | | | | | | | all_175_1 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (172), (189) imply: % 45.89/7.01 | | | | | | | (229) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0) = % 45.89/7.01 | | | | | | | all_167_1 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (184), (195) imply: % 45.89/7.01 | | | | | | | (230) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0) = % 45.89/7.01 | | | | | | | all_171_1 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | REDUCE: (115), (172) imply: % 45.89/7.01 | | | | | | | (231) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2EF_2E0) = % 45.89/7.01 | | | | | | | mono_2Ec_2Ebool_2ET_2E0 % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | BETA: splitting (166) gives: % 45.89/7.01 | | | | | | | % 45.89/7.01 | | | | | | | Case 1: % 45.89/7.01 | | | | | | | | % 45.89/7.01 | | | | | | | | (232) all_83_0 = 0 % 45.89/7.01 | | | | | | | | % 45.89/7.01 | | | | | | | | REDUCE: (68), (232) imply: % 45.89/7.01 | | | | | | | | (233) $false % 45.89/7.01 | | | | | | | | % 45.89/7.01 | | | | | | | | CLOSE: (233) is inconsistent. % 45.89/7.01 | | | | | | | | % 45.89/7.01 | | | | | | | Case 2: % 45.89/7.01 | | | | | | | | % 45.89/7.01 | | | | | | | | (234) all_83_1 = all_81_1 | all_81_0 = 0 % 45.89/7.01 | | | | | | | | % 45.89/7.01 | | | | | | | | BETA: splitting (167) gives: % 45.89/7.01 | | | | | | | | % 45.89/7.01 | | | | | | | | Case 1: % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | (235) all_83_0 = 0 % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | REDUCE: (68), (235) imply: % 45.89/7.01 | | | | | | | | | (236) $false % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | CLOSE: (236) is inconsistent. % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | Case 2: % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | (237) ? [v0: mono_2Etyop_2Emin_2Ebool] : % 45.89/7.01 | | | | | | | | | (mono_2Ec_2Ebool_2E_7E_2E1(all_83_1) = v0 & p(v0) = 0 % 45.89/7.01 | | | | | | | | | & mono_2Etyop_2Emin_2Ebool(v0)) % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | DELTA: instantiating (237) with fresh symbol all_414_0 gives: % 45.89/7.01 | | | | | | | | | (238) mono_2Ec_2Ebool_2E_7E_2E1(all_83_1) = all_414_0 & % 45.89/7.01 | | | | | | | | | p(all_414_0) = 0 & % 45.89/7.01 | | | | | | | | | mono_2Etyop_2Emin_2Ebool(all_414_0) % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | ALPHA: (238) implies: % 45.89/7.01 | | | | | | | | | (239) p(all_414_0) = 0 % 45.89/7.01 | | | | | | | | | (240) mono_2Ec_2Ebool_2E_7E_2E1(all_83_1) = all_414_0 % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | BETA: splitting (164) gives: % 45.89/7.01 | | | | | | | | | % 45.89/7.01 | | | | | | | | | Case 1: % 45.89/7.01 | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | (241) all_81_0 = 0 % 45.89/7.01 | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | REDUCE: (63), (241) imply: % 45.89/7.01 | | | | | | | | | | (242) $false % 45.89/7.01 | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | CLOSE: (242) is inconsistent. % 45.89/7.01 | | | | | | | | | | % 45.89/7.01 | | | | | | | | | Case 2: % 45.89/7.01 | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | (243) all_81_1 = mono_2Ec_2Ebool_2EF_2E0 | all_45_0 = 0 % 45.89/7.01 | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | BETA: splitting (171) gives: % 45.89/7.01 | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | Case 1: % 45.89/7.01 | | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | | (244) all_123_0 = 0 % 45.89/7.01 | | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | | REDUCE: (148), (244) imply: % 45.89/7.01 | | | | | | | | | | | (245) $false % 45.89/7.01 | | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | | CLOSE: (245) is inconsistent. % 45.89/7.01 | | | | | | | | | | | % 45.89/7.01 | | | | | | | | | | Case 2: % 45.89/7.01 | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | (246) ? [v0: mono_2Etyop_2Emin_2Ebool] : % 46.49/7.01 | | | | | | | | | | | (mono_2Ec_2Ebool_2E_7E_2E1(all_123_1) = v0 & p(v0) % 46.49/7.01 | | | | | | | | | | | = 0 & mono_2Etyop_2Emin_2Ebool(v0)) % 46.49/7.01 | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | DELTA: instantiating (246) with fresh symbol all_437_0 % 46.49/7.01 | | | | | | | | | | | gives: % 46.49/7.01 | | | | | | | | | | | (247) mono_2Ec_2Ebool_2E_7E_2E1(all_123_1) = all_437_0 & % 46.49/7.01 | | | | | | | | | | | p(all_437_0) = 0 & % 46.49/7.01 | | | | | | | | | | | mono_2Etyop_2Emin_2Ebool(all_437_0) % 46.49/7.01 | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | ALPHA: (247) implies: % 46.49/7.01 | | | | | | | | | | | (248) mono_2Ec_2Ebool_2E_7E_2E1(all_123_1) = all_437_0 % 46.49/7.01 | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | BETA: splitting (165) gives: % 46.49/7.01 | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | Case 1: % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | (249) all_81_0 = 0 % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | REDUCE: (63), (249) imply: % 46.49/7.01 | | | | | | | | | | | | (250) $false % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | CLOSE: (250) is inconsistent. % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | Case 2: % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | (251) ? [v0: mono_2Etyop_2Emin_2Ebool] : % 46.49/7.01 | | | | | | | | | | | | (mono_2Ec_2Ebool_2E_7E_2E1(all_81_1) = v0 & p(v0) % 46.49/7.01 | | | | | | | | | | | | = 0 & mono_2Etyop_2Emin_2Ebool(v0)) % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | DELTA: instantiating (251) with fresh symbol all_446_0 % 46.49/7.01 | | | | | | | | | | | | gives: % 46.49/7.01 | | | | | | | | | | | | (252) mono_2Ec_2Ebool_2E_7E_2E1(all_81_1) = all_446_0 & % 46.49/7.01 | | | | | | | | | | | | p(all_446_0) = 0 & % 46.49/7.01 | | | | | | | | | | | | mono_2Etyop_2Emin_2Ebool(all_446_0) % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | ALPHA: (252) implies: % 46.49/7.01 | | | | | | | | | | | | (253) mono_2Ec_2Ebool_2E_7E_2E1(all_81_1) = all_446_0 % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | BETA: splitting (243) gives: % 46.49/7.01 | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | Case 1: % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | (254) all_45_0 = 0 % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | REDUCE: (30), (254) imply: % 46.49/7.01 | | | | | | | | | | | | | (255) $false % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | CLOSE: (255) is inconsistent. % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | Case 2: % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | (256) all_81_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | REDUCE: (253), (256) imply: % 46.49/7.01 | | | | | | | | | | | | | (257) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2EF_2E0) % 46.49/7.01 | | | | | | | | | | | | | = all_446_0 % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | REDUCE: (66), (256) imply: % 46.49/7.01 | | | | | | | | | | | | | (258) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0) % 46.49/7.01 | | | | | | | | | | | | | = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | REDUCE: (65), (256) imply: % 46.49/7.01 | | | | | | | | | | | | | (259) p(mono_2Ec_2Ebool_2EF_2E0) = all_81_0 % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | BETA: splitting (234) gives: % 46.49/7.01 | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | Case 1: % 46.49/7.01 | | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | | (260) all_81_0 = 0 % 46.49/7.01 | | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | | REDUCE: (63), (260) imply: % 46.49/7.01 | | | | | | | | | | | | | | (261) $false % 46.49/7.01 | | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | | CLOSE: (261) is inconsistent. % 46.49/7.01 | | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | Case 2: % 46.49/7.01 | | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | | (262) all_83_1 = all_81_1 % 46.49/7.01 | | | | | | | | | | | | | | % 46.49/7.01 | | | | | | | | | | | | | | COMBINE_EQS: (256), (262) imply: % 46.49/7.01 | | | | | | | | | | | | | | (263) all_83_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.01 | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | REDUCE: (71), (263) imply: % 46.49/7.02 | | | | | | | | | | | | | | (264) mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E0, % 46.49/7.02 | | | | | | | | | | | | | | mono_2Ec_2Ebool_2ET_2E0) = % 46.49/7.02 | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | REDUCE: (240), (263) imply: % 46.49/7.02 | | | | | | | | | | | | | | (265) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2EF_2E0) % 46.49/7.02 | | | | | | | | | | | | | | = all_414_0 % 46.49/7.02 | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | REDUCE: (70), (263) imply: % 46.49/7.02 | | | | | | | | | | | | | | (266) p(mono_2Ec_2Ebool_2EF_2E0) = all_83_0 % 46.49/7.02 | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | BETA: splitting (170) gives: % 46.49/7.02 | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | Case 1: % 46.49/7.02 | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | (267) all_123_0 = 0 % 46.49/7.02 | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | REDUCE: (148), (267) imply: % 46.49/7.02 | | | | | | | | | | | | | | | (268) $false % 46.49/7.02 | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | CLOSE: (268) is inconsistent. % 46.49/7.02 | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | Case 2: % 46.49/7.02 | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | (269) all_123_1 = all_81_1 | all_81_0 = 0 % 46.49/7.02 | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | BETA: splitting (269) gives: % 46.49/7.02 | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | Case 1: % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | (270) all_81_0 = 0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (63), (270) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (271) $false % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | CLOSE: (271) is inconsistent. % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | Case 2: % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | (272) all_123_1 = all_81_1 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (256), (272) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (273) all_123_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (159), (273) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (274) j_mono_2Etyop_2Emin_2Ebool(all_123_2) = % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (248), (273) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (275) mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2EF_2E0) % 46.49/7.02 | | | | | | | | | | | | | | | | = all_437_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (157), (273) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (276) p(mono_2Ec_2Ebool_2EF_2E0) = all_123_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_123_6, all_379_8, % 46.49/7.02 | | | | | | | | | | | | | | | | all_123_7, tyop_2Emin_2Ebool, simplifying with % 46.49/7.02 | | | | | | | | | | | | | | | | (153), (219) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (277) all_379_8 = all_123_6 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_293_6, all_379_8, % 46.49/7.02 | | | | | | | | | | | | | | | | all_123_7, tyop_2Emin_2Ebool, simplifying with % 46.49/7.02 | | | | | | | | | | | | | | | | (210), (219) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (278) all_379_8 = all_293_6 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_123_2, all_381_8, % 46.49/7.02 | | | | | | | | | | | | | | | | all_123_3, tyop_2Emin_2Ebool, simplifying with % 46.49/7.02 | | | | | | | | | | | | | | | | (154), (222) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (279) all_381_8 = all_123_2 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_45_0, all_123_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (31), % 46.49/7.02 | | | | | | | | | | | | | | | | (276) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (280) all_123_0 = all_45_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_83_0, all_123_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (266), % 46.49/7.02 | | | | | | | | | | | | | | | | (276) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (281) all_123_0 = all_83_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_81_0, all_123_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (259), % 46.49/7.02 | | | | | | | | | | | | | | | | (276) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (282) all_123_0 = all_81_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_437_0, all_446_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (257), % 46.49/7.02 | | | | | | | | | | | | | | | | (275) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (283) all_446_0 = all_437_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_414_0, all_446_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (257), % 46.49/7.02 | | | | | | | | | | | | | | | | (265) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (284) all_446_0 = all_414_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with mono_2Ec_2Ebool_2ET_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | all_446_0, mono_2Ec_2Ebool_2EF_2E0, simplifying % 46.49/7.02 | | | | | | | | | | | | | | | | with (231), (257) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (285) all_446_0 = mono_2Ec_2Ebool_2ET_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with mono_2Ec_2Ebool_2EF_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | all_171_1, mono_2Ec_2Ebool_2ET_2E0, simplifying % 46.49/7.02 | | | | | | | | | | | | | | | | with (230), (258) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (286) all_171_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_171_1, all_175_1, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2ET_2E0, simplifying with (228), % 46.49/7.02 | | | | | | | | | | | | | | | | (230) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (287) all_175_1 = all_171_1 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (22) with all_167_1, all_175_1, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2ET_2E0, simplifying with (228), % 46.49/7.02 | | | | | | | | | | | | | | | | (229) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (288) all_175_1 = all_167_1 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2ET_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | all_189_1, all_123_6, simplifying with (208), % 46.49/7.02 | | | | | | | | | | | | | | | | (227) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (289) all_189_1 = mono_2Ec_2Ebool_2ET_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2EF_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | all_179_1, all_123_2, simplifying with (206), % 46.49/7.02 | | | | | | | | | | | | | | | | (274) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (290) all_179_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with all_169_1, all_173_1, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2ET_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2E_7E_2E0, simplifying with (225), % 46.49/7.02 | | | | | | | | | | | | | | | | (226) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (291) all_173_1 = all_169_1 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with all_173_1, all_177_1, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2ET_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2E_7E_2E0, simplifying with (224), % 46.49/7.02 | | | | | | | | | | | | | | | | (226) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (292) all_177_1 = all_173_1 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with mono_2Ec_2Ebool_2EF_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | all_177_1, mono_2Ec_2Ebool_2ET_2E0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2E_7E_2E0, simplifying with (224), % 46.49/7.02 | | | | | | | | | | | | | | | | (264) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (293) all_177_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with all_123_3, all_293_3, % 46.49/7.02 | | | | | | | | | | | | | | | | all_60_6, all_123_8, simplifying with (160), (216) % 46.49/7.02 | | | | | | | | | | | | | | | | gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (294) all_293_3 = all_123_3 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (283), (285) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (295) all_437_0 = mono_2Ec_2Ebool_2ET_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (283), (284) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (296) all_437_0 = all_414_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (295), (296) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (297) all_414_0 = mono_2Ec_2Ebool_2ET_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | SIMP: (297) implies: % 46.49/7.02 | | | | | | | | | | | | | | | | (298) all_414_0 = mono_2Ec_2Ebool_2ET_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (277), (278) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (299) all_293_6 = all_123_6 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | SIMP: (299) implies: % 46.49/7.02 | | | | | | | | | | | | | | | | (300) all_293_6 = all_123_6 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (292), (293) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (301) all_173_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | SIMP: (301) implies: % 46.49/7.02 | | | | | | | | | | | | | | | | (302) all_173_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (287), (288) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (303) all_171_1 = all_167_1 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | SIMP: (303) implies: % 46.49/7.02 | | | | | | | | | | | | | | | | (304) all_171_1 = all_167_1 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (291), (302) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (305) all_169_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | SIMP: (305) implies: % 46.49/7.02 | | | | | | | | | | | | | | | | (306) all_169_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (286), (304) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (307) all_167_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (280), (281) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (308) all_83_0 = all_45_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (281), (282) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (309) all_83_0 = all_81_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (308), (309) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (310) all_81_0 = all_45_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | COMBINE_EQS: (288), (307) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (311) all_175_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (223), (279) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (312) j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_381_7 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (220), (277) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (313) j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_379_7 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (214), (300) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (314) j_mono_2Etyop_2Emin_2Ebool(all_123_6) = all_293_5 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (203), (293) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (315) p(mono_2Ec_2Ebool_2EF_2E0) = all_177_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (200), (311) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (316) p(mono_2Ec_2Ebool_2EF_2E0) = all_175_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (197), (302) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (317) p(mono_2Ec_2Ebool_2EF_2E0) = all_173_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (194), (286) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (318) p(mono_2Ec_2Ebool_2EF_2E0) = all_171_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (191), (306) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (319) p(mono_2Ec_2Ebool_2EF_2E0) = all_169_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (188), (307) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (320) p(mono_2Ec_2Ebool_2EF_2E0) = all_167_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | REDUCE: (211), (294) imply: % 46.49/7.02 | | | | | | | | | | | | | | | | (321) s(tyop_2Emin_2Ebool, all_123_3) = all_293_2 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_123_2, all_293_2, % 46.49/7.02 | | | | | | | | | | | | | | | | all_123_3, tyop_2Emin_2Ebool, simplifying with % 46.49/7.02 | | | | | | | | | | | | | | | | (154), (321) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (322) all_293_2 = all_123_2 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_173_0, all_175_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (316), % 46.49/7.02 | | | | | | | | | | | | | | | | (317) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (323) all_175_0 = all_173_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_171_0, all_175_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (316), % 46.49/7.02 | | | | | | | | | | | | | | | | (318) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (324) all_175_0 = all_171_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_169_0, all_175_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (316), % 46.49/7.02 | | | | | | | | | | | | | | | | (319) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (325) all_175_0 = all_169_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_167_0, all_175_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (316), % 46.49/7.02 | | | | | | | | | | | | | | | | (320) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (326) all_175_0 = all_167_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_45_0, all_177_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (31), % 46.49/7.02 | | | | | | | | | | | | | | | | (315) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (327) all_177_0 = all_45_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.02 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with all_171_0, all_177_0, % 46.49/7.02 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2EF_2E0, simplifying with (315), % 46.49/7.02 | | | | | | | | | | | | | | | | (318) gives: % 46.49/7.02 | | | | | | | | | | | | | | | | (328) all_177_0 = all_171_0 % 46.49/7.02 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2ET_2E0, % 46.49/7.03 | | | | | | | | | | | | | | | | all_379_7, all_123_6, simplifying with (227), % 46.49/7.03 | | | | | | | | | | | | | | | | (313) gives: % 46.49/7.03 | | | | | | | | | | | | | | | | (329) all_379_7 = mono_2Ec_2Ebool_2ET_2E0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with all_293_5, all_379_7, % 46.49/7.03 | | | | | | | | | | | | | | | | all_123_6, simplifying with (313), (314) gives: % 46.49/7.03 | | | | | | | | | | | | | | | | (330) all_379_7 = all_293_5 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2EF_2E0, % 46.49/7.03 | | | | | | | | | | | | | | | | all_381_7, all_123_2, simplifying with (274), % 46.49/7.03 | | | | | | | | | | | | | | | | (312) gives: % 46.49/7.03 | | | | | | | | | | | | | | | | (331) all_381_7 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (329), (330) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (332) all_293_5 = mono_2Ec_2Ebool_2ET_2E0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (327), (328) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (333) all_171_0 = all_45_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | SIMP: (333) implies: % 46.49/7.03 | | | | | | | | | | | | | | | | (334) all_171_0 = all_45_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (323), (324) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (335) all_173_0 = all_171_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (323), (325) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (336) all_173_0 = all_169_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (323), (326) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (337) all_173_0 = all_167_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (336), (337) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (338) all_169_0 = all_167_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (335), (336) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (339) all_171_0 = all_169_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | SIMP: (339) implies: % 46.49/7.03 | | | | | | | | | | | | | | | | (340) all_171_0 = all_169_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (334), (340) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (341) all_169_0 = all_45_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | SIMP: (341) implies: % 46.49/7.03 | | | | | | | | | | | | | | | | (342) all_169_0 = all_45_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | COMBINE_EQS: (338), (342) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (343) all_167_0 = all_45_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | REDUCE: (215), (322) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (344) j_mono_2Etyop_2Emin_2Ebool(all_123_2) = all_293_1 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | REDUCE: (212), (332) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (345) p(mono_2Ec_2Ebool_2ET_2E0) = all_293_4 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (21) with 0, all_293_4, % 46.49/7.03 | | | | | | | | | | | | | | | | mono_2Ec_2Ebool_2ET_2E0, simplifying with (3), % 46.49/7.03 | | | | | | | | | | | | | | | | (345) gives: % 46.49/7.03 | | | | | | | | | | | | | | | | (346) all_293_4 = 0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2EF_2E0, % 46.49/7.03 | | | | | | | | | | | | | | | | all_293_1, all_123_2, simplifying with (274), % 46.49/7.03 | | | | | | | | | | | | | | | | (344) gives: % 46.49/7.03 | | | | | | | | | | | | | | | | (347) all_293_1 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | REDUCE: (213), (347) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | (348) p(mono_2Ec_2Ebool_2EF_2E0) = all_293_0 % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | BETA: splitting (217) gives: % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | Case 1: % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | | (349) ~ (all_293_4 = 0) % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | | REDUCE: (346), (349) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | | (350) $false % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | | CLOSE: (350) is inconsistent. % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | Case 2: % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | | (351) all_293_0 = 0 & ~ (all_123_8 = all_99_1) % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | | ALPHA: (351) implies: % 46.49/7.03 | | | | | | | | | | | | | | | | | (352) all_293_0 = 0 % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | | REDUCE: (348), (352) imply: % 46.49/7.03 | | | | | | | | | | | | | | | | | (353) p(mono_2Ec_2Ebool_2EF_2E0) = 0 % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | | REF_CLOSE: (21), (30), (31), (353) are inconsistent by % 46.49/7.03 | | | | | | | | | | | | | | | | | sub-proof #1. % 46.49/7.03 | | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | | | % 46.49/7.03 | | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | | % 46.49/7.03 | | | | | | | | | End of split % 46.49/7.03 | | | | | | | | | % 46.49/7.03 | | | | | | | | End of split % 46.49/7.03 | | | | | | | | % 46.49/7.03 | | | | | | | End of split % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | Case 2: % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | | (354) all_123_10 = 0 & j_mono_2Etyop_2Emin_2Ebool(all_123_12) = % 46.49/7.03 | | | | | | | all_123_11 & p(all_123_11) = 0 & s(tyop_2Emin_2Ebool, % 46.49/7.03 | | | | | | | all_60_3) = all_123_12 & % 46.49/7.03 | | | | | | | mono_2Etyop_2Emin_2Ebool(all_123_11) & du(all_123_12) % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | | ALPHA: (354) implies: % 46.49/7.03 | | | | | | | (355) s(tyop_2Emin_2Ebool, all_60_3) = all_123_12 % 46.49/7.03 | | | | | | | (356) p(all_123_11) = 0 % 46.49/7.03 | | | | | | | (357) j_mono_2Etyop_2Emin_2Ebool(all_123_12) = all_123_11 % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | | GROUND_INST: instantiating (26) with all_60_2, all_123_12, % 46.49/7.03 | | | | | | | all_60_3, tyop_2Emin_2Ebool, simplifying with (40), % 46.49/7.03 | | | | | | | (355) gives: % 46.49/7.03 | | | | | | | (358) all_123_12 = all_60_2 % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | | REDUCE: (357), (358) imply: % 46.49/7.03 | | | | | | | (359) j_mono_2Etyop_2Emin_2Ebool(all_60_2) = all_123_11 % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | | GROUND_INST: instantiating (23) with mono_2Ec_2Ebool_2EF_2E0, % 46.49/7.03 | | | | | | | all_123_11, all_60_2, simplifying with (106), (359) % 46.49/7.03 | | | | | | | gives: % 46.49/7.03 | | | | | | | (360) all_123_11 = mono_2Ec_2Ebool_2EF_2E0 % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | | REDUCE: (356), (360) imply: % 46.49/7.03 | | | | | | | (361) p(mono_2Ec_2Ebool_2EF_2E0) = 0 % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | | REF_CLOSE: (21), (30), (31), (361) are inconsistent by sub-proof % 46.49/7.03 | | | | | | | #1. % 46.49/7.03 | | | | | | | % 46.49/7.03 | | | | | | End of split % 46.49/7.03 | | | | | | % 46.49/7.03 | | | | | End of split % 46.49/7.03 | | | | | % 46.49/7.03 | | | | End of split % 46.49/7.03 | | | | % 46.49/7.03 | | | End of split % 46.49/7.03 | | | % 46.49/7.03 | | End of split % 46.49/7.03 | | % 46.49/7.03 | End of split % 46.49/7.03 | % 46.49/7.03 End of proof % 46.49/7.03 % 46.49/7.03 Sub-proof #1 shows that the following formulas are inconsistent: % 46.49/7.03 ---------------------------------------------------------------- % 46.49/7.03 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 46.49/7.03 mono_2Etyop_2Emin_2Ebool] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = % 46.49/7.03 v0)) % 46.49/7.03 (2) p(mono_2Ec_2Ebool_2EF_2E0) = all_45_0 % 46.49/7.03 (3) p(mono_2Ec_2Ebool_2EF_2E0) = 0 % 46.49/7.03 (4) ~ (all_45_0 = 0) % 46.49/7.03 % 46.49/7.03 Begin of proof % 46.49/7.03 | % 46.49/7.03 | GROUND_INST: instantiating (1) with all_45_0, 0, mono_2Ec_2Ebool_2EF_2E0, % 46.49/7.03 | simplifying with (2), (3) gives: % 46.49/7.03 | (5) all_45_0 = 0 % 46.49/7.03 | % 46.49/7.03 | REDUCE: (4), (5) imply: % 46.49/7.03 | (6) $false % 46.49/7.03 | % 46.49/7.03 | CLOSE: (6) is inconsistent. % 46.49/7.03 | % 46.49/7.03 End of proof % 46.49/7.03 % SZS output end Proof for theBenchmark % 46.49/7.03 % 46.49/7.03 6414ms %------------------------------------------------------------------------------