%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW585_2 : TPTP v8.1.2. Released v6.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Sep 1 00:50:48 EDT 2023 % Result : Theorem 33.08s 5.27s % Output : Proof 69.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW585_2 : TPTP v8.1.2. Released v6.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n021.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 20:26:57 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.60 ________ _____ % 0.19/0.60 ___ __ \_________(_)________________________________ % 0.19/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.60 % 0.19/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.60 (2023-06-19) % 0.19/0.60 % 0.19/0.60 (c) Philipp Rümmer, 2009-2023 % 0.19/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.60 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.73/1.48 Prover 4: Preprocessing ... % 4.73/1.49 Prover 0: Preprocessing ... % 4.73/1.49 Prover 3: Preprocessing ... % 5.49/1.52 Prover 6: Preprocessing ... % 5.49/1.52 Prover 5: Preprocessing ... % 5.71/1.55 Prover 2: Preprocessing ... % 5.71/1.55 Prover 1: Preprocessing ... % 13.86/2.65 Prover 1: Warning: ignoring some quantifiers % 14.14/2.72 Prover 3: Warning: ignoring some quantifiers % 14.14/2.78 Prover 4: Warning: ignoring some quantifiers % 14.14/2.80 Prover 3: Constructing countermodel ... % 14.14/2.83 Prover 1: Constructing countermodel ... % 14.14/2.84 Prover 6: Proving ... % 15.53/2.92 Prover 5: Proving ... % 16.09/2.96 Prover 4: Constructing countermodel ... % 16.57/3.02 Prover 0: Proving ... % 17.75/3.19 Prover 2: Proving ... % 33.08/5.26 Prover 0: proved (4643ms) % 33.08/5.26 % 33.08/5.27 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.08/5.27 % 33.08/5.27 Prover 3: stopped % 33.08/5.27 Prover 2: stopped % 33.08/5.27 Prover 6: stopped % 33.08/5.28 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 33.08/5.28 Prover 5: stopped % 33.08/5.29 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 33.08/5.29 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 33.08/5.29 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 33.08/5.29 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 35.38/5.59 Prover 13: Preprocessing ... % 35.38/5.60 Prover 11: Preprocessing ... % 35.38/5.60 Prover 7: Preprocessing ... % 35.38/5.60 Prover 10: Preprocessing ... % 36.02/5.64 Prover 8: Preprocessing ... % 38.40/5.94 Prover 7: Warning: ignoring some quantifiers % 38.40/5.97 Prover 8: Warning: ignoring some quantifiers % 38.40/5.97 Prover 10: Warning: ignoring some quantifiers % 38.40/5.98 Prover 13: Warning: ignoring some quantifiers % 38.40/5.99 Prover 7: Constructing countermodel ... % 38.40/5.99 Prover 10: Constructing countermodel ... % 38.97/6.03 Prover 8: Constructing countermodel ... % 38.97/6.03 Prover 13: Constructing countermodel ... % 38.97/6.06 Prover 11: Warning: ignoring some quantifiers % 39.52/6.09 Prover 11: Constructing countermodel ... % 68.13/9.88 Prover 11: Found proof (size 129) % 68.13/9.88 Prover 11: proved (4594ms) % 68.13/9.88 Prover 7: stopped % 68.13/9.88 Prover 10: stopped % 68.13/9.88 Prover 4: stopped % 68.13/9.88 Prover 13: stopped % 68.13/9.88 Prover 1: stopped % 68.13/9.89 Prover 8: stopped % 68.13/9.89 % 68.13/9.89 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 68.13/9.89 % 68.13/9.90 % SZS output start Proof for theBenchmark % 68.13/9.91 Assumptions after simplification: % 68.13/9.91 --------------------------------- % 68.13/9.91 % 68.13/9.91 (cps2_correct) % 68.13/9.92 lprp_mngt_value(fc3) & int_mngt_value(vnum_closure) & ty(value1) & ? [v0: % 68.13/9.92 uni] : ? [v1: uni] : (t2tb5(fc3) = v1 & t2tb4(vnum_closure) = v0 & uni(v1) % 68.13/9.92 & uni(v0) & ! [v2: expr] : ! [v3: uni] : ( ~ (eval_2(value1, v2, v0, v1) = % 68.13/9.92 v3) | ~ expr(v2) | ? [v4: value] : (tb2t(v3) = v4 & eval_0(v2) = v4 & % 68.13/9.92 value(v4))) & ! [v2: expr] : ! [v3: value] : ( ~ (eval_0(v2) = v3) | % 68.13/9.92 ~ expr(v2) | ? [v4: uni] : (eval_2(value1, v2, v0, v1) = v4 & tb2t(v4) = % 68.13/9.92 v3 & value(v3) & uni(v4)))) % 68.13/9.92 % 68.13/9.92 (cps2_correct_expr) % 68.13/9.93 tuple0(tuple02) & ty(tuple01) & ty(int) & ? [v0: uni] : (t2tb2(tuple02) = v0 % 68.13/9.93 & uni(v0) & ! [v1: ty] : ! [v2: expr] : ! [v3: uni] : ! [v4: uni] : ! % 68.13/9.93 [v5: value] : ! [v6: int] : ! [v7: uni] : ! [v8: uni] : ! [v9: uni] : ! % 68.13/9.93 [v10: uni] : ( ~ (t2tb3(v6) = v7) | ~ (infix_at(v1, tuple01, v3, v0) = v9) % 68.13/9.93 | ~ (infix_at(v1, int, v4, v7) = v8) | ~ (eval_0(v2) = v5) | ~ % 68.13/9.93 (vnum_proj_1(v5) = v6) | ~ (match_value(v1, v5, v8, v9) = v10) | ~ % 68.13/9.93 expr(v2) | ~ ty(v1) | ~ uni(v4) | ~ uni(v3) | (eval_2(v1, v2, v4, v3) = % 68.13/9.93 v10 & uni(v10))) & ! [v1: ty] : ! [v2: expr] : ! [v3: uni] : ! [v4: % 68.13/9.93 uni] : ! [v5: uni] : ( ~ (eval_2(v1, v2, v4, v3) = v5) | ~ expr(v2) | ~ % 68.13/9.93 ty(v1) | ~ uni(v4) | ~ uni(v3) | ? [v6: value] : ? [v7: int] : ? [v8: % 68.13/9.93 uni] : ? [v9: uni] : ? [v10: uni] : (t2tb3(v7) = v8 & infix_at(v1, % 68.13/9.93 tuple01, v3, v0) = v10 & infix_at(v1, int, v4, v8) = v9 & eval_0(v2) = % 68.13/9.93 v6 & vnum_proj_1(v6) = v7 & match_value(v1, v6, v9, v10) = v5 & % 68.13/9.93 value(v6) & uni(v10) & uni(v9) & uni(v8) & uni(v5)))) % 68.13/9.93 % 68.13/9.93 (cps3_correct) % 68.13/9.93 int_mngt_value(vnum_closure) & ! [v0: expr] : ! [v1: value] : ( ~ % 68.13/9.93 (eval_3(v0, vnum_closure) = v1) | ~ expr(v0) | (eval_0(v0) = v1 & % 68.13/9.93 value(v1))) & ! [v0: expr] : ! [v1: value] : ( ~ (eval_0(v0) = v1) | ~ % 68.13/9.93 expr(v0) | (eval_3(v0, vnum_closure) = v1 & value(v1))) % 68.13/9.93 % 68.13/9.93 (cps3_correct_expr) % 68.13/9.94 value(underflow) & ty(value1) & ty(int) & ? [v0: uni] : (t2tb(underflow) = v0 % 68.13/9.94 & uni(v0) & ! [v1: expr] : ! [v2: int_mngt_value] : ! [v3: value] : ! % 68.13/9.94 [v4: uni] : ! [v5: int] : ! [v6: uni] : ! [v7: uni] : ( ~ (t2tb4(v2) = % 68.13/9.94 v4) | ~ (t2tb3(v5) = v6) | ~ (infix_at(value1, int, v4, v6) = v7) | ~ % 68.13/9.94 (eval_0(v1) = v3) | ~ (vnum_proj_1(v3) = v5) | ~ int_mngt_value(v2) | ~ % 68.13/9.94 expr(v1) | ? [v8: value] : ? [v9: uni] : (eval_3(v1, v2) = v8 & tb2t(v9) % 68.13/9.94 = v8 & match_value(value1, v3, v7, v0) = v9 & value(v8) & uni(v9))) & ! % 68.13/9.94 [v1: expr] : ! [v2: int_mngt_value] : ! [v3: value] : ( ~ (eval_3(v1, v2) % 68.13/9.94 = v3) | ~ int_mngt_value(v2) | ~ expr(v1) | ? [v4: value] : ? [v5: % 68.13/9.94 uni] : ? [v6: int] : ? [v7: uni] : ? [v8: uni] : ? [v9: uni] : % 68.13/9.94 (t2tb4(v2) = v5 & t2tb3(v6) = v7 & tb2t(v9) = v3 & infix_at(value1, int, % 68.13/9.94 v5, v7) = v8 & eval_0(v1) = v4 & vnum_proj_1(v4) = v6 & % 68.13/9.94 match_value(value1, v4, v8, v0) = v9 & value(v4) & value(v3) & uni(v9) & % 68.13/9.94 uni(v8) & uni(v7) & uni(v5)))) % 68.13/9.94 % 68.13/9.94 (cps_correct) % 68.13/9.94 value_mngt_value(fc2) & ty(value1) & ? [v0: uni] : (t2tb1(fc2) = v0 & uni(v0) % 68.13/9.94 & ! [v1: expr] : ! [v2: uni] : ( ~ (eval_1(value1, v1, v0) = v2) | ~ % 68.13/9.94 expr(v1) | ? [v3: value] : (tb2t(v2) = v3 & eval_0(v1) = v3 & value(v3))) % 68.13/9.94 & ! [v1: expr] : ! [v2: value] : ( ~ (eval_0(v1) = v2) | ~ expr(v1) | ? % 68.13/9.94 [v3: uni] : (tb2t(v3) = v2 & eval_1(value1, v1, v0) = v3 & value(v2) & % 68.13/9.94 uni(v3)))) % 68.13/9.94 % 68.13/9.94 (cps_correct_expr) % 68.13/9.94 ty(value1) & ! [v0: ty] : ! [v1: expr] : ! [v2: uni] : ! [v3: value] : ! % 68.13/9.94 [v4: uni] : ! [v5: uni] : ( ~ (t2tb(v3) = v4) | ~ (infix_at(v0, value1, v2, % 68.13/9.94 v4) = v5) | ~ (eval_0(v1) = v3) | ~ expr(v1) | ~ ty(v0) | ~ uni(v2) % 68.13/9.94 | (eval_1(v0, v1, v2) = v5 & uni(v5))) & ! [v0: ty] : ! [v1: expr] : ! % 68.13/9.94 [v2: uni] : ! [v3: uni] : ( ~ (eval_1(v0, v1, v2) = v3) | ~ expr(v1) | ~ % 68.13/9.94 ty(v0) | ~ uni(v2) | ? [v4: value] : ? [v5: uni] : (t2tb(v4) = v5 & % 68.13/9.94 infix_at(v0, value1, v2, v5) = v3 & eval_0(v1) = v4 & value(v4) & uni(v5) % 68.13/9.94 & uni(v3))) % 68.13/9.94 % 68.13/9.94 (eval_0_def) % 68.13/9.95 value(underflow) & ! [v0: expr] : ! [v1: expr] : ! [v2: int] : ! [v3: % 68.13/9.95 value] : ! [v4: expr] : ! [v5: value] : ( ~ (eval_0(v4) = v5) | ~ % 68.13/9.95 (vnum(v2) = v3) | ~ (sub(v0, v1) = v4) | ~ expr(v1) | ~ expr(v0) | ? % 68.13/9.95 [v6: value] : ? [v7: value] : (( ~ (v6 = v3) & eval_0(v0) = v6 & value(v6)) % 68.13/9.95 | (eval_0(v1) = v7 & value(v7) & ! [v8: int] : ! [v9: value] : (v9 = v5 % 68.13/9.95 | ~ ($lesseq(v8, v2)) | ~ (vnum($difference(v2, v8)) = v9) | ? % 68.13/9.95 [v10: value] : ( ~ (v10 = v7) & vnum(v8) = v10 & value(v10))) & ! % 68.13/9.95 [v8: int] : ! [v9: value] : (v5 = underflow | ~ ($lesseq(1, % 68.13/9.95 $difference(v8, v2))) | ~ (vnum($difference(v2, v8)) = v9) | ? % 68.13/9.95 [v10: value] : ( ~ (v10 = v7) & vnum(v8) = v10 & value(v10))) & ! % 68.13/9.95 [v8: int] : (v5 = underflow | ~ ($lesseq(1, $difference(v8, v2))) | ~ % 68.13/9.95 (vnum(v8) = v7)) & ! [v8: int] : ( ~ ($lesseq(v8, v2)) | ~ (vnum(v8) % 68.13/9.95 = v7) | (vnum($difference(v2, v8)) = v5 & value(v5))) & ( ~ (v7 = % 68.13/9.95 underflow) | v5 = underflow)))) & ! [v0: expr] : ! [v1: expr] : ! % 68.13/9.95 [v2: int] : ! [v3: value] : ! [v4: value] : ( ~ (eval_0(v1) = v4) | ~ % 68.13/9.95 (eval_0(v0) = v3) | ~ (vnum(v2) = v3) | ~ expr(v1) | ~ expr(v0) | ? [v5: % 68.13/9.95 expr] : ? [v6: value] : (eval_0(v5) = v6 & sub(v0, v1) = v5 & value(v6) & % 68.13/9.95 expr(v5) & ! [v7: int] : ! [v8: value] : (v8 = v6 | ~ ($lesseq(v7, v2)) % 68.13/9.95 | ~ (vnum($difference(v2, v7)) = v8) | ? [v9: value] : ( ~ (v9 = v4) & % 68.13/9.95 vnum(v7) = v9 & value(v9))) & ! [v7: int] : ! [v8: value] : (v6 = % 68.13/9.95 underflow | ~ ($lesseq(1, $difference(v7, v2))) | ~ % 68.13/9.95 (vnum($difference(v2, v7)) = v8) | ? [v9: value] : ( ~ (v9 = v4) & % 68.13/9.95 vnum(v7) = v9 & value(v9))) & ! [v7: int] : (v6 = underflow | ~ % 68.13/9.95 ($lesseq(1, $difference(v7, v2))) | ~ (vnum(v7) = v4)) & ! [v7: int] : % 68.13/9.95 ( ~ ($lesseq(v7, v2)) | ~ (vnum(v7) = v4) | vnum($difference(v2, v7)) = % 68.13/9.95 v6) & ( ~ (v4 = underflow) | v6 = underflow))) & ! [v0: expr] : ! [v1: % 68.13/9.95 expr] : ! [v2: expr] : ( ~ (sub(v0, v1) = v2) | ~ expr(v1) | ~ expr(v0) | % 68.13/9.95 ? [v3: value] : ? [v4: value] : ((v4 = underflow & eval_0(v2) = underflow) % 68.13/9.95 | ( ~ (v3 = underflow) & eval_0(v0) = v3 & value(v3)))) & ! [v0: int] : % 68.13/9.95 ! [v1: expr] : ( ~ ($lesseq(v0, -1)) | ~ (cte(v0) = v1) | eval_0(v1) = % 68.13/9.95 underflow) & ! [v0: int] : ! [v1: value] : ( ~ ($lesseq(0, v0)) | ~ % 68.13/9.95 (vnum(v0) = v1) | ? [v2: expr] : (eval_0(v2) = v1 & cte(v0) = v2 & % 68.13/9.95 value(v1) & expr(v2))) & ! [v0: int] : ! [v1: expr] : ( ~ ($lesseq(0, % 68.13/9.95 v0)) | ~ (cte(v0) = v1) | ? [v2: value] : (eval_0(v1) = v2 & vnum(v0) % 68.13/9.95 = v2 & value(v2))) % 68.13/9.95 % 68.13/9.95 (fc_def2) % 68.13/9.95 value_mngt_value(fc2) & ty(value1) & ? [v0: uni] : (t2tb1(fc2) = v0 & uni(v0) % 68.13/9.95 & ! [v1: value] : ! [v2: uni] : ( ~ (t2tb(v1) = v2) | ~ value(v1) | ? % 68.13/9.95 [v3: uni] : (tb2t(v3) = v1 & infix_at(value1, value1, v0, v2) = v3 & % 68.13/9.95 uni(v3)))) % 68.13/9.95 % 68.13/9.95 (fc_def3) % 68.13/9.95 lprp_mngt_value(fc3) & value(underflow) & ty(value1) & ty(tuple01) & ? [v0: % 68.13/9.95 uni] : (t2tb5(fc3) = v0 & uni(v0) & ! [v1: tuple0] : ! [v2: uni] : ( ~ % 68.13/9.95 (t2tb2(v1) = v2) | ~ tuple0(v1) | ? [v3: uni] : (tb2t(v3) = underflow & % 68.13/9.95 infix_at(value1, tuple01, v0, v2) = v3 & uni(v3)))) % 68.13/9.95 % 68.13/9.95 (recompose_def) % 68.13/9.95 context(empty) & ! [v0: expr] : ! [v1: int] : ! [v2: context] : ! [v3: % 68.13/9.95 expr] : ! [v4: expr] : ! [v5: expr] : ( ~ (recompose(v2, v4) = v5) | ~ % 68.13/9.95 (sub(v3, v0) = v4) | ~ (cte(v1) = v3) | ~ context(v2) | ~ expr(v0) | ? % 68.13/9.95 [v6: context] : (recompose(v6, v0) = v5 & right(v1, v2) = v6 & context(v6) & % 68.13/9.95 expr(v5))) & ! [v0: expr] : ! [v1: int] : ! [v2: context] : ! [v3: % 68.13/9.95 context] : ! [v4: expr] : ( ~ (recompose(v3, v0) = v4) | ~ (right(v1, v2) % 68.13/9.95 = v3) | ~ context(v2) | ~ expr(v0) | ? [v5: expr] : ? [v6: expr] : % 68.13/9.95 (recompose(v2, v6) = v4 & sub(v5, v0) = v6 & cte(v1) = v5 & expr(v6) & % 68.13/9.95 expr(v5) & expr(v4))) & ! [v0: expr] : ! [v1: context] : ! [v2: expr] : % 68.13/9.95 ! [v3: context] : ! [v4: expr] : ( ~ (recompose(v3, v0) = v4) | ~ (left(v1, % 68.13/9.95 v2) = v3) | ~ context(v1) | ~ expr(v2) | ~ expr(v0) | ? [v5: expr] : % 68.13/9.95 (recompose(v1, v5) = v4 & sub(v0, v2) = v5 & expr(v5) & expr(v4))) & ! [v0: % 68.13/9.95 expr] : ! [v1: context] : ! [v2: expr] : ! [v3: expr] : ! [v4: expr] : ( % 68.13/9.95 ~ (recompose(v1, v3) = v4) | ~ (sub(v0, v2) = v3) | ~ context(v1) | ~ % 68.13/9.95 expr(v2) | ~ expr(v0) | ? [v5: context] : (recompose(v5, v0) = v4 & % 68.13/9.95 left(v1, v2) = v5 & context(v5) & expr(v4))) & ! [v0: expr] : ! [v1: % 68.13/9.95 expr] : (v1 = v0 | ~ (recompose(empty, v0) = v1) | ~ expr(v0)) % 68.13/9.95 % 68.13/9.95 (recompose_values) % 68.13/9.96 ! [v0: context] : ! [v1: expr] : ! [v2: expr] : ! [v3: expr] : ! [v4: % 68.13/9.96 value] : ! [v5: expr] : ! [v6: value] : (v6 = v4 | ~ (recompose(v0, v2) = % 68.13/9.96 v5) | ~ (recompose(v0, v1) = v3) | ~ (eval_0(v5) = v6) | ~ (eval_0(v3) % 68.13/9.96 = v4) | ~ context(v0) | ~ expr(v2) | ~ expr(v1) | ? [v7: value] : ? % 68.13/9.96 [v8: value] : ( ~ (v8 = v7) & eval_0(v2) = v8 & eval_0(v1) = v7 & value(v8) % 68.13/9.96 & value(v7))) & ! [v0: context] : ! [v1: expr] : ! [v2: expr] : ! [v3: % 68.13/9.96 value] : ! [v4: expr] : ! [v5: value] : ( ~ (recompose(v0, v2) = v4) | ~ % 68.13/9.96 (eval_0(v4) = v5) | ~ (eval_0(v1) = v3) | ~ context(v0) | ~ expr(v2) | ~ % 68.13/9.96 expr(v1) | ? [v6: value] : ? [v7: expr] : ? [v8: value] : ((v8 = v5 & % 68.13/9.96 recompose(v0, v1) = v7 & eval_0(v7) = v5 & value(v5) & expr(v7)) | ( ~ % 68.13/9.96 (v6 = v3) & eval_0(v2) = v6 & value(v6)))) & ! [v0: context] : ! [v1: % 68.13/9.96 expr] : ! [v2: expr] : ! [v3: value] : ! [v4: expr] : ! [v5: value] : ( % 68.13/9.96 ~ (recompose(v0, v1) = v4) | ~ (eval_0(v4) = v5) | ~ (eval_0(v2) = v3) | % 68.13/9.96 ~ context(v0) | ~ expr(v2) | ~ expr(v1) | ? [v6: value] : ? [v7: expr] : % 68.13/9.96 ? [v8: value] : ((v8 = v5 & recompose(v0, v2) = v7 & eval_0(v7) = v5 & % 68.13/9.96 value(v5) & expr(v7)) | ( ~ (v6 = v3) & eval_0(v1) = v6 & value(v6)))) % 68.13/9.96 % 68.13/9.96 (vnum_closure_def) % 68.13/9.96 int_mngt_value(vnum_closure) & ty(value1) & ty(int) & ? [v0: uni] : % 68.13/9.96 (t2tb4(vnum_closure) = v0 & uni(v0) & ! [v1: int] : ! [v2: uni] : ( ~ % 68.13/9.96 (t2tb3(v1) = v2) | ? [v3: uni] : ? [v4: value] : (tb2t(v3) = v4 & % 68.13/9.96 infix_at(value1, int, v0, v2) = v3 & vnum(v1) = v4 & value(v4) & % 68.13/9.96 uni(v3))) & ! [v1: int] : ! [v2: value] : ( ~ (vnum(v1) = v2) | ? % 68.13/9.96 [v3: uni] : ? [v4: uni] : (t2tb3(v1) = v3 & tb2t(v4) = v2 & % 68.13/9.96 infix_at(value1, int, v0, v3) = v4 & value(v2) & uni(v4) & uni(v3)))) % 68.13/9.96 % 68.13/9.96 (wP_parameter_eval_2) % 68.13/9.96 ? [v0: context] : ? [v1: int] : ? [v2: expr] : ? [v3: expr] : ? [v4: % 68.13/9.96 value] : ? [v5: int] : ? [v6: context] : ? [v7: expr] : ? [v8: expr] : % 68.13/9.96 ? [v9: value] : ( ~ (v9 = v4) & $lesseq(v1, v5) & $lesseq(0, v1) & % 68.13/9.96 recompose(v6, v7) = v8 & recompose(v0, v2) = v3 & right(v5, v6) = v0 & % 68.13/9.96 eval_0(v8) = v9 & eval_0(v3) = v4 & cte($difference(v5, v1)) = v7 & cte(v1) % 68.13/9.96 = v2 & context(v6) & context(v0) & value(v9) & value(v4) & expr(v8) & % 68.13/9.96 expr(v7) & expr(v3) & expr(v2)) % 68.13/9.96 % 68.13/9.96 (function-axioms) % 68.13/9.97 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 68.13/9.97 [v5: context] : ! [v6: ty] : (v1 = v0 | ~ (match_context(v6, v5, v4, v3, v2) % 68.13/9.97 = v1) | ~ (match_context(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! % 68.13/9.97 [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! [v5: cont2] : ! % 68.13/9.97 [v6: ty] : (v1 = v0 | ~ (match_cont1(v6, v5, v4, v3, v2) = v1) | ~ % 68.13/9.97 (match_cont1(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.13/9.97 [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! [v5: cont] : ! [v6: ty] : (v1 = % 68.13/9.97 v0 | ~ (match_cont(v6, v5, v4, v3, v2) = v1) | ~ (match_cont(v6, v5, v4, % 68.13/9.97 v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 68.13/9.97 uni] : ! [v4: int] : ! [v5: ty] : (v1 = v0 | ~ (eval_2b(v5, v4, v3, v2) = % 68.13/9.97 v1) | ~ (eval_2b(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : % 68.13/9.97 ! [v2: uni] : ! [v3: uni] : ! [v4: expr] : ! [v5: ty] : (v1 = v0 | ~ % 68.13/9.97 (eval_2a(v5, v4, v3, v2) = v1) | ~ (eval_2a(v5, v4, v3, v2) = v0)) & ! % 68.13/9.97 [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: expr] : ! % 68.13/9.97 [v5: ty] : (v1 = v0 | ~ (eval_2(v5, v4, v3, v2) = v1) | ~ (eval_2(v5, v4, % 68.13/9.97 v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 68.13/9.97 uni] : ! [v4: ty] : ! [v5: ty] : (v1 = v0 | ~ (infix_at(v5, v4, v3, v2) = % 68.13/9.97 v1) | ~ (infix_at(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : % 68.13/9.97 ! [v2: uni] : ! [v3: uni] : ! [v4: value] : ! [v5: ty] : (v1 = v0 | ~ % 68.13/9.97 (match_value(v5, v4, v3, v2) = v1) | ~ (match_value(v5, v4, v3, v2) = v0)) % 68.13/9.97 & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: expr] : % 68.13/9.97 ! [v5: ty] : (v1 = v0 | ~ (match_expr(v5, v4, v3, v2) = v1) | ~ % 68.13/9.97 (match_expr(v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 68.13/9.97 uni] : ! [v3: uni] : ! [v4: bool] : ! [v5: ty] : (v1 = v0 | ~ % 68.13/9.97 (match_bool(v5, v4, v3, v2) = v1) | ~ (match_bool(v5, v4, v3, v2) = v0)) & % 68.13/9.97 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! % 68.13/9.97 [v3: int] : ! [v4: cont2] : (v1 = v0 | ~ (eval_cont1(v4, v3, v2) = v1) | ~ % 68.13/9.97 (eval_cont1(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 68.13/9.97 MultipleValueBool] : ! [v2: value] : ! [v3: value] : ! [v4: cont] : (v1 = % 68.13/9.97 v0 | ~ (eval_cont(v4, v3, v2) = v1) | ~ (eval_cont(v4, v3, v2) = v0)) & ! % 68.13/9.97 [v0: uni] : ! [v1: uni] : ! [v2: expr] : ! [v3: uni] : ! [v4: ty] : (v1 = % 68.13/9.97 v0 | ~ (fc1(v4, v3, v2) = v1) | ~ (fc1(v4, v3, v2) = v0)) & ! [v0: uni] : % 68.13/9.97 ! [v1: uni] : ! [v2: int] : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ % 68.13/9.97 (fc(v4, v3, v2) = v1) | ~ (fc(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: % 68.13/9.97 uni] : ! [v2: uni] : ! [v3: expr] : ! [v4: ty] : (v1 = v0 | ~ % 68.13/9.97 (eval_1(v4, v3, v2) = v1) | ~ (eval_1(v4, v3, v2) = v0)) & ! [v0: expr] : % 68.13/9.97 ! [v1: expr] : ! [v2: expr] : ! [v3: context] : (v1 = v0 | ~ (recompose(v3, % 68.13/9.97 v2) = v1) | ~ (recompose(v3, v2) = v0)) & ! [v0: context] : ! [v1: % 68.13/9.97 context] : ! [v2: context] : ! [v3: int] : (v1 = v0 | ~ (right(v3, v2) = % 68.13/9.97 v1) | ~ (right(v3, v2) = v0)) & ! [v0: context] : ! [v1: context] : ! % 68.13/9.97 [v2: expr] : ! [v3: context] : (v1 = v0 | ~ (left(v3, v2) = v1) | ~ % 68.13/9.97 (left(v3, v2) = v0)) & ! [v0: cont2] : ! [v1: cont2] : ! [v2: cont2] : ! % 68.13/9.97 [v3: int] : (v1 = v0 | ~ (a2(v3, v2) = v1) | ~ (a2(v3, v2) = v0)) & ! [v0: % 68.13/9.97 cont2] : ! [v1: cont2] : ! [v2: cont2] : ! [v3: expr] : (v1 = v0 | ~ % 68.13/9.97 (a1(v3, v2) = v1) | ~ (a1(v3, v2) = v0)) & ! [v0: cont] : ! [v1: cont] : % 68.13/9.97 ! [v2: cont] : ! [v3: int] : (v1 = v0 | ~ (b(v3, v2) = v1) | ~ (b(v3, v2) = % 68.13/9.97 v0)) & ! [v0: cont] : ! [v1: cont] : ! [v2: cont] : ! [v3: expr] : (v1 % 68.13/9.97 = v0 | ~ (a(v3, v2) = v1) | ~ (a(v3, v2) = v0)) & ! [v0: int_mngt_value] % 68.13/9.97 : ! [v1: int_mngt_value] : ! [v2: int_mngt_value] : ! [v3: int] : (v1 = v0 % 68.13/9.97 | ~ (eval_3b(v3, v2) = v1) | ~ (eval_3b(v3, v2) = v0)) & ! [v0: % 68.13/9.97 int_mngt_value] : ! [v1: int_mngt_value] : ! [v2: int_mngt_value] : ! % 68.13/9.97 [v3: expr] : (v1 = v0 | ~ (eval_3a(v3, v2) = v1) | ~ (eval_3a(v3, v2) = v0)) % 68.13/9.97 & ! [v0: value] : ! [v1: value] : ! [v2: int_mngt_value] : ! [v3: expr] : % 68.13/9.97 (v1 = v0 | ~ (eval_3(v3, v2) = v1) | ~ (eval_3(v3, v2) = v0)) & ! [v0: ty] % 68.13/9.97 : ! [v1: ty] : ! [v2: ty] : ! [v3: ty] : (v1 = v0 | ~ (func(v3, v2) = v1) % 68.13/9.97 | ~ (func(v3, v2) = v0)) & ! [v0: expr] : ! [v1: expr] : ! [v2: expr] : % 68.13/9.97 ! [v3: expr] : (v1 = v0 | ~ (sub(v3, v2) = v1) | ~ (sub(v3, v2) = v0)) & ! % 68.13/9.97 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: % 68.13/9.97 ty] : (v1 = v0 | ~ (sort(v3, v2) = v1) | ~ (sort(v3, v2) = v0)) & ! [v0: % 68.13/9.97 int] : ! [v1: int] : ! [v2: context] : (v1 = v0 | ~ (size_c2(v2) = v1) | % 68.13/9.97 ~ (size_c2(v2) = v0)) & ! [v0: context] : ! [v1: context] : ! [v2: % 68.13/9.97 context] : (v1 = v0 | ~ (right_proj_2(v2) = v1) | ~ (right_proj_2(v2) = % 68.13/9.97 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: context] : (v1 = v0 | ~ % 68.13/9.97 (right_proj_1(v2) = v1) | ~ (right_proj_1(v2) = v0)) & ! [v0: expr] : ! % 68.13/9.97 [v1: expr] : ! [v2: context] : (v1 = v0 | ~ (left_proj_2(v2) = v1) | ~ % 68.13/9.97 (left_proj_2(v2) = v0)) & ! [v0: context] : ! [v1: context] : ! [v2: % 68.13/9.97 context] : (v1 = v0 | ~ (left_proj_1(v2) = v1) | ~ (left_proj_1(v2) = v0)) % 68.13/9.97 & ! [v0: int] : ! [v1: int] : ! [v2: cont] : (v1 = v0 | ~ (size_c1(v2) = % 68.13/9.97 v1) | ~ (size_c1(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 68.13/9.97 cont2] : (v1 = v0 | ~ (size_c(v2) = v1) | ~ (size_c(v2) = v0)) & ! [v0: % 68.13/9.97 int] : ! [v1: int] : ! [v2: expr] : (v1 = v0 | ~ (size_e1(v2) = v1) | ~ % 68.13/9.97 (size_e1(v2) = v0)) & ! [v0: cont2] : ! [v1: cont2] : ! [v2: cont2] : (v1 % 68.13/9.97 = v0 | ~ (a2_proj_2(v2) = v1) | ~ (a2_proj_2(v2) = v0)) & ! [v0: int] : % 68.13/9.97 ! [v1: int] : ! [v2: cont2] : (v1 = v0 | ~ (a2_proj_1(v2) = v1) | ~ % 68.13/9.97 (a2_proj_1(v2) = v0)) & ! [v0: cont2] : ! [v1: cont2] : ! [v2: cont2] : % 68.13/9.97 (v1 = v0 | ~ (a1_proj_2(v2) = v1) | ~ (a1_proj_2(v2) = v0)) & ! [v0: expr] % 68.13/9.97 : ! [v1: expr] : ! [v2: cont2] : (v1 = v0 | ~ (a1_proj_1(v2) = v1) | ~ % 68.13/9.97 (a1_proj_1(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: expr] : (v1 = % 68.13/9.97 v0 | ~ (eval_01(v2) = v1) | ~ (eval_01(v2) = v0)) & ! [v0: int] : ! [v1: % 68.13/9.97 int] : ! [v2: expr] : (v1 = v0 | ~ (size_e(v2) = v1) | ~ (size_e(v2) = % 68.13/9.97 v0)) & ! [v0: cont] : ! [v1: cont] : ! [v2: cont] : (v1 = v0 | ~ % 68.13/9.98 (b_proj_2(v2) = v1) | ~ (b_proj_2(v2) = v0)) & ! [v0: int] : ! [v1: int] % 68.13/9.98 : ! [v2: cont] : (v1 = v0 | ~ (b_proj_1(v2) = v1) | ~ (b_proj_1(v2) = v0)) % 68.13/9.98 & ! [v0: cont] : ! [v1: cont] : ! [v2: cont] : (v1 = v0 | ~ (a_proj_2(v2) % 68.13/9.98 = v1) | ~ (a_proj_2(v2) = v0)) & ! [v0: expr] : ! [v1: expr] : ! [v2: % 68.13/9.98 cont] : (v1 = v0 | ~ (a_proj_1(v2) = v1) | ~ (a_proj_1(v2) = v0)) & ! % 68.13/9.98 [v0: lprp_mngt_value] : ! [v1: lprp_mngt_value] : ! [v2: uni] : (v1 = v0 | % 68.13/9.98 ~ (tb2t5(v2) = v1) | ~ (tb2t5(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.13/9.98 [v2: lprp_mngt_value] : (v1 = v0 | ~ (t2tb5(v2) = v1) | ~ (t2tb5(v2) = v0)) % 68.13/9.98 & ! [v0: int_mngt_value] : ! [v1: int_mngt_value] : ! [v2: uni] : (v1 = v0 % 68.13/9.98 | ~ (tb2t4(v2) = v1) | ~ (tb2t4(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : % 68.13/9.98 ! [v2: int_mngt_value] : (v1 = v0 | ~ (t2tb4(v2) = v1) | ~ (t2tb4(v2) = % 68.13/9.98 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: uni] : (v1 = v0 | ~ % 68.13/9.98 (tb2t3(v2) = v1) | ~ (tb2t3(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 68.13/9.98 [v2: int] : (v1 = v0 | ~ (t2tb3(v2) = v1) | ~ (t2tb3(v2) = v0)) & ! [v0: % 68.13/9.98 tuple0] : ! [v1: tuple0] : ! [v2: uni] : (v1 = v0 | ~ (tb2t2(v2) = v1) | % 68.13/9.98 ~ (tb2t2(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: tuple0] : (v1 = % 68.13/9.98 v0 | ~ (t2tb2(v2) = v1) | ~ (t2tb2(v2) = v0)) & ! [v0: value_mngt_value] % 68.13/9.98 : ! [v1: value_mngt_value] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | % 68.13/9.98 ~ (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: % 68.13/9.98 value_mngt_value] : (v1 = v0 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & % 68.13/9.98 ! [v0: value] : ! [v1: value] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) % 68.13/9.98 | ~ (tb2t(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: value] : (v1 = % 68.13/9.98 v0 | ~ (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: value] : ! [v1: % 68.13/9.98 value] : ! [v2: expr] : (v1 = v0 | ~ (eval_0(v2) = v1) | ~ (eval_0(v2) = % 68.13/9.98 v0)) & ! [v0: int] : ! [v1: int] : ! [v2: value] : (v1 = v0 | ~ % 68.13/9.98 (vnum_proj_1(v2) = v1) | ~ (vnum_proj_1(v2) = v0)) & ! [v0: value] : ! % 68.13/9.98 [v1: value] : ! [v2: int] : (v1 = v0 | ~ (vnum(v2) = v1) | ~ (vnum(v2) = % 68.13/9.98 v0)) & ! [v0: expr] : ! [v1: expr] : ! [v2: expr] : (v1 = v0 | ~ % 68.13/9.98 (sub_proj_2(v2) = v1) | ~ (sub_proj_2(v2) = v0)) & ! [v0: expr] : ! [v1: % 68.13/9.98 expr] : ! [v2: expr] : (v1 = v0 | ~ (sub_proj_1(v2) = v1) | ~ % 68.13/9.98 (sub_proj_1(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: expr] : (v1 = % 68.13/9.98 v0 | ~ (cte_proj_1(v2) = v1) | ~ (cte_proj_1(v2) = v0)) & ! [v0: expr] : % 68.13/9.98 ! [v1: expr] : ! [v2: int] : (v1 = v0 | ~ (cte(v2) = v1) | ~ (cte(v2) = % 68.13/9.98 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ % 68.13/9.98 (witness(v2) = v1) | ~ (witness(v2) = v0)) % 68.13/9.98 % 68.13/9.98 Further assumptions not needed in the proof: % 68.13/9.98 -------------------------------------------- % 68.13/9.98 a1, a12, a1_A2, a1_I, a1_proj_1_def, a1_proj_2_def, a2, a22, a2_I, % 68.13/9.98 a2_proj_1_def, a2_proj_2_def, a3, a31, a_B, a_proj_1_def, a_proj_2_def, % 68.13/9.98 b_proj_1_def, b_proj_2_def, bool_inversion, bridgeL, bridgeL1, bridgeL2, % 68.13/9.98 bridgeL3, bridgeL4, bridgeL5, bridgeR, bridgeR1, bridgeR2, bridgeR3, bridgeR4, % 68.13/9.98 bridgeR5, compatOrderMult, cont_inversion, cont_inversion1, context_inversion, % 68.13/9.98 cps2_correct_expr_aux, cte_Sub, cte_proj_1_def, empty_Left, empty_Right, % 68.13/9.98 eval_0_def1, eval_1_def, eval_1_sort, eval_2_def, eval_2_sort, eval_2a_def, % 68.13/9.98 eval_2a_sort, eval_2b_def, eval_2b_sort, eval_3_def, eval_3a_def, eval_3b_def, % 68.13/9.98 eval_cont_inversion, eval_cont_inversion1, expr_inversion, fc_def, fc_def1, % 68.13/9.98 fc_sort, fc_sort1, i_A, i_B, infix_at_sort, left_Right, left_proj_1_def, % 68.13/9.98 left_proj_2_def, match_bool_False, match_bool_True, match_bool_sort, % 68.13/9.98 match_cont_A, match_cont_A1, match_cont_A2, match_cont_B, match_cont_I, % 68.13/9.98 match_cont_I1, match_cont_sort, match_cont_sort1, match_context_Empty, % 68.13/9.98 match_context_Left, match_context_Right, match_context_sort, match_expr_Cte, % 68.13/9.98 match_expr_Sub, match_expr_sort, match_value_Underflow, match_value_Vnum, % 68.13/9.98 match_value_sort, recompose_underflow, right_proj_1_def, right_proj_2_def, % 68.13/9.98 size_c_def, size_c_def1, size_c_def2, size_c_pos, size_c_pos1, size_c_pos2, % 68.13/9.98 size_e_def, size_e_def1, size_e_pos, size_e_pos1, sub_proj_1_def, % 68.13/9.98 sub_proj_2_def, t2tb_sort, t2tb_sort1, t2tb_sort2, t2tb_sort3, t2tb_sort4, % 68.13/9.98 t2tb_sort5, true_False, tuple0_inversion, underflow1, value_inversion, % 68.13/9.98 vnum_Underflow, vnum_proj_1_def, witness_sort % 68.13/9.98 % 68.13/9.98 Those formulas are unsatisfiable: % 68.13/9.98 --------------------------------- % 68.13/9.98 % 68.13/9.98 Begin of proof % 68.13/9.98 | % 68.13/9.98 | ALPHA: (eval_0_def) implies: % 68.13/9.98 | (1) ! [v0: int] : ! [v1: expr] : ( ~ ($lesseq(0, v0)) | ~ (cte(v0) = v1) % 68.13/9.98 | | ? [v2: value] : (eval_0(v1) = v2 & vnum(v0) = v2 & value(v2))) % 68.13/9.98 | (2) ! [v0: expr] : ! [v1: expr] : ! [v2: int] : ! [v3: value] : ! [v4: % 68.13/9.98 | expr] : ! [v5: value] : ( ~ (eval_0(v4) = v5) | ~ (vnum(v2) = v3) | % 68.13/9.98 | ~ (sub(v0, v1) = v4) | ~ expr(v1) | ~ expr(v0) | ? [v6: value] : % 68.13/9.98 | ? [v7: value] : (( ~ (v6 = v3) & eval_0(v0) = v6 & value(v6)) | % 68.13/9.98 | (eval_0(v1) = v7 & value(v7) & ! [v8: int] : ! [v9: value] : (v9 % 68.13/9.98 | = v5 | ~ ($lesseq(v8, v2)) | ~ (vnum($difference(v2, v8)) = % 68.13/9.98 | v9) | ? [v10: value] : ( ~ (v10 = v7) & vnum(v8) = v10 & % 68.13/9.98 | value(v10))) & ! [v8: int] : ! [v9: value] : (v5 = % 68.13/9.98 | underflow | ~ ($lesseq(1, $difference(v8, v2))) | ~ % 68.13/9.98 | (vnum($difference(v2, v8)) = v9) | ? [v10: value] : ( ~ (v10 = % 68.13/9.98 | v7) & vnum(v8) = v10 & value(v10))) & ! [v8: int] : (v5 = % 68.13/9.98 | underflow | ~ ($lesseq(1, $difference(v8, v2))) | ~ (vnum(v8) % 68.13/9.98 | = v7)) & ! [v8: int] : ( ~ ($lesseq(v8, v2)) | ~ (vnum(v8) % 68.13/9.98 | = v7) | (vnum($difference(v2, v8)) = v5 & value(v5))) & ( ~ % 68.13/9.98 | (v7 = underflow) | v5 = underflow)))) % 68.13/9.98 | % 68.13/9.98 | ALPHA: (cps_correct_expr) implies: % 68.13/9.98 | (3) ! [v0: ty] : ! [v1: expr] : ! [v2: uni] : ! [v3: uni] : ( ~ % 68.13/9.98 | (eval_1(v0, v1, v2) = v3) | ~ expr(v1) | ~ ty(v0) | ~ uni(v2) | ? % 68.13/9.98 | [v4: value] : ? [v5: uni] : (t2tb(v4) = v5 & infix_at(v0, value1, % 68.13/9.98 | v2, v5) = v3 & eval_0(v1) = v4 & value(v4) & uni(v5) & uni(v3))) % 68.13/9.98 | % 68.13/9.98 | ALPHA: (fc_def2) implies: % 68.13/9.98 | (4) ? [v0: uni] : (t2tb1(fc2) = v0 & uni(v0) & ! [v1: value] : ! [v2: % 68.13/9.98 | uni] : ( ~ (t2tb(v1) = v2) | ~ value(v1) | ? [v3: uni] : % 68.13/9.98 | (tb2t(v3) = v1 & infix_at(value1, value1, v0, v2) = v3 & uni(v3)))) % 68.13/9.98 | % 68.13/9.98 | ALPHA: (cps_correct) implies: % 68.13/9.99 | (5) ? [v0: uni] : (t2tb1(fc2) = v0 & uni(v0) & ! [v1: expr] : ! [v2: % 68.13/9.99 | uni] : ( ~ (eval_1(value1, v1, v0) = v2) | ~ expr(v1) | ? [v3: % 68.13/9.99 | value] : (tb2t(v2) = v3 & eval_0(v1) = v3 & value(v3))) & ! [v1: % 68.13/9.99 | expr] : ! [v2: value] : ( ~ (eval_0(v1) = v2) | ~ expr(v1) | ? % 68.13/9.99 | [v3: uni] : (tb2t(v3) = v2 & eval_1(value1, v1, v0) = v3 & % 68.13/9.99 | value(v2) & uni(v3)))) % 68.13/9.99 | % 68.13/9.99 | ALPHA: (cps2_correct_expr) implies: % 68.13/9.99 | (6) ? [v0: uni] : (t2tb2(tuple02) = v0 & uni(v0) & ! [v1: ty] : ! [v2: % 68.13/9.99 | expr] : ! [v3: uni] : ! [v4: uni] : ! [v5: value] : ! [v6: int] % 68.13/9.99 | : ! [v7: uni] : ! [v8: uni] : ! [v9: uni] : ! [v10: uni] : ( ~ % 68.13/9.99 | (t2tb3(v6) = v7) | ~ (infix_at(v1, tuple01, v3, v0) = v9) | ~ % 68.13/9.99 | (infix_at(v1, int, v4, v7) = v8) | ~ (eval_0(v2) = v5) | ~ % 68.13/9.99 | (vnum_proj_1(v5) = v6) | ~ (match_value(v1, v5, v8, v9) = v10) | % 68.13/9.99 | ~ expr(v2) | ~ ty(v1) | ~ uni(v4) | ~ uni(v3) | (eval_2(v1, v2, % 68.13/9.99 | v4, v3) = v10 & uni(v10))) & ! [v1: ty] : ! [v2: expr] : ! % 68.13/9.99 | [v3: uni] : ! [v4: uni] : ! [v5: uni] : ( ~ (eval_2(v1, v2, v4, v3) % 68.13/9.99 | = v5) | ~ expr(v2) | ~ ty(v1) | ~ uni(v4) | ~ uni(v3) | ? % 68.13/9.99 | [v6: value] : ? [v7: int] : ? [v8: uni] : ? [v9: uni] : ? [v10: % 68.13/9.99 | uni] : (t2tb3(v7) = v8 & infix_at(v1, tuple01, v3, v0) = v10 & % 68.13/9.99 | infix_at(v1, int, v4, v8) = v9 & eval_0(v2) = v6 & % 68.13/9.99 | vnum_proj_1(v6) = v7 & match_value(v1, v6, v9, v10) = v5 & % 68.13/9.99 | value(v6) & uni(v10) & uni(v9) & uni(v8) & uni(v5)))) % 68.13/9.99 | % 68.13/9.99 | ALPHA: (vnum_closure_def) implies: % 68.13/9.99 | (7) ? [v0: uni] : (t2tb4(vnum_closure) = v0 & uni(v0) & ! [v1: int] : ! % 68.13/9.99 | [v2: uni] : ( ~ (t2tb3(v1) = v2) | ? [v3: uni] : ? [v4: value] : % 68.13/9.99 | (tb2t(v3) = v4 & infix_at(value1, int, v0, v2) = v3 & vnum(v1) = v4 % 68.13/9.99 | & value(v4) & uni(v3))) & ! [v1: int] : ! [v2: value] : ( ~ % 68.13/9.99 | (vnum(v1) = v2) | ? [v3: uni] : ? [v4: uni] : (t2tb3(v1) = v3 & % 68.13/9.99 | tb2t(v4) = v2 & infix_at(value1, int, v0, v3) = v4 & value(v2) & % 68.13/9.99 | uni(v4) & uni(v3)))) % 68.13/9.99 | % 68.13/9.99 | ALPHA: (fc_def3) implies: % 68.13/9.99 | (8) ? [v0: uni] : (t2tb5(fc3) = v0 & uni(v0) & ! [v1: tuple0] : ! [v2: % 68.13/9.99 | uni] : ( ~ (t2tb2(v1) = v2) | ~ tuple0(v1) | ? [v3: uni] : % 68.13/9.99 | (tb2t(v3) = underflow & infix_at(value1, tuple01, v0, v2) = v3 & % 68.13/9.99 | uni(v3)))) % 68.13/9.99 | % 68.13/9.99 | ALPHA: (cps2_correct) implies: % 68.13/9.99 | (9) ? [v0: uni] : ? [v1: uni] : (t2tb5(fc3) = v1 & t2tb4(vnum_closure) = % 68.13/9.99 | v0 & uni(v1) & uni(v0) & ! [v2: expr] : ! [v3: uni] : ( ~ % 68.13/9.99 | (eval_2(value1, v2, v0, v1) = v3) | ~ expr(v2) | ? [v4: value] : % 68.13/9.99 | (tb2t(v3) = v4 & eval_0(v2) = v4 & value(v4))) & ! [v2: expr] : ! % 68.13/9.99 | [v3: value] : ( ~ (eval_0(v2) = v3) | ~ expr(v2) | ? [v4: uni] : % 68.13/9.99 | (eval_2(value1, v2, v0, v1) = v4 & tb2t(v4) = v3 & value(v3) & % 68.13/9.99 | uni(v4)))) % 68.13/9.99 | % 68.13/9.99 | ALPHA: (cps3_correct_expr) implies: % 68.13/9.99 | (10) ty(value1) % 69.23/9.99 | (11) ? [v0: uni] : (t2tb(underflow) = v0 & uni(v0) & ! [v1: expr] : ! % 69.23/9.99 | [v2: int_mngt_value] : ! [v3: value] : ! [v4: uni] : ! [v5: int] % 69.23/9.99 | : ! [v6: uni] : ! [v7: uni] : ( ~ (t2tb4(v2) = v4) | ~ (t2tb3(v5) % 69.23/9.99 | = v6) | ~ (infix_at(value1, int, v4, v6) = v7) | ~ (eval_0(v1) % 69.23/9.99 | = v3) | ~ (vnum_proj_1(v3) = v5) | ~ int_mngt_value(v2) | ~ % 69.23/9.99 | expr(v1) | ? [v8: value] : ? [v9: uni] : (eval_3(v1, v2) = v8 & % 69.23/9.99 | tb2t(v9) = v8 & match_value(value1, v3, v7, v0) = v9 & value(v8) % 69.23/9.99 | & uni(v9))) & ! [v1: expr] : ! [v2: int_mngt_value] : ! [v3: % 69.23/9.99 | value] : ( ~ (eval_3(v1, v2) = v3) | ~ int_mngt_value(v2) | ~ % 69.23/9.99 | expr(v1) | ? [v4: value] : ? [v5: uni] : ? [v6: int] : ? [v7: % 69.23/9.99 | uni] : ? [v8: uni] : ? [v9: uni] : (t2tb4(v2) = v5 & t2tb3(v6) % 69.23/9.99 | = v7 & tb2t(v9) = v3 & infix_at(value1, int, v5, v7) = v8 & % 69.23/9.99 | eval_0(v1) = v4 & vnum_proj_1(v4) = v6 & match_value(value1, v4, % 69.23/9.99 | v8, v0) = v9 & value(v4) & value(v3) & uni(v9) & uni(v8) & % 69.23/9.99 | uni(v7) & uni(v5)))) % 69.23/9.99 | % 69.23/9.99 | ALPHA: (cps3_correct) implies: % 69.23/9.99 | (12) int_mngt_value(vnum_closure) % 69.23/9.99 | (13) ! [v0: expr] : ! [v1: value] : ( ~ (eval_0(v0) = v1) | ~ expr(v0) | % 69.23/9.99 | (eval_3(v0, vnum_closure) = v1 & value(v1))) % 69.23/9.99 | % 69.23/9.99 | ALPHA: (recompose_def) implies: % 69.23/9.99 | (14) ! [v0: expr] : ! [v1: int] : ! [v2: context] : ! [v3: context] : % 69.23/9.99 | ! [v4: expr] : ( ~ (recompose(v3, v0) = v4) | ~ (right(v1, v2) = v3) % 69.23/9.99 | | ~ context(v2) | ~ expr(v0) | ? [v5: expr] : ? [v6: expr] : % 69.23/9.99 | (recompose(v2, v6) = v4 & sub(v5, v0) = v6 & cte(v1) = v5 & expr(v6) % 69.23/9.99 | & expr(v5) & expr(v4))) % 69.23/9.99 | % 69.23/9.99 | ALPHA: (recompose_values) implies: % 69.23/10.00 | (15) ! [v0: context] : ! [v1: expr] : ! [v2: expr] : ! [v3: value] : ! % 69.23/10.00 | [v4: expr] : ! [v5: value] : ( ~ (recompose(v0, v2) = v4) | ~ % 69.23/10.00 | (eval_0(v4) = v5) | ~ (eval_0(v1) = v3) | ~ context(v0) | ~ % 69.23/10.00 | expr(v2) | ~ expr(v1) | ? [v6: value] : ? [v7: expr] : ? [v8: % 69.23/10.00 | value] : ((v8 = v5 & recompose(v0, v1) = v7 & eval_0(v7) = v5 & % 69.23/10.00 | value(v5) & expr(v7)) | ( ~ (v6 = v3) & eval_0(v2) = v6 & % 69.23/10.00 | value(v6)))) % 69.23/10.00 | (16) ! [v0: context] : ! [v1: expr] : ! [v2: expr] : ! [v3: expr] : ! % 69.23/10.00 | [v4: value] : ! [v5: expr] : ! [v6: value] : (v6 = v4 | ~ % 69.23/10.00 | (recompose(v0, v2) = v5) | ~ (recompose(v0, v1) = v3) | ~ % 69.23/10.00 | (eval_0(v5) = v6) | ~ (eval_0(v3) = v4) | ~ context(v0) | ~ % 69.23/10.00 | expr(v2) | ~ expr(v1) | ? [v7: value] : ? [v8: value] : ( ~ (v8 = % 69.23/10.00 | v7) & eval_0(v2) = v8 & eval_0(v1) = v7 & value(v8) & % 69.23/10.00 | value(v7))) % 69.23/10.00 | % 69.23/10.00 | ALPHA: (function-axioms) implies: % 69.23/10.00 | (17) ! [v0: value] : ! [v1: value] : ! [v2: int] : (v1 = v0 | ~ % 69.23/10.00 | (vnum(v2) = v1) | ~ (vnum(v2) = v0)) % 69.23/10.00 | (18) ! [v0: value] : ! [v1: value] : ! [v2: expr] : (v1 = v0 | ~ % 69.23/10.00 | (eval_0(v2) = v1) | ~ (eval_0(v2) = v0)) % 69.23/10.00 | (19) ! [v0: uni] : ! [v1: uni] : ! [v2: value_mngt_value] : (v1 = v0 | % 69.23/10.00 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) % 69.23/10.00 | (20) ! [v0: uni] : ! [v1: uni] : ! [v2: int_mngt_value] : (v1 = v0 | ~ % 69.23/10.00 | (t2tb4(v2) = v1) | ~ (t2tb4(v2) = v0)) % 69.23/10.00 | (21) ! [v0: uni] : ! [v1: uni] : ! [v2: lprp_mngt_value] : (v1 = v0 | ~ % 69.23/10.00 | (t2tb5(v2) = v1) | ~ (t2tb5(v2) = v0)) % 69.23/10.00 | (22) ! [v0: expr] : ! [v1: expr] : ! [v2: expr] : ! [v3: context] : (v1 % 69.23/10.00 | = v0 | ~ (recompose(v3, v2) = v1) | ~ (recompose(v3, v2) = v0)) % 69.23/10.00 | % 69.23/10.00 | DELTA: instantiating (8) with fresh symbol all_146_0 gives: % 69.23/10.00 | (23) t2tb5(fc3) = all_146_0 & uni(all_146_0) & ! [v0: tuple0] : ! [v1: % 69.23/10.00 | uni] : ( ~ (t2tb2(v0) = v1) | ~ tuple0(v0) | ? [v2: uni] : % 69.23/10.00 | (tb2t(v2) = underflow & infix_at(value1, tuple01, all_146_0, v1) = % 69.23/10.00 | v2 & uni(v2))) % 69.23/10.00 | % 69.23/10.00 | ALPHA: (23) implies: % 69.23/10.00 | (24) t2tb5(fc3) = all_146_0 % 69.23/10.00 | % 69.23/10.00 | DELTA: instantiating (4) with fresh symbol all_149_0 gives: % 69.23/10.00 | (25) t2tb1(fc2) = all_149_0 & uni(all_149_0) & ! [v0: value] : ! [v1: % 69.23/10.00 | uni] : ( ~ (t2tb(v0) = v1) | ~ value(v0) | ? [v2: uni] : (tb2t(v2) % 69.23/10.00 | = v0 & infix_at(value1, value1, all_149_0, v1) = v2 & uni(v2))) % 69.23/10.00 | % 69.23/10.00 | ALPHA: (25) implies: % 69.23/10.00 | (26) t2tb1(fc2) = all_149_0 % 69.23/10.00 | % 69.23/10.00 | DELTA: instantiating (5) with fresh symbol all_161_0 gives: % 69.23/10.00 | (27) t2tb1(fc2) = all_161_0 & uni(all_161_0) & ! [v0: expr] : ! [v1: uni] % 69.23/10.00 | : ( ~ (eval_1(value1, v0, all_161_0) = v1) | ~ expr(v0) | ? [v2: % 69.23/10.00 | value] : (tb2t(v1) = v2 & eval_0(v0) = v2 & value(v2))) & ! [v0: % 69.23/10.00 | expr] : ! [v1: value] : ( ~ (eval_0(v0) = v1) | ~ expr(v0) | ? % 69.23/10.00 | [v2: uni] : (tb2t(v2) = v1 & eval_1(value1, v0, all_161_0) = v2 & % 69.23/10.00 | value(v1) & uni(v2))) % 69.23/10.00 | % 69.23/10.00 | ALPHA: (27) implies: % 69.23/10.00 | (28) uni(all_161_0) % 69.23/10.00 | (29) t2tb1(fc2) = all_161_0 % 69.23/10.00 | (30) ! [v0: expr] : ! [v1: value] : ( ~ (eval_0(v0) = v1) | ~ expr(v0) | % 69.23/10.00 | ? [v2: uni] : (tb2t(v2) = v1 & eval_1(value1, v0, all_161_0) = v2 & % 69.23/10.00 | value(v1) & uni(v2))) % 69.23/10.00 | % 69.23/10.00 | DELTA: instantiating (7) with fresh symbol all_164_0 gives: % 69.23/10.00 | (31) t2tb4(vnum_closure) = all_164_0 & uni(all_164_0) & ! [v0: int] : ! % 69.23/10.00 | [v1: uni] : ( ~ (t2tb3(v0) = v1) | ? [v2: uni] : ? [v3: value] : % 69.23/10.00 | (tb2t(v2) = v3 & infix_at(value1, int, all_164_0, v1) = v2 & % 69.23/10.00 | vnum(v0) = v3 & value(v3) & uni(v2))) & ! [v0: int] : ! [v1: % 69.23/10.00 | value] : ( ~ (vnum(v0) = v1) | ? [v2: uni] : ? [v3: uni] : % 69.23/10.00 | (t2tb3(v0) = v2 & tb2t(v3) = v1 & infix_at(value1, int, all_164_0, % 69.23/10.00 | v2) = v3 & value(v1) & uni(v3) & uni(v2))) % 69.23/10.00 | % 69.23/10.00 | ALPHA: (31) implies: % 69.23/10.00 | (32) t2tb4(vnum_closure) = all_164_0 % 69.23/10.00 | % 69.23/10.00 | DELTA: instantiating (9) with fresh symbols all_167_0, all_167_1 gives: % 69.23/10.00 | (33) t2tb5(fc3) = all_167_0 & t2tb4(vnum_closure) = all_167_1 & % 69.23/10.00 | uni(all_167_0) & uni(all_167_1) & ! [v0: expr] : ! [v1: uni] : ( ~ % 69.23/10.00 | (eval_2(value1, v0, all_167_1, all_167_0) = v1) | ~ expr(v0) | ? % 69.23/10.00 | [v2: value] : (tb2t(v1) = v2 & eval_0(v0) = v2 & value(v2))) & ! % 69.23/10.00 | [v0: expr] : ! [v1: value] : ( ~ (eval_0(v0) = v1) | ~ expr(v0) | ? % 69.23/10.00 | [v2: uni] : (eval_2(value1, v0, all_167_1, all_167_0) = v2 & % 69.23/10.00 | tb2t(v2) = v1 & value(v1) & uni(v2))) % 69.23/10.00 | % 69.23/10.00 | ALPHA: (33) implies: % 69.23/10.00 | (34) uni(all_167_1) % 69.23/10.00 | (35) uni(all_167_0) % 69.23/10.00 | (36) t2tb4(vnum_closure) = all_167_1 % 69.23/10.00 | (37) t2tb5(fc3) = all_167_0 % 69.23/10.01 | (38) ! [v0: expr] : ! [v1: value] : ( ~ (eval_0(v0) = v1) | ~ expr(v0) | % 69.23/10.01 | ? [v2: uni] : (eval_2(value1, v0, all_167_1, all_167_0) = v2 & % 69.23/10.01 | tb2t(v2) = v1 & value(v1) & uni(v2))) % 69.23/10.01 | % 69.23/10.01 | DELTA: instantiating (wP_parameter_eval_2) with fresh symbols all_174_0, % 69.23/10.01 | all_174_1, all_174_2, all_174_3, all_174_4, all_174_5, all_174_6, % 69.23/10.01 | all_174_7, all_174_8, all_174_9 gives: % 69.23/10.01 | (39) ~ (all_174_0 = all_174_5) & $lesseq(all_174_8, all_174_4) & % 69.23/10.01 | $lesseq(0, all_174_8) & recompose(all_174_3, all_174_2) = all_174_1 & % 69.23/10.01 | recompose(all_174_9, all_174_7) = all_174_6 & right(all_174_4, % 69.23/10.01 | all_174_3) = all_174_9 & eval_0(all_174_1) = all_174_0 & % 69.23/10.01 | eval_0(all_174_6) = all_174_5 & cte($difference(all_174_4, all_174_8)) % 69.23/10.01 | = all_174_2 & cte(all_174_8) = all_174_7 & context(all_174_3) & % 69.23/10.01 | context(all_174_9) & value(all_174_0) & value(all_174_5) & % 69.23/10.01 | expr(all_174_1) & expr(all_174_2) & expr(all_174_6) & expr(all_174_7) % 69.23/10.01 | % 69.23/10.01 | ALPHA: (39) implies: % 69.23/10.01 | (40) ~ (all_174_0 = all_174_5) % 69.23/10.01 | (41) $lesseq(0, all_174_8) % 69.23/10.01 | (42) $lesseq(all_174_8, all_174_4) % 69.23/10.01 | (43) expr(all_174_7) % 69.23/10.01 | (44) expr(all_174_2) % 69.23/10.01 | (45) expr(all_174_1) % 69.23/10.01 | (46) context(all_174_3) % 69.23/10.01 | (47) cte(all_174_8) = all_174_7 % 69.23/10.01 | (48) cte($difference(all_174_4, all_174_8)) = all_174_2 % 69.23/10.01 | (49) eval_0(all_174_6) = all_174_5 % 69.23/10.01 | (50) eval_0(all_174_1) = all_174_0 % 69.23/10.01 | (51) right(all_174_4, all_174_3) = all_174_9 % 69.23/10.01 | (52) recompose(all_174_9, all_174_7) = all_174_6 % 69.23/10.01 | (53) recompose(all_174_3, all_174_2) = all_174_1 % 69.23/10.01 | % 69.23/10.01 | DELTA: instantiating (11) with fresh symbol all_180_0 gives: % 69.23/10.01 | (54) t2tb(underflow) = all_180_0 & uni(all_180_0) & ! [v0: expr] : ! [v1: % 69.23/10.01 | int_mngt_value] : ! [v2: value] : ! [v3: uni] : ! [v4: int] : ! % 69.23/10.01 | [v5: uni] : ! [v6: uni] : ( ~ (t2tb4(v1) = v3) | ~ (t2tb3(v4) = v5) % 69.23/10.01 | | ~ (infix_at(value1, int, v3, v5) = v6) | ~ (eval_0(v0) = v2) | % 69.23/10.01 | ~ (vnum_proj_1(v2) = v4) | ~ int_mngt_value(v1) | ~ expr(v0) | ? % 69.23/10.01 | [v7: value] : ? [v8: uni] : (eval_3(v0, v1) = v7 & tb2t(v8) = v7 & % 69.23/10.01 | match_value(value1, v2, v6, all_180_0) = v8 & value(v7) & % 69.23/10.01 | uni(v8))) & ! [v0: expr] : ! [v1: int_mngt_value] : ! [v2: % 69.23/10.01 | value] : ( ~ (eval_3(v0, v1) = v2) | ~ int_mngt_value(v1) | ~ % 69.23/10.01 | expr(v0) | ? [v3: value] : ? [v4: uni] : ? [v5: int] : ? [v6: % 69.23/10.01 | uni] : ? [v7: uni] : ? [v8: uni] : (t2tb4(v1) = v4 & t2tb3(v5) = % 69.23/10.01 | v6 & tb2t(v8) = v2 & infix_at(value1, int, v4, v6) = v7 & % 69.23/10.01 | eval_0(v0) = v3 & vnum_proj_1(v3) = v5 & match_value(value1, v3, % 69.23/10.01 | v7, all_180_0) = v8 & value(v3) & value(v2) & uni(v8) & uni(v7) % 69.23/10.01 | & uni(v6) & uni(v4))) % 69.23/10.01 | % 69.23/10.01 | ALPHA: (54) implies: % 69.23/10.01 | (55) ! [v0: expr] : ! [v1: int_mngt_value] : ! [v2: value] : ( ~ % 69.23/10.01 | (eval_3(v0, v1) = v2) | ~ int_mngt_value(v1) | ~ expr(v0) | ? % 69.23/10.01 | [v3: value] : ? [v4: uni] : ? [v5: int] : ? [v6: uni] : ? [v7: % 69.23/10.01 | uni] : ? [v8: uni] : (t2tb4(v1) = v4 & t2tb3(v5) = v6 & tb2t(v8) % 69.23/10.01 | = v2 & infix_at(value1, int, v4, v6) = v7 & eval_0(v0) = v3 & % 69.23/10.01 | vnum_proj_1(v3) = v5 & match_value(value1, v3, v7, all_180_0) = v8 % 69.23/10.01 | & value(v3) & value(v2) & uni(v8) & uni(v7) & uni(v6) & uni(v4))) % 69.23/10.01 | % 69.23/10.01 | DELTA: instantiating (6) with fresh symbol all_183_0 gives: % 69.23/10.01 | (56) t2tb2(tuple02) = all_183_0 & uni(all_183_0) & ! [v0: ty] : ! [v1: % 69.23/10.01 | expr] : ! [v2: uni] : ! [v3: uni] : ! [v4: value] : ! [v5: int] % 69.23/10.01 | : ! [v6: uni] : ! [v7: uni] : ! [v8: uni] : ! [v9: uni] : ( ~ % 69.23/10.01 | (t2tb3(v5) = v6) | ~ (infix_at(v0, tuple01, v2, all_183_0) = v8) | % 69.23/10.01 | ~ (infix_at(v0, int, v3, v6) = v7) | ~ (eval_0(v1) = v4) | ~ % 69.23/10.01 | (vnum_proj_1(v4) = v5) | ~ (match_value(v0, v4, v7, v8) = v9) | ~ % 69.23/10.01 | expr(v1) | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | (eval_2(v0, v1, v3, % 69.23/10.01 | v2) = v9 & uni(v9))) & ! [v0: ty] : ! [v1: expr] : ! [v2: % 69.23/10.01 | uni] : ! [v3: uni] : ! [v4: uni] : ( ~ (eval_2(v0, v1, v3, v2) = % 69.23/10.01 | v4) | ~ expr(v1) | ~ ty(v0) | ~ uni(v3) | ~ uni(v2) | ? [v5: % 69.23/10.01 | value] : ? [v6: int] : ? [v7: uni] : ? [v8: uni] : ? [v9: uni] % 69.23/10.01 | : (t2tb3(v6) = v7 & infix_at(v0, tuple01, v2, all_183_0) = v9 & % 69.23/10.01 | infix_at(v0, int, v3, v7) = v8 & eval_0(v1) = v5 & vnum_proj_1(v5) % 69.23/10.01 | = v6 & match_value(v0, v5, v8, v9) = v4 & value(v5) & uni(v9) & % 69.23/10.01 | uni(v8) & uni(v7) & uni(v4))) % 69.23/10.01 | % 69.23/10.01 | ALPHA: (56) implies: % 69.23/10.01 | (57) ! [v0: ty] : ! [v1: expr] : ! [v2: uni] : ! [v3: uni] : ! [v4: % 69.23/10.01 | uni] : ( ~ (eval_2(v0, v1, v3, v2) = v4) | ~ expr(v1) | ~ ty(v0) | % 69.23/10.01 | ~ uni(v3) | ~ uni(v2) | ? [v5: value] : ? [v6: int] : ? [v7: % 69.23/10.01 | uni] : ? [v8: uni] : ? [v9: uni] : (t2tb3(v6) = v7 & % 69.23/10.01 | infix_at(v0, tuple01, v2, all_183_0) = v9 & infix_at(v0, int, v3, % 69.23/10.01 | v7) = v8 & eval_0(v1) = v5 & vnum_proj_1(v5) = v6 & % 69.23/10.01 | match_value(v0, v5, v8, v9) = v4 & value(v5) & uni(v9) & uni(v8) & % 69.23/10.01 | uni(v7) & uni(v4))) % 69.23/10.01 | % 69.23/10.01 | GROUND_INST: instantiating (19) with all_149_0, all_161_0, fc2, simplifying % 69.23/10.01 | with (26), (29) gives: % 69.23/10.01 | (58) all_161_0 = all_149_0 % 69.23/10.01 | % 69.23/10.01 | GROUND_INST: instantiating (20) with all_164_0, all_167_1, vnum_closure, % 69.23/10.01 | simplifying with (32), (36) gives: % 69.23/10.01 | (59) all_167_1 = all_164_0 % 69.23/10.01 | % 69.23/10.01 | GROUND_INST: instantiating (21) with all_146_0, all_167_0, fc3, simplifying % 69.23/10.01 | with (24), (37) gives: % 69.23/10.01 | (60) all_167_0 = all_146_0 % 69.23/10.01 | % 69.23/10.01 | REDUCE: (35), (60) imply: % 69.23/10.01 | (61) uni(all_146_0) % 69.23/10.01 | % 69.23/10.01 | REDUCE: (34), (59) imply: % 69.23/10.01 | (62) uni(all_164_0) % 69.23/10.01 | % 69.23/10.01 | REDUCE: (28), (58) imply: % 69.23/10.01 | (63) uni(all_149_0) % 69.23/10.01 | % 69.23/10.01 | GROUND_INST: instantiating (1) with all_174_8, all_174_7, simplifying with % 69.23/10.01 | (47) gives: % 69.23/10.01 | (64) ~ ($lesseq(0, all_174_8)) | ? [v0: value] : (eval_0(all_174_7) = v0 % 69.23/10.01 | & vnum(all_174_8) = v0 & value(v0)) % 69.23/10.01 | % 69.23/10.01 | GROUND_INST: instantiating (1) with $difference(all_174_4, all_174_8), % 69.23/10.01 | all_174_2, simplifying with (48) gives: % 69.23/10.01 | (65) ~ ($lesseq(all_174_8, all_174_4)) | ? [v0: value] : % 69.23/10.01 | (eval_0(all_174_2) = v0 & vnum($difference(all_174_4, all_174_8)) = v0 % 69.23/10.01 | & value(v0)) % 69.23/10.01 | % 69.23/10.01 | GROUND_INST: instantiating (38) with all_174_1, all_174_0, simplifying with % 69.23/10.01 | (45), (50) gives: % 69.23/10.01 | (66) ? [v0: uni] : (eval_2(value1, all_174_1, all_167_1, all_167_0) = v0 & % 69.23/10.01 | tb2t(v0) = all_174_0 & value(all_174_0) & uni(v0)) % 69.23/10.01 | % 69.23/10.02 | GROUND_INST: instantiating (30) with all_174_1, all_174_0, simplifying with % 69.23/10.02 | (45), (50) gives: % 69.23/10.02 | (67) ? [v0: uni] : (tb2t(v0) = all_174_0 & eval_1(value1, all_174_1, % 69.23/10.02 | all_161_0) = v0 & value(all_174_0) & uni(v0)) % 69.23/10.02 | % 69.23/10.02 | GROUND_INST: instantiating (13) with all_174_1, all_174_0, simplifying with % 69.23/10.02 | (45), (50) gives: % 69.23/10.02 | (68) eval_3(all_174_1, vnum_closure) = all_174_0 & value(all_174_0) % 69.23/10.02 | % 69.23/10.02 | ALPHA: (68) implies: % 69.23/10.02 | (69) eval_3(all_174_1, vnum_closure) = all_174_0 % 69.23/10.02 | % 69.23/10.02 | GROUND_INST: instantiating (14) with all_174_7, all_174_4, all_174_3, % 69.23/10.02 | all_174_9, all_174_6, simplifying with (43), (46), (51), (52) % 69.23/10.02 | gives: % 69.23/10.02 | (70) ? [v0: expr] : ? [v1: expr] : (recompose(all_174_3, v1) = all_174_6 % 69.23/10.02 | & sub(v0, all_174_7) = v1 & cte(all_174_4) = v0 & expr(v1) & % 69.23/10.02 | expr(v0) & expr(all_174_6)) % 69.23/10.02 | % 69.23/10.02 | DELTA: instantiating (67) with fresh symbol all_217_0 gives: % 69.23/10.02 | (71) tb2t(all_217_0) = all_174_0 & eval_1(value1, all_174_1, all_161_0) = % 69.23/10.02 | all_217_0 & value(all_174_0) & uni(all_217_0) % 69.23/10.02 | % 69.23/10.02 | ALPHA: (71) implies: % 69.23/10.02 | (72) eval_1(value1, all_174_1, all_161_0) = all_217_0 % 69.23/10.02 | % 69.23/10.02 | DELTA: instantiating (66) with fresh symbol all_223_0 gives: % 69.23/10.02 | (73) eval_2(value1, all_174_1, all_167_1, all_167_0) = all_223_0 & % 69.23/10.02 | tb2t(all_223_0) = all_174_0 & value(all_174_0) & uni(all_223_0) % 69.23/10.02 | % 69.23/10.02 | ALPHA: (73) implies: % 69.23/10.02 | (74) eval_2(value1, all_174_1, all_167_1, all_167_0) = all_223_0 % 69.23/10.02 | % 69.23/10.02 | DELTA: instantiating (70) with fresh symbols all_227_0, all_227_1 gives: % 69.23/10.02 | (75) recompose(all_174_3, all_227_0) = all_174_6 & sub(all_227_1, % 69.23/10.02 | all_174_7) = all_227_0 & cte(all_174_4) = all_227_1 & % 69.23/10.02 | expr(all_227_0) & expr(all_227_1) & expr(all_174_6) % 69.23/10.02 | % 69.23/10.02 | ALPHA: (75) implies: % 69.23/10.02 | (76) expr(all_227_1) % 69.23/10.02 | (77) expr(all_227_0) % 69.23/10.02 | (78) cte(all_174_4) = all_227_1 % 69.23/10.02 | (79) sub(all_227_1, all_174_7) = all_227_0 % 69.23/10.02 | (80) recompose(all_174_3, all_227_0) = all_174_6 % 69.23/10.02 | % 69.23/10.02 | REDUCE: (59), (60), (74) imply: % 69.23/10.02 | (81) eval_2(value1, all_174_1, all_164_0, all_146_0) = all_223_0 % 69.23/10.02 | % 69.23/10.02 | REDUCE: (58), (72) imply: % 69.23/10.02 | (82) eval_1(value1, all_174_1, all_149_0) = all_217_0 % 69.23/10.02 | % 69.23/10.02 | BETA: splitting (64) gives: % 69.23/10.02 | % 69.23/10.02 | Case 1: % 69.23/10.02 | | % 69.23/10.02 | | (83) $lesseq(all_174_8, -1) % 69.23/10.02 | | % 69.23/10.02 | | COMBINE_INEQS: (41), (83) imply: % 69.23/10.02 | | (84) $false % 69.23/10.02 | | % 69.23/10.02 | | CLOSE: (84) is inconsistent. % 69.23/10.02 | | % 69.23/10.02 | Case 2: % 69.23/10.02 | | % 69.23/10.02 | | (85) ? [v0: value] : (eval_0(all_174_7) = v0 & vnum(all_174_8) = v0 & % 69.23/10.02 | | value(v0)) % 69.23/10.02 | | % 69.23/10.02 | | DELTA: instantiating (85) with fresh symbol all_238_0 gives: % 69.23/10.02 | | (86) eval_0(all_174_7) = all_238_0 & vnum(all_174_8) = all_238_0 & % 69.23/10.02 | | value(all_238_0) % 69.23/10.02 | | % 69.23/10.02 | | ALPHA: (86) implies: % 69.23/10.02 | | (87) vnum(all_174_8) = all_238_0 % 69.23/10.02 | | (88) eval_0(all_174_7) = all_238_0 % 69.23/10.02 | | % 69.23/10.02 | | BETA: splitting (65) gives: % 69.23/10.02 | | % 69.23/10.02 | | Case 1: % 69.23/10.02 | | | % 69.23/10.02 | | | (89) $lesseq(1, $difference(all_174_8, all_174_4)) % 69.23/10.02 | | | % 69.23/10.02 | | | COMBINE_INEQS: (42), (89) imply: % 69.23/10.02 | | | (90) $false % 69.23/10.02 | | | % 69.23/10.02 | | | CLOSE: (90) is inconsistent. % 69.23/10.02 | | | % 69.23/10.02 | | Case 2: % 69.23/10.02 | | | % 69.23/10.02 | | | (91) ? [v0: value] : (eval_0(all_174_2) = v0 & % 69.23/10.02 | | | vnum($difference(all_174_4, all_174_8)) = v0 & value(v0)) % 69.23/10.02 | | | % 69.23/10.02 | | | DELTA: instantiating (91) with fresh symbol all_243_0 gives: % 69.23/10.02 | | | (92) eval_0(all_174_2) = all_243_0 & vnum($difference(all_174_4, % 69.23/10.02 | | | all_174_8)) = all_243_0 & value(all_243_0) % 69.23/10.02 | | | % 69.23/10.02 | | | ALPHA: (92) implies: % 69.23/10.02 | | | (93) vnum($difference(all_174_4, all_174_8)) = all_243_0 % 69.23/10.02 | | | (94) eval_0(all_174_2) = all_243_0 % 69.23/10.02 | | | % 69.23/10.02 | | | GROUND_INST: instantiating (1) with all_174_4, all_227_1, simplifying with % 69.23/10.02 | | | (78) gives: % 69.23/10.02 | | | (95) ~ ($lesseq(0, all_174_4)) | ? [v0: value] : (eval_0(all_227_1) = % 69.23/10.02 | | | v0 & vnum(all_174_4) = v0 & value(v0)) % 69.23/10.02 | | | % 69.23/10.02 | | | GROUND_INST: instantiating (3) with value1, all_174_1, all_149_0, % 69.23/10.02 | | | all_217_0, simplifying with (10), (45), (63), (82) gives: % 69.23/10.02 | | | (96) ? [v0: value] : ? [v1: uni] : (t2tb(v0) = v1 & infix_at(value1, % 69.23/10.02 | | | value1, all_149_0, v1) = all_217_0 & eval_0(all_174_1) = v0 & % 69.23/10.02 | | | value(v0) & uni(v1) & uni(all_217_0)) % 69.23/10.02 | | | % 69.23/10.02 | | | GROUND_INST: instantiating (57) with value1, all_174_1, all_146_0, % 69.23/10.02 | | | all_164_0, all_223_0, simplifying with (10), (45), (61), % 69.23/10.02 | | | (62), (81) gives: % 69.23/10.02 | | | (97) ? [v0: value] : ? [v1: int] : ? [v2: uni] : ? [v3: uni] : ? % 69.23/10.02 | | | [v4: uni] : (t2tb3(v1) = v2 & infix_at(value1, tuple01, all_146_0, % 69.23/10.02 | | | all_183_0) = v4 & infix_at(value1, int, all_164_0, v2) = v3 & % 69.23/10.02 | | | eval_0(all_174_1) = v0 & vnum_proj_1(v0) = v1 & % 69.23/10.02 | | | match_value(value1, v0, v3, v4) = all_223_0 & value(v0) & % 69.23/10.02 | | | uni(v4) & uni(v3) & uni(v2) & uni(all_223_0)) % 69.23/10.02 | | | % 69.23/10.02 | | | GROUND_INST: instantiating (55) with all_174_1, vnum_closure, all_174_0, % 69.23/10.02 | | | simplifying with (12), (45), (69) gives: % 69.23/10.02 | | | (98) ? [v0: value] : ? [v1: uni] : ? [v2: int] : ? [v3: uni] : ? % 69.23/10.02 | | | [v4: uni] : ? [v5: uni] : (t2tb4(vnum_closure) = v1 & t2tb3(v2) = % 69.23/10.02 | | | v3 & tb2t(v5) = all_174_0 & infix_at(value1, int, v1, v3) = v4 & % 69.23/10.02 | | | eval_0(all_174_1) = v0 & vnum_proj_1(v0) = v2 & % 69.23/10.02 | | | match_value(value1, v0, v4, all_180_0) = v5 & value(v0) & % 69.23/10.02 | | | value(all_174_0) & uni(v5) & uni(v4) & uni(v3) & uni(v1)) % 69.23/10.02 | | | % 69.23/10.02 | | | GROUND_INST: instantiating (16) with all_174_3, all_174_2, all_227_0, % 69.23/10.02 | | | all_174_1, all_174_0, all_174_6, all_174_5, simplifying with % 69.23/10.02 | | | (44), (46), (49), (50), (53), (77), (80) gives: % 69.23/10.03 | | | (99) all_174_0 = all_174_5 | ? [v0: value] : ? [v1: value] : ( ~ (v1 % 69.23/10.03 | | | = v0) & eval_0(all_227_0) = v1 & eval_0(all_174_2) = v0 & % 69.23/10.03 | | | value(v1) & value(v0)) % 69.23/10.03 | | | % 69.23/10.03 | | | GROUND_INST: instantiating (15) with all_174_3, all_174_2, all_227_0, % 69.23/10.03 | | | all_243_0, all_174_6, all_174_5, simplifying with (44), (46), % 69.23/10.03 | | | (49), (77), (80), (94) gives: % 69.23/10.03 | | | (100) ? [v0: any] : ? [v1: expr] : ? [v2: int] : ((v2 = all_174_5 & % 69.23/10.03 | | | recompose(all_174_3, all_174_2) = v1 & eval_0(v1) = all_174_5 % 69.23/10.03 | | | & value(all_174_5) & expr(v1)) | ( ~ (v0 = all_243_0) & % 69.23/10.03 | | | eval_0(all_227_0) = v0 & value(v0))) % 69.23/10.03 | | | % 69.23/10.03 | | | DELTA: instantiating (96) with fresh symbols all_276_0, all_276_1 gives: % 69.23/10.03 | | | (101) t2tb(all_276_1) = all_276_0 & infix_at(value1, value1, all_149_0, % 69.23/10.03 | | | all_276_0) = all_217_0 & eval_0(all_174_1) = all_276_1 & % 69.23/10.03 | | | value(all_276_1) & uni(all_276_0) & uni(all_217_0) % 69.23/10.03 | | | % 69.23/10.03 | | | ALPHA: (101) implies: % 69.23/10.03 | | | (102) eval_0(all_174_1) = all_276_1 % 69.23/10.03 | | | % 69.23/10.03 | | | DELTA: instantiating (100) with fresh symbols all_284_0, all_284_1, % 69.23/10.03 | | | all_284_2 gives: % 69.23/10.03 | | | (103) (all_284_0 = all_174_5 & recompose(all_174_3, all_174_2) = % 69.23/10.03 | | | all_284_1 & eval_0(all_284_1) = all_174_5 & value(all_174_5) & % 69.23/10.03 | | | expr(all_284_1)) | ( ~ (all_284_2 = all_243_0) & % 69.23/10.03 | | | eval_0(all_227_0) = all_284_2 & value(all_284_2)) % 69.23/10.03 | | | % 69.23/10.03 | | | DELTA: instantiating (97) with fresh symbols all_290_0, all_290_1, % 69.23/10.03 | | | all_290_2, all_290_3, all_290_4 gives: % 69.23/10.03 | | | (104) t2tb3(all_290_3) = all_290_2 & infix_at(value1, tuple01, % 69.23/10.03 | | | all_146_0, all_183_0) = all_290_0 & infix_at(value1, int, % 69.23/10.03 | | | all_164_0, all_290_2) = all_290_1 & eval_0(all_174_1) = % 69.23/10.03 | | | all_290_4 & vnum_proj_1(all_290_4) = all_290_3 & % 69.23/10.03 | | | match_value(value1, all_290_4, all_290_1, all_290_0) = all_223_0 % 69.23/10.03 | | | & value(all_290_4) & uni(all_290_0) & uni(all_290_1) & % 69.23/10.03 | | | uni(all_290_2) & uni(all_223_0) % 69.23/10.03 | | | % 69.23/10.03 | | | ALPHA: (104) implies: % 69.23/10.03 | | | (105) eval_0(all_174_1) = all_290_4 % 69.23/10.03 | | | % 69.23/10.03 | | | DELTA: instantiating (98) with fresh symbols all_292_0, all_292_1, % 69.23/10.03 | | | all_292_2, all_292_3, all_292_4, all_292_5 gives: % 69.23/10.03 | | | (106) t2tb4(vnum_closure) = all_292_4 & t2tb3(all_292_3) = all_292_2 & % 69.23/10.03 | | | tb2t(all_292_0) = all_174_0 & infix_at(value1, int, all_292_4, % 69.23/10.03 | | | all_292_2) = all_292_1 & eval_0(all_174_1) = all_292_5 & % 69.23/10.03 | | | vnum_proj_1(all_292_5) = all_292_3 & match_value(value1, % 69.23/10.03 | | | all_292_5, all_292_1, all_180_0) = all_292_0 & value(all_292_5) % 69.23/10.03 | | | & value(all_174_0) & uni(all_292_0) & uni(all_292_1) & % 69.23/10.03 | | | uni(all_292_2) & uni(all_292_4) % 69.23/10.03 | | | % 69.23/10.03 | | | ALPHA: (106) implies: % 69.23/10.03 | | | (107) eval_0(all_174_1) = all_292_5 % 69.23/10.03 | | | % 69.23/10.03 | | | BETA: splitting (103) gives: % 69.23/10.03 | | | % 69.23/10.03 | | | Case 1: % 69.23/10.03 | | | | % 69.23/10.03 | | | | (108) all_284_0 = all_174_5 & recompose(all_174_3, all_174_2) = % 69.23/10.03 | | | | all_284_1 & eval_0(all_284_1) = all_174_5 & value(all_174_5) & % 69.23/10.03 | | | | expr(all_284_1) % 69.23/10.03 | | | | % 69.23/10.03 | | | | ALPHA: (108) implies: % 69.23/10.03 | | | | (109) eval_0(all_284_1) = all_174_5 % 69.23/10.03 | | | | (110) recompose(all_174_3, all_174_2) = all_284_1 % 69.23/10.03 | | | | % 69.23/10.03 | | | | GROUND_INST: instantiating (18) with all_174_0, all_290_4, all_174_1, % 69.23/10.03 | | | | simplifying with (50), (105) gives: % 69.23/10.03 | | | | (111) all_290_4 = all_174_0 % 69.23/10.03 | | | | % 69.23/10.03 | | | | GROUND_INST: instantiating (18) with all_290_4, all_292_5, all_174_1, % 69.23/10.03 | | | | simplifying with (105), (107) gives: % 69.23/10.03 | | | | (112) all_292_5 = all_290_4 % 69.23/10.03 | | | | % 69.23/10.03 | | | | GROUND_INST: instantiating (18) with all_276_1, all_292_5, all_174_1, % 69.23/10.03 | | | | simplifying with (102), (107) gives: % 69.23/10.03 | | | | (113) all_292_5 = all_276_1 % 69.23/10.03 | | | | % 69.23/10.03 | | | | GROUND_INST: instantiating (22) with all_174_1, all_284_1, all_174_2, % 69.23/10.03 | | | | all_174_3, simplifying with (53), (110) gives: % 69.23/10.03 | | | | (114) all_284_1 = all_174_1 % 69.23/10.03 | | | | % 69.23/10.03 | | | | COMBINE_EQS: (112), (113) imply: % 69.23/10.03 | | | | (115) all_290_4 = all_276_1 % 69.23/10.03 | | | | % 69.23/10.03 | | | | SIMP: (115) implies: % 69.23/10.03 | | | | (116) all_290_4 = all_276_1 % 69.23/10.03 | | | | % 69.23/10.03 | | | | COMBINE_EQS: (111), (116) imply: % 69.23/10.03 | | | | (117) all_276_1 = all_174_0 % 69.23/10.03 | | | | % 69.23/10.03 | | | | REDUCE: (109), (114) imply: % 69.23/10.03 | | | | (118) eval_0(all_174_1) = all_174_5 % 69.23/10.03 | | | | % 69.23/10.03 | | | | GROUND_INST: instantiating (18) with all_174_0, all_174_5, all_174_1, % 69.23/10.03 | | | | simplifying with (50), (118) gives: % 69.23/10.03 | | | | (119) all_174_0 = all_174_5 % 69.23/10.03 | | | | % 69.23/10.03 | | | | REDUCE: (40), (119) imply: % 69.23/10.03 | | | | (120) $false % 69.23/10.03 | | | | % 69.23/10.03 | | | | CLOSE: (120) is inconsistent. % 69.23/10.03 | | | | % 69.23/10.03 | | | Case 2: % 69.23/10.03 | | | | % 69.23/10.03 | | | | (121) ~ (all_284_2 = all_243_0) & eval_0(all_227_0) = all_284_2 & % 69.23/10.03 | | | | value(all_284_2) % 69.23/10.03 | | | | % 69.23/10.03 | | | | ALPHA: (121) implies: % 69.23/10.03 | | | | (122) eval_0(all_227_0) = all_284_2 % 69.23/10.03 | | | | % 69.23/10.03 | | | | BETA: splitting (99) gives: % 69.23/10.03 | | | | % 69.23/10.03 | | | | Case 1: % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | (123) all_174_0 = all_174_5 % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | REDUCE: (40), (123) imply: % 69.23/10.03 | | | | | (124) $false % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | CLOSE: (124) is inconsistent. % 69.23/10.03 | | | | | % 69.23/10.03 | | | | Case 2: % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | (125) ? [v0: value] : ? [v1: value] : ( ~ (v1 = v0) & % 69.23/10.03 | | | | | eval_0(all_227_0) = v1 & eval_0(all_174_2) = v0 & value(v1) % 69.23/10.03 | | | | | & value(v0)) % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | DELTA: instantiating (125) with fresh symbols all_330_0, all_330_1 % 69.23/10.03 | | | | | gives: % 69.23/10.03 | | | | | (126) ~ (all_330_0 = all_330_1) & eval_0(all_227_0) = all_330_0 & % 69.23/10.03 | | | | | eval_0(all_174_2) = all_330_1 & value(all_330_0) & % 69.23/10.03 | | | | | value(all_330_1) % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | ALPHA: (126) implies: % 69.23/10.03 | | | | | (127) ~ (all_330_0 = all_330_1) % 69.23/10.03 | | | | | (128) eval_0(all_174_2) = all_330_1 % 69.23/10.03 | | | | | (129) eval_0(all_227_0) = all_330_0 % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | BETA: splitting (95) gives: % 69.23/10.03 | | | | | % 69.23/10.03 | | | | | Case 1: % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | (130) $lesseq(all_174_4, -1) % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | COMBINE_INEQS: (42), (130) imply: % 69.23/10.03 | | | | | | (131) $lesseq(all_174_8, -1) % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | COMBINE_INEQS: (41), (131) imply: % 69.23/10.03 | | | | | | (132) $false % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | CLOSE: (132) is inconsistent. % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | Case 2: % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | (133) ? [v0: value] : (eval_0(all_227_1) = v0 & vnum(all_174_4) % 69.23/10.03 | | | | | | = v0 & value(v0)) % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | DELTA: instantiating (133) with fresh symbol all_337_0 gives: % 69.23/10.03 | | | | | | (134) eval_0(all_227_1) = all_337_0 & vnum(all_174_4) = all_337_0 % 69.23/10.03 | | | | | | & value(all_337_0) % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | ALPHA: (134) implies: % 69.23/10.03 | | | | | | (135) vnum(all_174_4) = all_337_0 % 69.23/10.03 | | | | | | (136) eval_0(all_227_1) = all_337_0 % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | GROUND_INST: instantiating (18) with all_243_0, all_330_1, % 69.23/10.03 | | | | | | all_174_2, simplifying with (94), (128) gives: % 69.23/10.03 | | | | | | (137) all_330_1 = all_243_0 % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | GROUND_INST: instantiating (18) with all_284_2, all_330_0, % 69.23/10.03 | | | | | | all_227_0, simplifying with (122), (129) gives: % 69.23/10.03 | | | | | | (138) all_330_0 = all_284_2 % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | REDUCE: (127), (137), (138) imply: % 69.23/10.03 | | | | | | (139) ~ (all_284_2 = all_243_0) % 69.23/10.03 | | | | | | % 69.23/10.03 | | | | | | GROUND_INST: instantiating (2) with all_227_1, all_174_7, all_174_4, % 69.23/10.03 | | | | | | all_337_0, all_227_0, all_284_2, simplifying with (43), % 69.23/10.03 | | | | | | (76), (79), (122), (135) gives: % 69.23/10.04 | | | | | | (140) ? [v0: any] : ? [v1: value] : (( ~ (v0 = all_337_0) & % 69.23/10.04 | | | | | | eval_0(all_227_1) = v0 & value(v0)) | % 69.23/10.04 | | | | | | (eval_0(all_174_7) = v1 & value(v1) & ! [v2: int] : ! % 69.23/10.04 | | | | | | [v3: int] : (v3 = all_284_2 | ~ ($lesseq(v2, % 69.23/10.04 | | | | | | all_174_4)) | ~ (vnum($difference(all_174_4, % 69.23/10.04 | | | | | | v2)) = v3) | ? [v4: value] : ( ~ (v4 = v1) & % 69.23/10.04 | | | | | | vnum(v2) = v4 & value(v4))) & ! [v2: int] : ! % 69.23/10.04 | | | | | | [v3: value] : (all_284_2 = underflow | ~ ($lesseq(1, % 69.23/10.04 | | | | | | $difference(v2, all_174_4))) | ~ % 69.23/10.04 | | | | | | (vnum($difference(all_174_4, v2)) = v3) | ? [v4: % 69.23/10.04 | | | | | | value] : ( ~ (v4 = v1) & vnum(v2) = v4 & % 69.23/10.04 | | | | | | value(v4))) & ! [v2: int] : (all_284_2 = underflow % 69.23/10.04 | | | | | | | ~ ($lesseq(1, $difference(v2, all_174_4))) | ~ % 69.23/10.04 | | | | | | (vnum(v2) = v1)) & ! [v2: int] : ( ~ ($lesseq(v2, % 69.23/10.04 | | | | | | all_174_4)) | ~ (vnum(v2) = v1) | % 69.23/10.04 | | | | | | (vnum($difference(all_174_4, v2)) = all_284_2 & % 69.23/10.04 | | | | | | value(all_284_2))) & ( ~ (v1 = underflow) | % 69.23/10.04 | | | | | | all_284_2 = underflow))) % 69.23/10.04 | | | | | | % 69.23/10.04 | | | | | | DELTA: instantiating (140) with fresh symbols all_775_0, all_775_1 % 69.23/10.04 | | | | | | gives: % 69.23/10.04 | | | | | | (141) ( ~ (all_775_1 = all_337_0) & eval_0(all_227_1) = all_775_1 % 69.23/10.04 | | | | | | & value(all_775_1)) | (eval_0(all_174_7) = all_775_0 & % 69.23/10.04 | | | | | | value(all_775_0) & ! [v0: int] : ! [v1: int] : (v1 = % 69.23/10.04 | | | | | | all_284_2 | ~ ($lesseq(v0, all_174_4)) | ~ % 69.23/10.04 | | | | | | (vnum($difference(all_174_4, v0)) = v1) | ? [v2: any] % 69.23/10.04 | | | | | | : ( ~ (v2 = all_775_0) & vnum(v0) = v2 & value(v2))) & % 69.23/10.04 | | | | | | ! [v0: int] : ! [v1: value] : (all_284_2 = underflow | % 69.23/10.04 | | | | | | ~ ($lesseq(1, $difference(v0, all_174_4))) | ~ % 69.23/10.04 | | | | | | (vnum($difference(all_174_4, v0)) = v1) | ? [v2: any] % 69.23/10.04 | | | | | | : ( ~ (v2 = all_775_0) & vnum(v0) = v2 & value(v2))) & % 69.23/10.04 | | | | | | ! [v0: int] : (all_284_2 = underflow | ~ ($lesseq(1, % 69.23/10.04 | | | | | | $difference(v0, all_174_4))) | ~ (vnum(v0) = % 69.23/10.04 | | | | | | all_775_0)) & ! [v0: int] : ( ~ ($lesseq(v0, % 69.23/10.04 | | | | | | all_174_4)) | ~ (vnum(v0) = all_775_0) | % 69.23/10.04 | | | | | | (vnum($difference(all_174_4, v0)) = all_284_2 & % 69.23/10.04 | | | | | | value(all_284_2))) & ( ~ (all_775_0 = underflow) | % 69.23/10.04 | | | | | | all_284_2 = underflow)) % 69.23/10.04 | | | | | | % 69.23/10.04 | | | | | | BETA: splitting (141) gives: % 69.23/10.04 | | | | | | % 69.23/10.04 | | | | | | Case 1: % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | (142) ~ (all_775_1 = all_337_0) & eval_0(all_227_1) = % 69.23/10.04 | | | | | | | all_775_1 & value(all_775_1) % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | ALPHA: (142) implies: % 69.23/10.04 | | | | | | | (143) ~ (all_775_1 = all_337_0) % 69.23/10.04 | | | | | | | (144) eval_0(all_227_1) = all_775_1 % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | GROUND_INST: instantiating (18) with all_337_0, all_775_1, % 69.23/10.04 | | | | | | | all_227_1, simplifying with (136), (144) gives: % 69.23/10.04 | | | | | | | (145) all_775_1 = all_337_0 % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | REDUCE: (143), (145) imply: % 69.23/10.04 | | | | | | | (146) $false % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | CLOSE: (146) is inconsistent. % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | Case 2: % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | (147) eval_0(all_174_7) = all_775_0 & value(all_775_0) & ! % 69.23/10.04 | | | | | | | [v0: int] : ! [v1: int] : (v1 = all_284_2 | ~ % 69.23/10.04 | | | | | | | ($lesseq(v0, all_174_4)) | ~ % 69.23/10.04 | | | | | | | (vnum($difference(all_174_4, v0)) = v1) | ? [v2: any] % 69.23/10.04 | | | | | | | : ( ~ (v2 = all_775_0) & vnum(v0) = v2 & value(v2))) & % 69.23/10.04 | | | | | | | ! [v0: int] : ! [v1: value] : (all_284_2 = underflow | % 69.23/10.04 | | | | | | | ~ ($lesseq(1, $difference(v0, all_174_4))) | ~ % 69.23/10.04 | | | | | | | (vnum($difference(all_174_4, v0)) = v1) | ? [v2: any] % 69.23/10.04 | | | | | | | : ( ~ (v2 = all_775_0) & vnum(v0) = v2 & value(v2))) & % 69.23/10.04 | | | | | | | ! [v0: int] : (all_284_2 = underflow | ~ ($lesseq(1, % 69.23/10.04 | | | | | | | $difference(v0, all_174_4))) | ~ (vnum(v0) = % 69.23/10.04 | | | | | | | all_775_0)) & ! [v0: int] : ( ~ ($lesseq(v0, % 69.23/10.04 | | | | | | | all_174_4)) | ~ (vnum(v0) = all_775_0) | % 69.23/10.04 | | | | | | | (vnum($difference(all_174_4, v0)) = all_284_2 & % 69.23/10.04 | | | | | | | value(all_284_2))) & ( ~ (all_775_0 = underflow) | % 69.23/10.04 | | | | | | | all_284_2 = underflow) % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | ALPHA: (147) implies: % 69.23/10.04 | | | | | | | (148) eval_0(all_174_7) = all_775_0 % 69.23/10.04 | | | | | | | (149) ! [v0: int] : ! [v1: int] : (v1 = all_284_2 | ~ % 69.23/10.04 | | | | | | | ($lesseq(v0, all_174_4)) | ~ % 69.23/10.04 | | | | | | | (vnum($difference(all_174_4, v0)) = v1) | ? [v2: any] % 69.23/10.04 | | | | | | | : ( ~ (v2 = all_775_0) & vnum(v0) = v2 & value(v2))) % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | GROUND_INST: instantiating (149) with all_174_8, all_243_0, % 69.23/10.04 | | | | | | | simplifying with (93) gives: % 69.23/10.04 | | | | | | | (150) all_284_2 = all_243_0 | ~ ($lesseq(all_174_8, % 69.23/10.04 | | | | | | | all_174_4)) | ? [v0: any] : ( ~ (v0 = all_775_0) & % 69.23/10.04 | | | | | | | vnum(all_174_8) = v0 & value(v0)) % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | BETA: splitting (150) gives: % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | | Case 1: % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | | (151) $lesseq(1, $difference(all_174_8, all_174_4)) % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | | COMBINE_INEQS: (42), (151) imply: % 69.23/10.04 | | | | | | | | (152) $false % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | | CLOSE: (152) is inconsistent. % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | Case 2: % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | | (153) all_284_2 = all_243_0 | ? [v0: any] : ( ~ (v0 = % 69.23/10.04 | | | | | | | | all_775_0) & vnum(all_174_8) = v0 & value(v0)) % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | | BETA: splitting (153) gives: % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | | Case 1: % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | (154) all_284_2 = all_243_0 % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | REDUCE: (139), (154) imply: % 69.23/10.04 | | | | | | | | | (155) $false % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | CLOSE: (155) is inconsistent. % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | Case 2: % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | (156) ? [v0: any] : ( ~ (v0 = all_775_0) & vnum(all_174_8) % 69.23/10.04 | | | | | | | | | = v0 & value(v0)) % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | DELTA: instantiating (156) with fresh symbol all_881_0 gives: % 69.23/10.04 | | | | | | | | | (157) ~ (all_881_0 = all_775_0) & vnum(all_174_8) = % 69.23/10.04 | | | | | | | | | all_881_0 & value(all_881_0) % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | ALPHA: (157) implies: % 69.23/10.04 | | | | | | | | | (158) ~ (all_881_0 = all_775_0) % 69.23/10.04 | | | | | | | | | (159) vnum(all_174_8) = all_881_0 % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | GROUND_INST: instantiating (17) with all_238_0, all_881_0, % 69.23/10.04 | | | | | | | | | all_174_8, simplifying with (87), (159) gives: % 69.23/10.04 | | | | | | | | | (160) all_881_0 = all_238_0 % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | GROUND_INST: instantiating (18) with all_238_0, all_775_0, % 69.23/10.04 | | | | | | | | | all_174_7, simplifying with (88), (148) gives: % 69.23/10.04 | | | | | | | | | (161) all_775_0 = all_238_0 % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | REDUCE: (158), (160), (161) imply: % 69.23/10.04 | | | | | | | | | (162) $false % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | | CLOSE: (162) is inconsistent. % 69.23/10.04 | | | | | | | | | % 69.23/10.04 | | | | | | | | End of split % 69.23/10.04 | | | | | | | | % 69.23/10.04 | | | | | | | End of split % 69.23/10.04 | | | | | | | % 69.23/10.04 | | | | | | End of split % 69.23/10.04 | | | | | | % 69.23/10.04 | | | | | End of split % 69.23/10.04 | | | | | % 69.23/10.04 | | | | End of split % 69.23/10.04 | | | | % 69.23/10.04 | | | End of split % 69.23/10.04 | | | % 69.23/10.04 | | End of split % 69.23/10.04 | | % 69.23/10.04 | End of split % 69.23/10.04 | % 69.23/10.04 End of proof % 69.23/10.04 % SZS output end Proof for theBenchmark % 69.23/10.04 % 69.23/10.04 9444ms %------------------------------------------------------------------------------