%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM301_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 : n007.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:43 PM UTC 2026 % Result : Theorem 106.05s 14.72s % Output : Proof 106.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM301_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.34 % Computer : n007.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.35 % DateTime : Mon May 4 20:36:08 EDT 2026 % 0.16/0.35 % CPUTime : % 0.33/0.57 ________ _____ % 0.33/0.57 ___ __ \_________(_)________________________________ % 0.33/0.57 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.33/0.57 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.33/0.57 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.33/0.57 % 0.33/0.57 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.33/0.57 (2023-06-19) % 0.33/0.57 % 0.33/0.57 (c) Philipp Rümmer, 2009-2023 % 0.33/0.57 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.33/0.57 Amanda Stjerna. % 0.33/0.57 Free software under BSD-3-Clause. % 0.33/0.57 % 0.33/0.57 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.33/0.57 % 0.33/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.56/0.60 Running up to 7 provers in parallel. % 0.56/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.56/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.56/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.56/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.56/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.56/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.56/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 12.32/2.41 Prover 4: Preprocessing ... % 12.32/2.45 Prover 1: Preprocessing ... % 12.32/2.46 Prover 6: Preprocessing ... % 12.32/2.46 Prover 2: Preprocessing ... % 12.32/2.46 Prover 5: Preprocessing ... % 12.32/2.46 Prover 3: Preprocessing ... % 13.10/2.52 Prover 0: Preprocessing ... % 32.26/5.08 Prover 1: Warning: ignoring some quantifiers % 33.69/5.28 Prover 4: Warning: ignoring some quantifiers % 34.32/5.32 Prover 1: Constructing countermodel ... % 34.32/5.36 Prover 3: Warning: ignoring some quantifiers % 34.32/5.40 Prover 3: Constructing countermodel ... % 35.06/5.40 Prover 6: Proving ... % 35.06/5.45 Prover 4: Constructing countermodel ... % 35.06/5.45 Prover 0: Proving ... % 36.61/5.65 Prover 5: Proving ... % 39.88/6.05 Prover 2: Proving ... % 82.41/11.57 Prover 2: stopped % 82.41/11.58 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 88.50/12.37 Prover 7: Preprocessing ... % 97.14/13.42 Prover 7: Warning: ignoring some quantifiers % 97.93/13.56 Prover 7: Constructing countermodel ... % 101.00/13.96 Prover 5: stopped % 101.00/13.98 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 104.12/14.36 Prover 1: Found proof (size 211) % 104.12/14.37 Prover 1: proved (13756ms) % 104.12/14.37 Prover 3: stopped % 104.12/14.37 Prover 7: stopped % 104.12/14.37 Prover 4: stopped % 104.12/14.37 Prover 8: Preprocessing ... % 104.12/14.37 Prover 6: stopped % 104.12/14.38 Prover 0: stopped % 105.65/14.68 Prover 8: Warning: ignoring some quantifiers % 106.05/14.71 Prover 8: Constructing countermodel ... % 106.05/14.72 Prover 8: stopped % 106.05/14.72 % 106.05/14.72 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 106.05/14.72 % 106.05/14.77 % SZS output start Proof for theBenchmark % 106.05/14.79 Assumptions after simplification: % 106.05/14.79 --------------------------------- % 106.05/14.79 % 106.05/14.79 (DIFF-aempty-acons) % 106.47/14.83 vAttrL(vaempty) & ! [v0: vName] : ! [v1: vAttrL] : ( ~ (vacons(v0, v1) = % 106.47/14.83 vaempty) | ~ vAttrL(v1) | ~ vName(v0)) % 106.47/14.83 % 106.47/14.83 (DIFF-noRawTable-someRawTable) % 106.47/14.83 vOptRawTable(vnoRawTable) & ! [v0: vRawTable] : ( ~ (vsomeRawTable(v0) = % 106.47/14.83 vnoRawTable) | ~ vRawTable(v0)) % 106.47/14.83 % 106.47/14.83 (DIFF-tempty-tcons) % 106.47/14.83 vRawTable(vtempty) & ! [v0: vRow] : ! [v1: vRawTable] : ( ~ (vtcons(v0, v1) % 106.47/14.83 = vtempty) | ~ vRawTable(v1) | ~ vRow(v0)) % 106.47/14.83 % 106.47/14.83 (EQ-acons) % 106.47/14.83 ! [v0: vName] : ! [v1: vAttrL] : ! [v2: vName] : ! [v3: vAttrL] : ! [v4: % 106.47/14.83 vAttrL] : ( ~ (vacons(v2, v3) = v4) | ~ (vacons(v0, v1) = v4) | ~ % 106.47/14.83 vAttrL(v3) | ~ vAttrL(v1) | ~ vName(v2) | ~ vName(v0) | (v3 = v1 & v2 = % 106.47/14.83 v0)) % 106.47/14.83 % 106.47/14.83 (attachColToFrontRaw-2) % 106.47/14.84 vRawTable(vtempty) & vRow(vrempty) & ? [v0: vRawTable] : (vtcons(vrempty, % 106.47/14.84 vtempty) = v0 & vRawTable(v0) & ! [v1: vRawTable] : ! [v2: vRawTable] : % 106.47/14.84 ! [v3: vRawTable] : (v3 = v0 | ~ (vattachColToFrontRaw(v1, v2) = v3) | ~ % 106.47/14.84 vRawTable(v2) | ~ vRawTable(v1) | (v2 = vtempty & v1 = vtempty) | ( ? % 106.47/14.84 [v4: vVal] : ? [v5: vRawTable] : ? [v6: vRow] : (vtcons(v6, v5) = v1 & % 106.47/14.84 vrcons(v4, vrempty) = v6 & vVal(v4) & vRawTable(v5) & vRow(v6)) & ? % 106.47/14.84 [v4: vRow] : ? [v5: vRawTable] : (vtcons(v4, v5) = v2 & vRawTable(v5) & % 106.47/14.84 vRow(v4))))) % 106.47/14.84 % 106.47/14.84 (attachColToFrontRaw-INV) % 106.47/14.84 vRawTable(vtempty) & vRow(vrempty) & ? [v0: vRawTable] : (vtcons(vrempty, % 106.47/14.84 vtempty) = v0 & vRawTable(v0) & ! [v1: vRawTable] : ! [v2: vRawTable] : % 106.47/14.84 ! [v3: vRawTable] : ( ~ (vattachColToFrontRaw(v1, v2) = v3) | ~ % 106.47/14.84 vRawTable(v2) | ~ vRawTable(v1) | ? [v4: vVal] : ? [v5: vRawTable] : ? % 106.47/14.84 [v6: vRow] : ? [v7: vRawTable] : ? [v8: vRow] : ? [v9: vRow] : ? [v10: % 106.47/14.84 vRawTable] : (vattachColToFrontRaw(v5, v7) = v10 & vtcons(v9, v10) = v3 % 106.47/14.84 & vtcons(v8, v5) = v1 & vtcons(v6, v7) = v2 & vrcons(v4, v6) = v9 & % 106.47/14.84 vrcons(v4, vrempty) = v8 & vVal(v4) & vRawTable(v10) & vRawTable(v7) & % 106.47/14.84 vRawTable(v5) & vRawTable(v3) & vRow(v9) & vRow(v8) & vRow(v6)) | (v3 = % 106.47/14.84 v0 & ( ~ (v2 = vtempty) | ~ (v1 = vtempty)) & ( ! [v4: vVal] : ! [v5: % 106.47/14.84 vRawTable] : ! [v6: vRow] : ( ~ (vtcons(v6, v5) = v1) | ~ % 106.47/14.84 (vrcons(v4, vrempty) = v6) | ~ vVal(v4) | ~ vRawTable(v5)) | ! % 106.47/14.84 [v4: vRow] : ! [v5: vRawTable] : ( ~ (vtcons(v4, v5) = v2) | ~ % 106.47/14.84 vRawTable(v5) | ~ vRow(v4)))) | (v3 = vtempty & v2 = vtempty & v1 = % 106.47/14.84 vtempty))) % 106.47/14.84 % 106.47/14.84 (dropFirstColRaw-0) % 106.47/14.84 vdropFirstColRaw(vtempty) = vtempty & vRawTable(vtempty) % 106.47/14.84 % 106.47/14.84 (dropFirstColRaw-1) % 106.47/14.84 vRow(vrempty) & ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ (vtcons(vrempty, % 106.47/14.84 v0) = v1) | ~ vRawTable(v0) | ? [v2: vRawTable] : ? [v3: vRawTable] : % 106.47/14.84 (vdropFirstColRaw(v1) = v2 & vdropFirstColRaw(v0) = v3 & vtcons(vrempty, v3) % 106.47/14.84 = v2 & vRawTable(v3) & vRawTable(v2))) % 106.47/14.84 % 106.47/14.84 (dropFirstColRaw-INV) % 106.47/14.85 vRawTable(vtempty) & vRow(vrempty) & ! [v0: vRawTable] : ! [v1: vRawTable] : % 106.47/14.85 ( ~ (vdropFirstColRaw(v0) = v1) | ~ vRawTable(v0) | ? [v2: vVal] : ? [v3: % 106.47/14.85 vRow] : ? [v4: vRawTable] : ? [v5: vRow] : ? [v6: vRawTable] : % 106.47/14.85 (vdropFirstColRaw(v4) = v6 & vtcons(v5, v4) = v0 & vtcons(v3, v6) = v1 & % 106.47/14.85 vrcons(v2, v3) = v5 & vVal(v2) & vRawTable(v6) & vRawTable(v4) & % 106.47/14.85 vRawTable(v1) & vRow(v5) & vRow(v3)) | ? [v2: vRawTable] : ? [v3: % 106.47/14.85 vRawTable] : (vdropFirstColRaw(v2) = v3 & vtcons(vrempty, v3) = v1 & % 106.47/14.85 vtcons(vrempty, v2) = v0 & vRawTable(v3) & vRawTable(v2) & vRawTable(v1)) % 106.47/14.85 | (v1 = vtempty & v0 = vtempty)) % 106.47/14.85 % 106.47/14.85 (filterRows-INV) % 106.47/14.85 vRawTable(vtempty) & ! [v0: vRawTable] : ! [v1: vAttrL] : ! [v2: vPred] : % 106.47/14.85 ! [v3: vRawTable] : ( ~ (vfilterRows(v0, v1, v2) = v3) | ~ vRawTable(v0) | ~ % 106.47/14.85 vAttrL(v1) | ~ vPred(v2) | ? [v4: vRow] : ? [v5: vRawTable] : ? [v6: % 106.47/14.85 int] : ( ~ (v6 = 0) & vfilterRows(v5, v1, v2) = v3 & vfilterSingleRow(v2, % 106.47/14.85 v1, v4) = v6 & vtcons(v4, v5) = v0 & vRawTable(v5) & vRawTable(v3) & % 106.47/14.85 vRow(v4)) | ? [v4: vRow] : ? [v5: vRawTable] : ? [v6: vRawTable] : % 106.47/14.85 (vfilterRows(v6, v1, v2) = v5 & vfilterSingleRow(v2, v1, v4) = 0 & % 106.47/14.85 vtcons(v4, v6) = v0 & vtcons(v4, v5) = v3 & vRawTable(v6) & vRawTable(v5) % 106.47/14.85 & vRawTable(v3) & vRow(v4)) | (v3 = vtempty & v0 = vtempty)) % 106.47/14.85 % 106.47/14.85 (findColTypeImpliesfindCol) % 106.47/14.85 ! [v0: vRawTable] : ! [v1: vFType] : ! [v2: vAttrL] : ! [v3: vName] : ! % 106.47/14.85 [v4: vTType] : ! [v5: vOptFType] : ! [v6: vOptRawTable] : ( ~ % 106.47/14.85 (vfindColType(v3, v4) = v5) | ~ (vfindCol(v3, v2, v0) = v6) | ~ % 106.47/14.85 (vsomeFType(v1) = v5) | ~ vTType(v4) | ~ vFType(v1) | ~ vRawTable(v0) | % 106.47/14.85 ~ vAttrL(v2) | ~ vName(v3) | ? [v7: any] : ? [v8: any] : % 106.47/14.85 (vwelltypedRawtable(v4, v0) = v7 & vmatchingAttrL(v4, v2) = v8 & ( ~ (v8 = % 106.47/14.85 0) | ~ (v7 = 0))) | ? [v7: vRawTable] : (vsomeRawTable(v7) = v6 & % 106.47/14.85 vOptRawTable(v6) & vRawTable(v7))) % 106.47/14.85 % 106.47/14.85 (isSomeFType-true-INV) % 106.47/14.85 ! [v0: vOptFType] : ( ~ (visSomeFType(v0) = 0) | ~ vOptFType(v0) | ? [v1: % 106.47/14.85 vFType] : (vsomeFType(v1) = v0 & vFType(v1))) % 106.47/14.85 % 106.47/14.85 (isSomeRawTable-false-INV) % 106.47/14.86 vOptRawTable(vnoRawTable) & ! [v0: vOptRawTable] : ! [v1: int] : (v1 = 0 | % 106.47/14.86 v0 = vnoRawTable | ~ (visSomeRawTable(v0) = v1) | ~ vOptRawTable(v0)) % 106.47/14.86 % 106.47/14.86 (isSomeTType-0) % 106.47/14.86 vOptTType(vnoTType) & ? [v0: int] : ( ~ (v0 = 0) & visSomeTType(vnoTType) = % 106.47/14.86 v0) % 106.47/14.86 % 106.47/14.86 (isSomeTType-1) % 106.47/14.86 ! [v0: vTType] : ! [v1: vOptTType] : ( ~ (vsomeTType(v0) = v1) | ~ % 106.47/14.86 vTType(v0) | visSomeTType(v1) = 0) % 106.47/14.86 % 106.47/14.86 (isSomeTType-true-INV) % 106.47/14.86 ! [v0: vOptTType] : ( ~ (visSomeTType(v0) = 0) | ~ vOptTType(v0) | ? [v1: % 106.47/14.86 vTType] : (vsomeTType(v1) = v0 & vTType(v1))) % 106.47/14.86 % 106.47/14.86 (projectCols-2) % 106.47/14.86 vOptRawTable(vnoRawTable) & ! [v0: vName] : ! [v1: vAttrL] : ! [v2: % 106.47/14.86 vRawTable] : ! [v3: vAttrL] : ! [v4: vAttrL] : ! [v5: vOptRawTable] : (v5 % 106.47/14.86 = vnoRawTable | ~ (vprojectCols(v4, v1, v2) = v5) | ~ (vacons(v0, v3) = % 106.47/14.86 v4) | ~ vRawTable(v2) | ~ vAttrL(v3) | ~ vAttrL(v1) | ~ vName(v0) | ? % 106.47/14.86 [v6: vOptRawTable] : ? [v7: vOptRawTable] : (vprojectCols(v3, v1, v2) = v7 % 106.47/14.86 & vfindCol(v0, v1, v2) = v6 & visSomeRawTable(v7) = 0 & % 106.47/14.86 visSomeRawTable(v6) = 0 & vOptRawTable(v7) & vOptRawTable(v6))) % 106.47/14.86 % 106.47/14.86 (projectCols-INV) % 106.47/14.86 vOptRawTable(vnoRawTable) & vAttrL(vaempty) & ! [v0: vAttrL] : ! [v1: % 106.47/14.86 vAttrL] : ! [v2: vRawTable] : ! [v3: vOptRawTable] : ( ~ (vprojectCols(v0, % 106.47/14.86 v1, v2) = v3) | ~ vRawTable(v2) | ~ vAttrL(v1) | ~ vAttrL(v0) | ? % 106.47/14.86 [v4: vOptRawTable] : ? [v5: vOptRawTable] : ? [v6: vAttrL] : ? [v7: % 106.47/14.86 vName] : ? [v8: vRawTable] : ? [v9: vRawTable] : ? [v10: vRawTable] : % 106.47/14.86 (vprojectCols(v6, v1, v2) = v4 & vfindCol(v7, v1, v2) = v5 & % 106.47/14.86 vattachColToFrontRaw(v8, v9) = v10 & visSomeRawTable(v5) = 0 & % 106.47/14.86 visSomeRawTable(v4) = 0 & vgetRawTable(v5) = v8 & vgetRawTable(v4) = v9 & % 106.47/14.86 vacons(v7, v6) = v0 & vsomeRawTable(v10) = v3 & vOptRawTable(v5) & % 106.47/14.86 vOptRawTable(v4) & vOptRawTable(v3) & vRawTable(v10) & vRawTable(v9) & % 106.47/14.86 vRawTable(v8) & vAttrL(v6) & vName(v7)) | ? [v4: vOptRawTable] : ? [v5: % 106.47/14.86 vOptRawTable] : ? [v6: vAttrL] : ? [v7: vName] : ? [v8: any] : ? [v9: % 106.47/14.86 any] : (v3 = vnoRawTable & vprojectCols(v6, v1, v2) = v4 & vfindCol(v7, % 106.47/14.86 v1, v2) = v5 & visSomeRawTable(v5) = v8 & visSomeRawTable(v4) = v9 & % 106.47/14.86 vacons(v7, v6) = v0 & vOptRawTable(v5) & vOptRawTable(v4) & vAttrL(v6) & % 106.47/14.86 vName(v7) & ( ~ (v9 = 0) | ~ (v8 = 0))) | ? [v4: vRawTable] : (v0 = % 106.47/14.86 vaempty & vprojectEmptyCol(v2) = v4 & vsomeRawTable(v4) = v3 & % 106.47/14.86 vOptRawTable(v3) & vRawTable(v4))) % 106.47/14.86 % 106.47/14.86 (projectColsProgress-acons-IH0) % 106.47/14.86 vAttrL(val1) & ! [v0: vTType] : ! [v1: vRawTable] : ! [v2: vAttrL] : ! % 106.47/14.86 [v3: vTType] : ! [v4: vOptTType] : ! [v5: vOptRawTable] : ( ~ % 106.47/14.86 (vprojectTypeAttrL(val1, v0) = v4) | ~ (vprojectCols(val1, v2, v1) = v5) | % 106.47/14.86 ~ (vsomeTType(v3) = v4) | ~ vTType(v3) | ~ vTType(v0) | ~ vRawTable(v1) | % 106.47/14.86 ~ vAttrL(v2) | ? [v6: any] : ? [v7: any] : (vwelltypedRawtable(v0, v1) = % 106.47/14.86 v6 & vmatchingAttrL(v0, v2) = v7 & ( ~ (v7 = 0) | ~ (v6 = 0))) | ? [v6: % 106.47/14.86 vRawTable] : (vsomeRawTable(v6) = v5 & vOptRawTable(v5) & vRawTable(v6))) % 106.47/14.86 % 106.47/14.87 (projectColsProgress-acons-isSomeRawTable-isSomeRawTable-False) % 106.47/14.87 vAttrL(val1) & ? [v0: vAttrL] : ? [v1: vRawTable] : ? [v2: vTType] : ? % 106.47/14.87 [v3: vAttrL] : ? [v4: vName] : ? [v5: vTType] : ? [v6: vOptRawTable] : ? % 106.47/14.87 [v7: any] : ? [v8: vOptRawTable] : ? [v9: any] : ? [v10: vAttrL] : ? [v11: % 106.47/14.87 vOptTType] : ? [v12: vOptRawTable] : (vprojectTypeAttrL(v10, v5) = v11 & % 106.47/14.87 vprojectCols(v10, v0, v1) = v12 & vprojectCols(v3, val1, v1) = v8 & % 106.47/14.87 vfindCol(v4, val1, v1) = v6 & visSomeRawTable(v8) = v9 & visSomeRawTable(v6) % 106.47/14.87 = v7 & vwelltypedRawtable(v5, v1) = 0 & vmatchingAttrL(v5, v0) = 0 & % 106.47/14.87 vacons(v4, val1) = v10 & vsomeTType(v2) = v11 & vTType(v5) & vTType(v2) & % 106.47/14.87 vOptTType(v11) & vOptRawTable(v12) & vOptRawTable(v8) & vOptRawTable(v6) & % 106.47/14.87 vRawTable(v1) & vAttrL(v10) & vAttrL(v3) & vAttrL(v0) & vName(v4) & ! [v13: % 106.47/14.87 vRawTable] : ( ~ (vsomeRawTable(v13) = v12) | ~ vRawTable(v13)) & ( ~ (v9 % 106.47/14.87 = 0) | ~ (v7 = 0))) % 106.47/14.87 % 106.47/14.87 (projectEmptyCol-0) % 106.47/14.87 vprojectEmptyCol(vtempty) = vtempty & vRawTable(vtempty) % 106.47/14.87 % 106.47/14.87 (projectEmptyCol-1) % 106.47/14.87 vRow(vrempty) & ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRawTable] : ( ~ % 106.47/14.87 (vtcons(v0, v1) = v2) | ~ vRawTable(v1) | ~ vRow(v0) | ? [v3: vRawTable] % 106.47/14.87 : ? [v4: vRawTable] : (vprojectEmptyCol(v2) = v3 & vprojectEmptyCol(v1) = % 106.47/14.87 v4 & vtcons(vrempty, v4) = v3 & vRawTable(v4) & vRawTable(v3))) % 106.47/14.87 % 106.47/14.87 (projectEmptyCol-INV) % 106.47/14.87 vRawTable(vtempty) & vRow(vrempty) & ! [v0: vRawTable] : ! [v1: vRawTable] : % 106.47/14.87 ( ~ (vprojectEmptyCol(v0) = v1) | ~ vRawTable(v0) | ? [v2: vRow] : ? [v3: % 106.47/14.87 vRawTable] : ? [v4: vRawTable] : (vprojectEmptyCol(v3) = v4 & vtcons(v2, % 106.47/14.87 v3) = v0 & vtcons(vrempty, v4) = v1 & vRawTable(v4) & vRawTable(v3) & % 106.47/14.87 vRawTable(v1) & vRow(v2)) | (v1 = vtempty & v0 = vtempty)) % 106.47/14.87 % 106.47/14.87 (projectFirstRaw-0) % 106.47/14.87 vprojectFirstRaw(vtempty) = vtempty & vRawTable(vtempty) % 106.47/14.87 % 106.47/14.87 (projectFirstRaw-1) % 106.47/14.87 vRow(vrempty) & ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ (vtcons(vrempty, % 106.47/14.87 v0) = v1) | ~ vRawTable(v0) | ? [v2: vRawTable] : ? [v3: vRawTable] : % 106.47/14.87 (vprojectFirstRaw(v1) = v2 & vprojectFirstRaw(v0) = v3 & vtcons(vrempty, v3) % 106.47/14.87 = v2 & vRawTable(v3) & vRawTable(v2))) % 106.47/14.87 % 106.47/14.87 (projectTypeAttrL-2) % 106.47/14.87 vOptTType(vnoTType) & ! [v0: vName] : ! [v1: vTType] : ! [v2: vAttrL] : ! % 106.47/14.87 [v3: vAttrL] : ! [v4: vOptTType] : (v4 = vnoTType | ~ (vprojectTypeAttrL(v3, % 106.47/14.87 v1) = v4) | ~ (vacons(v0, v2) = v3) | ~ vTType(v1) | ~ vAttrL(v2) | % 106.47/14.87 ~ vName(v0) | ? [v5: vOptFType] : ? [v6: vOptTType] : % 106.47/14.87 (vprojectTypeAttrL(v2, v1) = v6 & vfindColType(v0, v1) = v5 & % 106.47/14.87 visSomeFType(v5) = 0 & visSomeTType(v6) = 0 & vOptFType(v5) & % 106.47/14.87 vOptTType(v6))) % 106.47/14.87 % 106.47/14.87 (projectTypeAttrL-INV) % 106.47/14.88 vTType(vttempty) & vOptTType(vnoTType) & vAttrL(vaempty) & ? [v0: vOptTType] % 106.47/14.88 : (vsomeTType(vttempty) = v0 & vOptTType(v0) & ! [v1: vAttrL] : ! [v2: % 106.47/14.88 vTType] : ! [v3: vOptTType] : ( ~ (vprojectTypeAttrL(v1, v2) = v3) | ~ % 106.47/14.88 vTType(v2) | ~ vAttrL(v1) | ? [v4: vName] : ? [v5: vOptFType] : ? [v6: % 106.47/14.88 vAttrL] : ? [v7: vOptTType] : ? [v8: vFType] : ? [v9: vTType] : ? % 106.47/14.88 [v10: vTType] : (vprojectTypeAttrL(v6, v2) = v7 & vfindColType(v4, v2) = % 106.47/14.88 v5 & visSomeFType(v5) = 0 & visSomeTType(v7) = 0 & vgetFType(v5) = v8 & % 106.47/14.88 vgetTType(v7) = v9 & vacons(v4, v6) = v1 & vsomeTType(v10) = v3 & % 106.47/14.88 vttcons(v4, v8, v9) = v10 & vOptFType(v5) & vTType(v10) & vTType(v9) & % 106.47/14.88 vOptTType(v7) & vOptTType(v3) & vFType(v8) & vAttrL(v6) & vName(v4)) | % 106.47/14.88 ? [v4: vName] : ? [v5: vOptFType] : ? [v6: vAttrL] : ? [v7: vOptTType] % 106.47/14.88 : ? [v8: any] : ? [v9: any] : (v3 = vnoTType & vprojectTypeAttrL(v6, v2) % 106.47/14.88 = v7 & vfindColType(v4, v2) = v5 & visSomeFType(v5) = v8 & % 106.47/14.88 visSomeTType(v7) = v9 & vacons(v4, v6) = v1 & vOptFType(v5) & % 106.47/14.88 vOptTType(v7) & vAttrL(v6) & vName(v4) & ( ~ (v9 = 0) | ~ (v8 = 0))) | % 106.47/14.88 (v3 = v0 & v1 = vaempty))) % 106.47/14.88 % 106.47/14.88 (function-axioms) % 106.95/14.90 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTType] : ! % 106.95/14.90 [v3: vQuery] : ! [v4: vTTContext] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) % 106.95/14.90 | ~ (vptcheck(v4, v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] % 106.95/14.90 : ! [v2: vPred] : ! [v3: vAttrL] : ! [v4: vRawTable] : (v1 = v0 | ~ % 106.95/14.90 (vfilterRows(v4, v3, v2) = v1) | ~ (vfilterRows(v4, v3, v2) = v0)) & ! % 106.95/14.90 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! [v3: % 106.95/14.90 vAttrL] : ! [v4: vPred] : (v1 = v0 | ~ (vfilterSingleRow(v4, v3, v2) = v1) % 106.95/14.90 | ~ (vfilterSingleRow(v4, v3, v2) = v0)) & ! [v0: vOptVal] : ! [v1: % 106.95/14.90 vOptVal] : ! [v2: vRow] : ! [v3: vAttrL] : ! [v4: vExp] : (v1 = v0 | ~ % 106.95/14.90 (vevalExpRow(v4, v3, v2) = v1) | ~ (vevalExpRow(v4, v3, v2) = v0)) & ! % 106.95/14.90 [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! [v2: vRawTable] : ! [v3: % 106.95/14.90 vAttrL] : ! [v4: vAttrL] : (v1 = v0 | ~ (vprojectCols(v4, v3, v2) = v1) | % 106.95/14.90 ~ (vprojectCols(v4, v3, v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: % 106.95/14.90 vOptRawTable] : ! [v2: vRawTable] : ! [v3: vAttrL] : ! [v4: vName] : (v1 % 106.95/14.90 = v0 | ~ (vfindCol(v4, v3, v2) = v1) | ~ (vfindCol(v4, v3, v2) = v0)) & ! % 106.95/14.90 [v0: vTStore] : ! [v1: vTStore] : ! [v2: vTStore] : ! [v3: vTable] : ! % 106.95/14.90 [v4: vName] : (v1 = v0 | ~ (vbindStore(v4, v3, v2) = v1) | ~ (vbindStore(v4, % 106.95/14.90 v3, v2) = v0)) & ! [v0: vTTContext] : ! [v1: vTTContext] : ! [v2: % 106.95/14.90 vTTContext] : ! [v3: vTType] : ! [v4: vName] : (v1 = v0 | ~ % 106.95/14.90 (vbindContext(v4, v3, v2) = v1) | ~ (vbindContext(v4, v3, v2) = v0)) & ! % 106.95/14.90 [v0: vTType] : ! [v1: vTType] : ! [v2: vTType] : ! [v3: vFType] : ! [v4: % 106.95/14.90 vName] : (v1 = v0 | ~ (vttcons(v4, v3, v2) = v1) | ~ (vttcons(v4, v3, v2) % 106.95/14.90 = v0)) & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vPred] : ! [v3: % 106.95/14.90 vName] : ! [v4: vSelect] : (v1 = v0 | ~ (vselectFromWhere(v4, v3, v2) = % 106.95/14.90 v1) | ~ (vselectFromWhere(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 106.95/14.90 : ! [v1: MultipleValueBool] : ! [v2: vTTContext] : ! [v3: vTStore] : (v1 = % 106.95/14.90 v0 | ~ (vstoreContextConsistent(v3, v2) = v1) | ~ % 106.95/14.90 (vstoreContextConsistent(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 106.95/14.90 [v1: MultipleValueBool] : ! [v2: vTType] : ! [v3: vPred] : (v1 = v0 | ~ % 106.95/14.90 (vtcheckPred(v3, v2) = v1) | ~ (vtcheckPred(v3, v2) = v0)) & ! [v0: % 106.95/14.90 vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: vExp] : (v1 = v0 % 106.95/14.90 | ~ (vtypeOfExp(v3, v2) = v1) | ~ (vtypeOfExp(v3, v2) = v0)) & ! [v0: % 106.95/14.90 vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vSelect] : (v1 = % 106.95/14.90 v0 | ~ (vprojectType(v3, v2) = v1) | ~ (vprojectType(v3, v2) = v0)) & ! % 106.95/14.90 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vAttrL] : (v1 % 106.95/14.90 = v0 | ~ (vprojectTypeAttrL(v3, v2) = v1) | ~ (vprojectTypeAttrL(v3, v2) = % 106.95/14.90 v0)) & ! [v0: vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: % 106.95/14.90 vName] : (v1 = v0 | ~ (vfindColType(v3, v2) = v1) | ~ (vfindColType(v3, % 106.95/14.90 v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: vTStore] % 106.95/14.90 : ! [v3: vQuery] : (v1 = v0 | ~ (vreduce(v3, v2) = v1) | ~ (vreduce(v3, v2) % 106.95/14.90 = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: vPred] : ! [v3: % 106.95/14.90 vTable] : (v1 = v0 | ~ (vfilterTable(v3, v2) = v1) | ~ (vfilterTable(v3, % 106.95/14.90 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 106.95/14.90 ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ (vlessThan(v3, v2) = v1) | ~ % 106.95/14.90 (vlessThan(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 106.95/14.90 MultipleValueBool] : ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ % 106.95/14.90 (vgreaterThan(v3, v2) = v1) | ~ (vgreaterThan(v3, v2) = v0)) & ! [v0: % 106.95/14.90 vOptTable] : ! [v1: vOptTable] : ! [v2: vTable] : ! [v3: vSelect] : (v1 = % 106.95/14.90 v0 | ~ (vprojectTable(v3, v2) = v1) | ~ (vprojectTable(v3, v2) = v0)) & ! % 106.95/14.90 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTTContext] : ! [v3: vName] : % 106.95/14.90 (v1 = v0 | ~ (vlookupContext(v3, v2) = v1) | ~ (vlookupContext(v3, v2) = % 106.95/14.90 v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! [v2: vTStore] : ! % 106.95/14.90 [v3: vName] : (v1 = v0 | ~ (vlookupStore(v3, v2) = v1) | ~ (vlookupStore(v3, % 106.95/14.90 v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 106.95/14.90 vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ (vrawDifference(v3, v2) = % 106.95/14.90 v1) | ~ (vrawDifference(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: % 106.95/14.90 vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 106.95/14.90 (vrawIntersection(v3, v2) = v1) | ~ (vrawIntersection(v3, v2) = v0)) & ! % 106.95/14.90 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 106.95/14.90 : (v1 = v0 | ~ (vrawUnion(v3, v2) = v1) | ~ (vrawUnion(v3, v2) = v0)) & ! % 106.95/14.90 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 106.95/14.90 : (v1 = v0 | ~ (vattachColToFrontRaw(v3, v2) = v1) | ~ % 106.95/14.90 (vattachColToFrontRaw(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 106.95/14.90 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 106.95/14.90 (vsameLength(v3, v2) = v1) | ~ (vsameLength(v3, v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRawTable] : ! % 106.95/14.90 [v3: vRow] : (v1 = v0 | ~ (vrowIn(v3, v2) = v1) | ~ (vrowIn(v3, v2) = v0)) & % 106.95/14.90 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTable] : ! % 106.95/14.90 [v3: vTType] : (v1 = v0 | ~ (vwelltypedtable(v3, v2) = v1) | ~ % 106.95/14.90 (vwelltypedtable(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 106.95/14.90 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ % 106.95/14.90 (vwelltypedRawtable(v3, v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) & % 106.95/14.90 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! % 106.95/14.90 [v3: vTType] : (v1 = v0 | ~ (vwelltypedRow(v3, v2) = v1) | ~ % 106.95/14.90 (vwelltypedRow(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 106.95/14.90 MultipleValueBool] : ! [v2: vAttrL] : ! [v3: vTType] : (v1 = v0 | ~ % 106.95/14.90 (vmatchingAttrL(v3, v2) = v1) | ~ (vmatchingAttrL(v3, v2) = v0)) & ! [v0: % 106.95/14.90 vAttrL] : ! [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vAttrL] : (v1 = v0 | % 106.95/14.90 ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vAttrL] : ! % 106.95/14.90 [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vName] : (v1 = v0 | ~ (vacons(v3, % 106.95/14.90 v2) = v1) | ~ (vacons(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] % 106.95/14.90 : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 106.95/14.90 (vlt(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! % 106.95/14.90 [v3: vExp] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! % 106.95/14.90 [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ % 106.95/14.90 (veq(v3, v2) = v1) | ~ (veq(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: % 106.95/14.90 vPred] : ! [v2: vPred] : ! [v3: vPred] : (v1 = v0 | ~ (vand(v3, v2) = v1) % 106.95/14.90 | ~ (vand(v3, v2) = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: % 106.95/14.90 vRawTable] : ! [v3: vAttrL] : (v1 = v0 | ~ (vtable(v3, v2) = v1) | ~ % 106.95/14.90 (vtable(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 106.95/14.90 vRawTable] : ! [v3: vRow] : (v1 = v0 | ~ (vtcons(v3, v2) = v1) | ~ % 106.95/14.90 (vtcons(v3, v2) = v0)) & ! [v0: vRow] : ! [v1: vRow] : ! [v2: vRow] : ! % 106.95/14.90 [v3: vVal] : (v1 = v0 | ~ (vrcons(v3, v2) = v1) | ~ (vrcons(v3, v2) = v0)) & % 106.95/14.90 ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = % 106.95/14.90 v0 | ~ (vDifference(v3, v2) = v1) | ~ (vDifference(v3, v2) = v0)) & ! % 106.95/14.90 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 106.95/14.90 | ~ (vIntersection(v3, v2) = v1) | ~ (vIntersection(v3, v2) = v0)) & ! % 106.95/14.90 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 106.95/14.90 | ~ (vUnion(v3, v2) = v1) | ~ (vUnion(v3, v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptFType] : (v1 = % 106.95/14.90 v0 | ~ (visSomeFType(v2) = v1) | ~ (visSomeFType(v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptVal] : (v1 = % 106.95/14.90 v0 | ~ (visSomeVal(v2) = v1) | ~ (visSomeVal(v2) = v0)) & ! [v0: % 106.95/14.90 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 106.95/14.90 (vprojectEmptyCol(v2) = v1) | ~ (vprojectEmptyCol(v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQuery] : (v1 = % 106.95/14.90 v0 | ~ (visSomeQuery(v2) = v1) | ~ (visSomeQuery(v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuery] : (v1 = v0 % 106.95/14.90 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTType] : (v1 = % 106.95/14.90 v0 | ~ (visSomeTType(v2) = v1) | ~ (visSomeTType(v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTable] : (v1 = % 106.95/14.90 v0 | ~ (visSomeTable(v2) = v1) | ~ (visSomeTable(v2) = v0)) & ! [v0: % 106.95/14.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptRawTable] : % 106.95/14.90 (v1 = v0 | ~ (visSomeRawTable(v2) = v1) | ~ (visSomeRawTable(v2) = v0)) & ! % 106.95/14.90 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 106.95/14.90 (vdropFirstColRaw(v2) = v1) | ~ (vdropFirstColRaw(v2) = v0)) & ! [v0: % 106.95/14.90 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 106.95/14.90 (vprojectFirstRaw(v2) = v1) | ~ (vprojectFirstRaw(v2) = v0)) & ! [v0: % 106.95/14.90 vFType] : ! [v1: vFType] : ! [v2: vVal] : (v1 = v0 | ~ (vfieldType(v2) = % 106.95/14.90 v1) | ~ (vfieldType(v2) = v0)) & ! [v0: vAttrL] : ! [v1: vAttrL] : ! % 106.95/14.90 [v2: vTable] : (v1 = v0 | ~ (vgetAttrL(v2) = v1) | ~ (vgetAttrL(v2) = v0)) & % 106.95/14.90 ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vTable] : (v1 = v0 | ~ % 106.95/14.90 (vgetRaw(v2) = v1) | ~ (vgetRaw(v2) = v0)) & ! [v0: vFType] : ! [v1: % 106.95/14.90 vFType] : ! [v2: vOptFType] : (v1 = v0 | ~ (vgetFType(v2) = v1) | ~ % 106.95/14.90 (vgetFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vOptVal] : % 106.95/14.90 (v1 = v0 | ~ (vgetVal(v2) = v1) | ~ (vgetVal(v2) = v0)) & ! [v0: vQuery] : % 106.95/14.90 ! [v1: vQuery] : ! [v2: vOptQuery] : (v1 = v0 | ~ (vgetQuery(v2) = v1) | ~ % 106.95/14.90 (vgetQuery(v2) = v0)) & ! [v0: vTType] : ! [v1: vTType] : ! [v2: % 106.95/14.90 vOptTType] : (v1 = v0 | ~ (vgetTType(v2) = v1) | ~ (vgetTType(v2) = v0)) & % 106.95/14.90 ! [v0: vTable] : ! [v1: vTable] : ! [v2: vOptTable] : (v1 = v0 | ~ % 106.95/14.90 (vgetTable(v2) = v1) | ~ (vgetTable(v2) = v0)) & ! [v0: vRawTable] : ! % 106.95/14.90 [v1: vRawTable] : ! [v2: vOptRawTable] : (v1 = v0 | ~ (vgetRawTable(v2) = % 106.95/14.90 v1) | ~ (vgetRawTable(v2) = v0)) & ! [v0: vOptFType] : ! [v1: % 106.95/14.90 vOptFType] : ! [v2: vFType] : (v1 = v0 | ~ (vsomeFType(v2) = v1) | ~ % 106.95/14.90 (vsomeFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vVal] : (v1 % 106.95/14.90 = v0 | ~ (venumVal(v2) = v1) | ~ (venumVal(v2) = v0)) & ! [v0: vPred] : % 106.95/14.90 ! [v1: vPred] : ! [v2: vPred] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) % 106.95/14.90 = v0)) & ! [v0: vOptVal] : ! [v1: vOptVal] : ! [v2: vVal] : (v1 = v0 | % 106.95/14.90 ~ (vsomeVal(v2) = v1) | ~ (vsomeVal(v2) = v0)) & ! [v0: vExp] : ! [v1: % 106.95/14.90 vExp] : ! [v2: vName] : (v1 = v0 | ~ (vlookup(v2) = v1) | ~ (vlookup(v2) % 106.95/14.90 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vVal] : (v1 = v0 | ~ % 106.95/14.90 (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & ! [v0: vName] : ! [v1: % 106.95/14.90 vName] : ! [v2: vName] : (v1 = v0 | ~ (venumName(v2) = v1) | ~ % 106.95/14.90 (venumName(v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: % 106.95/14.90 vQuery] : (v1 = v0 | ~ (vsomeQuery(v2) = v1) | ~ (vsomeQuery(v2) = v0)) & % 106.95/14.90 ! [v0: vFType] : ! [v1: vFType] : ! [v2: vFType] : (v1 = v0 | ~ % 106.95/14.90 (venumFType(v2) = v1) | ~ (venumFType(v2) = v0)) & ! [v0: vOptTType] : ! % 106.95/14.90 [v1: vOptTType] : ! [v2: vTType] : (v1 = v0 | ~ (vsomeTType(v2) = v1) | ~ % 106.95/14.90 (vsomeTType(v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! % 106.95/14.90 [v2: vRawTable] : (v1 = v0 | ~ (vsomeRawTable(v2) = v1) | ~ % 106.95/14.90 (vsomeRawTable(v2) = v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! % 106.95/14.90 [v2: vTable] : (v1 = v0 | ~ (vsomeTable(v2) = v1) | ~ (vsomeTable(v2) = v0)) % 106.95/14.90 & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vTable] : (v1 = v0 | ~ % 106.95/14.90 (vtvalue(v2) = v1) | ~ (vtvalue(v2) = v0)) & ! [v0: vSelect] : ! [v1: % 106.95/14.90 vSelect] : ! [v2: vAttrL] : (v1 = v0 | ~ (vlist(v2) = v1) | ~ (vlist(v2) % 106.95/14.90 = v0)) % 106.95/14.90 % 106.95/14.90 Further assumptions not needed in the proof: % 106.95/14.90 -------------------------------------------- % 106.95/14.90 DIFF-Intersection-Difference, DIFF-Union-Difference, DIFF-Union-Intersection, % 106.95/14.90 DIFF-all-list, DIFF-and-eq, DIFF-and-gt, DIFF-and-lt, DIFF-and-not, % 106.95/14.90 DIFF-constant-lookup, DIFF-emptyContext-bindContext, DIFF-emptyStore-bindStore, % 106.95/14.90 DIFF-eq-gt, DIFF-eq-lt, DIFF-gt-lt, DIFF-initFType-enumFType, % 106.95/14.90 DIFF-initName-enumName, DIFF-initVal-enumVal, DIFF-noFType-someFType, % 106.95/14.90 DIFF-noQuery-someQuery, DIFF-noTType-someTType, DIFF-noTable-someTable, % 106.95/14.90 DIFF-noVal-someVal, DIFF-not-eq, DIFF-not-gt, DIFF-not-lt, DIFF-ptrue-and, % 106.95/14.90 DIFF-ptrue-eq, DIFF-ptrue-gt, DIFF-ptrue-lt, DIFF-ptrue-not, DIFF-rempty-rcons, % 106.95/14.90 DIFF-selectFromWhere-Difference, DIFF-selectFromWhere-Intersection, % 106.95/14.90 DIFF-selectFromWhere-Union, DIFF-ttempty-ttcons, DIFF-tvalue-Difference, % 106.95/14.90 DIFF-tvalue-Intersection, DIFF-tvalue-Union, DIFF-tvalue-selectFromWhere, % 106.95/14.90 EQ-Difference, EQ-Intersection, EQ-Union, EQ-and, EQ-bindContext, EQ-bindStore, % 106.95/14.90 EQ-constant, EQ-enumFType, EQ-enumName, EQ-enumVal, EQ-eq, EQ-gt, EQ-list, % 106.95/14.90 EQ-lookup, EQ-lt, EQ-not, EQ-rcons, EQ-selectFromWhere, EQ-someFType, % 106.95/14.90 EQ-someQuery, EQ-someRawTable, EQ-someTType, EQ-someTable, EQ-someVal, EQ-table, % 106.95/14.90 EQ-tcons, EQ-ttcons, EQ-tvalue, TDifference, TDifference_inv1, TDifference_inv2, % 106.95/14.90 TIntersection, TIntersection_inv1, TIntersection_inv2, TSelectFromWhere, % 106.95/14.90 TSelectFromWhere_inv, TTTContextDuplicate, TTTContextSwap, TUnion, TUnion_inv1, % 106.95/14.90 TUnion_inv2, Ttvalue, Ttvalue_inv, append-0, append-1, append-INV, % 106.95/14.90 attachColToFrontRaw-0, attachColToFrontRaw-1, dom-AttrL, dom-Exp, dom-OptFType, % 106.95/14.90 dom-OptQuery, dom-OptRawTable, dom-OptTType, dom-OptTable, dom-OptVal, dom-Pred, % 106.95/14.90 dom-Query, dom-RawTable, dom-Row, dom-Select, dom-TStore, dom-TTContext, % 106.95/14.90 dom-TType, dom-Table, dropFirstColRaw-2, evalExpRow-0, evalExpRow-1, % 106.95/14.90 evalExpRow-2, evalExpRow-3, evalExpRow-INV, filterRows-0, filterRows-1, % 106.95/14.90 filterRows-2, filterSingleRow-0, filterSingleRow-1, filterSingleRow-2, % 106.95/14.90 filterSingleRow-3, filterSingleRow-4, filterSingleRow-5, % 106.95/14.90 filterSingleRow-false-INV, filterSingleRow-true-INV, filterTable-0, % 106.95/14.90 filterTable-INV, findCol-0, findCol-1, findCol-2, findCol-INV, % 106.95/14.90 findColPreservesRowCount, findColPreservesWelltypedRaw, findColType-0, % 106.95/14.90 findColType-1, findColType-2, findColType-INV, getAttrL-0, getAttrL-INV, % 106.95/14.90 getFType-0, getQuery-0, getRaw-0, getRaw-INV, getRawTable-0, getTType-0, % 106.95/14.90 getTable-0, getVal-0, isSomeFType-0, isSomeFType-1, isSomeFType-false-INV, % 106.95/14.90 isSomeQuery-0, isSomeQuery-1, isSomeQuery-false-INV, isSomeQuery-true-INV, % 106.95/14.90 isSomeRawTable-0, isSomeRawTable-1, isSomeRawTable-true-INV, % 106.95/14.90 isSomeTType-false-INV, isSomeTable-0, isSomeTable-1, isSomeTable-false-INV, % 106.95/14.90 isSomeTable-true-INV, isSomeVal-0, isSomeVal-1, isSomeVal-false-INV, % 106.95/14.90 isSomeVal-true-INV, isValue-0, isValue-1, isValue-2, isValue-3, isValue-4, % 106.95/14.90 isValue-false-INV, isValue-true-INV, lookupContext-0, lookupContext-1, % 106.95/14.90 lookupContext-2, lookupContext-INV, lookupStore-0, lookupStore-1, lookupStore-2, % 106.95/14.90 lookupStore-INV, matchingAttrL-0, matchingAttrL-1, matchingAttrL-2, % 106.95/14.90 matchingAttrL-false-INV, matchingAttrL-true-INV, projectCols-0, projectCols-1, % 106.95/14.90 projectFirstRaw-2, projectFirstRaw-INV, projectTable-0, projectTable-1, % 106.95/14.90 projectTable-2, projectTable-INV, projectType-0, projectType-1, projectType-INV, % 106.95/14.90 projectTypeAttrL-0, projectTypeAttrL-1, rawDifference-0, rawDifference-1, % 106.95/14.90 rawDifference-2, rawDifference-3, rawDifference-4, rawDifference-INV, % 106.95/14.90 rawIntersection-0, rawIntersection-1, rawIntersection-2, rawIntersection-3, % 106.95/14.90 rawIntersection-4, rawIntersection-INV, rawUnion-0, rawUnion-1, rawUnion-2, % 106.95/14.90 rawUnion-INV, reduce-0, reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, % 106.95/14.90 reduce-14, reduce-15, reduce-16, reduce-17, reduce-18, reduce-2, reduce-3, % 106.95/14.90 reduce-4, reduce-5, reduce-6, reduce-7, reduce-8, reduce-9, reduce-INV, rowIn-0, % 106.95/14.90 rowIn-1, rowIn-false-INV, rowIn-true-INV, sameLength-0, sameLength-1, % 106.95/14.90 sameLength-2, sameLength-false-INV, sameLength-true-INV, % 106.95/14.90 storeContextConsistent-0, storeContextConsistent-1, storeContextConsistent-2, % 106.95/14.90 storeContextConsistent-false-INV, storeContextConsistent-true-INV, tcheckPred-0, % 106.95/14.90 tcheckPred-1, tcheckPred-2, tcheckPred-3, tcheckPred-4, tcheckPred-5, % 106.95/14.90 tcheckPred-false-INV, tcheckPred-true-INV, typeOfExp-0, typeOfExp-1, % 106.95/14.90 typeOfExp-2, typeOfExp-3, typeOfExp-INV, welltypedRawtable-0, % 106.95/14.90 welltypedRawtable-1, welltypedRawtable-false-INV, welltypedRawtable-true-INV, % 106.95/14.90 welltypedRow-0, welltypedRow-1, welltypedRow-2, welltypedRow-false-INV, % 106.95/14.90 welltypedRow-true-INV, welltypedtable-0, welltypedtable-false-INV, % 106.95/14.90 welltypedtable-true-INV % 106.95/14.90 % 106.95/14.90 Those formulas are unsatisfiable: % 106.95/14.90 --------------------------------- % 106.95/14.90 % 106.95/14.90 Begin of proof % 106.95/14.91 | % 106.95/14.91 | ALPHA: (DIFF-noRawTable-someRawTable) implies: % 106.95/14.91 | (1) ! [v0: vRawTable] : ( ~ (vsomeRawTable(v0) = vnoRawTable) | ~ % 106.95/14.91 | vRawTable(v0)) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (DIFF-tempty-tcons) implies: % 106.95/14.91 | (2) ! [v0: vRow] : ! [v1: vRawTable] : ( ~ (vtcons(v0, v1) = vtempty) | % 106.95/14.91 | ~ vRawTable(v1) | ~ vRow(v0)) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (DIFF-aempty-acons) implies: % 106.95/14.91 | (3) ! [v0: vName] : ! [v1: vAttrL] : ( ~ (vacons(v0, v1) = vaempty) | ~ % 106.95/14.91 | vAttrL(v1) | ~ vName(v0)) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (projectFirstRaw-0) implies: % 106.95/14.91 | (4) vprojectFirstRaw(vtempty) = vtempty % 106.95/14.91 | % 106.95/14.91 | ALPHA: (projectFirstRaw-1) implies: % 106.95/14.91 | (5) ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ (vtcons(vrempty, v0) = % 106.95/14.91 | v1) | ~ vRawTable(v0) | ? [v2: vRawTable] : ? [v3: vRawTable] : % 106.95/14.91 | (vprojectFirstRaw(v1) = v2 & vprojectFirstRaw(v0) = v3 & % 106.95/14.91 | vtcons(vrempty, v3) = v2 & vRawTable(v3) & vRawTable(v2))) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (dropFirstColRaw-0) implies: % 106.95/14.91 | (6) vdropFirstColRaw(vtempty) = vtempty % 106.95/14.91 | % 106.95/14.91 | ALPHA: (dropFirstColRaw-1) implies: % 106.95/14.91 | (7) ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ (vtcons(vrempty, v0) = % 106.95/14.91 | v1) | ~ vRawTable(v0) | ? [v2: vRawTable] : ? [v3: vRawTable] : % 106.95/14.91 | (vdropFirstColRaw(v1) = v2 & vdropFirstColRaw(v0) = v3 & % 106.95/14.91 | vtcons(vrempty, v3) = v2 & vRawTable(v3) & vRawTable(v2))) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (dropFirstColRaw-INV) implies: % 106.95/14.91 | (8) ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ (vdropFirstColRaw(v0) = % 106.95/14.91 | v1) | ~ vRawTable(v0) | ? [v2: vVal] : ? [v3: vRow] : ? [v4: % 106.95/14.91 | vRawTable] : ? [v5: vRow] : ? [v6: vRawTable] : % 106.95/14.91 | (vdropFirstColRaw(v4) = v6 & vtcons(v5, v4) = v0 & vtcons(v3, v6) = % 106.95/14.91 | v1 & vrcons(v2, v3) = v5 & vVal(v2) & vRawTable(v6) & vRawTable(v4) % 106.95/14.91 | & vRawTable(v1) & vRow(v5) & vRow(v3)) | ? [v2: vRawTable] : ? % 106.95/14.91 | [v3: vRawTable] : (vdropFirstColRaw(v2) = v3 & vtcons(vrempty, v3) = % 106.95/14.91 | v1 & vtcons(vrempty, v2) = v0 & vRawTable(v3) & vRawTable(v2) & % 106.95/14.91 | vRawTable(v1)) | (v1 = vtempty & v0 = vtempty)) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (isSomeRawTable-false-INV) implies: % 106.95/14.91 | (9) ! [v0: vOptRawTable] : ! [v1: int] : (v1 = 0 | v0 = vnoRawTable | ~ % 106.95/14.91 | (visSomeRawTable(v0) = v1) | ~ vOptRawTable(v0)) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (attachColToFrontRaw-2) implies: % 106.95/14.91 | (10) ? [v0: vRawTable] : (vtcons(vrempty, vtempty) = v0 & vRawTable(v0) & % 106.95/14.91 | ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v3 = % 106.95/14.91 | v0 | ~ (vattachColToFrontRaw(v1, v2) = v3) | ~ vRawTable(v2) | % 106.95/14.91 | ~ vRawTable(v1) | (v2 = vtempty & v1 = vtempty) | ( ? [v4: vVal] : % 106.95/14.91 | ? [v5: vRawTable] : ? [v6: vRow] : (vtcons(v6, v5) = v1 & % 106.95/14.91 | vrcons(v4, vrempty) = v6 & vVal(v4) & vRawTable(v5) & % 106.95/14.91 | vRow(v6)) & ? [v4: vRow] : ? [v5: vRawTable] : (vtcons(v4, % 106.95/14.91 | v5) = v2 & vRawTable(v5) & vRow(v4))))) % 106.95/14.91 | % 106.95/14.91 | ALPHA: (attachColToFrontRaw-INV) implies: % 106.95/14.92 | (11) ? [v0: vRawTable] : (vtcons(vrempty, vtempty) = v0 & vRawTable(v0) & % 106.95/14.92 | ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : ( ~ % 106.95/14.92 | (vattachColToFrontRaw(v1, v2) = v3) | ~ vRawTable(v2) | ~ % 106.95/14.92 | vRawTable(v1) | ? [v4: vVal] : ? [v5: vRawTable] : ? [v6: vRow] % 106.95/14.92 | : ? [v7: vRawTable] : ? [v8: vRow] : ? [v9: vRow] : ? [v10: % 106.95/14.92 | vRawTable] : (vattachColToFrontRaw(v5, v7) = v10 & vtcons(v9, % 106.95/14.92 | v10) = v3 & vtcons(v8, v5) = v1 & vtcons(v6, v7) = v2 & % 106.95/14.92 | vrcons(v4, v6) = v9 & vrcons(v4, vrempty) = v8 & vVal(v4) & % 106.95/14.92 | vRawTable(v10) & vRawTable(v7) & vRawTable(v5) & vRawTable(v3) & % 106.95/14.92 | vRow(v9) & vRow(v8) & vRow(v6)) | (v3 = v0 & ( ~ (v2 = vtempty) % 106.95/14.92 | | ~ (v1 = vtempty)) & ( ! [v4: vVal] : ! [v5: vRawTable] : % 106.95/14.92 | ! [v6: vRow] : ( ~ (vtcons(v6, v5) = v1) | ~ (vrcons(v4, % 106.95/14.92 | vrempty) = v6) | ~ vVal(v4) | ~ vRawTable(v5)) | ! % 106.95/14.92 | [v4: vRow] : ! [v5: vRawTable] : ( ~ (vtcons(v4, v5) = v2) | % 106.95/14.92 | ~ vRawTable(v5) | ~ vRow(v4)))) | (v3 = vtempty & v2 = % 106.95/14.92 | vtempty & v1 = vtempty))) % 106.95/14.92 | % 106.95/14.92 | ALPHA: (isSomeTType-0) implies: % 106.95/14.92 | (12) ? [v0: int] : ( ~ (v0 = 0) & visSomeTType(vnoTType) = v0) % 106.95/14.92 | % 106.95/14.92 | ALPHA: (projectEmptyCol-0) implies: % 106.95/14.92 | (13) vprojectEmptyCol(vtempty) = vtempty % 106.95/14.92 | % 106.95/14.92 | ALPHA: (projectEmptyCol-1) implies: % 106.95/14.92 | (14) ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRawTable] : ( ~ % 106.95/14.92 | (vtcons(v0, v1) = v2) | ~ vRawTable(v1) | ~ vRow(v0) | ? [v3: % 106.95/14.92 | vRawTable] : ? [v4: vRawTable] : (vprojectEmptyCol(v2) = v3 & % 106.95/14.92 | vprojectEmptyCol(v1) = v4 & vtcons(vrempty, v4) = v3 & % 106.95/14.92 | vRawTable(v4) & vRawTable(v3))) % 106.95/14.92 | % 106.95/14.92 | ALPHA: (projectEmptyCol-INV) implies: % 106.95/14.92 | (15) vRow(vrempty) % 106.95/14.92 | (16) ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ (vprojectEmptyCol(v0) = % 106.95/14.92 | v1) | ~ vRawTable(v0) | ? [v2: vRow] : ? [v3: vRawTable] : ? % 106.95/14.92 | [v4: vRawTable] : (vprojectEmptyCol(v3) = v4 & vtcons(v2, v3) = v0 & % 106.95/14.92 | vtcons(vrempty, v4) = v1 & vRawTable(v4) & vRawTable(v3) & % 106.95/14.92 | vRawTable(v1) & vRow(v2)) | (v1 = vtempty & v0 = vtempty)) % 106.95/14.92 | % 106.95/14.92 | ALPHA: (projectCols-2) implies: % 106.95/14.92 | (17) ! [v0: vName] : ! [v1: vAttrL] : ! [v2: vRawTable] : ! [v3: % 106.95/14.92 | vAttrL] : ! [v4: vAttrL] : ! [v5: vOptRawTable] : (v5 = % 106.95/14.92 | vnoRawTable | ~ (vprojectCols(v4, v1, v2) = v5) | ~ (vacons(v0, % 106.95/14.92 | v3) = v4) | ~ vRawTable(v2) | ~ vAttrL(v3) | ~ vAttrL(v1) | % 106.95/14.92 | ~ vName(v0) | ? [v6: vOptRawTable] : ? [v7: vOptRawTable] : % 106.95/14.92 | (vprojectCols(v3, v1, v2) = v7 & vfindCol(v0, v1, v2) = v6 & % 106.95/14.92 | visSomeRawTable(v7) = 0 & visSomeRawTable(v6) = 0 & % 106.95/14.92 | vOptRawTable(v7) & vOptRawTable(v6))) % 106.95/14.92 | % 106.95/14.92 | ALPHA: (projectCols-INV) implies: % 106.95/14.92 | (18) ! [v0: vAttrL] : ! [v1: vAttrL] : ! [v2: vRawTable] : ! [v3: % 106.95/14.92 | vOptRawTable] : ( ~ (vprojectCols(v0, v1, v2) = v3) | ~ % 106.95/14.92 | vRawTable(v2) | ~ vAttrL(v1) | ~ vAttrL(v0) | ? [v4: % 106.95/14.92 | vOptRawTable] : ? [v5: vOptRawTable] : ? [v6: vAttrL] : ? [v7: % 106.95/14.92 | vName] : ? [v8: vRawTable] : ? [v9: vRawTable] : ? [v10: % 106.95/14.92 | vRawTable] : (vprojectCols(v6, v1, v2) = v4 & vfindCol(v7, v1, v2) % 106.95/14.92 | = v5 & vattachColToFrontRaw(v8, v9) = v10 & visSomeRawTable(v5) = % 106.95/14.92 | 0 & visSomeRawTable(v4) = 0 & vgetRawTable(v5) = v8 & % 106.95/14.92 | vgetRawTable(v4) = v9 & vacons(v7, v6) = v0 & vsomeRawTable(v10) = % 106.95/14.92 | v3 & vOptRawTable(v5) & vOptRawTable(v4) & vOptRawTable(v3) & % 106.95/14.92 | vRawTable(v10) & vRawTable(v9) & vRawTable(v8) & vAttrL(v6) & % 106.95/14.92 | vName(v7)) | ? [v4: vOptRawTable] : ? [v5: vOptRawTable] : ? % 106.95/14.92 | [v6: vAttrL] : ? [v7: vName] : ? [v8: any] : ? [v9: any] : (v3 = % 106.95/14.92 | vnoRawTable & vprojectCols(v6, v1, v2) = v4 & vfindCol(v7, v1, v2) % 106.95/14.92 | = v5 & visSomeRawTable(v5) = v8 & visSomeRawTable(v4) = v9 & % 106.95/14.92 | vacons(v7, v6) = v0 & vOptRawTable(v5) & vOptRawTable(v4) & % 106.95/14.92 | vAttrL(v6) & vName(v7) & ( ~ (v9 = 0) | ~ (v8 = 0))) | ? [v4: % 106.95/14.92 | vRawTable] : (v0 = vaempty & vprojectEmptyCol(v2) = v4 & % 106.95/14.92 | vsomeRawTable(v4) = v3 & vOptRawTable(v3) & vRawTable(v4))) % 106.95/14.92 | % 106.95/14.92 | ALPHA: (filterRows-INV) implies: % 106.95/14.92 | (19) vRawTable(vtempty) % 106.95/14.92 | % 106.95/14.92 | ALPHA: (projectTypeAttrL-2) implies: % 106.95/14.93 | (20) ! [v0: vName] : ! [v1: vTType] : ! [v2: vAttrL] : ! [v3: vAttrL] : % 106.95/14.93 | ! [v4: vOptTType] : (v4 = vnoTType | ~ (vprojectTypeAttrL(v3, v1) = % 106.95/14.93 | v4) | ~ (vacons(v0, v2) = v3) | ~ vTType(v1) | ~ vAttrL(v2) | % 106.95/14.93 | ~ vName(v0) | ? [v5: vOptFType] : ? [v6: vOptTType] : % 106.95/14.93 | (vprojectTypeAttrL(v2, v1) = v6 & vfindColType(v0, v1) = v5 & % 106.95/14.93 | visSomeFType(v5) = 0 & visSomeTType(v6) = 0 & vOptFType(v5) & % 106.95/14.93 | vOptTType(v6))) % 106.95/14.93 | % 106.95/14.93 | ALPHA: (projectTypeAttrL-INV) implies: % 106.95/14.93 | (21) ? [v0: vOptTType] : (vsomeTType(vttempty) = v0 & vOptTType(v0) & ! % 106.95/14.93 | [v1: vAttrL] : ! [v2: vTType] : ! [v3: vOptTType] : ( ~ % 106.95/14.93 | (vprojectTypeAttrL(v1, v2) = v3) | ~ vTType(v2) | ~ vAttrL(v1) | % 106.95/14.93 | ? [v4: vName] : ? [v5: vOptFType] : ? [v6: vAttrL] : ? [v7: % 106.95/14.93 | vOptTType] : ? [v8: vFType] : ? [v9: vTType] : ? [v10: % 106.95/14.93 | vTType] : (vprojectTypeAttrL(v6, v2) = v7 & vfindColType(v4, v2) % 106.95/14.93 | = v5 & visSomeFType(v5) = 0 & visSomeTType(v7) = 0 & % 106.95/14.93 | vgetFType(v5) = v8 & vgetTType(v7) = v9 & vacons(v4, v6) = v1 & % 106.95/14.93 | vsomeTType(v10) = v3 & vttcons(v4, v8, v9) = v10 & vOptFType(v5) % 106.95/14.93 | & vTType(v10) & vTType(v9) & vOptTType(v7) & vOptTType(v3) & % 106.95/14.93 | vFType(v8) & vAttrL(v6) & vName(v4)) | ? [v4: vName] : ? [v5: % 106.95/14.93 | vOptFType] : ? [v6: vAttrL] : ? [v7: vOptTType] : ? [v8: any] % 106.95/14.93 | : ? [v9: any] : (v3 = vnoTType & vprojectTypeAttrL(v6, v2) = v7 & % 106.95/14.93 | vfindColType(v4, v2) = v5 & visSomeFType(v5) = v8 & % 106.95/14.93 | visSomeTType(v7) = v9 & vacons(v4, v6) = v1 & vOptFType(v5) & % 106.95/14.93 | vOptTType(v7) & vAttrL(v6) & vName(v4) & ( ~ (v9 = 0) | ~ (v8 = % 106.95/14.93 | 0))) | (v3 = v0 & v1 = vaempty))) % 106.95/14.93 | % 106.95/14.93 | ALPHA: (projectColsProgress-acons-IH0) implies: % 106.95/14.93 | (22) ! [v0: vTType] : ! [v1: vRawTable] : ! [v2: vAttrL] : ! [v3: % 106.95/14.93 | vTType] : ! [v4: vOptTType] : ! [v5: vOptRawTable] : ( ~ % 106.95/14.93 | (vprojectTypeAttrL(val1, v0) = v4) | ~ (vprojectCols(val1, v2, v1) % 106.95/14.93 | = v5) | ~ (vsomeTType(v3) = v4) | ~ vTType(v3) | ~ vTType(v0) | % 106.95/14.93 | ~ vRawTable(v1) | ~ vAttrL(v2) | ? [v6: any] : ? [v7: any] : % 106.95/14.93 | (vwelltypedRawtable(v0, v1) = v6 & vmatchingAttrL(v0, v2) = v7 & ( ~ % 106.95/14.93 | (v7 = 0) | ~ (v6 = 0))) | ? [v6: vRawTable] : % 106.95/14.93 | (vsomeRawTable(v6) = v5 & vOptRawTable(v5) & vRawTable(v6))) % 106.95/14.93 | % 106.95/14.93 | ALPHA: (projectColsProgress-acons-isSomeRawTable-isSomeRawTable-False) % 106.95/14.93 | implies: % 106.95/14.93 | (23) vAttrL(val1) % 106.95/14.93 | (24) ? [v0: vAttrL] : ? [v1: vRawTable] : ? [v2: vTType] : ? [v3: % 106.95/14.93 | vAttrL] : ? [v4: vName] : ? [v5: vTType] : ? [v6: vOptRawTable] : % 106.95/14.93 | ? [v7: any] : ? [v8: vOptRawTable] : ? [v9: any] : ? [v10: vAttrL] % 106.95/14.93 | : ? [v11: vOptTType] : ? [v12: vOptRawTable] : % 106.95/14.93 | (vprojectTypeAttrL(v10, v5) = v11 & vprojectCols(v10, v0, v1) = v12 & % 106.95/14.93 | vprojectCols(v3, val1, v1) = v8 & vfindCol(v4, val1, v1) = v6 & % 106.95/14.93 | visSomeRawTable(v8) = v9 & visSomeRawTable(v6) = v7 & % 106.95/14.93 | vwelltypedRawtable(v5, v1) = 0 & vmatchingAttrL(v5, v0) = 0 & % 106.95/14.93 | vacons(v4, val1) = v10 & vsomeTType(v2) = v11 & vTType(v5) & % 106.95/14.93 | vTType(v2) & vOptTType(v11) & vOptRawTable(v12) & vOptRawTable(v8) & % 106.95/14.93 | vOptRawTable(v6) & vRawTable(v1) & vAttrL(v10) & vAttrL(v3) & % 106.95/14.93 | vAttrL(v0) & vName(v4) & ! [v13: vRawTable] : ( ~ % 106.95/14.93 | (vsomeRawTable(v13) = v12) | ~ vRawTable(v13)) & ( ~ (v9 = 0) | % 106.95/14.93 | ~ (v7 = 0))) % 106.95/14.93 | % 106.95/14.93 | ALPHA: (function-axioms) implies: % 106.95/14.93 | (25) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = % 106.95/14.93 | v0 | ~ (vprojectFirstRaw(v2) = v1) | ~ (vprojectFirstRaw(v2) = % 106.95/14.93 | v0)) % 106.95/14.93 | (26) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = % 106.95/14.93 | v0 | ~ (vdropFirstColRaw(v2) = v1) | ~ (vdropFirstColRaw(v2) = % 106.95/14.93 | v0)) % 106.95/14.93 | (27) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 106.95/14.93 | vOptTType] : (v1 = v0 | ~ (visSomeTType(v2) = v1) | ~ % 106.95/14.93 | (visSomeTType(v2) = v0)) % 106.95/14.93 | (28) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = % 106.95/14.93 | v0 | ~ (vprojectEmptyCol(v2) = v1) | ~ (vprojectEmptyCol(v2) = % 106.95/14.93 | v0)) % 106.95/14.93 | (29) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: % 106.95/14.93 | vRow] : (v1 = v0 | ~ (vtcons(v3, v2) = v1) | ~ (vtcons(v3, v2) = % 106.95/14.93 | v0)) % 106.95/14.93 | (30) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 106.95/14.93 | vAttrL] : ! [v3: vTType] : (v1 = v0 | ~ (vmatchingAttrL(v3, v2) = % 106.95/14.93 | v1) | ~ (vmatchingAttrL(v3, v2) = v0)) % 106.95/14.93 | (31) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 106.95/14.93 | vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ (vwelltypedRawtable(v3, % 106.95/14.93 | v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) % 106.95/14.93 | (32) ! [v0: vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: % 106.95/14.93 | vName] : (v1 = v0 | ~ (vfindColType(v3, v2) = v1) | ~ % 106.95/14.93 | (vfindColType(v3, v2) = v0)) % 106.95/14.93 | (33) ! [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: % 106.95/14.93 | vAttrL] : (v1 = v0 | ~ (vprojectTypeAttrL(v3, v2) = v1) | ~ % 106.95/14.93 | (vprojectTypeAttrL(v3, v2) = v0)) % 106.95/14.93 | % 106.95/14.93 | DELTA: instantiating (12) with fresh symbol all_311_0 gives: % 106.95/14.93 | (34) ~ (all_311_0 = 0) & visSomeTType(vnoTType) = all_311_0 % 106.95/14.93 | % 106.95/14.93 | ALPHA: (34) implies: % 106.95/14.93 | (35) ~ (all_311_0 = 0) % 106.95/14.93 | (36) visSomeTType(vnoTType) = all_311_0 % 106.95/14.93 | % 106.95/14.93 | DELTA: instantiating (10) with fresh symbol all_335_0 gives: % 106.95/14.94 | (37) vtcons(vrempty, vtempty) = all_335_0 & vRawTable(all_335_0) & ! [v0: % 106.95/14.94 | vRawTable] : ! [v1: vRawTable] : ! [v2: int] : (v2 = all_335_0 | % 106.95/14.94 | ~ (vattachColToFrontRaw(v0, v1) = v2) | ~ vRawTable(v1) | ~ % 106.95/14.94 | vRawTable(v0) | (v1 = vtempty & v0 = vtempty) | ( ? [v3: vVal] : ? % 106.95/14.94 | [v4: vRawTable] : ? [v5: vRow] : (vtcons(v5, v4) = v0 & % 106.95/14.94 | vrcons(v3, vrempty) = v5 & vVal(v3) & vRawTable(v4) & vRow(v5)) % 106.95/14.94 | & ? [v3: vRow] : ? [v4: vRawTable] : (vtcons(v3, v4) = v1 & % 106.95/14.94 | vRawTable(v4) & vRow(v3)))) % 106.95/14.94 | % 106.95/14.94 | ALPHA: (37) implies: % 106.95/14.94 | (38) vtcons(vrempty, vtempty) = all_335_0 % 106.95/14.94 | % 106.95/14.94 | DELTA: instantiating (24) with fresh symbols all_340_0, all_340_1, all_340_2, % 106.95/14.94 | all_340_3, all_340_4, all_340_5, all_340_6, all_340_7, all_340_8, % 106.95/14.94 | all_340_9, all_340_10, all_340_11, all_340_12 gives: % 106.95/14.94 | (39) vprojectTypeAttrL(all_340_2, all_340_7) = all_340_1 & % 106.95/14.94 | vprojectCols(all_340_2, all_340_12, all_340_11) = all_340_0 & % 106.95/14.94 | vprojectCols(all_340_9, val1, all_340_11) = all_340_4 & % 106.95/14.94 | vfindCol(all_340_8, val1, all_340_11) = all_340_6 & % 106.95/14.94 | visSomeRawTable(all_340_4) = all_340_3 & visSomeRawTable(all_340_6) = % 106.95/14.94 | all_340_5 & vwelltypedRawtable(all_340_7, all_340_11) = 0 & % 106.95/14.94 | vmatchingAttrL(all_340_7, all_340_12) = 0 & vacons(all_340_8, val1) = % 106.95/14.94 | all_340_2 & vsomeTType(all_340_10) = all_340_1 & vTType(all_340_7) & % 106.95/14.94 | vTType(all_340_10) & vOptTType(all_340_1) & vOptRawTable(all_340_0) & % 106.95/14.94 | vOptRawTable(all_340_4) & vOptRawTable(all_340_6) & % 106.95/14.94 | vRawTable(all_340_11) & vAttrL(all_340_2) & vAttrL(all_340_9) & % 106.95/14.94 | vAttrL(all_340_12) & vName(all_340_8) & ! [v0: vRawTable] : ( ~ % 106.95/14.94 | (vsomeRawTable(v0) = all_340_0) | ~ vRawTable(v0)) & ( ~ (all_340_3 % 106.95/14.94 | = 0) | ~ (all_340_5 = 0)) % 106.95/14.94 | % 106.95/14.94 | ALPHA: (39) implies: % 106.95/14.94 | (40) vName(all_340_8) % 106.95/14.94 | (41) vAttrL(all_340_12) % 106.95/14.94 | (42) vAttrL(all_340_2) % 106.95/14.94 | (43) vRawTable(all_340_11) % 106.95/14.94 | (44) vTType(all_340_10) % 106.95/14.94 | (45) vTType(all_340_7) % 106.95/14.94 | (46) vsomeTType(all_340_10) = all_340_1 % 106.95/14.94 | (47) vacons(all_340_8, val1) = all_340_2 % 106.95/14.94 | (48) vmatchingAttrL(all_340_7, all_340_12) = 0 % 106.95/14.94 | (49) vwelltypedRawtable(all_340_7, all_340_11) = 0 % 106.95/14.94 | (50) vprojectCols(all_340_2, all_340_12, all_340_11) = all_340_0 % 106.95/14.94 | (51) vprojectTypeAttrL(all_340_2, all_340_7) = all_340_1 % 106.95/14.94 | (52) ! [v0: vRawTable] : ( ~ (vsomeRawTable(v0) = all_340_0) | ~ % 106.95/14.94 | vRawTable(v0)) % 106.95/14.94 | % 106.95/14.94 | DELTA: instantiating (11) with fresh symbol all_343_0 gives: % 106.95/14.94 | (53) vtcons(vrempty, vtempty) = all_343_0 & vRawTable(all_343_0) & ! [v0: % 106.95/14.94 | vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ( ~ % 106.95/14.94 | (vattachColToFrontRaw(v0, v1) = v2) | ~ vRawTable(v1) | ~ % 106.95/14.94 | vRawTable(v0) | ? [v3: vVal] : ? [v4: vRawTable] : ? [v5: vRow] : % 106.95/14.94 | ? [v6: vRawTable] : ? [v7: vRow] : ? [v8: vRow] : ? [v9: % 106.95/14.94 | vRawTable] : (vattachColToFrontRaw(v4, v6) = v9 & vtcons(v8, v9) = % 106.95/14.94 | v2 & vtcons(v7, v4) = v0 & vtcons(v5, v6) = v1 & vrcons(v3, v5) = % 106.95/14.94 | v8 & vrcons(v3, vrempty) = v7 & vVal(v3) & vRawTable(v9) & % 106.95/14.94 | vRawTable(v6) & vRawTable(v4) & vRawTable(v2) & vRow(v8) & % 106.95/14.94 | vRow(v7) & vRow(v5)) | (v2 = all_343_0 & ( ~ (v1 = vtempty) | ~ % 106.95/14.94 | (v0 = vtempty)) & ( ! [v3: vVal] : ! [v4: vRawTable] : ! [v5: % 106.95/14.94 | vRow] : ( ~ (vtcons(v5, v4) = v0) | ~ (vrcons(v3, vrempty) = % 106.95/14.94 | v5) | ~ vVal(v3) | ~ vRawTable(v4)) | ! [v3: vRow] : ! % 106.95/14.94 | [v4: vRawTable] : ( ~ (vtcons(v3, v4) = v1) | ~ vRawTable(v4) | % 106.95/14.94 | ~ vRow(v3)))) | (v2 = vtempty & v1 = vtempty & v0 = vtempty)) % 106.95/14.94 | % 106.95/14.94 | ALPHA: (53) implies: % 106.95/14.94 | (54) vtcons(vrempty, vtempty) = all_343_0 % 106.95/14.94 | % 106.95/14.94 | DELTA: instantiating (21) with fresh symbol all_346_0 gives: % 106.95/14.94 | (55) vsomeTType(vttempty) = all_346_0 & vOptTType(all_346_0) & ! [v0: % 106.95/14.94 | vAttrL] : ! [v1: vTType] : ! [v2: vOptTType] : ( ~ % 106.95/14.94 | (vprojectTypeAttrL(v0, v1) = v2) | ~ vTType(v1) | ~ vAttrL(v0) | % 106.95/14.94 | ? [v3: vName] : ? [v4: vOptFType] : ? [v5: vAttrL] : ? [v6: % 106.95/14.94 | vOptTType] : ? [v7: vFType] : ? [v8: vTType] : ? [v9: vTType] : % 106.95/14.94 | (vprojectTypeAttrL(v5, v1) = v6 & vfindColType(v3, v1) = v4 & % 106.95/14.94 | visSomeFType(v4) = 0 & visSomeTType(v6) = 0 & vgetFType(v4) = v7 & % 106.95/14.94 | vgetTType(v6) = v8 & vacons(v3, v5) = v0 & vsomeTType(v9) = v2 & % 106.95/14.94 | vttcons(v3, v7, v8) = v9 & vOptFType(v4) & vTType(v9) & vTType(v8) % 106.95/14.94 | & vOptTType(v6) & vOptTType(v2) & vFType(v7) & vAttrL(v5) & % 106.95/14.94 | vName(v3)) | ? [v3: vName] : ? [v4: vOptFType] : ? [v5: vAttrL] % 106.95/14.94 | : ? [v6: vOptTType] : ? [v7: any] : ? [v8: any] : (v2 = vnoTType % 106.95/14.94 | & vprojectTypeAttrL(v5, v1) = v6 & vfindColType(v3, v1) = v4 & % 106.95/14.94 | visSomeFType(v4) = v7 & visSomeTType(v6) = v8 & vacons(v3, v5) = % 106.95/14.94 | v0 & vOptFType(v4) & vOptTType(v6) & vAttrL(v5) & vName(v3) & ( ~ % 106.95/14.94 | (v8 = 0) | ~ (v7 = 0))) | (v2 = all_346_0 & v0 = vaempty)) % 106.95/14.94 | % 106.95/14.94 | ALPHA: (55) implies: % 106.95/14.94 | (56) ! [v0: vAttrL] : ! [v1: vTType] : ! [v2: vOptTType] : ( ~ % 106.95/14.94 | (vprojectTypeAttrL(v0, v1) = v2) | ~ vTType(v1) | ~ vAttrL(v0) | % 106.95/14.94 | ? [v3: vName] : ? [v4: vOptFType] : ? [v5: vAttrL] : ? [v6: % 106.95/14.94 | vOptTType] : ? [v7: vFType] : ? [v8: vTType] : ? [v9: vTType] : % 106.95/14.94 | (vprojectTypeAttrL(v5, v1) = v6 & vfindColType(v3, v1) = v4 & % 106.95/14.94 | visSomeFType(v4) = 0 & visSomeTType(v6) = 0 & vgetFType(v4) = v7 & % 106.95/14.94 | vgetTType(v6) = v8 & vacons(v3, v5) = v0 & vsomeTType(v9) = v2 & % 106.95/14.94 | vttcons(v3, v7, v8) = v9 & vOptFType(v4) & vTType(v9) & vTType(v8) % 106.95/14.94 | & vOptTType(v6) & vOptTType(v2) & vFType(v7) & vAttrL(v5) & % 106.95/14.94 | vName(v3)) | ? [v3: vName] : ? [v4: vOptFType] : ? [v5: vAttrL] % 106.95/14.94 | : ? [v6: vOptTType] : ? [v7: any] : ? [v8: any] : (v2 = vnoTType % 106.95/14.94 | & vprojectTypeAttrL(v5, v1) = v6 & vfindColType(v3, v1) = v4 & % 106.95/14.94 | visSomeFType(v4) = v7 & visSomeTType(v6) = v8 & vacons(v3, v5) = % 106.95/14.94 | v0 & vOptFType(v4) & vOptTType(v6) & vAttrL(v5) & vName(v3) & ( ~ % 106.95/14.94 | (v8 = 0) | ~ (v7 = 0))) | (v2 = all_346_0 & v0 = vaempty)) % 106.95/14.94 | % 106.95/14.95 | GROUND_INST: instantiating (29) with all_335_0, all_343_0, vtempty, vrempty, % 106.95/14.95 | simplifying with (38), (54) gives: % 106.95/14.95 | (57) all_343_0 = all_335_0 % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (isSomeTType-1) with all_340_10, all_340_1, % 106.95/14.95 | simplifying with (44), (46) gives: % 106.95/14.95 | (58) visSomeTType(all_340_1) = 0 % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (7) with vtempty, all_335_0, simplifying with (19), % 106.95/14.95 | (38) gives: % 106.95/14.95 | (59) ? [v0: vRawTable] : ? [v1: vRawTable] : (vdropFirstColRaw(all_335_0) % 106.95/14.95 | = v0 & vdropFirstColRaw(vtempty) = v1 & vtcons(vrempty, v1) = v0 & % 106.95/14.95 | vRawTable(v1) & vRawTable(v0)) % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (5) with vtempty, all_335_0, simplifying with (19), % 106.95/14.95 | (38) gives: % 106.95/14.95 | (60) ? [v0: vRawTable] : ? [v1: vRawTable] : (vprojectFirstRaw(all_335_0) % 106.95/14.95 | = v0 & vprojectFirstRaw(vtempty) = v1 & vtcons(vrempty, v1) = v0 & % 106.95/14.95 | vRawTable(v1) & vRawTable(v0)) % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (14) with vrempty, vtempty, all_335_0, simplifying % 106.95/14.95 | with (15), (19), (38) gives: % 106.95/14.95 | (61) ? [v0: vRawTable] : ? [v1: vRawTable] : (vprojectEmptyCol(all_335_0) % 106.95/14.95 | = v0 & vprojectEmptyCol(vtempty) = v1 & vtcons(vrempty, v1) = v0 & % 106.95/14.95 | vRawTable(v1) & vRawTable(v0)) % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (17) with all_340_8, all_340_12, all_340_11, val1, % 106.95/14.95 | all_340_2, all_340_0, simplifying with (23), (40), (41), (43), % 106.95/14.95 | (47), (50) gives: % 106.95/14.95 | (62) all_340_0 = vnoRawTable | ? [v0: vOptRawTable] : ? [v1: % 106.95/14.95 | vOptRawTable] : (vprojectCols(val1, all_340_12, all_340_11) = v1 & % 106.95/14.95 | vfindCol(all_340_8, all_340_12, all_340_11) = v0 & % 106.95/14.95 | visSomeRawTable(v1) = 0 & visSomeRawTable(v0) = 0 & vOptRawTable(v1) % 106.95/14.95 | & vOptRawTable(v0)) % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (18) with all_340_2, all_340_12, all_340_11, % 106.95/14.95 | all_340_0, simplifying with (41), (42), (43), (50) gives: % 106.95/14.95 | (63) ? [v0: vOptRawTable] : ? [v1: vOptRawTable] : ? [v2: vAttrL] : ? % 106.95/14.95 | [v3: vName] : ? [v4: vRawTable] : ? [v5: vRawTable] : ? [v6: % 106.95/14.95 | vRawTable] : (vprojectCols(v2, all_340_12, all_340_11) = v0 & % 106.95/14.95 | vfindCol(v3, all_340_12, all_340_11) = v1 & vattachColToFrontRaw(v4, % 106.95/14.95 | v5) = v6 & visSomeRawTable(v1) = 0 & visSomeRawTable(v0) = 0 & % 106.95/14.95 | vgetRawTable(v1) = v4 & vgetRawTable(v0) = v5 & vacons(v3, v2) = % 106.95/14.95 | all_340_2 & vsomeRawTable(v6) = all_340_0 & vOptRawTable(v1) & % 106.95/14.95 | vOptRawTable(v0) & vOptRawTable(all_340_0) & vRawTable(v6) & % 106.95/14.95 | vRawTable(v5) & vRawTable(v4) & vAttrL(v2) & vName(v3)) | ? [v0: % 106.95/14.95 | vOptRawTable] : ? [v1: vOptRawTable] : ? [v2: vAttrL] : ? [v3: % 106.95/14.95 | vName] : ? [v4: any] : ? [v5: any] : (all_340_0 = vnoRawTable & % 106.95/14.95 | vprojectCols(v2, all_340_12, all_340_11) = v0 & vfindCol(v3, % 106.95/14.95 | all_340_12, all_340_11) = v1 & visSomeRawTable(v1) = v4 & % 106.95/14.95 | visSomeRawTable(v0) = v5 & vacons(v3, v2) = all_340_2 & % 106.95/14.95 | vOptRawTable(v1) & vOptRawTable(v0) & vAttrL(v2) & vName(v3) & ( ~ % 106.95/14.95 | (v5 = 0) | ~ (v4 = 0))) | ? [v0: vRawTable] : (all_340_2 = % 106.95/14.95 | vaempty & vprojectEmptyCol(all_340_11) = v0 & vsomeRawTable(v0) = % 106.95/14.95 | all_340_0 & vOptRawTable(all_340_0) & vRawTable(v0)) % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (20) with all_340_8, all_340_7, val1, all_340_2, % 106.95/14.95 | all_340_1, simplifying with (23), (40), (45), (47), (51) gives: % 106.95/14.95 | (64) all_340_1 = vnoTType | ? [v0: vOptFType] : ? [v1: vOptTType] : % 106.95/14.95 | (vprojectTypeAttrL(val1, all_340_7) = v1 & vfindColType(all_340_8, % 106.95/14.95 | all_340_7) = v0 & visSomeFType(v0) = 0 & visSomeTType(v1) = 0 & % 106.95/14.95 | vOptFType(v0) & vOptTType(v1)) % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (56) with all_340_2, all_340_7, all_340_1, % 106.95/14.95 | simplifying with (42), (45), (51) gives: % 106.95/14.95 | (65) ? [v0: vName] : ? [v1: vOptFType] : ? [v2: vAttrL] : ? [v3: % 106.95/14.95 | vOptTType] : ? [v4: vFType] : ? [v5: vTType] : ? [v6: vTType] : % 106.95/14.95 | (vprojectTypeAttrL(v2, all_340_7) = v3 & vfindColType(v0, all_340_7) = % 106.95/14.95 | v1 & visSomeFType(v1) = 0 & visSomeTType(v3) = 0 & vgetFType(v1) = % 106.95/14.95 | v4 & vgetTType(v3) = v5 & vacons(v0, v2) = all_340_2 & % 106.95/14.95 | vsomeTType(v6) = all_340_1 & vttcons(v0, v4, v5) = v6 & % 106.95/14.95 | vOptFType(v1) & vTType(v6) & vTType(v5) & vOptTType(v3) & % 106.95/14.95 | vOptTType(all_340_1) & vFType(v4) & vAttrL(v2) & vName(v0)) | ? % 106.95/14.95 | [v0: vName] : ? [v1: vOptFType] : ? [v2: vAttrL] : ? [v3: % 106.95/14.95 | vOptTType] : ? [v4: any] : ? [v5: any] : (all_340_1 = vnoTType & % 106.95/14.95 | vprojectTypeAttrL(v2, all_340_7) = v3 & vfindColType(v0, all_340_7) % 106.95/14.95 | = v1 & visSomeFType(v1) = v4 & visSomeTType(v3) = v5 & vacons(v0, % 106.95/14.95 | v2) = all_340_2 & vOptFType(v1) & vOptTType(v3) & vAttrL(v2) & % 106.95/14.95 | vName(v0) & ( ~ (v5 = 0) | ~ (v4 = 0))) | (all_346_0 = all_340_1 & % 106.95/14.95 | all_340_2 = vaempty) % 106.95/14.95 | % 106.95/14.95 | DELTA: instantiating (61) with fresh symbols all_359_0, all_359_1 gives: % 106.95/14.95 | (66) vprojectEmptyCol(all_335_0) = all_359_1 & vprojectEmptyCol(vtempty) = % 106.95/14.95 | all_359_0 & vtcons(vrempty, all_359_0) = all_359_1 & % 106.95/14.95 | vRawTable(all_359_0) & vRawTable(all_359_1) % 106.95/14.95 | % 106.95/14.95 | ALPHA: (66) implies: % 106.95/14.95 | (67) vRawTable(all_359_1) % 106.95/14.95 | (68) vtcons(vrempty, all_359_0) = all_359_1 % 106.95/14.95 | (69) vprojectEmptyCol(vtempty) = all_359_0 % 106.95/14.95 | (70) vprojectEmptyCol(all_335_0) = all_359_1 % 106.95/14.95 | % 106.95/14.95 | DELTA: instantiating (60) with fresh symbols all_361_0, all_361_1 gives: % 106.95/14.95 | (71) vprojectFirstRaw(all_335_0) = all_361_1 & vprojectFirstRaw(vtempty) = % 106.95/14.95 | all_361_0 & vtcons(vrempty, all_361_0) = all_361_1 & % 106.95/14.95 | vRawTable(all_361_0) & vRawTable(all_361_1) % 106.95/14.95 | % 106.95/14.95 | ALPHA: (71) implies: % 106.95/14.95 | (72) vtcons(vrempty, all_361_0) = all_361_1 % 106.95/14.95 | (73) vprojectFirstRaw(vtempty) = all_361_0 % 106.95/14.95 | % 106.95/14.95 | DELTA: instantiating (59) with fresh symbols all_363_0, all_363_1 gives: % 106.95/14.95 | (74) vdropFirstColRaw(all_335_0) = all_363_1 & vdropFirstColRaw(vtempty) = % 106.95/14.95 | all_363_0 & vtcons(vrempty, all_363_0) = all_363_1 & % 106.95/14.95 | vRawTable(all_363_0) & vRawTable(all_363_1) % 106.95/14.95 | % 106.95/14.95 | ALPHA: (74) implies: % 106.95/14.95 | (75) vtcons(vrempty, all_363_0) = all_363_1 % 106.95/14.95 | (76) vdropFirstColRaw(vtempty) = all_363_0 % 106.95/14.95 | (77) vdropFirstColRaw(all_335_0) = all_363_1 % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (25) with vtempty, all_361_0, vtempty, simplifying % 106.95/14.95 | with (4), (73) gives: % 106.95/14.95 | (78) all_361_0 = vtempty % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (26) with vtempty, all_363_0, vtempty, simplifying % 106.95/14.95 | with (6), (76) gives: % 106.95/14.95 | (79) all_363_0 = vtempty % 106.95/14.95 | % 106.95/14.95 | GROUND_INST: instantiating (28) with vtempty, all_359_0, vtempty, simplifying % 106.95/14.95 | with (13), (69) gives: % 106.95/14.95 | (80) all_359_0 = vtempty % 106.95/14.95 | % 106.95/14.96 | REDUCE: (75), (79) imply: % 106.95/14.96 | (81) vtcons(vrempty, vtempty) = all_363_1 % 106.95/14.96 | % 106.95/14.96 | REDUCE: (72), (78) imply: % 106.95/14.96 | (82) vtcons(vrempty, vtempty) = all_361_1 % 106.95/14.96 | % 106.95/14.96 | REDUCE: (68), (80) imply: % 106.95/14.96 | (83) vtcons(vrempty, vtempty) = all_359_1 % 106.95/14.96 | % 106.95/14.96 | GROUND_INST: instantiating (29) with all_335_0, all_363_1, vtempty, vrempty, % 106.95/14.96 | simplifying with (38), (81) gives: % 106.95/14.96 | (84) all_363_1 = all_335_0 % 106.95/14.96 | % 106.95/14.96 | GROUND_INST: instantiating (29) with all_361_1, all_363_1, vtempty, vrempty, % 106.95/14.96 | simplifying with (81), (82) gives: % 106.95/14.96 | (85) all_363_1 = all_361_1 % 106.95/14.96 | % 106.95/14.96 | GROUND_INST: instantiating (29) with all_359_1, all_363_1, vtempty, vrempty, % 106.95/14.96 | simplifying with (81), (83) gives: % 106.95/14.96 | (86) all_363_1 = all_359_1 % 106.95/14.96 | % 106.95/14.96 | COMBINE_EQS: (85), (86) imply: % 106.95/14.96 | (87) all_361_1 = all_359_1 % 106.95/14.96 | % 106.95/14.96 | COMBINE_EQS: (84), (85) imply: % 106.95/14.96 | (88) all_361_1 = all_335_0 % 106.95/14.96 | % 106.95/14.96 | COMBINE_EQS: (87), (88) imply: % 106.95/14.96 | (89) all_359_1 = all_335_0 % 106.95/14.96 | % 106.95/14.96 | SIMP: (89) implies: % 106.95/14.96 | (90) all_359_1 = all_335_0 % 106.95/14.96 | % 106.95/14.96 | REDUCE: (70), (90) imply: % 106.95/14.96 | (91) vprojectEmptyCol(all_335_0) = all_335_0 % 106.95/14.96 | % 106.95/14.96 | REDUCE: (77), (84) imply: % 106.95/14.96 | (92) vdropFirstColRaw(all_335_0) = all_335_0 % 106.95/14.96 | % 106.95/14.96 | REDUCE: (67), (90) imply: % 106.95/14.96 | (93) vRawTable(all_335_0) % 106.95/14.96 | % 106.95/14.96 | GROUND_INST: instantiating (8) with all_335_0, all_335_0, simplifying with % 106.95/14.96 | (92), (93) gives: % 106.95/14.96 | (94) all_335_0 = vtempty | ? [v0: vVal] : ? [v1: vRow] : ? [v2: % 106.95/14.96 | vRawTable] : ? [v3: vRow] : ? [v4: vRawTable] : % 106.95/14.96 | (vdropFirstColRaw(v2) = v4 & vtcons(v3, v2) = all_335_0 & vtcons(v1, % 106.95/14.96 | v4) = all_335_0 & vrcons(v0, v1) = v3 & vVal(v0) & vRawTable(v4) & % 106.95/14.96 | vRawTable(v2) & vRow(v3) & vRow(v1)) | ? [v0: vRawTable] : ? [v1: % 106.95/14.96 | vRawTable] : (vdropFirstColRaw(v0) = v1 & vtcons(vrempty, v1) = % 106.95/14.96 | all_335_0 & vtcons(vrempty, v0) = all_335_0 & vRawTable(v1) & % 106.95/14.96 | vRawTable(v0)) % 106.95/14.96 | % 106.95/14.96 | GROUND_INST: instantiating (16) with all_335_0, all_335_0, simplifying with % 106.95/14.96 | (91), (93) gives: % 106.95/14.96 | (95) all_335_0 = vtempty | ? [v0: vRow] : ? [v1: vRawTable] : ? [v2: % 106.95/14.96 | vRawTable] : (vprojectEmptyCol(v1) = v2 & vtcons(v0, v1) = all_335_0 % 106.95/14.96 | & vtcons(vrempty, v2) = all_335_0 & vRawTable(v2) & vRawTable(v1) & % 106.95/14.96 | vRow(v0)) % 106.95/14.96 | % 106.95/14.96 | BETA: splitting (63) gives: % 106.95/14.96 | % 106.95/14.96 | Case 1: % 106.95/14.96 | | % 106.95/14.96 | | (96) ? [v0: vOptRawTable] : ? [v1: vOptRawTable] : ? [v2: vAttrL] : ? % 106.95/14.96 | | [v3: vName] : ? [v4: vRawTable] : ? [v5: vRawTable] : ? [v6: % 106.95/14.96 | | vRawTable] : (vprojectCols(v2, all_340_12, all_340_11) = v0 & % 106.95/14.96 | | vfindCol(v3, all_340_12, all_340_11) = v1 & % 106.95/14.96 | | vattachColToFrontRaw(v4, v5) = v6 & visSomeRawTable(v1) = 0 & % 106.95/14.96 | | visSomeRawTable(v0) = 0 & vgetRawTable(v1) = v4 & vgetRawTable(v0) % 106.95/14.96 | | = v5 & vacons(v3, v2) = all_340_2 & vsomeRawTable(v6) = all_340_0 % 106.95/14.96 | | & vOptRawTable(v1) & vOptRawTable(v0) & vOptRawTable(all_340_0) & % 106.95/14.96 | | vRawTable(v6) & vRawTable(v5) & vRawTable(v4) & vAttrL(v2) & % 106.95/14.96 | | vName(v3)) % 106.95/14.96 | | % 106.95/14.96 | | DELTA: instantiating (96) with fresh symbols all_544_0, all_544_1, % 106.95/14.96 | | all_544_2, all_544_3, all_544_4, all_544_5, all_544_6 gives: % 106.95/14.96 | | (97) vprojectCols(all_544_4, all_340_12, all_340_11) = all_544_6 & % 106.95/14.96 | | vfindCol(all_544_3, all_340_12, all_340_11) = all_544_5 & % 106.95/14.96 | | vattachColToFrontRaw(all_544_2, all_544_1) = all_544_0 & % 106.95/14.96 | | visSomeRawTable(all_544_5) = 0 & visSomeRawTable(all_544_6) = 0 & % 106.95/14.96 | | vgetRawTable(all_544_5) = all_544_2 & vgetRawTable(all_544_6) = % 106.95/14.96 | | all_544_1 & vacons(all_544_3, all_544_4) = all_340_2 & % 106.95/14.96 | | vsomeRawTable(all_544_0) = all_340_0 & vOptRawTable(all_544_5) & % 106.95/14.96 | | vOptRawTable(all_544_6) & vOptRawTable(all_340_0) & % 106.95/14.96 | | vRawTable(all_544_0) & vRawTable(all_544_1) & vRawTable(all_544_2) & % 106.95/14.96 | | vAttrL(all_544_4) & vName(all_544_3) % 106.95/14.96 | | % 106.95/14.96 | | ALPHA: (97) implies: % 106.95/14.96 | | (98) vRawTable(all_544_0) % 106.95/14.96 | | (99) vsomeRawTable(all_544_0) = all_340_0 % 106.95/14.96 | | % 106.95/14.96 | | BETA: splitting (62) gives: % 106.95/14.96 | | % 106.95/14.96 | | Case 1: % 106.95/14.96 | | | % 106.95/14.96 | | | (100) all_340_0 = vnoRawTable % 106.95/14.96 | | | % 106.95/14.96 | | | REDUCE: (99), (100) imply: % 106.95/14.96 | | | (101) vsomeRawTable(all_544_0) = vnoRawTable % 106.95/14.96 | | | % 106.95/14.96 | | | GROUND_INST: instantiating (1) with all_544_0, simplifying with (98), % 106.95/14.96 | | | (101) gives: % 106.95/14.96 | | | (102) $false % 106.95/14.96 | | | % 106.95/14.96 | | | CLOSE: (102) is inconsistent. % 106.95/14.96 | | | % 106.95/14.96 | | Case 2: % 106.95/14.96 | | | % 106.95/14.96 | | | (103) ~ (all_340_0 = vnoRawTable) % 106.95/14.96 | | | % 106.95/14.96 | | | BETA: splitting (63) gives: % 106.95/14.96 | | | % 106.95/14.96 | | | Case 1: % 106.95/14.96 | | | | % 106.95/14.96 | | | | % 106.95/14.96 | | | | DELTA: instantiating (96) with fresh symbols all_550_0, all_550_1, % 106.95/14.96 | | | | all_550_2, all_550_3, all_550_4, all_550_5, all_550_6 gives: % 106.95/14.96 | | | | (104) vprojectCols(all_550_4, all_340_12, all_340_11) = all_550_6 & % 106.95/14.96 | | | | vfindCol(all_550_3, all_340_12, all_340_11) = all_550_5 & % 106.95/14.96 | | | | vattachColToFrontRaw(all_550_2, all_550_1) = all_550_0 & % 106.95/14.96 | | | | visSomeRawTable(all_550_5) = 0 & visSomeRawTable(all_550_6) = 0 % 106.95/14.96 | | | | & vgetRawTable(all_550_5) = all_550_2 & vgetRawTable(all_550_6) % 106.95/14.96 | | | | = all_550_1 & vacons(all_550_3, all_550_4) = all_340_2 & % 106.95/14.96 | | | | vsomeRawTable(all_550_0) = all_340_0 & vOptRawTable(all_550_5) % 106.95/14.96 | | | | & vOptRawTable(all_550_6) & vOptRawTable(all_340_0) & % 106.95/14.96 | | | | vRawTable(all_550_0) & vRawTable(all_550_1) & % 106.95/14.96 | | | | vRawTable(all_550_2) & vAttrL(all_550_4) & vName(all_550_3) % 106.95/14.96 | | | | % 106.95/14.96 | | | | ALPHA: (104) implies: % 106.95/14.96 | | | | (105) vRawTable(all_550_0) % 106.95/14.96 | | | | (106) vsomeRawTable(all_550_0) = all_340_0 % 106.95/14.96 | | | | % 106.95/14.96 | | | | GROUND_INST: instantiating (52) with all_550_0, simplifying with (105), % 106.95/14.96 | | | | (106) gives: % 106.95/14.96 | | | | (107) $false % 106.95/14.96 | | | | % 106.95/14.96 | | | | CLOSE: (107) is inconsistent. % 106.95/14.96 | | | | % 106.95/14.96 | | | Case 2: % 106.95/14.96 | | | | % 106.95/14.97 | | | | (108) ? [v0: vOptRawTable] : ? [v1: vOptRawTable] : ? [v2: vAttrL] % 106.95/14.97 | | | | : ? [v3: vName] : ? [v4: any] : ? [v5: any] : (all_340_0 = % 106.95/14.97 | | | | vnoRawTable & vprojectCols(v2, all_340_12, all_340_11) = v0 & % 106.95/14.97 | | | | vfindCol(v3, all_340_12, all_340_11) = v1 & % 106.95/14.97 | | | | visSomeRawTable(v1) = v4 & visSomeRawTable(v0) = v5 & % 106.95/14.97 | | | | vacons(v3, v2) = all_340_2 & vOptRawTable(v1) & % 106.95/14.97 | | | | vOptRawTable(v0) & vAttrL(v2) & vName(v3) & ( ~ (v5 = 0) | ~ % 106.95/14.97 | | | | (v4 = 0))) | ? [v0: vRawTable] : (all_340_2 = vaempty & % 106.95/14.97 | | | | vprojectEmptyCol(all_340_11) = v0 & vsomeRawTable(v0) = % 106.95/14.97 | | | | all_340_0 & vOptRawTable(all_340_0) & vRawTable(v0)) % 106.95/14.97 | | | | % 106.95/14.97 | | | | BETA: splitting (108) gives: % 106.95/14.97 | | | | % 106.95/14.97 | | | | Case 1: % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | (109) ? [v0: vOptRawTable] : ? [v1: vOptRawTable] : ? [v2: % 106.95/14.97 | | | | | vAttrL] : ? [v3: vName] : ? [v4: any] : ? [v5: any] : % 106.95/14.97 | | | | | (all_340_0 = vnoRawTable & vprojectCols(v2, all_340_12, % 106.95/14.97 | | | | | all_340_11) = v0 & vfindCol(v3, all_340_12, all_340_11) = % 106.95/14.97 | | | | | v1 & visSomeRawTable(v1) = v4 & visSomeRawTable(v0) = v5 & % 106.95/14.97 | | | | | vacons(v3, v2) = all_340_2 & vOptRawTable(v1) & % 106.95/14.97 | | | | | vOptRawTable(v0) & vAttrL(v2) & vName(v3) & ( ~ (v5 = 0) | % 106.95/14.97 | | | | | ~ (v4 = 0))) % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | DELTA: instantiating (109) with fresh symbols all_550_0, all_550_1, % 106.95/14.97 | | | | | all_550_2, all_550_3, all_550_4, all_550_5 gives: % 106.95/14.97 | | | | | (110) all_340_0 = vnoRawTable & vprojectCols(all_550_3, all_340_12, % 106.95/14.97 | | | | | all_340_11) = all_550_5 & vfindCol(all_550_2, all_340_12, % 106.95/14.97 | | | | | all_340_11) = all_550_4 & visSomeRawTable(all_550_4) = % 106.95/14.97 | | | | | all_550_1 & visSomeRawTable(all_550_5) = all_550_0 & % 106.95/14.97 | | | | | vacons(all_550_2, all_550_3) = all_340_2 & % 106.95/14.97 | | | | | vOptRawTable(all_550_4) & vOptRawTable(all_550_5) & % 106.95/14.97 | | | | | vAttrL(all_550_3) & vName(all_550_2) & ( ~ (all_550_0 = 0) | % 106.95/14.97 | | | | | ~ (all_550_1 = 0)) % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | ALPHA: (110) implies: % 106.95/14.97 | | | | | (111) all_340_0 = vnoRawTable % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | REDUCE: (103), (111) imply: % 106.95/14.97 | | | | | (112) $false % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | CLOSE: (112) is inconsistent. % 106.95/14.97 | | | | | % 106.95/14.97 | | | | Case 2: % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | (113) ? [v0: vRawTable] : (all_340_2 = vaempty & % 106.95/14.97 | | | | | vprojectEmptyCol(all_340_11) = v0 & vsomeRawTable(v0) = % 106.95/14.97 | | | | | all_340_0 & vOptRawTable(all_340_0) & vRawTable(v0)) % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | DELTA: instantiating (113) with fresh symbol all_550_0 gives: % 106.95/14.97 | | | | | (114) all_340_2 = vaempty & vprojectEmptyCol(all_340_11) = % 106.95/14.97 | | | | | all_550_0 & vsomeRawTable(all_550_0) = all_340_0 & % 106.95/14.97 | | | | | vOptRawTable(all_340_0) & vRawTable(all_550_0) % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | ALPHA: (114) implies: % 106.95/14.97 | | | | | (115) all_340_2 = vaempty % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | REDUCE: (47), (115) imply: % 106.95/14.97 | | | | | (116) vacons(all_340_8, val1) = vaempty % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | GROUND_INST: instantiating (3) with all_340_8, val1, simplifying with % 106.95/14.97 | | | | | (23), (40), (116) gives: % 106.95/14.97 | | | | | (117) $false % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | CLOSE: (117) is inconsistent. % 106.95/14.97 | | | | | % 106.95/14.97 | | | | End of split % 106.95/14.97 | | | | % 106.95/14.97 | | | End of split % 106.95/14.97 | | | % 106.95/14.97 | | End of split % 106.95/14.97 | | % 106.95/14.97 | Case 2: % 106.95/14.97 | | % 106.95/14.97 | | (118) ? [v0: vOptRawTable] : ? [v1: vOptRawTable] : ? [v2: vAttrL] : % 106.95/14.97 | | ? [v3: vName] : ? [v4: any] : ? [v5: any] : (all_340_0 = % 106.95/14.97 | | vnoRawTable & vprojectCols(v2, all_340_12, all_340_11) = v0 & % 106.95/14.97 | | vfindCol(v3, all_340_12, all_340_11) = v1 & visSomeRawTable(v1) = % 106.95/14.97 | | v4 & visSomeRawTable(v0) = v5 & vacons(v3, v2) = all_340_2 & % 106.95/14.97 | | vOptRawTable(v1) & vOptRawTable(v0) & vAttrL(v2) & vName(v3) & ( % 106.95/14.97 | | ~ (v5 = 0) | ~ (v4 = 0))) | ? [v0: vRawTable] : (all_340_2 = % 106.95/14.97 | | vaempty & vprojectEmptyCol(all_340_11) = v0 & vsomeRawTable(v0) = % 106.95/14.97 | | all_340_0 & vOptRawTable(all_340_0) & vRawTable(v0)) % 106.95/14.97 | | % 106.95/14.97 | | BETA: splitting (118) gives: % 106.95/14.97 | | % 106.95/14.97 | | Case 1: % 106.95/14.97 | | | % 106.95/14.97 | | | (119) ? [v0: vOptRawTable] : ? [v1: vOptRawTable] : ? [v2: vAttrL] : % 106.95/14.97 | | | ? [v3: vName] : ? [v4: any] : ? [v5: any] : (all_340_0 = % 106.95/14.97 | | | vnoRawTable & vprojectCols(v2, all_340_12, all_340_11) = v0 & % 106.95/14.97 | | | vfindCol(v3, all_340_12, all_340_11) = v1 & visSomeRawTable(v1) % 106.95/14.97 | | | = v4 & visSomeRawTable(v0) = v5 & vacons(v3, v2) = all_340_2 & % 106.95/14.97 | | | vOptRawTable(v1) & vOptRawTable(v0) & vAttrL(v2) & vName(v3) & % 106.95/14.97 | | | ( ~ (v5 = 0) | ~ (v4 = 0))) % 106.95/14.97 | | | % 106.95/14.97 | | | DELTA: instantiating (119) with fresh symbols all_544_0, all_544_1, % 106.95/14.97 | | | all_544_2, all_544_3, all_544_4, all_544_5 gives: % 106.95/14.97 | | | (120) all_340_0 = vnoRawTable & vprojectCols(all_544_3, all_340_12, % 106.95/14.97 | | | all_340_11) = all_544_5 & vfindCol(all_544_2, all_340_12, % 106.95/14.97 | | | all_340_11) = all_544_4 & visSomeRawTable(all_544_4) = % 106.95/14.97 | | | all_544_1 & visSomeRawTable(all_544_5) = all_544_0 & % 106.95/14.97 | | | vacons(all_544_2, all_544_3) = all_340_2 & % 106.95/14.97 | | | vOptRawTable(all_544_4) & vOptRawTable(all_544_5) & % 106.95/14.97 | | | vAttrL(all_544_3) & vName(all_544_2) & ( ~ (all_544_0 = 0) | ~ % 106.95/14.97 | | | (all_544_1 = 0)) % 106.95/14.97 | | | % 106.95/14.97 | | | ALPHA: (120) implies: % 106.95/14.97 | | | (121) vName(all_544_2) % 106.95/14.97 | | | (122) vAttrL(all_544_3) % 106.95/14.97 | | | (123) vOptRawTable(all_544_5) % 106.95/14.97 | | | (124) vOptRawTable(all_544_4) % 106.95/14.97 | | | (125) vacons(all_544_2, all_544_3) = all_340_2 % 106.95/14.97 | | | (126) visSomeRawTable(all_544_5) = all_544_0 % 106.95/14.97 | | | (127) visSomeRawTable(all_544_4) = all_544_1 % 106.95/14.97 | | | (128) vfindCol(all_544_2, all_340_12, all_340_11) = all_544_4 % 106.95/14.97 | | | (129) vprojectCols(all_544_3, all_340_12, all_340_11) = all_544_5 % 106.95/14.97 | | | (130) ~ (all_544_0 = 0) | ~ (all_544_1 = 0) % 106.95/14.97 | | | % 106.95/14.97 | | | BETA: splitting (64) gives: % 106.95/14.97 | | | % 106.95/14.97 | | | Case 1: % 106.95/14.97 | | | | % 106.95/14.97 | | | | (131) all_340_1 = vnoTType % 106.95/14.97 | | | | % 106.95/14.97 | | | | REDUCE: (58), (131) imply: % 106.95/14.97 | | | | (132) visSomeTType(vnoTType) = 0 % 106.95/14.97 | | | | % 106.95/14.97 | | | | GROUND_INST: instantiating (27) with all_311_0, 0, vnoTType, simplifying % 106.95/14.97 | | | | with (36), (132) gives: % 106.95/14.97 | | | | (133) all_311_0 = 0 % 106.95/14.97 | | | | % 106.95/14.97 | | | | REDUCE: (35), (133) imply: % 106.95/14.97 | | | | (134) $false % 106.95/14.97 | | | | % 106.95/14.97 | | | | CLOSE: (134) is inconsistent. % 106.95/14.97 | | | | % 106.95/14.97 | | | Case 2: % 106.95/14.97 | | | | % 106.95/14.97 | | | | (135) ~ (all_340_1 = vnoTType) % 106.95/14.97 | | | | (136) ? [v0: vOptFType] : ? [v1: vOptTType] : % 106.95/14.97 | | | | (vprojectTypeAttrL(val1, all_340_7) = v1 & % 106.95/14.97 | | | | vfindColType(all_340_8, all_340_7) = v0 & visSomeFType(v0) = % 106.95/14.97 | | | | 0 & visSomeTType(v1) = 0 & vOptFType(v0) & vOptTType(v1)) % 106.95/14.97 | | | | % 106.95/14.97 | | | | DELTA: instantiating (136) with fresh symbols all_552_0, all_552_1 % 106.95/14.97 | | | | gives: % 106.95/14.97 | | | | (137) vprojectTypeAttrL(val1, all_340_7) = all_552_0 & % 106.95/14.97 | | | | vfindColType(all_340_8, all_340_7) = all_552_1 & % 106.95/14.97 | | | | visSomeFType(all_552_1) = 0 & visSomeTType(all_552_0) = 0 & % 106.95/14.97 | | | | vOptFType(all_552_1) & vOptTType(all_552_0) % 106.95/14.97 | | | | % 106.95/14.97 | | | | ALPHA: (137) implies: % 106.95/14.97 | | | | (138) vfindColType(all_340_8, all_340_7) = all_552_1 % 106.95/14.97 | | | | (139) vprojectTypeAttrL(val1, all_340_7) = all_552_0 % 106.95/14.97 | | | | % 106.95/14.97 | | | | BETA: splitting (65) gives: % 106.95/14.97 | | | | % 106.95/14.97 | | | | Case 1: % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | (140) ? [v0: vName] : ? [v1: vOptFType] : ? [v2: vAttrL] : ? % 106.95/14.97 | | | | | [v3: vOptTType] : ? [v4: vFType] : ? [v5: vTType] : ? [v6: % 106.95/14.97 | | | | | vTType] : (vprojectTypeAttrL(v2, all_340_7) = v3 & % 106.95/14.97 | | | | | vfindColType(v0, all_340_7) = v1 & visSomeFType(v1) = 0 & % 106.95/14.97 | | | | | visSomeTType(v3) = 0 & vgetFType(v1) = v4 & vgetTType(v3) = % 106.95/14.97 | | | | | v5 & vacons(v0, v2) = all_340_2 & vsomeTType(v6) = % 106.95/14.97 | | | | | all_340_1 & vttcons(v0, v4, v5) = v6 & vOptFType(v1) & % 106.95/14.97 | | | | | vTType(v6) & vTType(v5) & vOptTType(v3) & % 106.95/14.97 | | | | | vOptTType(all_340_1) & vFType(v4) & vAttrL(v2) & vName(v0)) % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | DELTA: instantiating (140) with fresh symbols all_595_0, all_595_1, % 106.95/14.97 | | | | | all_595_2, all_595_3, all_595_4, all_595_5, all_595_6 gives: % 106.95/14.97 | | | | | (141) vprojectTypeAttrL(all_595_4, all_340_7) = all_595_3 & % 106.95/14.97 | | | | | vfindColType(all_595_6, all_340_7) = all_595_5 & % 106.95/14.97 | | | | | visSomeFType(all_595_5) = 0 & visSomeTType(all_595_3) = 0 & % 106.95/14.97 | | | | | vgetFType(all_595_5) = all_595_2 & vgetTType(all_595_3) = % 106.95/14.97 | | | | | all_595_1 & vacons(all_595_6, all_595_4) = all_340_2 & % 106.95/14.97 | | | | | vsomeTType(all_595_0) = all_340_1 & vttcons(all_595_6, % 106.95/14.97 | | | | | all_595_2, all_595_1) = all_595_0 & vOptFType(all_595_5) & % 106.95/14.97 | | | | | vTType(all_595_0) & vTType(all_595_1) & vOptTType(all_595_3) % 106.95/14.97 | | | | | & vOptTType(all_340_1) & vFType(all_595_2) & % 106.95/14.97 | | | | | vAttrL(all_595_4) & vName(all_595_6) % 106.95/14.97 | | | | | % 106.95/14.97 | | | | | ALPHA: (141) implies: % 106.95/14.97 | | | | | (142) vName(all_595_6) % 106.95/14.97 | | | | | (143) vAttrL(all_595_4) % 106.95/14.97 | | | | | (144) vOptTType(all_595_3) % 106.95/14.97 | | | | | (145) vOptFType(all_595_5) % 106.95/14.97 | | | | | (146) vacons(all_595_6, all_595_4) = all_340_2 % 106.95/14.98 | | | | | (147) visSomeTType(all_595_3) = 0 % 106.95/14.98 | | | | | (148) visSomeFType(all_595_5) = 0 % 106.95/14.98 | | | | | (149) vfindColType(all_595_6, all_340_7) = all_595_5 % 106.95/14.98 | | | | | (150) vprojectTypeAttrL(all_595_4, all_340_7) = all_595_3 % 106.95/14.98 | | | | | % 106.95/14.98 | | | | | BETA: splitting (95) gives: % 106.95/14.98 | | | | | % 106.95/14.98 | | | | | Case 1: % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | | (151) all_335_0 = vtempty % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | | REDUCE: (38), (151) imply: % 106.95/14.98 | | | | | | (152) vtcons(vrempty, vtempty) = vtempty % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | | GROUND_INST: instantiating (2) with vrempty, vtempty, simplifying % 106.95/14.98 | | | | | | with (15), (19), (152) gives: % 106.95/14.98 | | | | | | (153) $false % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | | CLOSE: (153) is inconsistent. % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | Case 2: % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | | (154) ~ (all_335_0 = vtempty) % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | | BETA: splitting (94) gives: % 106.95/14.98 | | | | | | % 106.95/14.98 | | | | | | Case 1: % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | (155) all_335_0 = vtempty % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | REDUCE: (154), (155) imply: % 106.95/14.98 | | | | | | | (156) $false % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | CLOSE: (156) is inconsistent. % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | Case 2: % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (EQ-acons) with all_340_8, val1, % 106.95/14.98 | | | | | | | all_595_6, all_595_4, all_340_2, simplifying with % 106.95/14.98 | | | | | | | (23), (40), (47), (142), (143), (146) gives: % 106.95/14.98 | | | | | | | (157) all_595_4 = val1 & all_595_6 = all_340_8 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | ALPHA: (157) implies: % 106.95/14.98 | | | | | | | (158) all_595_6 = all_340_8 % 106.95/14.98 | | | | | | | (159) all_595_4 = val1 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (EQ-acons) with all_544_2, all_544_3, % 106.95/14.98 | | | | | | | all_595_6, all_595_4, all_340_2, simplifying with % 106.95/14.98 | | | | | | | (121), (122), (125), (142), (143), (146) gives: % 106.95/14.98 | | | | | | | (160) all_595_4 = all_544_3 & all_595_6 = all_544_2 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | ALPHA: (160) implies: % 106.95/14.98 | | | | | | | (161) all_595_6 = all_544_2 % 106.95/14.98 | | | | | | | (162) all_595_4 = all_544_3 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (9) with all_544_5, all_544_0, % 106.95/14.98 | | | | | | | simplifying with (123), (126) gives: % 106.95/14.98 | | | | | | | (163) all_544_0 = 0 | all_544_5 = vnoRawTable % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (9) with all_544_4, all_544_1, % 106.95/14.98 | | | | | | | simplifying with (124), (127) gives: % 106.95/14.98 | | | | | | | (164) all_544_1 = 0 | all_544_4 = vnoRawTable % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (isSomeTType-true-INV) with all_595_3, % 106.95/14.98 | | | | | | | simplifying with (144), (147) gives: % 106.95/14.98 | | | | | | | (165) ? [v0: vTType] : (vsomeTType(v0) = all_595_3 & % 106.95/14.98 | | | | | | | vTType(v0)) % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (isSomeFType-true-INV) with all_595_5, % 106.95/14.98 | | | | | | | simplifying with (145), (148) gives: % 106.95/14.98 | | | | | | | (166) ? [v0: vFType] : (vsomeFType(v0) = all_595_5 & % 106.95/14.98 | | | | | | | vFType(v0)) % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | COMBINE_EQS: (159), (162) imply: % 106.95/14.98 | | | | | | | (167) all_544_3 = val1 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | COMBINE_EQS: (158), (161) imply: % 106.95/14.98 | | | | | | | (168) all_544_2 = all_340_8 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | DELTA: instantiating (166) with fresh symbol all_623_0 gives: % 106.95/14.98 | | | | | | | (169) vsomeFType(all_623_0) = all_595_5 & vFType(all_623_0) % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | ALPHA: (169) implies: % 106.95/14.98 | | | | | | | (170) vFType(all_623_0) % 106.95/14.98 | | | | | | | (171) vsomeFType(all_623_0) = all_595_5 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | DELTA: instantiating (165) with fresh symbol all_625_0 gives: % 106.95/14.98 | | | | | | | (172) vsomeTType(all_625_0) = all_595_3 & vTType(all_625_0) % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | ALPHA: (172) implies: % 106.95/14.98 | | | | | | | (173) vTType(all_625_0) % 106.95/14.98 | | | | | | | (174) vsomeTType(all_625_0) = all_595_3 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | REDUCE: (150), (159) imply: % 106.95/14.98 | | | | | | | (175) vprojectTypeAttrL(val1, all_340_7) = all_595_3 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | REDUCE: (149), (158) imply: % 106.95/14.98 | | | | | | | (176) vfindColType(all_340_8, all_340_7) = all_595_5 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | REDUCE: (129), (167) imply: % 106.95/14.98 | | | | | | | (177) vprojectCols(val1, all_340_12, all_340_11) = all_544_5 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | REDUCE: (128), (168) imply: % 106.95/14.98 | | | | | | | (178) vfindCol(all_340_8, all_340_12, all_340_11) = all_544_4 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (32) with all_552_1, all_595_5, % 106.95/14.98 | | | | | | | all_340_7, all_340_8, simplifying with (138), (176) % 106.95/14.98 | | | | | | | gives: % 106.95/14.98 | | | | | | | (179) all_595_5 = all_552_1 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (33) with all_552_0, all_595_3, % 106.95/14.98 | | | | | | | all_340_7, val1, simplifying with (139), (175) gives: % 106.95/14.98 | | | | | | | (180) all_595_3 = all_552_0 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | REDUCE: (171), (179) imply: % 106.95/14.98 | | | | | | | (181) vsomeFType(all_623_0) = all_552_1 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | REDUCE: (174), (180) imply: % 106.95/14.98 | | | | | | | (182) vsomeTType(all_625_0) = all_552_0 % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (findColTypeImpliesfindCol) with % 106.95/14.98 | | | | | | | all_340_11, all_623_0, all_340_12, all_340_8, % 106.95/14.98 | | | | | | | all_340_7, all_552_1, all_544_4, simplifying with % 106.95/14.98 | | | | | | | (40), (41), (43), (45), (138), (170), (178), (181) % 106.95/14.98 | | | | | | | gives: % 106.95/14.98 | | | | | | | (183) ? [v0: any] : ? [v1: any] : % 106.95/14.98 | | | | | | | (vwelltypedRawtable(all_340_7, all_340_11) = v0 & % 106.95/14.98 | | | | | | | vmatchingAttrL(all_340_7, all_340_12) = v1 & ( ~ (v1 = % 106.95/14.98 | | | | | | | 0) | ~ (v0 = 0))) | ? [v0: vRawTable] : % 106.95/14.98 | | | | | | | (vsomeRawTable(v0) = all_544_4 & vOptRawTable(all_544_4) % 106.95/14.98 | | | | | | | & vRawTable(v0)) % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | GROUND_INST: instantiating (22) with all_340_7, all_340_11, % 106.95/14.98 | | | | | | | all_340_12, all_625_0, all_552_0, all_544_5, % 106.95/14.98 | | | | | | | simplifying with (41), (43), (45), (139), (173), % 106.95/14.98 | | | | | | | (177), (182) gives: % 106.95/14.98 | | | | | | | (184) ? [v0: any] : ? [v1: any] : % 106.95/14.98 | | | | | | | (vwelltypedRawtable(all_340_7, all_340_11) = v0 & % 106.95/14.98 | | | | | | | vmatchingAttrL(all_340_7, all_340_12) = v1 & ( ~ (v1 = % 106.95/14.98 | | | | | | | 0) | ~ (v0 = 0))) | ? [v0: vRawTable] : % 106.95/14.98 | | | | | | | (vsomeRawTable(v0) = all_544_5 & vOptRawTable(all_544_5) % 106.95/14.98 | | | | | | | & vRawTable(v0)) % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | BETA: splitting (183) gives: % 106.95/14.98 | | | | | | | % 106.95/14.98 | | | | | | | Case 1: % 106.95/14.98 | | | | | | | | % 106.95/14.98 | | | | | | | | (185) ? [v0: any] : ? [v1: any] : % 106.95/14.98 | | | | | | | | (vwelltypedRawtable(all_340_7, all_340_11) = v0 & % 106.95/14.98 | | | | | | | | vmatchingAttrL(all_340_7, all_340_12) = v1 & ( ~ (v1 % 106.95/14.98 | | | | | | | | = 0) | ~ (v0 = 0))) % 106.95/14.98 | | | | | | | | % 106.95/14.98 | | | | | | | | DELTA: instantiating (185) with fresh symbols all_736_0, % 106.95/14.98 | | | | | | | | all_736_1 gives: % 106.95/14.98 | | | | | | | | (186) vwelltypedRawtable(all_340_7, all_340_11) = all_736_1 & % 106.95/14.98 | | | | | | | | vmatchingAttrL(all_340_7, all_340_12) = all_736_0 & ( ~ % 106.95/14.98 | | | | | | | | (all_736_0 = 0) | ~ (all_736_1 = 0)) % 106.95/14.98 | | | | | | | | % 106.95/14.98 | | | | | | | | ALPHA: (186) implies: % 106.95/14.98 | | | | | | | | (187) vmatchingAttrL(all_340_7, all_340_12) = all_736_0 % 106.95/14.98 | | | | | | | | (188) vwelltypedRawtable(all_340_7, all_340_11) = all_736_1 % 106.95/14.98 | | | | | | | | (189) ~ (all_736_0 = 0) | ~ (all_736_1 = 0) % 106.95/14.98 | | | | | | | | % 106.95/14.98 | | | | | | | | GROUND_INST: instantiating (30) with 0, all_736_0, all_340_12, % 106.95/14.98 | | | | | | | | all_340_7, simplifying with (48), (187) gives: % 106.95/14.98 | | | | | | | | (190) all_736_0 = 0 % 106.95/14.98 | | | | | | | | % 106.95/14.98 | | | | | | | | GROUND_INST: instantiating (31) with 0, all_736_1, all_340_11, % 106.95/14.98 | | | | | | | | all_340_7, simplifying with (49), (188) gives: % 106.95/14.98 | | | | | | | | (191) all_736_1 = 0 % 106.95/14.98 | | | | | | | | % 106.95/14.98 | | | | | | | | BETA: splitting (189) gives: % 106.95/14.98 | | | | | | | | % 106.95/14.98 | | | | | | | | Case 1: % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | | (192) ~ (all_736_0 = 0) % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | | REDUCE: (190), (192) imply: % 106.95/14.98 | | | | | | | | | (193) $false % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | | CLOSE: (193) is inconsistent. % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | Case 2: % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | | (194) ~ (all_736_1 = 0) % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | | REDUCE: (191), (194) imply: % 106.95/14.98 | | | | | | | | | (195) $false % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | | CLOSE: (195) is inconsistent. % 106.95/14.98 | | | | | | | | | % 106.95/14.98 | | | | | | | | End of split % 106.95/14.99 | | | | | | | | % 106.95/14.99 | | | | | | | Case 2: % 106.95/14.99 | | | | | | | | % 106.95/14.99 | | | | | | | | (196) ? [v0: vRawTable] : (vsomeRawTable(v0) = all_544_4 & % 106.95/14.99 | | | | | | | | vOptRawTable(all_544_4) & vRawTable(v0)) % 106.95/14.99 | | | | | | | | % 106.95/14.99 | | | | | | | | DELTA: instantiating (196) with fresh symbol all_739_0 gives: % 106.95/14.99 | | | | | | | | (197) vsomeRawTable(all_739_0) = all_544_4 & % 106.95/14.99 | | | | | | | | vOptRawTable(all_544_4) & vRawTable(all_739_0) % 106.95/14.99 | | | | | | | | % 106.95/14.99 | | | | | | | | ALPHA: (197) implies: % 106.95/14.99 | | | | | | | | (198) vRawTable(all_739_0) % 106.95/14.99 | | | | | | | | (199) vsomeRawTable(all_739_0) = all_544_4 % 106.95/14.99 | | | | | | | | % 106.95/14.99 | | | | | | | | BETA: splitting (184) gives: % 106.95/14.99 | | | | | | | | % 106.95/14.99 | | | | | | | | Case 1: % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | (200) ? [v0: any] : ? [v1: any] : % 106.95/14.99 | | | | | | | | | (vwelltypedRawtable(all_340_7, all_340_11) = v0 & % 106.95/14.99 | | | | | | | | | vmatchingAttrL(all_340_7, all_340_12) = v1 & ( ~ % 106.95/14.99 | | | | | | | | | (v1 = 0) | ~ (v0 = 0))) % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | DELTA: instantiating (200) with fresh symbols all_743_0, % 106.95/14.99 | | | | | | | | | all_743_1 gives: % 106.95/14.99 | | | | | | | | | (201) vwelltypedRawtable(all_340_7, all_340_11) = all_743_1 % 106.95/14.99 | | | | | | | | | & vmatchingAttrL(all_340_7, all_340_12) = all_743_0 & % 106.95/14.99 | | | | | | | | | ( ~ (all_743_0 = 0) | ~ (all_743_1 = 0)) % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | ALPHA: (201) implies: % 106.95/14.99 | | | | | | | | | (202) vmatchingAttrL(all_340_7, all_340_12) = all_743_0 % 106.95/14.99 | | | | | | | | | (203) vwelltypedRawtable(all_340_7, all_340_11) = all_743_1 % 106.95/14.99 | | | | | | | | | (204) ~ (all_743_0 = 0) | ~ (all_743_1 = 0) % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | GROUND_INST: instantiating (30) with 0, all_743_0, all_340_12, % 106.95/14.99 | | | | | | | | | all_340_7, simplifying with (48), (202) gives: % 106.95/14.99 | | | | | | | | | (205) all_743_0 = 0 % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | GROUND_INST: instantiating (31) with 0, all_743_1, all_340_11, % 106.95/14.99 | | | | | | | | | all_340_7, simplifying with (49), (203) gives: % 106.95/14.99 | | | | | | | | | (206) all_743_1 = 0 % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | BETA: splitting (204) gives: % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | Case 1: % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | (207) ~ (all_743_0 = 0) % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | REDUCE: (205), (207) imply: % 106.95/14.99 | | | | | | | | | | (208) $false % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | CLOSE: (208) is inconsistent. % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | Case 2: % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | (209) ~ (all_743_1 = 0) % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | REDUCE: (206), (209) imply: % 106.95/14.99 | | | | | | | | | | (210) $false % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | CLOSE: (210) is inconsistent. % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | End of split % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | Case 2: % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | (211) ? [v0: vRawTable] : (vsomeRawTable(v0) = all_544_5 & % 106.95/14.99 | | | | | | | | | vOptRawTable(all_544_5) & vRawTable(v0)) % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | DELTA: instantiating (211) with fresh symbol all_743_0 gives: % 106.95/14.99 | | | | | | | | | (212) vsomeRawTable(all_743_0) = all_544_5 & % 106.95/14.99 | | | | | | | | | vOptRawTable(all_544_5) & vRawTable(all_743_0) % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | ALPHA: (212) implies: % 106.95/14.99 | | | | | | | | | (213) vRawTable(all_743_0) % 106.95/14.99 | | | | | | | | | (214) vsomeRawTable(all_743_0) = all_544_5 % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | BETA: splitting (130) gives: % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | | Case 1: % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | (215) ~ (all_544_0 = 0) % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | BETA: splitting (163) gives: % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | Case 1: % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | (216) all_544_0 = 0 % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | REDUCE: (215), (216) imply: % 106.95/14.99 | | | | | | | | | | | (217) $false % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | CLOSE: (217) is inconsistent. % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | Case 2: % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | (218) all_544_5 = vnoRawTable % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | REDUCE: (214), (218) imply: % 106.95/14.99 | | | | | | | | | | | (219) vsomeRawTable(all_743_0) = vnoRawTable % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | GROUND_INST: instantiating (1) with all_743_0, simplifying with % 106.95/14.99 | | | | | | | | | | | (213), (219) gives: % 106.95/14.99 | | | | | | | | | | | (220) $false % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | CLOSE: (220) is inconsistent. % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | End of split % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | Case 2: % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | (221) ~ (all_544_1 = 0) % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | BETA: splitting (164) gives: % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | Case 1: % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | (222) all_544_1 = 0 % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | REDUCE: (221), (222) imply: % 106.95/14.99 | | | | | | | | | | | (223) $false % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | CLOSE: (223) is inconsistent. % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | Case 2: % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | (224) all_544_4 = vnoRawTable % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | REDUCE: (199), (224) imply: % 106.95/14.99 | | | | | | | | | | | (225) vsomeRawTable(all_739_0) = vnoRawTable % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | GROUND_INST: instantiating (1) with all_739_0, simplifying with % 106.95/14.99 | | | | | | | | | | | (198), (225) gives: % 106.95/14.99 | | | | | | | | | | | (226) $false % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | | CLOSE: (226) is inconsistent. % 106.95/14.99 | | | | | | | | | | | % 106.95/14.99 | | | | | | | | | | End of split % 106.95/14.99 | | | | | | | | | | % 106.95/14.99 | | | | | | | | | End of split % 106.95/14.99 | | | | | | | | | % 106.95/14.99 | | | | | | | | End of split % 106.95/14.99 | | | | | | | | % 106.95/14.99 | | | | | | | End of split % 106.95/14.99 | | | | | | | % 106.95/14.99 | | | | | | End of split % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | End of split % 106.95/14.99 | | | | | % 106.95/14.99 | | | | Case 2: % 106.95/14.99 | | | | | % 106.95/14.99 | | | | | (227) ? [v0: vName] : ? [v1: vOptFType] : ? [v2: vAttrL] : ? % 106.95/14.99 | | | | | [v3: vOptTType] : ? [v4: any] : ? [v5: any] : (all_340_1 = % 106.95/14.99 | | | | | vnoTType & vprojectTypeAttrL(v2, all_340_7) = v3 & % 106.95/14.99 | | | | | vfindColType(v0, all_340_7) = v1 & visSomeFType(v1) = v4 & % 106.95/14.99 | | | | | visSomeTType(v3) = v5 & vacons(v0, v2) = all_340_2 & % 106.95/14.99 | | | | | vOptFType(v1) & vOptTType(v3) & vAttrL(v2) & vName(v0) & ( % 106.95/14.99 | | | | | ~ (v5 = 0) | ~ (v4 = 0))) | (all_346_0 = all_340_1 & % 106.95/14.99 | | | | | all_340_2 = vaempty) % 106.95/14.99 | | | | | % 106.95/14.99 | | | | | BETA: splitting (227) gives: % 106.95/14.99 | | | | | % 106.95/14.99 | | | | | Case 1: % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | (228) ? [v0: vName] : ? [v1: vOptFType] : ? [v2: vAttrL] : ? % 106.95/14.99 | | | | | | [v3: vOptTType] : ? [v4: any] : ? [v5: any] : (all_340_1 % 106.95/14.99 | | | | | | = vnoTType & vprojectTypeAttrL(v2, all_340_7) = v3 & % 106.95/14.99 | | | | | | vfindColType(v0, all_340_7) = v1 & visSomeFType(v1) = v4 % 106.95/14.99 | | | | | | & visSomeTType(v3) = v5 & vacons(v0, v2) = all_340_2 & % 106.95/14.99 | | | | | | vOptFType(v1) & vOptTType(v3) & vAttrL(v2) & vName(v0) & % 106.95/14.99 | | | | | | ( ~ (v5 = 0) | ~ (v4 = 0))) % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | DELTA: instantiating (228) with fresh symbols all_617_0, all_617_1, % 106.95/14.99 | | | | | | all_617_2, all_617_3, all_617_4, all_617_5 gives: % 106.95/14.99 | | | | | | (229) all_340_1 = vnoTType & vprojectTypeAttrL(all_617_3, % 106.95/14.99 | | | | | | all_340_7) = all_617_2 & vfindColType(all_617_5, % 106.95/14.99 | | | | | | all_340_7) = all_617_4 & visSomeFType(all_617_4) = % 106.95/14.99 | | | | | | all_617_1 & visSomeTType(all_617_2) = all_617_0 & % 106.95/14.99 | | | | | | vacons(all_617_5, all_617_3) = all_340_2 & % 106.95/14.99 | | | | | | vOptFType(all_617_4) & vOptTType(all_617_2) & % 106.95/14.99 | | | | | | vAttrL(all_617_3) & vName(all_617_5) & ( ~ (all_617_0 = 0) % 106.95/14.99 | | | | | | | ~ (all_617_1 = 0)) % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | ALPHA: (229) implies: % 106.95/14.99 | | | | | | (230) all_340_1 = vnoTType % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | REDUCE: (135), (230) imply: % 106.95/14.99 | | | | | | (231) $false % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | CLOSE: (231) is inconsistent. % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | Case 2: % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | (232) all_346_0 = all_340_1 & all_340_2 = vaempty % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | ALPHA: (232) implies: % 106.95/14.99 | | | | | | (233) all_340_2 = vaempty % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | REDUCE: (47), (233) imply: % 106.95/14.99 | | | | | | (234) vacons(all_340_8, val1) = vaempty % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | GROUND_INST: instantiating (3) with all_340_8, val1, simplifying % 106.95/14.99 | | | | | | with (23), (40), (234) gives: % 106.95/14.99 | | | | | | (235) $false % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | | CLOSE: (235) is inconsistent. % 106.95/14.99 | | | | | | % 106.95/14.99 | | | | | End of split % 106.95/14.99 | | | | | % 106.95/14.99 | | | | End of split % 106.95/14.99 | | | | % 106.95/14.99 | | | End of split % 106.95/14.99 | | | % 106.95/14.99 | | Case 2: % 106.95/14.99 | | | % 106.95/14.99 | | | (236) ? [v0: vRawTable] : (all_340_2 = vaempty & % 106.95/14.99 | | | vprojectEmptyCol(all_340_11) = v0 & vsomeRawTable(v0) = % 106.95/14.99 | | | all_340_0 & vOptRawTable(all_340_0) & vRawTable(v0)) % 106.95/14.99 | | | % 106.95/14.99 | | | DELTA: instantiating (236) with fresh symbol all_544_0 gives: % 106.95/14.99 | | | (237) all_340_2 = vaempty & vprojectEmptyCol(all_340_11) = all_544_0 & % 106.95/14.99 | | | vsomeRawTable(all_544_0) = all_340_0 & vOptRawTable(all_340_0) & % 106.95/14.99 | | | vRawTable(all_544_0) % 106.95/14.99 | | | % 106.95/14.99 | | | ALPHA: (237) implies: % 106.95/14.99 | | | (238) all_340_2 = vaempty % 106.95/14.99 | | | % 106.95/14.99 | | | REDUCE: (47), (238) imply: % 106.95/14.99 | | | (239) vacons(all_340_8, val1) = vaempty % 106.95/14.99 | | | % 106.95/14.99 | | | GROUND_INST: instantiating (3) with all_340_8, val1, simplifying with % 106.95/14.99 | | | (23), (40), (239) gives: % 106.95/14.99 | | | (240) $false % 106.95/14.99 | | | % 106.95/14.99 | | | CLOSE: (240) is inconsistent. % 106.95/14.99 | | | % 106.95/15.00 | | End of split % 106.95/15.00 | | % 106.95/15.00 | End of split % 106.95/15.00 | % 106.95/15.00 End of proof % 106.95/15.00 % SZS output end Proof for theBenchmark % 106.95/15.00 % 106.95/15.00 14420ms %------------------------------------------------------------------------------