%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM288_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n031.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 06:21:42 PM UTC 2026 % Result : Theorem 29.94s 4.60s % Output : Proof 40.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : COM288_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.17/0.35 % Computer : n031.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Mon May 4 20:23:08 EDT 2026 % 0.17/0.35 % CPUTime : % 0.48/0.62 ________ _____ % 0.48/0.62 ___ __ \_________(_)________________________________ % 0.48/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.48/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.48/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.48/0.62 % 0.48/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.48/0.62 (2023-06-19) % 0.48/0.62 % 0.48/0.62 (c) Philipp Rümmer, 2009-2023 % 0.48/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.48/0.62 Amanda Stjerna. % 0.48/0.62 Free software under BSD-3-Clause. % 0.48/0.62 % 0.48/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.48/0.62 % 0.48/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.66/0.63 Running up to 7 provers in parallel. % 0.66/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.66/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.66/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.66/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.66/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.66/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.66/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.06/1.96 Prover 1: Preprocessing ... % 9.06/1.97 Prover 4: Preprocessing ... % 9.06/2.00 Prover 0: Preprocessing ... % 9.06/2.00 Prover 5: Preprocessing ... % 9.06/2.00 Prover 3: Preprocessing ... % 9.06/2.00 Prover 6: Preprocessing ... % 9.06/2.00 Prover 2: Preprocessing ... % 23.01/3.75 Prover 1: Warning: ignoring some quantifiers % 23.78/3.83 Prover 4: Warning: ignoring some quantifiers % 23.78/3.89 Prover 3: Warning: ignoring some quantifiers % 24.57/3.90 Prover 1: Constructing countermodel ... % 24.57/3.93 Prover 3: Constructing countermodel ... % 24.57/3.95 Prover 4: Constructing countermodel ... % 24.57/3.98 Prover 6: Proving ... % 24.57/4.00 Prover 5: Proving ... % 25.39/4.01 Prover 0: Proving ... % 27.60/4.33 Prover 2: Proving ... % 29.94/4.60 Prover 3: proved (3956ms) % 29.94/4.60 % 29.94/4.60 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 29.94/4.60 % 29.94/4.61 Prover 6: stopped % 29.94/4.61 Prover 0: stopped % 29.94/4.62 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.94/4.62 Prover 5: stopped % 29.94/4.62 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 29.94/4.62 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.94/4.63 Prover 2: stopped % 29.94/4.63 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 29.94/4.63 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 35.30/5.37 Prover 1: Found proof (size 204) % 35.30/5.37 Prover 1: proved (4731ms) % 35.30/5.37 Prover 4: stopped % 36.09/5.43 Prover 7: Preprocessing ... % 36.09/5.46 Prover 8: Preprocessing ... % 36.09/5.48 Prover 10: Preprocessing ... % 36.09/5.49 Prover 13: Preprocessing ... % 36.09/5.49 Prover 11: Preprocessing ... % 37.63/5.60 Prover 7: stopped % 37.63/5.62 Prover 10: stopped % 37.63/5.64 Prover 11: stopped % 38.22/5.70 Prover 13: stopped % 38.63/5.88 Prover 8: Warning: ignoring some quantifiers % 39.06/5.92 Prover 8: Constructing countermodel ... % 39.06/5.93 Prover 8: stopped % 39.06/5.93 % 39.06/5.93 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.06/5.93 % 39.06/6.01 % SZS output start Proof for theBenchmark % 39.59/6.03 Assumptions after simplification: % 39.59/6.03 --------------------------------- % 39.59/6.03 % 39.59/6.03 (EQ-someQuery) % 39.59/6.06 ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vOptQuery] : (v1 = v0 | ~ % 39.59/6.06 (vsomeQuery(v1) = v2) | ~ (vsomeQuery(v0) = v2) | ~ vQuery(v1) | ~ % 39.59/6.06 vQuery(v0)) % 39.59/6.06 % 39.59/6.06 (EQ-table) % 39.59/6.06 ! [v0: vAttrL] : ! [v1: vRawTable] : ! [v2: vAttrL] : ! [v3: vRawTable] : % 39.59/6.06 ! [v4: vTable] : ( ~ (vtable(v2, v3) = v4) | ~ (vtable(v0, v1) = v4) | ~ % 39.59/6.06 vRawTable(v3) | ~ vRawTable(v1) | ~ vAttrL(v2) | ~ vAttrL(v0) | (v3 = v1 % 39.59/6.06 & v2 = v0)) % 39.59/6.06 % 39.59/6.06 (EQ-tvalue) % 39.59/6.06 ! [v0: vTable] : ! [v1: vTable] : ! [v2: vQuery] : (v1 = v0 | ~ % 39.59/6.06 (vtvalue(v1) = v2) | ~ (vtvalue(v0) = v2) | ~ vTable(v1) | ~ vTable(v0)) % 39.59/6.06 % 39.59/6.06 (Preservation-Difference-tvalue-tvalue) % 39.59/6.06 vQuery(vq2) & vQuery(vq1) & ? [v0: vQuery] : (vDifference(vq1, vq2) = v0 & % 39.59/6.06 vQuery(v0) & ? [v1: vQuery] : ? [v2: vTable] : ? [v3: vTTContext] : ? % 39.59/6.07 [v4: vTable] : ? [v5: vTStore] : ? [v6: vTType] : ? [v7: vOptQuery] : ? % 39.59/6.07 [v8: int] : ( ~ (v8 = 0) & vptcheck(v3, v1, v6) = v8 & vptcheck(v3, v0, v6) % 39.59/6.07 = 0 & vstoreContextConsistent(v5, v3) = 0 & vreduce(v0, v5) = v7 & % 39.59/6.07 vsomeQuery(v1) = v7 & vtvalue(v4) = vq2 & vtvalue(v2) = vq1 & % 39.59/6.07 vOptQuery(v7) & vTType(v6) & vTable(v4) & vTable(v2) & vTStore(v5) & % 39.59/6.07 vQuery(v1) & vTTContext(v3))) % 39.59/6.07 % 39.59/6.07 (TDifference_inv1) % 39.59/6.07 ! [v0: vTTContext] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vTType] : ! % 39.59/6.07 [v4: vQuery] : ( ~ (vptcheck(v0, v4, v3) = 0) | ~ (vDifference(v1, v2) = v4) % 39.59/6.07 | ~ vTType(v3) | ~ vQuery(v2) | ~ vQuery(v1) | ~ vTTContext(v0) | % 39.59/6.07 vptcheck(v0, v1, v3) = 0) % 39.59/6.07 % 39.59/6.07 (TDifference_inv2) % 39.59/6.07 ! [v0: vTTContext] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vTType] : ! % 39.59/6.07 [v4: vQuery] : ( ~ (vptcheck(v0, v4, v3) = 0) | ~ (vDifference(v1, v2) = v4) % 39.59/6.07 | ~ vTType(v3) | ~ vQuery(v2) | ~ vQuery(v1) | ~ vTTContext(v0) | % 39.59/6.07 vptcheck(v0, v2, v3) = 0) % 39.59/6.07 % 39.59/6.07 (Ttvalue) % 39.59/6.07 ! [v0: vTType] : ! [v1: vTable] : ! [v2: vTTContext] : ! [v3: vQuery] : ! % 39.59/6.07 [v4: int] : (v4 = 0 | ~ (vptcheck(v2, v3, v0) = v4) | ~ (vtvalue(v1) = v3) | % 39.59/6.07 ~ vTType(v0) | ~ vTable(v1) | ~ vTTContext(v2) | ? [v5: int] : ( ~ (v5 = % 39.59/6.07 0) & vwelltypedtable(v0, v1) = v5)) % 39.59/6.07 % 39.59/6.07 (Ttvalue_inv) % 39.59/6.07 ! [v0: vTTContext] : ! [v1: vTable] : ! [v2: vTType] : ! [v3: vQuery] : ( % 39.59/6.07 ~ (vptcheck(v0, v3, v2) = 0) | ~ (vtvalue(v1) = v3) | ~ vTType(v2) | ~ % 39.59/6.07 vTable(v1) | ~ vTTContext(v0) | vwelltypedtable(v2, v1) = 0) % 39.59/6.07 % 39.59/6.07 (getAttrL-0) % 39.59/6.07 ! [v0: vAttrL] : ! [v1: vRawTable] : ! [v2: vTable] : ( ~ (vtable(v0, v1) = % 39.59/6.07 v2) | ~ vRawTable(v1) | ~ vAttrL(v0) | vgetAttrL(v2) = v0) % 39.59/6.07 % 39.59/6.07 (getAttrL-INV) % 39.59/6.07 ! [v0: vTable] : ! [v1: vAttrL] : ( ~ (vgetAttrL(v0) = v1) | ~ vTable(v0) | % 39.59/6.07 ? [v2: vRawTable] : (vtable(v1, v2) = v0 & vRawTable(v2) & vAttrL(v1))) % 39.59/6.07 % 39.59/6.07 (getRaw-0) % 39.59/6.07 ! [v0: vAttrL] : ! [v1: vRawTable] : ! [v2: vTable] : ( ~ (vtable(v0, v1) = % 39.59/6.07 v2) | ~ vRawTable(v1) | ~ vAttrL(v0) | vgetRaw(v2) = v1) % 39.59/6.07 % 39.59/6.07 (getRaw-INV) % 39.59/6.07 ! [v0: vTable] : ! [v1: vRawTable] : ( ~ (vgetRaw(v0) = v1) | ~ vTable(v0) % 39.59/6.07 | ? [v2: vAttrL] : (vtable(v2, v1) = v0 & vRawTable(v1) & vAttrL(v2))) % 39.59/6.07 % 39.59/6.07 (isValue-0) % 39.59/6.07 ! [v0: vTable] : ! [v1: vQuery] : ( ~ (vtvalue(v0) = v1) | ~ vTable(v0) | % 39.59/6.07 visValue(v1) = 0) % 39.59/6.07 % 39.59/6.07 (isValue-true-INV) % 39.59/6.07 ! [v0: vQuery] : ( ~ (visValue(v0) = 0) | ~ vQuery(v0) | ? [v1: vTable] : % 39.59/6.07 (vtvalue(v1) = v0 & vTable(v1))) % 39.59/6.07 % 39.59/6.07 (rawDifferencePreservesWellTypedRaw) % 39.59/6.08 ! [v0: vTType] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 39.59/6.08 : ! [v4: int] : (v4 = 0 | ~ (vrawDifference(v1, v2) = v3) | ~ % 39.59/6.08 (vwelltypedRawtable(v0, v3) = v4) | ~ vTType(v0) | ~ vRawTable(v2) | ~ % 39.59/6.08 vRawTable(v1) | ? [v5: any] : ? [v6: any] : (vwelltypedRawtable(v0, v2) = % 39.59/6.08 v6 & vwelltypedRawtable(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0)))) % 39.59/6.08 % 39.59/6.08 (reduce-14) % 39.59/6.08 ! [v0: vTable] : ! [v1: vTable] : ! [v2: vTStore] : ! [v3: vQuery] : ! % 39.59/6.08 [v4: vQuery] : ! [v5: vQuery] : ! [v6: vOptQuery] : ( ~ (vreduce(v5, v2) = % 39.59/6.08 v6) | ~ (vDifference(v3, v4) = v5) | ~ (vtvalue(v1) = v4) | ~ % 39.59/6.08 (vtvalue(v0) = v3) | ~ vTable(v1) | ~ vTable(v0) | ~ vTStore(v2) | ? % 39.59/6.08 [v7: vAttrL] : ? [v8: vRawTable] : ? [v9: vRawTable] : ? [v10: vRawTable] % 39.59/6.08 : ? [v11: vTable] : ? [v12: vQuery] : (vrawDifference(v8, v9) = v10 & % 39.59/6.08 vgetAttrL(v0) = v7 & vgetRaw(v1) = v9 & vgetRaw(v0) = v8 & vtable(v7, v10) % 39.59/6.08 = v11 & vsomeQuery(v12) = v6 & vtvalue(v11) = v12 & vOptQuery(v6) & % 39.59/6.08 vTable(v11) & vQuery(v12) & vRawTable(v10) & vRawTable(v9) & vRawTable(v8) % 39.59/6.08 & vAttrL(v7))) % 39.59/6.08 % 39.59/6.08 (welltypedtable-0) % 39.59/6.08 ! [v0: vTType] : ! [v1: vAttrL] : ! [v2: vRawTable] : ! [v3: vTable] : ! % 39.59/6.08 [v4: int] : (v4 = 0 | ~ (vwelltypedtable(v0, v3) = v4) | ~ (vtable(v1, v2) = % 39.59/6.08 v3) | ~ vTType(v0) | ~ vRawTable(v2) | ~ vAttrL(v1) | ? [v5: any] : ? % 39.59/6.08 [v6: any] : (vwelltypedRawtable(v0, v2) = v6 & vmatchingAttrL(v0, v1) = v5 & % 39.59/6.08 ( ~ (v6 = 0) | ~ (v5 = 0)))) & ! [v0: vTType] : ! [v1: vAttrL] : ! % 39.59/6.08 [v2: vRawTable] : ! [v3: vTable] : ( ~ (vwelltypedtable(v0, v3) = 0) | ~ % 39.59/6.08 (vtable(v1, v2) = v3) | ~ vTType(v0) | ~ vRawTable(v2) | ~ vAttrL(v1) | % 39.59/6.08 (vwelltypedRawtable(v0, v2) = 0 & vmatchingAttrL(v0, v1) = 0)) % 39.59/6.08 % 39.59/6.08 (welltypedtable-true-INV) % 39.59/6.08 ! [v0: vTType] : ! [v1: vTable] : ( ~ (vwelltypedtable(v0, v1) = 0) | ~ % 39.59/6.08 vTType(v0) | ~ vTable(v1) | ? [v2: vAttrL] : ? [v3: vRawTable] : % 39.59/6.08 (vwelltypedRawtable(v0, v3) = 0 & vmatchingAttrL(v0, v2) = 0 & vtable(v2, % 39.59/6.08 v3) = v1 & vRawTable(v3) & vAttrL(v2))) % 39.59/6.08 % 39.59/6.08 (function-axioms) % 39.59/6.10 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTType] : ! % 39.59/6.10 [v3: vQuery] : ! [v4: vTTContext] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) % 39.59/6.10 | ~ (vptcheck(v4, v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] % 39.59/6.10 : ! [v2: vPred] : ! [v3: vAttrL] : ! [v4: vRawTable] : (v1 = v0 | ~ % 39.59/6.10 (vfilterRows(v4, v3, v2) = v1) | ~ (vfilterRows(v4, v3, v2) = v0)) & ! % 39.59/6.10 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! [v3: % 39.59/6.10 vAttrL] : ! [v4: vPred] : (v1 = v0 | ~ (vfilterSingleRow(v4, v3, v2) = v1) % 39.59/6.10 | ~ (vfilterSingleRow(v4, v3, v2) = v0)) & ! [v0: vOptVal] : ! [v1: % 39.59/6.10 vOptVal] : ! [v2: vRow] : ! [v3: vAttrL] : ! [v4: vExp] : (v1 = v0 | ~ % 39.59/6.10 (vevalExpRow(v4, v3, v2) = v1) | ~ (vevalExpRow(v4, v3, v2) = v0)) & ! % 39.59/6.10 [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! [v2: vRawTable] : ! [v3: % 39.59/6.10 vAttrL] : ! [v4: vAttrL] : (v1 = v0 | ~ (vprojectCols(v4, v3, v2) = v1) | % 39.59/6.10 ~ (vprojectCols(v4, v3, v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: % 39.59/6.10 vOptRawTable] : ! [v2: vRawTable] : ! [v3: vAttrL] : ! [v4: vName] : (v1 % 39.59/6.10 = v0 | ~ (vfindCol(v4, v3, v2) = v1) | ~ (vfindCol(v4, v3, v2) = v0)) & ! % 39.59/6.10 [v0: vTStore] : ! [v1: vTStore] : ! [v2: vTStore] : ! [v3: vTable] : ! % 39.59/6.10 [v4: vName] : (v1 = v0 | ~ (vbindStore(v4, v3, v2) = v1) | ~ (vbindStore(v4, % 39.59/6.10 v3, v2) = v0)) & ! [v0: vTTContext] : ! [v1: vTTContext] : ! [v2: % 39.59/6.10 vTTContext] : ! [v3: vTType] : ! [v4: vName] : (v1 = v0 | ~ % 39.59/6.10 (vbindContext(v4, v3, v2) = v1) | ~ (vbindContext(v4, v3, v2) = v0)) & ! % 39.59/6.10 [v0: vTType] : ! [v1: vTType] : ! [v2: vTType] : ! [v3: vFType] : ! [v4: % 39.59/6.10 vName] : (v1 = v0 | ~ (vttcons(v4, v3, v2) = v1) | ~ (vttcons(v4, v3, v2) % 39.59/6.10 = v0)) & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vPred] : ! [v3: % 39.59/6.10 vName] : ! [v4: vSelect] : (v1 = v0 | ~ (vselectFromWhere(v4, v3, v2) = % 39.59/6.10 v1) | ~ (vselectFromWhere(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 39.59/6.10 : ! [v1: MultipleValueBool] : ! [v2: vTTContext] : ! [v3: vTStore] : (v1 = % 39.59/6.10 v0 | ~ (vstoreContextConsistent(v3, v2) = v1) | ~ % 39.59/6.10 (vstoreContextConsistent(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 39.59/6.10 [v1: MultipleValueBool] : ! [v2: vTType] : ! [v3: vPred] : (v1 = v0 | ~ % 39.59/6.10 (vtcheckPred(v3, v2) = v1) | ~ (vtcheckPred(v3, v2) = v0)) & ! [v0: % 39.59/6.10 vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: vExp] : (v1 = v0 % 39.59/6.10 | ~ (vtypeOfExp(v3, v2) = v1) | ~ (vtypeOfExp(v3, v2) = v0)) & ! [v0: % 39.59/6.10 vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vSelect] : (v1 = % 39.59/6.10 v0 | ~ (vprojectType(v3, v2) = v1) | ~ (vprojectType(v3, v2) = v0)) & ! % 39.59/6.10 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vAttrL] : (v1 % 39.59/6.10 = v0 | ~ (vprojectTypeAttrL(v3, v2) = v1) | ~ (vprojectTypeAttrL(v3, v2) = % 39.59/6.10 v0)) & ! [v0: vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: % 39.59/6.10 vName] : (v1 = v0 | ~ (vfindColType(v3, v2) = v1) | ~ (vfindColType(v3, % 39.59/6.10 v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: vTStore] % 39.59/6.10 : ! [v3: vQuery] : (v1 = v0 | ~ (vreduce(v3, v2) = v1) | ~ (vreduce(v3, v2) % 39.59/6.10 = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: vPred] : ! [v3: % 39.59/6.10 vTable] : (v1 = v0 | ~ (vfilterTable(v3, v2) = v1) | ~ (vfilterTable(v3, % 39.59/6.10 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 39.59/6.10 ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ (vlessThan(v3, v2) = v1) | ~ % 39.59/6.10 (vlessThan(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 39.59/6.10 MultipleValueBool] : ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ % 39.59/6.10 (vgreaterThan(v3, v2) = v1) | ~ (vgreaterThan(v3, v2) = v0)) & ! [v0: % 39.59/6.10 vOptTable] : ! [v1: vOptTable] : ! [v2: vTable] : ! [v3: vSelect] : (v1 = % 39.59/6.10 v0 | ~ (vprojectTable(v3, v2) = v1) | ~ (vprojectTable(v3, v2) = v0)) & ! % 39.59/6.10 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTTContext] : ! [v3: vName] : % 39.59/6.10 (v1 = v0 | ~ (vlookupContext(v3, v2) = v1) | ~ (vlookupContext(v3, v2) = % 39.59/6.10 v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! [v2: vTStore] : ! % 39.59/6.10 [v3: vName] : (v1 = v0 | ~ (vlookupStore(v3, v2) = v1) | ~ (vlookupStore(v3, % 39.59/6.10 v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 39.59/6.10 vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ (vrawDifference(v3, v2) = % 39.59/6.10 v1) | ~ (vrawDifference(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: % 39.59/6.10 vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 39.59/6.10 (vrawIntersection(v3, v2) = v1) | ~ (vrawIntersection(v3, v2) = v0)) & ! % 39.59/6.10 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 39.59/6.10 : (v1 = v0 | ~ (vrawUnion(v3, v2) = v1) | ~ (vrawUnion(v3, v2) = v0)) & ! % 39.59/6.10 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 39.59/6.10 : (v1 = v0 | ~ (vattachColToFrontRaw(v3, v2) = v1) | ~ % 39.59/6.10 (vattachColToFrontRaw(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 39.59/6.10 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 39.59/6.10 (vsameLength(v3, v2) = v1) | ~ (vsameLength(v3, v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRawTable] : ! % 39.59/6.10 [v3: vRow] : (v1 = v0 | ~ (vrowIn(v3, v2) = v1) | ~ (vrowIn(v3, v2) = v0)) & % 39.59/6.10 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTable] : ! % 39.59/6.10 [v3: vTType] : (v1 = v0 | ~ (vwelltypedtable(v3, v2) = v1) | ~ % 39.59/6.10 (vwelltypedtable(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 39.59/6.10 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ % 39.59/6.10 (vwelltypedRawtable(v3, v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) & % 39.59/6.10 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! % 39.59/6.10 [v3: vTType] : (v1 = v0 | ~ (vwelltypedRow(v3, v2) = v1) | ~ % 39.59/6.10 (vwelltypedRow(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 39.59/6.10 MultipleValueBool] : ! [v2: vAttrL] : ! [v3: vTType] : (v1 = v0 | ~ % 39.59/6.10 (vmatchingAttrL(v3, v2) = v1) | ~ (vmatchingAttrL(v3, v2) = v0)) & ! [v0: % 39.59/6.10 vAttrL] : ! [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vAttrL] : (v1 = v0 | % 39.59/6.10 ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vAttrL] : ! % 39.59/6.10 [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vName] : (v1 = v0 | ~ (vacons(v3, % 39.59/6.10 v2) = v1) | ~ (vacons(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] % 39.59/6.10 : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 39.59/6.10 (vlt(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! % 39.59/6.10 [v3: vExp] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! % 39.59/6.10 [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ % 39.59/6.10 (veq(v3, v2) = v1) | ~ (veq(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: % 39.59/6.10 vPred] : ! [v2: vPred] : ! [v3: vPred] : (v1 = v0 | ~ (vand(v3, v2) = v1) % 39.59/6.10 | ~ (vand(v3, v2) = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: % 39.59/6.10 vRawTable] : ! [v3: vAttrL] : (v1 = v0 | ~ (vtable(v3, v2) = v1) | ~ % 39.59/6.10 (vtable(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 39.59/6.10 vRawTable] : ! [v3: vRow] : (v1 = v0 | ~ (vtcons(v3, v2) = v1) | ~ % 39.59/6.10 (vtcons(v3, v2) = v0)) & ! [v0: vRow] : ! [v1: vRow] : ! [v2: vRow] : ! % 39.59/6.10 [v3: vVal] : (v1 = v0 | ~ (vrcons(v3, v2) = v1) | ~ (vrcons(v3, v2) = v0)) & % 39.59/6.10 ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = % 39.59/6.10 v0 | ~ (vDifference(v3, v2) = v1) | ~ (vDifference(v3, v2) = v0)) & ! % 39.59/6.10 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 39.59/6.10 | ~ (vIntersection(v3, v2) = v1) | ~ (vIntersection(v3, v2) = v0)) & ! % 39.59/6.10 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 39.59/6.10 | ~ (vUnion(v3, v2) = v1) | ~ (vUnion(v3, v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptFType] : (v1 = % 39.59/6.10 v0 | ~ (visSomeFType(v2) = v1) | ~ (visSomeFType(v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptVal] : (v1 = % 39.59/6.10 v0 | ~ (visSomeVal(v2) = v1) | ~ (visSomeVal(v2) = v0)) & ! [v0: % 39.59/6.10 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 39.59/6.10 (vprojectEmptyCol(v2) = v1) | ~ (vprojectEmptyCol(v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQuery] : (v1 = % 39.59/6.10 v0 | ~ (visSomeQuery(v2) = v1) | ~ (visSomeQuery(v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuery] : (v1 = v0 % 39.59/6.10 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTType] : (v1 = % 39.59/6.10 v0 | ~ (visSomeTType(v2) = v1) | ~ (visSomeTType(v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTable] : (v1 = % 39.59/6.10 v0 | ~ (visSomeTable(v2) = v1) | ~ (visSomeTable(v2) = v0)) & ! [v0: % 39.59/6.10 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptRawTable] : % 39.59/6.10 (v1 = v0 | ~ (visSomeRawTable(v2) = v1) | ~ (visSomeRawTable(v2) = v0)) & ! % 39.59/6.10 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 39.59/6.10 (vdropFirstColRaw(v2) = v1) | ~ (vdropFirstColRaw(v2) = v0)) & ! [v0: % 39.59/6.10 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 39.59/6.10 (vprojectFirstRaw(v2) = v1) | ~ (vprojectFirstRaw(v2) = v0)) & ! [v0: % 39.59/6.10 vFType] : ! [v1: vFType] : ! [v2: vVal] : (v1 = v0 | ~ (vfieldType(v2) = % 39.59/6.10 v1) | ~ (vfieldType(v2) = v0)) & ! [v0: vAttrL] : ! [v1: vAttrL] : ! % 39.59/6.10 [v2: vTable] : (v1 = v0 | ~ (vgetAttrL(v2) = v1) | ~ (vgetAttrL(v2) = v0)) & % 39.59/6.10 ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vTable] : (v1 = v0 | ~ % 39.59/6.10 (vgetRaw(v2) = v1) | ~ (vgetRaw(v2) = v0)) & ! [v0: vFType] : ! [v1: % 39.59/6.10 vFType] : ! [v2: vOptFType] : (v1 = v0 | ~ (vgetFType(v2) = v1) | ~ % 39.59/6.10 (vgetFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vOptVal] : % 39.59/6.10 (v1 = v0 | ~ (vgetVal(v2) = v1) | ~ (vgetVal(v2) = v0)) & ! [v0: vQuery] : % 39.59/6.10 ! [v1: vQuery] : ! [v2: vOptQuery] : (v1 = v0 | ~ (vgetQuery(v2) = v1) | ~ % 39.59/6.10 (vgetQuery(v2) = v0)) & ! [v0: vTType] : ! [v1: vTType] : ! [v2: % 39.59/6.10 vOptTType] : (v1 = v0 | ~ (vgetTType(v2) = v1) | ~ (vgetTType(v2) = v0)) & % 39.59/6.10 ! [v0: vTable] : ! [v1: vTable] : ! [v2: vOptTable] : (v1 = v0 | ~ % 39.59/6.10 (vgetTable(v2) = v1) | ~ (vgetTable(v2) = v0)) & ! [v0: vRawTable] : ! % 39.59/6.10 [v1: vRawTable] : ! [v2: vOptRawTable] : (v1 = v0 | ~ (vgetRawTable(v2) = % 39.59/6.10 v1) | ~ (vgetRawTable(v2) = v0)) & ! [v0: vOptFType] : ! [v1: % 39.59/6.10 vOptFType] : ! [v2: vFType] : (v1 = v0 | ~ (vsomeFType(v2) = v1) | ~ % 39.59/6.10 (vsomeFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vVal] : (v1 % 39.59/6.10 = v0 | ~ (venumVal(v2) = v1) | ~ (venumVal(v2) = v0)) & ! [v0: vPred] : % 39.59/6.10 ! [v1: vPred] : ! [v2: vPred] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) % 39.59/6.10 = v0)) & ! [v0: vOptVal] : ! [v1: vOptVal] : ! [v2: vVal] : (v1 = v0 | % 39.59/6.10 ~ (vsomeVal(v2) = v1) | ~ (vsomeVal(v2) = v0)) & ! [v0: vExp] : ! [v1: % 39.59/6.10 vExp] : ! [v2: vName] : (v1 = v0 | ~ (vlookup(v2) = v1) | ~ (vlookup(v2) % 39.59/6.10 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vVal] : (v1 = v0 | ~ % 39.59/6.10 (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & ! [v0: vName] : ! [v1: % 39.59/6.11 vName] : ! [v2: vName] : (v1 = v0 | ~ (venumName(v2) = v1) | ~ % 39.59/6.11 (venumName(v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: % 39.59/6.11 vQuery] : (v1 = v0 | ~ (vsomeQuery(v2) = v1) | ~ (vsomeQuery(v2) = v0)) & % 39.59/6.11 ! [v0: vFType] : ! [v1: vFType] : ! [v2: vFType] : (v1 = v0 | ~ % 39.59/6.11 (venumFType(v2) = v1) | ~ (venumFType(v2) = v0)) & ! [v0: vOptTType] : ! % 39.59/6.11 [v1: vOptTType] : ! [v2: vTType] : (v1 = v0 | ~ (vsomeTType(v2) = v1) | ~ % 39.59/6.11 (vsomeTType(v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! % 39.59/6.11 [v2: vRawTable] : (v1 = v0 | ~ (vsomeRawTable(v2) = v1) | ~ % 39.59/6.11 (vsomeRawTable(v2) = v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! % 39.59/6.11 [v2: vTable] : (v1 = v0 | ~ (vsomeTable(v2) = v1) | ~ (vsomeTable(v2) = v0)) % 39.59/6.11 & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vTable] : (v1 = v0 | ~ % 39.59/6.11 (vtvalue(v2) = v1) | ~ (vtvalue(v2) = v0)) & ! [v0: vSelect] : ! [v1: % 39.59/6.11 vSelect] : ! [v2: vAttrL] : (v1 = v0 | ~ (vlist(v2) = v1) | ~ (vlist(v2) % 39.59/6.11 = v0)) % 39.59/6.11 % 39.59/6.11 Further assumptions not needed in the proof: % 39.59/6.11 -------------------------------------------- % 39.59/6.11 DIFF-Intersection-Difference, DIFF-Union-Difference, DIFF-Union-Intersection, % 39.59/6.11 DIFF-aempty-acons, DIFF-all-list, DIFF-and-eq, DIFF-and-gt, DIFF-and-lt, % 39.59/6.11 DIFF-and-not, DIFF-constant-lookup, DIFF-emptyContext-bindContext, % 39.59/6.11 DIFF-emptyStore-bindStore, DIFF-eq-gt, DIFF-eq-lt, DIFF-gt-lt, % 39.59/6.11 DIFF-initFType-enumFType, DIFF-initName-enumName, DIFF-initVal-enumVal, % 39.59/6.11 DIFF-noFType-someFType, DIFF-noQuery-someQuery, DIFF-noRawTable-someRawTable, % 39.59/6.11 DIFF-noTType-someTType, DIFF-noTable-someTable, DIFF-noVal-someVal, DIFF-not-eq, % 39.59/6.11 DIFF-not-gt, DIFF-not-lt, DIFF-ptrue-and, DIFF-ptrue-eq, DIFF-ptrue-gt, % 39.59/6.11 DIFF-ptrue-lt, DIFF-ptrue-not, DIFF-rempty-rcons, % 39.59/6.11 DIFF-selectFromWhere-Difference, DIFF-selectFromWhere-Intersection, % 39.59/6.11 DIFF-selectFromWhere-Union, DIFF-tempty-tcons, DIFF-ttempty-ttcons, % 39.59/6.11 DIFF-tvalue-Difference, DIFF-tvalue-Intersection, DIFF-tvalue-Union, % 39.59/6.11 DIFF-tvalue-selectFromWhere, EQ-Difference, EQ-Intersection, EQ-Union, EQ-acons, % 39.59/6.11 EQ-and, EQ-bindContext, EQ-bindStore, EQ-constant, EQ-enumFType, EQ-enumName, % 39.59/6.11 EQ-enumVal, EQ-eq, EQ-gt, EQ-list, EQ-lookup, EQ-lt, EQ-not, EQ-rcons, % 39.59/6.11 EQ-selectFromWhere, EQ-someFType, EQ-someRawTable, EQ-someTType, EQ-someTable, % 39.59/6.11 EQ-someVal, EQ-tcons, EQ-ttcons, Preservation-Difference-IH0, % 39.59/6.11 Preservation-Difference-IH1, TDifference, TIntersection, TIntersection_inv1, % 39.59/6.11 TIntersection_inv2, TSelectFromWhere, TSelectFromWhere_inv, TTTContextDuplicate, % 39.59/6.11 TTTContextSwap, TUnion, TUnion_inv1, TUnion_inv2, append-0, append-1, % 39.59/6.11 append-INV, attachColToFrontRaw-0, attachColToFrontRaw-1, attachColToFrontRaw-2, % 39.59/6.11 attachColToFrontRaw-INV, dom-AttrL, dom-Exp, dom-OptFType, dom-OptQuery, % 39.59/6.11 dom-OptRawTable, dom-OptTType, dom-OptTable, dom-OptVal, dom-Pred, dom-Query, % 39.59/6.11 dom-RawTable, dom-Row, dom-Select, dom-TStore, dom-TTContext, dom-TType, % 39.59/6.11 dom-Table, dropFirstColRaw-0, dropFirstColRaw-1, dropFirstColRaw-2, % 39.59/6.11 dropFirstColRaw-INV, evalExpRow-0, evalExpRow-1, evalExpRow-2, evalExpRow-3, % 39.59/6.11 evalExpRow-INV, filterRows-0, filterRows-1, filterRows-2, filterRows-INV, % 39.59/6.11 filterSingleRow-0, filterSingleRow-1, filterSingleRow-2, filterSingleRow-3, % 39.59/6.11 filterSingleRow-4, filterSingleRow-5, filterSingleRow-false-INV, % 39.59/6.11 filterSingleRow-true-INV, filterTable-0, filterTable-INV, findCol-0, findCol-1, % 39.59/6.11 findCol-2, findCol-INV, findColType-0, findColType-1, findColType-2, % 39.59/6.11 findColType-INV, getFType-0, getQuery-0, getRawTable-0, getTType-0, getTable-0, % 39.59/6.11 getVal-0, isSomeFType-0, isSomeFType-1, isSomeFType-false-INV, % 39.59/6.11 isSomeFType-true-INV, isSomeQuery-0, isSomeQuery-1, isSomeQuery-false-INV, % 39.59/6.11 isSomeQuery-true-INV, isSomeRawTable-0, isSomeRawTable-1, % 39.59/6.11 isSomeRawTable-false-INV, isSomeRawTable-true-INV, isSomeTType-0, isSomeTType-1, % 39.59/6.11 isSomeTType-false-INV, isSomeTType-true-INV, isSomeTable-0, isSomeTable-1, % 39.59/6.11 isSomeTable-false-INV, isSomeTable-true-INV, isSomeVal-0, isSomeVal-1, % 39.59/6.11 isSomeVal-false-INV, isSomeVal-true-INV, isValue-1, isValue-2, isValue-3, % 39.59/6.11 isValue-4, isValue-false-INV, lookupContext-0, lookupContext-1, lookupContext-2, % 39.59/6.11 lookupContext-INV, lookupStore-0, lookupStore-1, lookupStore-2, lookupStore-INV, % 39.59/6.11 matchingAttrL-0, matchingAttrL-1, matchingAttrL-2, matchingAttrL-false-INV, % 39.59/6.11 matchingAttrL-true-INV, projectCols-0, projectCols-1, projectCols-2, % 39.59/6.11 projectCols-INV, projectEmptyCol-0, projectEmptyCol-1, projectEmptyCol-INV, % 39.59/6.11 projectFirstRaw-0, projectFirstRaw-1, projectFirstRaw-2, projectFirstRaw-INV, % 39.59/6.11 projectTable-0, projectTable-1, projectTable-2, projectTable-INV, projectType-0, % 39.59/6.11 projectType-1, projectType-INV, projectTypeAttrL-0, projectTypeAttrL-1, % 39.59/6.11 projectTypeAttrL-2, projectTypeAttrL-INV, rawDifference-0, rawDifference-1, % 39.59/6.11 rawDifference-2, rawDifference-3, rawDifference-4, rawDifference-INV, % 39.59/6.11 rawIntersection-0, rawIntersection-1, rawIntersection-2, rawIntersection-3, % 39.59/6.11 rawIntersection-4, rawIntersection-INV, rawUnion-0, rawUnion-1, rawUnion-2, % 39.59/6.11 rawUnion-INV, reduce-0, reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, % 39.59/6.11 reduce-15, reduce-16, reduce-17, reduce-18, reduce-2, reduce-3, reduce-4, % 39.59/6.11 reduce-5, reduce-6, reduce-7, reduce-8, reduce-9, reduce-INV, rowIn-0, rowIn-1, % 39.59/6.11 rowIn-false-INV, rowIn-true-INV, sameLength-0, sameLength-1, sameLength-2, % 39.59/6.11 sameLength-false-INV, sameLength-true-INV, storeContextConsistent-0, % 39.59/6.11 storeContextConsistent-1, storeContextConsistent-2, % 39.59/6.11 storeContextConsistent-false-INV, storeContextConsistent-true-INV, tcheckPred-0, % 39.59/6.11 tcheckPred-1, tcheckPred-2, tcheckPred-3, tcheckPred-4, tcheckPred-5, % 39.59/6.11 tcheckPred-false-INV, tcheckPred-true-INV, typeOfExp-0, typeOfExp-1, % 39.59/6.11 typeOfExp-2, typeOfExp-3, typeOfExp-INV, welltypedRawtable-0, % 39.59/6.11 welltypedRawtable-1, welltypedRawtable-false-INV, welltypedRawtable-true-INV, % 39.59/6.11 welltypedRow-0, welltypedRow-1, welltypedRow-2, welltypedRow-false-INV, % 39.59/6.11 welltypedRow-true-INV, welltypedtable-false-INV % 39.59/6.11 % 39.59/6.11 Those formulas are unsatisfiable: % 39.59/6.11 --------------------------------- % 39.59/6.11 % 39.59/6.11 Begin of proof % 39.59/6.11 | % 39.59/6.11 | ALPHA: (welltypedtable-0) implies: % 39.59/6.11 | (1) ! [v0: vTType] : ! [v1: vAttrL] : ! [v2: vRawTable] : ! [v3: % 39.59/6.11 | vTable] : ( ~ (vwelltypedtable(v0, v3) = 0) | ~ (vtable(v1, v2) = % 39.59/6.11 | v3) | ~ vTType(v0) | ~ vRawTable(v2) | ~ vAttrL(v1) | % 39.59/6.11 | (vwelltypedRawtable(v0, v2) = 0 & vmatchingAttrL(v0, v1) = 0)) % 39.59/6.11 | (2) ! [v0: vTType] : ! [v1: vAttrL] : ! [v2: vRawTable] : ! [v3: % 39.59/6.11 | vTable] : ! [v4: int] : (v4 = 0 | ~ (vwelltypedtable(v0, v3) = v4) % 39.59/6.11 | | ~ (vtable(v1, v2) = v3) | ~ vTType(v0) | ~ vRawTable(v2) | ~ % 39.59/6.11 | vAttrL(v1) | ? [v5: any] : ? [v6: any] : (vwelltypedRawtable(v0, % 39.59/6.11 | v2) = v6 & vmatchingAttrL(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = % 39.59/6.11 | 0)))) % 39.59/6.11 | % 39.59/6.11 | ALPHA: (Preservation-Difference-tvalue-tvalue) implies: % 39.59/6.11 | (3) vQuery(vq1) % 39.59/6.11 | (4) vQuery(vq2) % 39.59/6.11 | (5) ? [v0: vQuery] : (vDifference(vq1, vq2) = v0 & vQuery(v0) & ? [v1: % 39.59/6.11 | vQuery] : ? [v2: vTable] : ? [v3: vTTContext] : ? [v4: vTable] : % 39.59/6.11 | ? [v5: vTStore] : ? [v6: vTType] : ? [v7: vOptQuery] : ? [v8: % 39.59/6.11 | int] : ( ~ (v8 = 0) & vptcheck(v3, v1, v6) = v8 & vptcheck(v3, v0, % 39.59/6.11 | v6) = 0 & vstoreContextConsistent(v5, v3) = 0 & vreduce(v0, v5) = % 39.59/6.11 | v7 & vsomeQuery(v1) = v7 & vtvalue(v4) = vq2 & vtvalue(v2) = vq1 & % 39.59/6.11 | vOptQuery(v7) & vTType(v6) & vTable(v4) & vTable(v2) & vTStore(v5) % 39.59/6.11 | & vQuery(v1) & vTTContext(v3))) % 39.59/6.11 | % 39.59/6.11 | ALPHA: (function-axioms) implies: % 39.59/6.11 | (6) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vTable] : (v1 = v0 | % 39.59/6.11 | ~ (vgetRaw(v2) = v1) | ~ (vgetRaw(v2) = v0)) % 39.59/6.12 | (7) ! [v0: vAttrL] : ! [v1: vAttrL] : ! [v2: vTable] : (v1 = v0 | ~ % 39.59/6.12 | (vgetAttrL(v2) = v1) | ~ (vgetAttrL(v2) = v0)) % 39.59/6.12 | (8) ! [v0: vTable] : ! [v1: vTable] : ! [v2: vRawTable] : ! [v3: % 39.59/6.12 | vAttrL] : (v1 = v0 | ~ (vtable(v3, v2) = v1) | ~ (vtable(v3, v2) = % 39.59/6.12 | v0)) % 39.59/6.12 | (9) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 39.59/6.12 | vAttrL] : ! [v3: vTType] : (v1 = v0 | ~ (vmatchingAttrL(v3, v2) = % 39.59/6.12 | v1) | ~ (vmatchingAttrL(v3, v2) = v0)) % 39.59/6.12 | (10) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 39.59/6.12 | vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ (vwelltypedRawtable(v3, % 39.59/6.12 | v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) % 39.59/6.12 | (11) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: % 39.59/6.12 | vRawTable] : (v1 = v0 | ~ (vrawDifference(v3, v2) = v1) | ~ % 39.59/6.12 | (vrawDifference(v3, v2) = v0)) % 39.59/6.12 | % 39.59/6.12 | DELTA: instantiating (5) with fresh symbol all_339_0 gives: % 39.59/6.12 | (12) vDifference(vq1, vq2) = all_339_0 & vQuery(all_339_0) & ? [v0: % 39.59/6.12 | vQuery] : ? [v1: vTable] : ? [v2: vTTContext] : ? [v3: vTable] : % 39.59/6.12 | ? [v4: vTStore] : ? [v5: vTType] : ? [v6: vOptQuery] : ? [v7: int] % 39.59/6.12 | : ( ~ (v7 = 0) & vptcheck(v2, v0, v5) = v7 & vptcheck(v2, all_339_0, % 39.59/6.12 | v5) = 0 & vstoreContextConsistent(v4, v2) = 0 & vreduce(all_339_0, % 39.59/6.12 | v4) = v6 & vsomeQuery(v0) = v6 & vtvalue(v3) = vq2 & vtvalue(v1) = % 39.59/6.12 | vq1 & vOptQuery(v6) & vTType(v5) & vTable(v3) & vTable(v1) & % 39.59/6.12 | vTStore(v4) & vQuery(v0) & vTTContext(v2)) % 39.59/6.12 | % 39.59/6.12 | ALPHA: (12) implies: % 39.59/6.12 | (13) vDifference(vq1, vq2) = all_339_0 % 39.59/6.12 | (14) ? [v0: vQuery] : ? [v1: vTable] : ? [v2: vTTContext] : ? [v3: % 39.59/6.12 | vTable] : ? [v4: vTStore] : ? [v5: vTType] : ? [v6: vOptQuery] : % 39.59/6.12 | ? [v7: int] : ( ~ (v7 = 0) & vptcheck(v2, v0, v5) = v7 & vptcheck(v2, % 39.59/6.12 | all_339_0, v5) = 0 & vstoreContextConsistent(v4, v2) = 0 & % 39.59/6.12 | vreduce(all_339_0, v4) = v6 & vsomeQuery(v0) = v6 & vtvalue(v3) = % 39.59/6.12 | vq2 & vtvalue(v1) = vq1 & vOptQuery(v6) & vTType(v5) & vTable(v3) & % 39.59/6.12 | vTable(v1) & vTStore(v4) & vQuery(v0) & vTTContext(v2)) % 39.59/6.12 | % 39.59/6.12 | DELTA: instantiating (14) with fresh symbols all_347_0, all_347_1, all_347_2, % 39.59/6.12 | all_347_3, all_347_4, all_347_5, all_347_6, all_347_7 gives: % 39.59/6.12 | (15) ~ (all_347_0 = 0) & vptcheck(all_347_5, all_347_7, all_347_2) = % 39.59/6.12 | all_347_0 & vptcheck(all_347_5, all_339_0, all_347_2) = 0 & % 39.59/6.12 | vstoreContextConsistent(all_347_3, all_347_5) = 0 & vreduce(all_339_0, % 39.59/6.12 | all_347_3) = all_347_1 & vsomeQuery(all_347_7) = all_347_1 & % 39.59/6.12 | vtvalue(all_347_4) = vq2 & vtvalue(all_347_6) = vq1 & % 39.59/6.12 | vOptQuery(all_347_1) & vTType(all_347_2) & vTable(all_347_4) & % 39.59/6.12 | vTable(all_347_6) & vTStore(all_347_3) & vQuery(all_347_7) & % 39.59/6.12 | vTTContext(all_347_5) % 39.59/6.12 | % 39.59/6.12 | ALPHA: (15) implies: % 39.59/6.12 | (16) ~ (all_347_0 = 0) % 39.59/6.12 | (17) vTTContext(all_347_5) % 39.59/6.12 | (18) vQuery(all_347_7) % 39.59/6.12 | (19) vTStore(all_347_3) % 39.59/6.12 | (20) vTable(all_347_6) % 39.59/6.12 | (21) vTable(all_347_4) % 39.59/6.12 | (22) vTType(all_347_2) % 39.59/6.12 | (23) vtvalue(all_347_6) = vq1 % 39.59/6.12 | (24) vtvalue(all_347_4) = vq2 % 39.59/6.12 | (25) vsomeQuery(all_347_7) = all_347_1 % 39.59/6.12 | (26) vreduce(all_339_0, all_347_3) = all_347_1 % 39.59/6.12 | (27) vptcheck(all_347_5, all_339_0, all_347_2) = 0 % 39.59/6.12 | (28) vptcheck(all_347_5, all_347_7, all_347_2) = all_347_0 % 39.59/6.12 | % 39.59/6.12 | GROUND_INST: instantiating (isValue-0) with all_347_6, vq1, simplifying with % 39.59/6.12 | (20), (23) gives: % 39.59/6.13 | (29) visValue(vq1) = 0 % 39.59/6.13 | % 39.59/6.13 | GROUND_INST: instantiating (isValue-0) with all_347_4, vq2, simplifying with % 39.59/6.13 | (21), (24) gives: % 39.59/6.13 | (30) visValue(vq2) = 0 % 40.09/6.13 | % 40.09/6.13 | GROUND_INST: instantiating (reduce-14) with all_347_6, all_347_4, all_347_3, % 40.09/6.13 | vq1, vq2, all_339_0, all_347_1, simplifying with (13), (19), % 40.09/6.13 | (20), (21), (23), (24), (26) gives: % 40.09/6.13 | (31) ? [v0: vAttrL] : ? [v1: vRawTable] : ? [v2: vRawTable] : ? [v3: % 40.09/6.13 | vRawTable] : ? [v4: vTable] : ? [v5: vQuery] : (vrawDifference(v1, % 40.09/6.13 | v2) = v3 & vgetAttrL(all_347_6) = v0 & vgetRaw(all_347_4) = v2 & % 40.09/6.13 | vgetRaw(all_347_6) = v1 & vtable(v0, v3) = v4 & vsomeQuery(v5) = % 40.09/6.13 | all_347_1 & vtvalue(v4) = v5 & vOptQuery(all_347_1) & vTable(v4) & % 40.09/6.13 | vQuery(v5) & vRawTable(v3) & vRawTable(v2) & vRawTable(v1) & % 40.09/6.13 | vAttrL(v0)) % 40.09/6.13 | % 40.09/6.13 | GROUND_INST: instantiating (TDifference_inv2) with all_347_5, vq1, vq2, % 40.09/6.13 | all_347_2, all_339_0, simplifying with (3), (4), (13), (17), % 40.09/6.13 | (22), (27) gives: % 40.09/6.13 | (32) vptcheck(all_347_5, vq2, all_347_2) = 0 % 40.09/6.13 | % 40.09/6.13 | GROUND_INST: instantiating (TDifference_inv1) with all_347_5, vq1, vq2, % 40.09/6.13 | all_347_2, all_339_0, simplifying with (3), (4), (13), (17), % 40.09/6.13 | (22), (27) gives: % 40.09/6.13 | (33) vptcheck(all_347_5, vq1, all_347_2) = 0 % 40.09/6.13 | % 40.09/6.13 | DELTA: instantiating (31) with fresh symbols all_367_0, all_367_1, all_367_2, % 40.09/6.13 | all_367_3, all_367_4, all_367_5 gives: % 40.09/6.13 | (34) vrawDifference(all_367_4, all_367_3) = all_367_2 & % 40.09/6.13 | vgetAttrL(all_347_6) = all_367_5 & vgetRaw(all_347_4) = all_367_3 & % 40.09/6.13 | vgetRaw(all_347_6) = all_367_4 & vtable(all_367_5, all_367_2) = % 40.09/6.13 | all_367_1 & vsomeQuery(all_367_0) = all_347_1 & vtvalue(all_367_1) = % 40.09/6.13 | all_367_0 & vOptQuery(all_347_1) & vTable(all_367_1) & % 40.09/6.13 | vQuery(all_367_0) & vRawTable(all_367_2) & vRawTable(all_367_3) & % 40.09/6.13 | vRawTable(all_367_4) & vAttrL(all_367_5) % 40.09/6.13 | % 40.09/6.13 | ALPHA: (34) implies: % 40.09/6.13 | (35) vAttrL(all_367_5) % 40.09/6.13 | (36) vRawTable(all_367_2) % 40.09/6.13 | (37) vQuery(all_367_0) % 40.09/6.13 | (38) vTable(all_367_1) % 40.09/6.13 | (39) vtvalue(all_367_1) = all_367_0 % 40.09/6.13 | (40) vsomeQuery(all_367_0) = all_347_1 % 40.09/6.13 | (41) vtable(all_367_5, all_367_2) = all_367_1 % 40.09/6.13 | (42) vgetRaw(all_347_6) = all_367_4 % 40.09/6.13 | (43) vgetRaw(all_347_4) = all_367_3 % 40.09/6.13 | (44) vgetAttrL(all_347_6) = all_367_5 % 40.09/6.13 | (45) vrawDifference(all_367_4, all_367_3) = all_367_2 % 40.09/6.13 | % 40.09/6.13 | GROUND_INST: instantiating (EQ-someQuery) with all_347_7, all_367_0, % 40.09/6.13 | all_347_1, simplifying with (18), (25), (37), (40) gives: % 40.09/6.13 | (46) all_367_0 = all_347_7 % 40.09/6.13 | % 40.09/6.13 | GROUND_INST: instantiating (getAttrL-0) with all_367_5, all_367_2, all_367_1, % 40.09/6.13 | simplifying with (35), (36), (41) gives: % 40.09/6.13 | (47) vgetAttrL(all_367_1) = all_367_5 % 40.09/6.13 | % 40.09/6.13 | GROUND_INST: instantiating (getRaw-0) with all_367_5, all_367_2, all_367_1, % 40.09/6.13 | simplifying with (35), (36), (41) gives: % 40.09/6.13 | (48) vgetRaw(all_367_1) = all_367_2 % 40.09/6.13 | % 40.09/6.13 | GROUND_INST: instantiating (getRaw-INV) with all_347_6, all_367_4, simplifying % 40.09/6.13 | with (20), (42) gives: % 40.09/6.14 | (49) ? [v0: vAttrL] : (vtable(v0, all_367_4) = all_347_6 & % 40.09/6.14 | vRawTable(all_367_4) & vAttrL(v0)) % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (getRaw-INV) with all_347_4, all_367_3, simplifying % 40.09/6.14 | with (21), (43) gives: % 40.09/6.14 | (50) ? [v0: vAttrL] : (vtable(v0, all_367_3) = all_347_4 & % 40.09/6.14 | vRawTable(all_367_3) & vAttrL(v0)) % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (getAttrL-INV) with all_347_6, all_367_5, % 40.09/6.14 | simplifying with (20), (44) gives: % 40.09/6.14 | (51) ? [v0: vRawTable] : (vtable(all_367_5, v0) = all_347_6 & % 40.09/6.14 | vRawTable(v0) & vAttrL(all_367_5)) % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (isValue-true-INV) with vq1, simplifying with (3), % 40.09/6.14 | (29) gives: % 40.09/6.14 | (52) ? [v0: vTable] : (vtvalue(v0) = vq1 & vTable(v0)) % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (isValue-true-INV) with vq2, simplifying with (4), % 40.09/6.14 | (30) gives: % 40.09/6.14 | (53) ? [v0: vTable] : (vtvalue(v0) = vq2 & vTable(v0)) % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (Ttvalue_inv) with all_347_5, all_347_6, all_347_2, % 40.09/6.14 | vq1, simplifying with (17), (20), (22), (23), (33) gives: % 40.09/6.14 | (54) vwelltypedtable(all_347_2, all_347_6) = 0 % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (Ttvalue_inv) with all_347_5, all_347_4, all_347_2, % 40.09/6.14 | vq2, simplifying with (17), (21), (22), (24), (32) gives: % 40.09/6.14 | (55) vwelltypedtable(all_347_2, all_347_4) = 0 % 40.09/6.14 | % 40.09/6.14 | DELTA: instantiating (53) with fresh symbol all_387_0 gives: % 40.09/6.14 | (56) vtvalue(all_387_0) = vq2 & vTable(all_387_0) % 40.09/6.14 | % 40.09/6.14 | ALPHA: (56) implies: % 40.09/6.14 | (57) vTable(all_387_0) % 40.09/6.14 | (58) vtvalue(all_387_0) = vq2 % 40.09/6.14 | % 40.09/6.14 | DELTA: instantiating (52) with fresh symbol all_389_0 gives: % 40.09/6.14 | (59) vtvalue(all_389_0) = vq1 & vTable(all_389_0) % 40.09/6.14 | % 40.09/6.14 | ALPHA: (59) implies: % 40.09/6.14 | (60) vTable(all_389_0) % 40.09/6.14 | (61) vtvalue(all_389_0) = vq1 % 40.09/6.14 | % 40.09/6.14 | DELTA: instantiating (49) with fresh symbol all_391_0 gives: % 40.09/6.14 | (62) vtable(all_391_0, all_367_4) = all_347_6 & vRawTable(all_367_4) & % 40.09/6.14 | vAttrL(all_391_0) % 40.09/6.14 | % 40.09/6.14 | ALPHA: (62) implies: % 40.09/6.14 | (63) vAttrL(all_391_0) % 40.09/6.14 | (64) vRawTable(all_367_4) % 40.09/6.14 | (65) vtable(all_391_0, all_367_4) = all_347_6 % 40.09/6.14 | % 40.09/6.14 | DELTA: instantiating (51) with fresh symbol all_393_0 gives: % 40.09/6.14 | (66) vtable(all_367_5, all_393_0) = all_347_6 & vRawTable(all_393_0) & % 40.09/6.14 | vAttrL(all_367_5) % 40.09/6.14 | % 40.09/6.14 | ALPHA: (66) implies: % 40.09/6.14 | (67) vRawTable(all_393_0) % 40.09/6.14 | (68) vtable(all_367_5, all_393_0) = all_347_6 % 40.09/6.14 | % 40.09/6.14 | DELTA: instantiating (50) with fresh symbol all_395_0 gives: % 40.09/6.14 | (69) vtable(all_395_0, all_367_3) = all_347_4 & vRawTable(all_367_3) & % 40.09/6.14 | vAttrL(all_395_0) % 40.09/6.14 | % 40.09/6.14 | ALPHA: (69) implies: % 40.09/6.14 | (70) vAttrL(all_395_0) % 40.09/6.14 | (71) vRawTable(all_367_3) % 40.09/6.14 | (72) vtable(all_395_0, all_367_3) = all_347_4 % 40.09/6.14 | % 40.09/6.14 | REDUCE: (39), (46) imply: % 40.09/6.14 | (73) vtvalue(all_367_1) = all_347_7 % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (Ttvalue) with all_347_2, all_367_1, all_347_5, % 40.09/6.14 | all_347_7, all_347_0, simplifying with (17), (22), (28), (38), % 40.09/6.14 | (73) gives: % 40.09/6.14 | (74) all_347_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 40.09/6.14 | vwelltypedtable(all_347_2, all_367_1) = v0) % 40.09/6.14 | % 40.09/6.14 | GROUND_INST: instantiating (reduce-14) with all_347_6, all_387_0, all_347_3, % 40.09/6.14 | vq1, vq2, all_339_0, all_347_1, simplifying with (13), (19), % 40.09/6.14 | (20), (23), (26), (57), (58) gives: % 40.09/6.14 | (75) ? [v0: vAttrL] : ? [v1: vRawTable] : ? [v2: vRawTable] : ? [v3: % 40.09/6.14 | vRawTable] : ? [v4: vTable] : ? [v5: vQuery] : (vrawDifference(v1, % 40.09/6.14 | v2) = v3 & vgetAttrL(all_347_6) = v0 & vgetRaw(all_387_0) = v2 & % 40.09/6.14 | vgetRaw(all_347_6) = v1 & vtable(v0, v3) = v4 & vsomeQuery(v5) = % 40.09/6.14 | all_347_1 & vtvalue(v4) = v5 & vOptQuery(all_347_1) & vTable(v4) & % 40.09/6.14 | vQuery(v5) & vRawTable(v3) & vRawTable(v2) & vRawTable(v1) & % 40.09/6.14 | vAttrL(v0)) % 40.09/6.14 | % 40.09/6.15 | GROUND_INST: instantiating (Ttvalue_inv) with all_347_5, all_387_0, all_347_2, % 40.09/6.15 | vq2, simplifying with (17), (22), (32), (57), (58) gives: % 40.09/6.15 | (76) vwelltypedtable(all_347_2, all_387_0) = 0 % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (EQ-tvalue) with all_347_4, all_387_0, vq2, % 40.09/6.15 | simplifying with (21), (24), (57), (58) gives: % 40.09/6.15 | (77) all_387_0 = all_347_4 % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (reduce-14) with all_389_0, all_347_4, all_347_3, % 40.09/6.15 | vq1, vq2, all_339_0, all_347_1, simplifying with (13), (19), % 40.09/6.15 | (21), (24), (26), (60), (61) gives: % 40.09/6.15 | (78) ? [v0: vAttrL] : ? [v1: vRawTable] : ? [v2: vRawTable] : ? [v3: % 40.09/6.15 | vRawTable] : ? [v4: vTable] : ? [v5: vQuery] : (vrawDifference(v1, % 40.09/6.15 | v2) = v3 & vgetAttrL(all_389_0) = v0 & vgetRaw(all_389_0) = v1 & % 40.09/6.15 | vgetRaw(all_347_4) = v2 & vtable(v0, v3) = v4 & vsomeQuery(v5) = % 40.09/6.15 | all_347_1 & vtvalue(v4) = v5 & vOptQuery(all_347_1) & vTable(v4) & % 40.09/6.15 | vQuery(v5) & vRawTable(v3) & vRawTable(v2) & vRawTable(v1) & % 40.09/6.15 | vAttrL(v0)) % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (reduce-14) with all_389_0, all_387_0, all_347_3, % 40.09/6.15 | vq1, vq2, all_339_0, all_347_1, simplifying with (13), (19), % 40.09/6.15 | (26), (57), (58), (60), (61) gives: % 40.09/6.15 | (79) ? [v0: vAttrL] : ? [v1: vRawTable] : ? [v2: vRawTable] : ? [v3: % 40.09/6.15 | vRawTable] : ? [v4: vTable] : ? [v5: vQuery] : (vrawDifference(v1, % 40.09/6.15 | v2) = v3 & vgetAttrL(all_389_0) = v0 & vgetRaw(all_389_0) = v1 & % 40.09/6.15 | vgetRaw(all_387_0) = v2 & vtable(v0, v3) = v4 & vsomeQuery(v5) = % 40.09/6.15 | all_347_1 & vtvalue(v4) = v5 & vOptQuery(all_347_1) & vTable(v4) & % 40.09/6.15 | vQuery(v5) & vRawTable(v3) & vRawTable(v2) & vRawTable(v1) & % 40.09/6.15 | vAttrL(v0)) % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (EQ-tvalue) with all_347_6, all_389_0, vq1, % 40.09/6.15 | simplifying with (20), (23), (60), (61) gives: % 40.09/6.15 | (80) all_389_0 = all_347_6 % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (getRaw-0) with all_367_5, all_393_0, all_347_6, % 40.09/6.15 | simplifying with (35), (67), (68) gives: % 40.09/6.15 | (81) vgetRaw(all_347_6) = all_393_0 % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (EQ-table) with all_367_5, all_393_0, all_391_0, % 40.09/6.15 | all_367_4, all_347_6, simplifying with (35), (63), (64), (65), % 40.09/6.15 | (67), (68) gives: % 40.09/6.15 | (82) all_393_0 = all_367_4 & all_391_0 = all_367_5 % 40.09/6.15 | % 40.09/6.15 | ALPHA: (82) implies: % 40.09/6.15 | (83) all_391_0 = all_367_5 % 40.09/6.15 | (84) all_393_0 = all_367_4 % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (getAttrL-0) with all_391_0, all_367_4, all_347_6, % 40.09/6.15 | simplifying with (63), (64), (65) gives: % 40.09/6.15 | (85) vgetAttrL(all_347_6) = all_391_0 % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (getAttrL-0) with all_395_0, all_367_3, all_347_4, % 40.09/6.15 | simplifying with (70), (71), (72) gives: % 40.09/6.15 | (86) vgetAttrL(all_347_4) = all_395_0 % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (getRaw-INV) with all_367_1, all_367_2, simplifying % 40.09/6.15 | with (38), (48) gives: % 40.09/6.15 | (87) ? [v0: vAttrL] : (vtable(v0, all_367_2) = all_367_1 & % 40.09/6.15 | vRawTable(all_367_2) & vAttrL(v0)) % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (getAttrL-INV) with all_367_1, all_367_5, % 40.09/6.15 | simplifying with (38), (47) gives: % 40.09/6.15 | (88) ? [v0: vRawTable] : (vtable(all_367_5, v0) = all_367_1 & % 40.09/6.15 | vRawTable(v0) & vAttrL(all_367_5)) % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (welltypedtable-true-INV) with all_347_2, % 40.09/6.15 | all_347_6, simplifying with (20), (22), (54) gives: % 40.09/6.15 | (89) ? [v0: vAttrL] : ? [v1: vRawTable] : (vwelltypedRawtable(all_347_2, % 40.09/6.15 | v1) = 0 & vmatchingAttrL(all_347_2, v0) = 0 & vtable(v0, v1) = % 40.09/6.15 | all_347_6 & vRawTable(v1) & vAttrL(v0)) % 40.09/6.15 | % 40.09/6.15 | GROUND_INST: instantiating (welltypedtable-true-INV) with all_347_2, % 40.09/6.15 | all_347_4, simplifying with (21), (22), (55) gives: % 40.09/6.15 | (90) ? [v0: vAttrL] : ? [v1: vRawTable] : (vwelltypedRawtable(all_347_2, % 40.09/6.15 | v1) = 0 & vmatchingAttrL(all_347_2, v0) = 0 & vtable(v0, v1) = % 40.09/6.15 | all_347_4 & vRawTable(v1) & vAttrL(v0)) % 40.09/6.15 | % 40.09/6.15 | DELTA: instantiating (88) with fresh symbol all_405_0 gives: % 40.09/6.15 | (91) vtable(all_367_5, all_405_0) = all_367_1 & vRawTable(all_405_0) & % 40.09/6.15 | vAttrL(all_367_5) % 40.09/6.15 | % 40.09/6.15 | ALPHA: (91) implies: % 40.09/6.15 | (92) vRawTable(all_405_0) % 40.09/6.15 | (93) vtable(all_367_5, all_405_0) = all_367_1 % 40.09/6.15 | % 40.09/6.15 | DELTA: instantiating (87) with fresh symbol all_407_0 gives: % 40.09/6.15 | (94) vtable(all_407_0, all_367_2) = all_367_1 & vRawTable(all_367_2) & % 40.09/6.15 | vAttrL(all_407_0) % 40.09/6.15 | % 40.09/6.15 | ALPHA: (94) implies: % 40.09/6.15 | (95) vAttrL(all_407_0) % 40.09/6.15 | (96) vtable(all_407_0, all_367_2) = all_367_1 % 40.09/6.15 | % 40.09/6.15 | DELTA: instantiating (89) with fresh symbols all_409_0, all_409_1 gives: % 40.09/6.15 | (97) vwelltypedRawtable(all_347_2, all_409_0) = 0 & % 40.09/6.15 | vmatchingAttrL(all_347_2, all_409_1) = 0 & vtable(all_409_1, % 40.09/6.15 | all_409_0) = all_347_6 & vRawTable(all_409_0) & vAttrL(all_409_1) % 40.09/6.15 | % 40.09/6.15 | ALPHA: (97) implies: % 40.09/6.15 | (98) vAttrL(all_409_1) % 40.09/6.15 | (99) vRawTable(all_409_0) % 40.09/6.15 | (100) vtable(all_409_1, all_409_0) = all_347_6 % 40.09/6.15 | (101) vmatchingAttrL(all_347_2, all_409_1) = 0 % 40.09/6.15 | (102) vwelltypedRawtable(all_347_2, all_409_0) = 0 % 40.09/6.15 | % 40.09/6.15 | DELTA: instantiating (90) with fresh symbols all_411_0, all_411_1 gives: % 40.09/6.15 | (103) vwelltypedRawtable(all_347_2, all_411_0) = 0 & % 40.09/6.15 | vmatchingAttrL(all_347_2, all_411_1) = 0 & vtable(all_411_1, % 40.09/6.15 | all_411_0) = all_347_4 & vRawTable(all_411_0) & vAttrL(all_411_1) % 40.09/6.15 | % 40.09/6.15 | ALPHA: (103) implies: % 40.09/6.15 | (104) vAttrL(all_411_1) % 40.09/6.15 | (105) vRawTable(all_411_0) % 40.09/6.15 | (106) vtable(all_411_1, all_411_0) = all_347_4 % 40.09/6.15 | % 40.09/6.15 | DELTA: instantiating (79) with fresh symbols all_413_0, all_413_1, all_413_2, % 40.09/6.15 | all_413_3, all_413_4, all_413_5 gives: % 40.09/6.16 | (107) vrawDifference(all_413_4, all_413_3) = all_413_2 & % 40.09/6.16 | vgetAttrL(all_389_0) = all_413_5 & vgetRaw(all_389_0) = all_413_4 & % 40.09/6.16 | vgetRaw(all_387_0) = all_413_3 & vtable(all_413_5, all_413_2) = % 40.09/6.16 | all_413_1 & vsomeQuery(all_413_0) = all_347_1 & vtvalue(all_413_1) = % 40.09/6.16 | all_413_0 & vOptQuery(all_347_1) & vTable(all_413_1) & % 40.09/6.16 | vQuery(all_413_0) & vRawTable(all_413_2) & vRawTable(all_413_3) & % 40.09/6.16 | vRawTable(all_413_4) & vAttrL(all_413_5) % 40.09/6.16 | % 40.09/6.16 | ALPHA: (107) implies: % 40.09/6.16 | (108) vAttrL(all_413_5) % 40.09/6.16 | (109) vRawTable(all_413_4) % 40.09/6.16 | (110) vRawTable(all_413_3) % 40.09/6.16 | (111) vRawTable(all_413_2) % 40.09/6.16 | (112) vtable(all_413_5, all_413_2) = all_413_1 % 40.09/6.16 | (113) vgetRaw(all_387_0) = all_413_3 % 40.09/6.16 | (114) vgetRaw(all_389_0) = all_413_4 % 40.09/6.16 | (115) vgetAttrL(all_389_0) = all_413_5 % 40.09/6.16 | (116) vrawDifference(all_413_4, all_413_3) = all_413_2 % 40.09/6.16 | % 40.09/6.16 | DELTA: instantiating (75) with fresh symbols all_415_0, all_415_1, all_415_2, % 40.09/6.16 | all_415_3, all_415_4, all_415_5 gives: % 40.09/6.16 | (117) vrawDifference(all_415_4, all_415_3) = all_415_2 & % 40.09/6.16 | vgetAttrL(all_347_6) = all_415_5 & vgetRaw(all_387_0) = all_415_3 & % 40.09/6.16 | vgetRaw(all_347_6) = all_415_4 & vtable(all_415_5, all_415_2) = % 40.09/6.16 | all_415_1 & vsomeQuery(all_415_0) = all_347_1 & vtvalue(all_415_1) = % 40.09/6.16 | all_415_0 & vOptQuery(all_347_1) & vTable(all_415_1) & % 40.09/6.16 | vQuery(all_415_0) & vRawTable(all_415_2) & vRawTable(all_415_3) & % 40.09/6.16 | vRawTable(all_415_4) & vAttrL(all_415_5) % 40.09/6.16 | % 40.09/6.16 | ALPHA: (117) implies: % 40.09/6.16 | (118) vtable(all_415_5, all_415_2) = all_415_1 % 40.09/6.16 | (119) vgetRaw(all_347_6) = all_415_4 % 40.09/6.16 | (120) vgetRaw(all_387_0) = all_415_3 % 40.09/6.16 | (121) vgetAttrL(all_347_6) = all_415_5 % 40.09/6.16 | (122) vrawDifference(all_415_4, all_415_3) = all_415_2 % 40.09/6.16 | % 40.09/6.16 | DELTA: instantiating (78) with fresh symbols all_417_0, all_417_1, all_417_2, % 40.09/6.16 | all_417_3, all_417_4, all_417_5 gives: % 40.09/6.16 | (123) vrawDifference(all_417_4, all_417_3) = all_417_2 & % 40.09/6.16 | vgetAttrL(all_389_0) = all_417_5 & vgetRaw(all_389_0) = all_417_4 & % 40.09/6.16 | vgetRaw(all_347_4) = all_417_3 & vtable(all_417_5, all_417_2) = % 40.09/6.16 | all_417_1 & vsomeQuery(all_417_0) = all_347_1 & vtvalue(all_417_1) = % 40.09/6.16 | all_417_0 & vOptQuery(all_347_1) & vTable(all_417_1) & % 40.09/6.16 | vQuery(all_417_0) & vRawTable(all_417_2) & vRawTable(all_417_3) & % 40.09/6.16 | vRawTable(all_417_4) & vAttrL(all_417_5) % 40.09/6.16 | % 40.09/6.16 | ALPHA: (123) implies: % 40.09/6.16 | (124) vtable(all_417_5, all_417_2) = all_417_1 % 40.09/6.16 | (125) vgetRaw(all_347_4) = all_417_3 % 40.09/6.16 | (126) vgetRaw(all_389_0) = all_417_4 % 40.09/6.16 | (127) vgetAttrL(all_389_0) = all_417_5 % 40.09/6.16 | (128) vrawDifference(all_417_4, all_417_3) = all_417_2 % 40.09/6.16 | % 40.09/6.16 | REDUCE: (80), (127) imply: % 40.09/6.16 | (129) vgetAttrL(all_347_6) = all_417_5 % 40.09/6.16 | % 40.09/6.16 | REDUCE: (80), (115) imply: % 40.09/6.16 | (130) vgetAttrL(all_347_6) = all_413_5 % 40.09/6.16 | % 40.09/6.16 | REDUCE: (80), (126) imply: % 40.09/6.16 | (131) vgetRaw(all_347_6) = all_417_4 % 40.09/6.16 | % 40.09/6.16 | REDUCE: (80), (114) imply: % 40.09/6.16 | (132) vgetRaw(all_347_6) = all_413_4 % 40.09/6.16 | % 40.09/6.16 | REDUCE: (77), (120) imply: % 40.09/6.16 | (133) vgetRaw(all_347_4) = all_415_3 % 40.09/6.16 | % 40.09/6.16 | REDUCE: (77), (113) imply: % 40.09/6.16 | (134) vgetRaw(all_347_4) = all_413_3 % 40.09/6.16 | % 40.09/6.16 | REDUCE: (68), (84) imply: % 40.09/6.16 | (135) vtable(all_367_5, all_367_4) = all_347_6 % 40.09/6.16 | % 40.09/6.16 | BETA: splitting (74) gives: % 40.09/6.16 | % 40.09/6.16 | Case 1: % 40.09/6.16 | | % 40.09/6.16 | | (136) all_347_0 = 0 % 40.09/6.16 | | % 40.09/6.16 | | REDUCE: (16), (136) imply: % 40.09/6.16 | | (137) $false % 40.09/6.16 | | % 40.09/6.16 | | CLOSE: (137) is inconsistent. % 40.09/6.16 | | % 40.09/6.16 | Case 2: % 40.09/6.16 | | % 40.09/6.16 | | (138) ? [v0: int] : ( ~ (v0 = 0) & vwelltypedtable(all_347_2, all_367_1) % 40.09/6.16 | | = v0) % 40.09/6.16 | | % 40.09/6.16 | | DELTA: instantiating (138) with fresh symbol all_423_0 gives: % 40.09/6.16 | | (139) ~ (all_423_0 = 0) & vwelltypedtable(all_347_2, all_367_1) = % 40.09/6.16 | | all_423_0 % 40.09/6.16 | | % 40.09/6.16 | | ALPHA: (139) implies: % 40.09/6.16 | | (140) ~ (all_423_0 = 0) % 40.09/6.16 | | (141) vwelltypedtable(all_347_2, all_367_1) = all_423_0 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (6) with all_367_4, all_415_4, all_347_6, % 40.09/6.16 | | simplifying with (42), (119) gives: % 40.09/6.16 | | (142) all_415_4 = all_367_4 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (6) with all_415_4, all_417_4, all_347_6, % 40.09/6.16 | | simplifying with (119), (131) gives: % 40.09/6.16 | | (143) all_417_4 = all_415_4 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (6) with all_413_4, all_417_4, all_347_6, % 40.09/6.16 | | simplifying with (131), (132) gives: % 40.09/6.16 | | (144) all_417_4 = all_413_4 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (6) with all_367_3, all_415_3, all_347_4, % 40.09/6.16 | | simplifying with (43), (133) gives: % 40.09/6.16 | | (145) all_415_3 = all_367_3 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (6) with all_415_3, all_417_3, all_347_4, % 40.09/6.16 | | simplifying with (125), (133) gives: % 40.09/6.16 | | (146) all_417_3 = all_415_3 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (6) with all_413_3, all_417_3, all_347_4, % 40.09/6.16 | | simplifying with (125), (134) gives: % 40.09/6.16 | | (147) all_417_3 = all_413_3 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (7) with all_413_5, all_415_5, all_347_6, % 40.09/6.16 | | simplifying with (121), (130) gives: % 40.09/6.16 | | (148) all_415_5 = all_413_5 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (7) with all_367_5, all_417_5, all_347_6, % 40.09/6.16 | | simplifying with (44), (129) gives: % 40.09/6.16 | | (149) all_417_5 = all_367_5 % 40.09/6.16 | | % 40.09/6.16 | | GROUND_INST: instantiating (7) with all_415_5, all_417_5, all_347_6, % 40.09/6.16 | | simplifying with (121), (129) gives: % 40.09/6.16 | | (150) all_417_5 = all_415_5 % 40.09/6.16 | | % 40.09/6.17 | | COMBINE_EQS: (146), (147) imply: % 40.09/6.17 | | (151) all_415_3 = all_413_3 % 40.09/6.17 | | % 40.09/6.17 | | SIMP: (151) implies: % 40.09/6.17 | | (152) all_415_3 = all_413_3 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (143), (144) imply: % 40.09/6.17 | | (153) all_415_4 = all_413_4 % 40.09/6.17 | | % 40.09/6.17 | | SIMP: (153) implies: % 40.09/6.17 | | (154) all_415_4 = all_413_4 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (149), (150) imply: % 40.09/6.17 | | (155) all_415_5 = all_367_5 % 40.09/6.17 | | % 40.09/6.17 | | SIMP: (155) implies: % 40.09/6.17 | | (156) all_415_5 = all_367_5 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (145), (152) imply: % 40.09/6.17 | | (157) all_413_3 = all_367_3 % 40.09/6.17 | | % 40.09/6.17 | | SIMP: (157) implies: % 40.09/6.17 | | (158) all_413_3 = all_367_3 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (142), (154) imply: % 40.09/6.17 | | (159) all_413_4 = all_367_4 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (148), (156) imply: % 40.09/6.17 | | (160) all_413_5 = all_367_5 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (144), (159) imply: % 40.09/6.17 | | (161) all_417_4 = all_367_4 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (147), (158) imply: % 40.09/6.17 | | (162) all_417_3 = all_367_3 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (128), (161), (162) imply: % 40.09/6.17 | | (163) vrawDifference(all_367_4, all_367_3) = all_417_2 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (122), (142), (145) imply: % 40.09/6.17 | | (164) vrawDifference(all_367_4, all_367_3) = all_415_2 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (116), (158), (159) imply: % 40.09/6.17 | | (165) vrawDifference(all_367_4, all_367_3) = all_413_2 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (124), (149) imply: % 40.09/6.17 | | (166) vtable(all_367_5, all_417_2) = all_417_1 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (118), (156) imply: % 40.09/6.17 | | (167) vtable(all_367_5, all_415_2) = all_415_1 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (112), (160) imply: % 40.09/6.17 | | (168) vtable(all_367_5, all_413_2) = all_413_1 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (11) with all_367_2, all_415_2, all_367_3, % 40.09/6.17 | | all_367_4, simplifying with (45), (164) gives: % 40.09/6.17 | | (169) all_415_2 = all_367_2 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (11) with all_415_2, all_417_2, all_367_3, % 40.09/6.17 | | all_367_4, simplifying with (163), (164) gives: % 40.09/6.17 | | (170) all_417_2 = all_415_2 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (11) with all_413_2, all_417_2, all_367_3, % 40.09/6.17 | | all_367_4, simplifying with (163), (165) gives: % 40.09/6.17 | | (171) all_417_2 = all_413_2 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (170), (171) imply: % 40.09/6.17 | | (172) all_415_2 = all_413_2 % 40.09/6.17 | | % 40.09/6.17 | | SIMP: (172) implies: % 40.09/6.17 | | (173) all_415_2 = all_413_2 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (169), (173) imply: % 40.09/6.17 | | (174) all_413_2 = all_367_2 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (171), (174) imply: % 40.09/6.17 | | (175) all_417_2 = all_367_2 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (166), (175) imply: % 40.09/6.17 | | (176) vtable(all_367_5, all_367_2) = all_417_1 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (167), (169) imply: % 40.09/6.17 | | (177) vtable(all_367_5, all_367_2) = all_415_1 % 40.09/6.17 | | % 40.09/6.17 | | REDUCE: (168), (174) imply: % 40.09/6.17 | | (178) vtable(all_367_5, all_367_2) = all_413_1 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (8) with all_367_1, all_415_1, all_367_2, % 40.09/6.17 | | all_367_5, simplifying with (41), (177) gives: % 40.09/6.17 | | (179) all_415_1 = all_367_1 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (8) with all_415_1, all_417_1, all_367_2, % 40.09/6.17 | | all_367_5, simplifying with (176), (177) gives: % 40.09/6.17 | | (180) all_417_1 = all_415_1 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (8) with all_413_1, all_417_1, all_367_2, % 40.09/6.17 | | all_367_5, simplifying with (176), (178) gives: % 40.09/6.17 | | (181) all_417_1 = all_413_1 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (180), (181) imply: % 40.09/6.17 | | (182) all_415_1 = all_413_1 % 40.09/6.17 | | % 40.09/6.17 | | SIMP: (182) implies: % 40.09/6.17 | | (183) all_415_1 = all_413_1 % 40.09/6.17 | | % 40.09/6.17 | | COMBINE_EQS: (179), (183) imply: % 40.09/6.17 | | (184) all_413_1 = all_367_1 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (EQ-table) with all_367_5, all_405_0, all_407_0, % 40.09/6.17 | | all_367_2, all_367_1, simplifying with (35), (36), (92), (93), % 40.09/6.17 | | (95), (96) gives: % 40.09/6.17 | | (185) all_407_0 = all_367_5 & all_405_0 = all_367_2 % 40.09/6.17 | | % 40.09/6.17 | | ALPHA: (185) implies: % 40.09/6.17 | | (186) all_405_0 = all_367_2 % 40.09/6.17 | | (187) all_407_0 = all_367_5 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (EQ-table) with all_367_5, all_367_4, all_409_1, % 40.09/6.17 | | all_409_0, all_347_6, simplifying with (35), (64), (98), (99), % 40.09/6.17 | | (100), (135) gives: % 40.09/6.17 | | (188) all_409_0 = all_367_4 & all_409_1 = all_367_5 % 40.09/6.17 | | % 40.09/6.17 | | ALPHA: (188) implies: % 40.09/6.17 | | (189) all_409_1 = all_367_5 % 40.09/6.17 | | (190) all_409_0 = all_367_4 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (EQ-table) with all_395_0, all_367_3, all_411_1, % 40.09/6.17 | | all_411_0, all_347_4, simplifying with (70), (71), (72), (104), % 40.09/6.17 | | (105), (106) gives: % 40.09/6.17 | | (191) all_411_0 = all_367_3 & all_411_1 = all_395_0 % 40.09/6.17 | | % 40.09/6.17 | | ALPHA: (191) implies: % 40.09/6.17 | | (192) all_411_1 = all_395_0 % 40.09/6.17 | | (193) all_411_0 = all_367_3 % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (getAttrL-INV) with all_347_4, all_395_0, % 40.09/6.17 | | simplifying with (21), (86) gives: % 40.09/6.17 | | (194) ? [v0: vRawTable] : (vtable(all_395_0, v0) = all_347_4 & % 40.09/6.17 | | vRawTable(v0) & vAttrL(all_395_0)) % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (2) with all_347_2, all_367_5, all_367_2, % 40.09/6.17 | | all_367_1, all_423_0, simplifying with (22), (35), (36), (41), % 40.09/6.17 | | (141) gives: % 40.09/6.17 | | (195) all_423_0 = 0 | ? [v0: any] : ? [v1: any] : % 40.09/6.17 | | (vwelltypedRawtable(all_347_2, all_367_2) = v1 & % 40.09/6.17 | | vmatchingAttrL(all_347_2, all_367_5) = v0 & ( ~ (v1 = 0) | ~ (v0 % 40.09/6.17 | | = 0))) % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (2) with all_347_2, all_407_0, all_367_2, % 40.09/6.17 | | all_367_1, all_423_0, simplifying with (22), (36), (95), (96), % 40.09/6.17 | | (141) gives: % 40.09/6.17 | | (196) all_423_0 = 0 | ? [v0: any] : ? [v1: any] : % 40.09/6.17 | | (vwelltypedRawtable(all_347_2, all_367_2) = v1 & % 40.09/6.17 | | vmatchingAttrL(all_347_2, all_407_0) = v0 & ( ~ (v1 = 0) | ~ (v0 % 40.09/6.17 | | = 0))) % 40.09/6.17 | | % 40.09/6.17 | | GROUND_INST: instantiating (2) with all_347_2, all_367_5, all_405_0, % 40.09/6.17 | | all_367_1, all_423_0, simplifying with (22), (35), (92), (93), % 40.09/6.17 | | (141) gives: % 40.09/6.17 | | (197) all_423_0 = 0 | ? [v0: any] : ? [v1: any] : % 40.09/6.17 | | (vwelltypedRawtable(all_347_2, all_405_0) = v1 & % 40.09/6.17 | | vmatchingAttrL(all_347_2, all_367_5) = v0 & ( ~ (v1 = 0) | ~ (v0 % 40.09/6.17 | | = 0))) % 40.09/6.17 | | % 40.09/6.17 | | DELTA: instantiating (194) with fresh symbol all_447_0 gives: % 40.09/6.17 | | (198) vtable(all_395_0, all_447_0) = all_347_4 & vRawTable(all_447_0) & % 40.09/6.17 | | vAttrL(all_395_0) % 40.09/6.17 | | % 40.09/6.17 | | ALPHA: (198) implies: % 40.09/6.18 | | (199) vRawTable(all_447_0) % 40.09/6.18 | | (200) vtable(all_395_0, all_447_0) = all_347_4 % 40.09/6.18 | | % 40.09/6.18 | | REDUCE: (102), (190) imply: % 40.09/6.18 | | (201) vwelltypedRawtable(all_347_2, all_367_4) = 0 % 40.09/6.18 | | % 40.09/6.18 | | REDUCE: (101), (189) imply: % 40.09/6.18 | | (202) vmatchingAttrL(all_347_2, all_367_5) = 0 % 40.09/6.18 | | % 40.09/6.18 | | BETA: splitting (197) gives: % 40.09/6.18 | | % 40.09/6.18 | | Case 1: % 40.09/6.18 | | | % 40.09/6.18 | | | (203) all_423_0 = 0 % 40.09/6.18 | | | % 40.09/6.18 | | | REDUCE: (140), (203) imply: % 40.09/6.18 | | | (204) $false % 40.09/6.18 | | | % 40.09/6.18 | | | CLOSE: (204) is inconsistent. % 40.09/6.18 | | | % 40.09/6.18 | | Case 2: % 40.09/6.18 | | | % 40.09/6.18 | | | (205) ? [v0: any] : ? [v1: any] : (vwelltypedRawtable(all_347_2, % 40.09/6.18 | | | all_405_0) = v1 & vmatchingAttrL(all_347_2, all_367_5) = v0 & % 40.09/6.18 | | | ( ~ (v1 = 0) | ~ (v0 = 0))) % 40.09/6.18 | | | % 40.09/6.18 | | | DELTA: instantiating (205) with fresh symbols all_458_0, all_458_1 gives: % 40.09/6.18 | | | (206) vwelltypedRawtable(all_347_2, all_405_0) = all_458_0 & % 40.09/6.18 | | | vmatchingAttrL(all_347_2, all_367_5) = all_458_1 & ( ~ (all_458_0 % 40.09/6.18 | | | = 0) | ~ (all_458_1 = 0)) % 40.09/6.18 | | | % 40.09/6.18 | | | ALPHA: (206) implies: % 40.09/6.18 | | | (207) vmatchingAttrL(all_347_2, all_367_5) = all_458_1 % 40.09/6.18 | | | (208) vwelltypedRawtable(all_347_2, all_405_0) = all_458_0 % 40.09/6.18 | | | % 40.09/6.18 | | | REDUCE: (186), (208) imply: % 40.09/6.18 | | | (209) vwelltypedRawtable(all_347_2, all_367_2) = all_458_0 % 40.09/6.18 | | | % 40.09/6.18 | | | BETA: splitting (196) gives: % 40.09/6.18 | | | % 40.09/6.18 | | | Case 1: % 40.09/6.18 | | | | % 40.09/6.18 | | | | (210) all_423_0 = 0 % 40.09/6.18 | | | | % 40.09/6.18 | | | | REDUCE: (140), (210) imply: % 40.09/6.18 | | | | (211) $false % 40.09/6.18 | | | | % 40.09/6.18 | | | | CLOSE: (211) is inconsistent. % 40.09/6.18 | | | | % 40.09/6.18 | | | Case 2: % 40.09/6.18 | | | | % 40.09/6.18 | | | | (212) ? [v0: any] : ? [v1: any] : (vwelltypedRawtable(all_347_2, % 40.09/6.18 | | | | all_367_2) = v1 & vmatchingAttrL(all_347_2, all_407_0) = v0 % 40.09/6.18 | | | | & ( ~ (v1 = 0) | ~ (v0 = 0))) % 40.09/6.18 | | | | % 40.09/6.18 | | | | DELTA: instantiating (212) with fresh symbols all_463_0, all_463_1 % 40.09/6.18 | | | | gives: % 40.09/6.18 | | | | (213) vwelltypedRawtable(all_347_2, all_367_2) = all_463_0 & % 40.09/6.18 | | | | vmatchingAttrL(all_347_2, all_407_0) = all_463_1 & ( ~ % 40.09/6.18 | | | | (all_463_0 = 0) | ~ (all_463_1 = 0)) % 40.09/6.18 | | | | % 40.09/6.18 | | | | ALPHA: (213) implies: % 40.09/6.18 | | | | (214) vmatchingAttrL(all_347_2, all_407_0) = all_463_1 % 40.09/6.18 | | | | (215) vwelltypedRawtable(all_347_2, all_367_2) = all_463_0 % 40.09/6.18 | | | | % 40.09/6.18 | | | | REDUCE: (187), (214) imply: % 40.09/6.18 | | | | (216) vmatchingAttrL(all_347_2, all_367_5) = all_463_1 % 40.09/6.18 | | | | % 40.09/6.18 | | | | BETA: splitting (195) gives: % 40.09/6.18 | | | | % 40.09/6.18 | | | | Case 1: % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | (217) all_423_0 = 0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | REDUCE: (140), (217) imply: % 40.09/6.18 | | | | | (218) $false % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | CLOSE: (218) is inconsistent. % 40.09/6.18 | | | | | % 40.09/6.18 | | | | Case 2: % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | (219) ? [v0: any] : ? [v1: any] : (vwelltypedRawtable(all_347_2, % 40.09/6.18 | | | | | all_367_2) = v1 & vmatchingAttrL(all_347_2, all_367_5) = % 40.09/6.18 | | | | | v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | DELTA: instantiating (219) with fresh symbols all_468_0, all_468_1 % 40.09/6.18 | | | | | gives: % 40.09/6.18 | | | | | (220) vwelltypedRawtable(all_347_2, all_367_2) = all_468_0 & % 40.09/6.18 | | | | | vmatchingAttrL(all_347_2, all_367_5) = all_468_1 & ( ~ % 40.09/6.18 | | | | | (all_468_0 = 0) | ~ (all_468_1 = 0)) % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | ALPHA: (220) implies: % 40.09/6.18 | | | | | (221) vmatchingAttrL(all_347_2, all_367_5) = all_468_1 % 40.09/6.18 | | | | | (222) vwelltypedRawtable(all_347_2, all_367_2) = all_468_0 % 40.09/6.18 | | | | | (223) ~ (all_468_0 = 0) | ~ (all_468_1 = 0) % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | GROUND_INST: instantiating (9) with 0, all_463_1, all_367_5, % 40.09/6.18 | | | | | all_347_2, simplifying with (202), (216) gives: % 40.09/6.18 | | | | | (224) all_463_1 = 0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | GROUND_INST: instantiating (9) with all_463_1, all_468_1, all_367_5, % 40.09/6.18 | | | | | all_347_2, simplifying with (216), (221) gives: % 40.09/6.18 | | | | | (225) all_468_1 = all_463_1 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | GROUND_INST: instantiating (9) with all_458_1, all_468_1, all_367_5, % 40.09/6.18 | | | | | all_347_2, simplifying with (207), (221) gives: % 40.09/6.18 | | | | | (226) all_468_1 = all_458_1 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | GROUND_INST: instantiating (10) with all_463_0, all_468_0, all_367_2, % 40.09/6.18 | | | | | all_347_2, simplifying with (215), (222) gives: % 40.09/6.18 | | | | | (227) all_468_0 = all_463_0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | GROUND_INST: instantiating (10) with all_458_0, all_468_0, all_367_2, % 40.09/6.18 | | | | | all_347_2, simplifying with (209), (222) gives: % 40.09/6.18 | | | | | (228) all_468_0 = all_458_0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | COMBINE_EQS: (227), (228) imply: % 40.09/6.18 | | | | | (229) all_463_0 = all_458_0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | SIMP: (229) implies: % 40.09/6.18 | | | | | (230) all_463_0 = all_458_0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | COMBINE_EQS: (225), (226) imply: % 40.09/6.18 | | | | | (231) all_463_1 = all_458_1 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | SIMP: (231) implies: % 40.09/6.18 | | | | | (232) all_463_1 = all_458_1 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | COMBINE_EQS: (224), (232) imply: % 40.09/6.18 | | | | | (233) all_458_1 = 0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | COMBINE_EQS: (226), (233) imply: % 40.09/6.18 | | | | | (234) all_468_1 = 0 % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | BETA: splitting (223) gives: % 40.09/6.18 | | | | | % 40.09/6.18 | | | | | Case 1: % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | (235) ~ (all_468_0 = 0) % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | REDUCE: (228), (235) imply: % 40.09/6.18 | | | | | | (236) ~ (all_458_0 = 0) % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | GROUND_INST: instantiating (1) with all_347_2, all_395_0, all_447_0, % 40.09/6.18 | | | | | | all_347_4, simplifying with (22), (55), (70), (199), % 40.09/6.18 | | | | | | (200) gives: % 40.09/6.18 | | | | | | (237) vwelltypedRawtable(all_347_2, all_447_0) = 0 & % 40.09/6.18 | | | | | | vmatchingAttrL(all_347_2, all_395_0) = 0 % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | ALPHA: (237) implies: % 40.09/6.18 | | | | | | (238) vwelltypedRawtable(all_347_2, all_447_0) = 0 % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | GROUND_INST: instantiating (EQ-table) with all_395_0, all_367_3, % 40.09/6.18 | | | | | | all_395_0, all_447_0, all_347_4, simplifying with (70), % 40.09/6.18 | | | | | | (71), (72), (199), (200) gives: % 40.09/6.18 | | | | | | (239) all_447_0 = all_367_3 % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | GROUND_INST: instantiating (rawDifferencePreservesWellTypedRaw) with % 40.09/6.18 | | | | | | all_347_2, all_367_4, all_367_3, all_367_2, all_458_0, % 40.09/6.18 | | | | | | simplifying with (22), (45), (64), (71), (209) gives: % 40.09/6.18 | | | | | | (240) all_458_0 = 0 | ? [v0: any] : ? [v1: any] : % 40.09/6.18 | | | | | | (vwelltypedRawtable(all_347_2, all_367_3) = v1 & % 40.09/6.18 | | | | | | vwelltypedRawtable(all_347_2, all_367_4) = v0 & ( ~ (v1 = % 40.09/6.18 | | | | | | 0) | ~ (v0 = 0))) % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | REDUCE: (238), (239) imply: % 40.09/6.18 | | | | | | (241) vwelltypedRawtable(all_347_2, all_367_3) = 0 % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | BETA: splitting (240) gives: % 40.09/6.18 | | | | | | % 40.09/6.18 | | | | | | Case 1: % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | (242) all_458_0 = 0 % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | REDUCE: (236), (242) imply: % 40.09/6.18 | | | | | | | (243) $false % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | CLOSE: (243) is inconsistent. % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | Case 2: % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | (244) ? [v0: any] : ? [v1: any] : % 40.09/6.18 | | | | | | | (vwelltypedRawtable(all_347_2, all_367_3) = v1 & % 40.09/6.18 | | | | | | | vwelltypedRawtable(all_347_2, all_367_4) = v0 & ( ~ (v1 % 40.09/6.18 | | | | | | | = 0) | ~ (v0 = 0))) % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | DELTA: instantiating (244) with fresh symbols all_578_0, all_578_1 % 40.09/6.18 | | | | | | | gives: % 40.09/6.18 | | | | | | | (245) vwelltypedRawtable(all_347_2, all_367_3) = all_578_0 & % 40.09/6.18 | | | | | | | vwelltypedRawtable(all_347_2, all_367_4) = all_578_1 & ( % 40.09/6.18 | | | | | | | ~ (all_578_0 = 0) | ~ (all_578_1 = 0)) % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | ALPHA: (245) implies: % 40.09/6.18 | | | | | | | (246) vwelltypedRawtable(all_347_2, all_367_4) = all_578_1 % 40.09/6.18 | | | | | | | (247) vwelltypedRawtable(all_347_2, all_367_3) = all_578_0 % 40.09/6.18 | | | | | | | (248) ~ (all_578_0 = 0) | ~ (all_578_1 = 0) % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | GROUND_INST: instantiating (10) with 0, all_578_1, all_367_4, % 40.09/6.18 | | | | | | | all_347_2, simplifying with (201), (246) gives: % 40.09/6.18 | | | | | | | (249) all_578_1 = 0 % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | GROUND_INST: instantiating (10) with 0, all_578_0, all_367_3, % 40.09/6.18 | | | | | | | all_347_2, simplifying with (241), (247) gives: % 40.09/6.18 | | | | | | | (250) all_578_0 = 0 % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | BETA: splitting (248) gives: % 40.09/6.18 | | | | | | | % 40.09/6.18 | | | | | | | Case 1: % 40.09/6.18 | | | | | | | | % 40.09/6.18 | | | | | | | | (251) ~ (all_578_0 = 0) % 40.09/6.18 | | | | | | | | % 40.09/6.18 | | | | | | | | REDUCE: (250), (251) imply: % 40.09/6.18 | | | | | | | | (252) $false % 40.09/6.18 | | | | | | | | % 40.09/6.18 | | | | | | | | CLOSE: (252) is inconsistent. % 40.09/6.18 | | | | | | | | % 40.09/6.18 | | | | | | | Case 2: % 40.09/6.18 | | | | | | | | % 40.09/6.18 | | | | | | | | (253) ~ (all_578_1 = 0) % 40.09/6.18 | | | | | | | | % 40.09/6.18 | | | | | | | | REDUCE: (249), (253) imply: % 40.09/6.18 | | | | | | | | (254) $false % 40.09/6.18 | | | | | | | | % 40.09/6.18 | | | | | | | | CLOSE: (254) is inconsistent. % 40.09/6.18 | | | | | | | | % 40.09/6.19 | | | | | | | End of split % 40.09/6.19 | | | | | | | % 40.09/6.19 | | | | | | End of split % 40.09/6.19 | | | | | | % 40.09/6.19 | | | | | Case 2: % 40.09/6.19 | | | | | | % 40.09/6.19 | | | | | | (255) ~ (all_468_1 = 0) % 40.09/6.19 | | | | | | % 40.09/6.19 | | | | | | REDUCE: (234), (255) imply: % 40.09/6.19 | | | | | | (256) $false % 40.09/6.19 | | | | | | % 40.09/6.19 | | | | | | CLOSE: (256) is inconsistent. % 40.09/6.19 | | | | | | % 40.09/6.19 | | | | | End of split % 40.09/6.19 | | | | | % 40.09/6.19 | | | | End of split % 40.09/6.19 | | | | % 40.09/6.19 | | | End of split % 40.09/6.19 | | | % 40.09/6.19 | | End of split % 40.09/6.19 | | % 40.09/6.19 | End of split % 40.09/6.19 | % 40.09/6.19 End of proof % 40.09/6.19 % SZS output end Proof for theBenchmark % 40.09/6.19 % 40.09/6.19 5567ms %------------------------------------------------------------------------------