%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM273_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 : n023.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:40 PM UTC 2026 % Result : Theorem 30.30s 4.71s % Output : Proof 42.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM273_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.34 % Computer : n023.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Mon May 4 20:07:53 EDT 2026 % 0.14/0.34 % CPUTime : % 0.49/0.60 ________ _____ % 0.49/0.60 ___ __ \_________(_)________________________________ % 0.49/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.49/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.49/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.49/0.60 % 0.49/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.49/0.60 (2023-06-19) % 0.49/0.60 % 0.49/0.60 (c) Philipp Rümmer, 2009-2023 % 0.49/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.49/0.60 Amanda Stjerna. % 0.49/0.60 Free software under BSD-3-Clause. % 0.49/0.60 % 0.49/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.49/0.60 % 0.49/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.49/0.62 Running up to 7 provers in parallel. % 0.71/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.71/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.71/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.71/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.71/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.71/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.71/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.71/2.11 Prover 0: Preprocessing ... % 9.71/2.11 Prover 2: Preprocessing ... % 9.71/2.13 Prover 4: Preprocessing ... % 9.71/2.13 Prover 6: Preprocessing ... % 9.71/2.13 Prover 1: Preprocessing ... % 9.71/2.14 Prover 3: Preprocessing ... % 9.71/2.14 Prover 5: Preprocessing ... % 25.00/4.08 Prover 3: Warning: ignoring some quantifiers % 25.82/4.14 Prover 3: Constructing countermodel ... % 25.82/4.14 Prover 6: Proving ... % 25.82/4.15 Prover 1: Warning: ignoring some quantifiers % 26.38/4.28 Prover 1: Constructing countermodel ... % 28.71/4.57 Prover 5: Proving ... % 29.50/4.68 Prover 4: Warning: ignoring some quantifiers % 30.30/4.70 Prover 3: proved (4071ms) % 30.30/4.70 % 30.30/4.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.30/4.71 % 30.30/4.73 Prover 5: stopped % 30.30/4.73 Prover 6: stopped % 30.30/4.75 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 30.30/4.75 Prover 0: Proving ... % 30.30/4.75 Prover 0: stopped % 30.30/4.79 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 30.30/4.79 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 31.05/4.80 Prover 4: Constructing countermodel ... % 31.05/4.80 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 36.44/5.50 Prover 7: Preprocessing ... % 36.44/5.55 Prover 11: Preprocessing ... % 36.44/5.59 Prover 10: Preprocessing ... % 37.18/5.64 Prover 8: Preprocessing ... % 37.99/5.79 Prover 1: Found proof (size 195) % 38.76/5.81 Prover 1: proved (5186ms) % 38.76/5.81 Prover 4: stopped % 38.76/5.81 Prover 7: stopped % 38.76/5.82 Prover 2: Proving ... % 38.76/5.82 Prover 2: stopped % 38.76/5.88 Prover 10: stopped % 39.38/5.92 Prover 11: stopped % 40.29/6.16 Prover 8: Warning: ignoring some quantifiers % 40.64/6.20 Prover 8: Constructing countermodel ... % 40.64/6.22 Prover 8: stopped % 40.64/6.22 % 40.64/6.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.64/6.22 % 41.07/6.32 % SZS output start Proof for theBenchmark % 41.07/6.33 Assumptions after simplification: % 41.07/6.33 --------------------------------- % 41.07/6.33 % 41.07/6.33 (evalBinOp-8) % 41.07/6.36 vBinOpT(veqop) & vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] % 41.07/6.36 : (vsomeExp(v1) = v2 & vB(vyes) = v0 & vconstant(v0) = v1 & vOptExp(v2) & % 41.07/6.36 vExp(v1) & vAval(v0) & ! [v3: vAval] : ! [v4: vOptExp] : (v4 = v2 | ~ % 41.07/6.36 (vevalBinOp(veqop, v3, v3) = v4) | ~ vAval(v3))) % 41.07/6.36 % 41.07/6.36 (evalBinOp-9) % 41.07/6.36 vBinOpT(veqop) & vYN(vno) & ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] % 41.07/6.36 : (vsomeExp(v1) = v2 & vB(vno) = v0 & vconstant(v0) = v1 & vOptExp(v2) & % 41.07/6.36 vExp(v1) & vAval(v0) & ! [v3: vAval] : ! [v4: vAval] : ! [v5: vOptExp] : % 41.07/6.36 (v5 = v2 | v4 = v3 | ~ (vevalBinOp(veqop, v3, v4) = v5) | ~ vAval(v4) | ~ % 41.07/6.36 vAval(v3))) % 41.07/6.36 % 41.07/6.36 (evalBinOp-INV) % 41.07/6.38 vBinOpT(vgtop) & vBinOpT(vltop) & vBinOpT(vaddop) & vBinOpT(veqop) & % 41.07/6.38 vBinOpT(vorop) & vBinOpT(vmulop) & vBinOpT(vdivop) & vBinOpT(vandop) & % 41.07/6.38 vBinOpT(vsubop) & vOptExp(vnoExp) & vYN(vno) & vYN(vyes) & ? [v0: vAval] : ? % 41.07/6.38 [v1: vExp] : ? [v2: vOptExp] : ? [v3: vAval] : ? [v4: vExp] : ? [v5: % 41.07/6.38 vOptExp] : (vsomeExp(v4) = v5 & vsomeExp(v1) = v2 & vB(vno) = v3 & vB(vyes) % 41.07/6.38 = v0 & vconstant(v3) = v4 & vconstant(v0) = v1 & vOptExp(v5) & vOptExp(v2) & % 41.07/6.38 vExp(v4) & vExp(v1) & vAval(v3) & vAval(v0) & ! [v6: vBinOpT] : ! [v7: % 41.07/6.38 vAval] : ! [v8: vAval] : ! [v9: vOptExp] : ( ~ (vevalBinOp(v6, v7, v8) = % 41.07/6.38 v9) | ~ vBinOpT(v6) | ~ vAval(v8) | ~ vAval(v7) | ? [v10: vnat] : ? % 41.07/6.38 [v11: vnat] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] : (v6 = % 41.07/6.38 vgtop & vgt(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v11) = v8 & % 41.07/6.38 vNum(v10) = v7 & vB(v12) = v13 & vconstant(v13) = v14 & vOptExp(v9) & % 41.07/6.38 vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13) & vYN(v12)) | ? [v10: % 41.07/6.38 vnat] : ? [v11: vnat] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: % 41.07/6.38 vExp] : (v6 = vltop & vlt(v10, v11) = v12 & vsomeExp(v14) = v9 & % 41.07/6.38 vNum(v11) = v8 & vNum(v10) = v7 & vB(v12) = v13 & vconstant(v13) = v14 & % 41.07/6.38 vOptExp(v9) & vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13) & vYN(v12)) % 41.07/6.38 | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] : ? [v13: vAval] : ? % 41.07/6.38 [v14: vExp] : (v6 = vaddop & vplus(v10, v11) = v12 & vsomeExp(v14) = v9 & % 41.07/6.38 vNum(v12) = v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 % 41.07/6.38 & vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 41.07/6.38 vAval(v13)) | ? [v10: vYN] : ? [v11: vYN] : ? [v12: vYN] : ? [v13: % 41.07/6.38 vAval] : ? [v14: vExp] : (v6 = vorop & vor(v10, v11) = v12 & % 41.07/6.38 vsomeExp(v14) = v9 & vB(v12) = v13 & vB(v11) = v8 & vB(v10) = v7 & % 41.07/6.38 vconstant(v13) = v14 & vOptExp(v9) & vExp(v14) & vAval(v13) & vYN(v12) & % 41.07/6.38 vYN(v11) & vYN(v10)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] % 41.07/6.38 : ? [v13: vAval] : ? [v14: vExp] : (v6 = vmulop & vmultiply(v10, v11) = % 41.07/6.38 v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & vNum(v11) = v8 & vNum(v10) % 41.07/6.38 = v7 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v12) & vnat(v11) & % 41.07/6.38 vnat(v10) & vExp(v14) & vAval(v13)) | ? [v10: vnat] : ? [v11: vnat] : % 41.07/6.38 ? [v12: vnat] : ? [v13: vAval] : ? [v14: vExp] : (v6 = vdivop & % 41.07/6.38 vdivide(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & % 41.07/6.38 vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & % 41.07/6.38 vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13)) | ? [v10: % 41.07/6.38 vYN] : ? [v11: vYN] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] % 41.07/6.38 : (v6 = vandop & vand(v10, v11) = v12 & vsomeExp(v14) = v9 & vB(v12) = v13 % 41.07/6.38 & vB(v11) = v8 & vB(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & % 41.07/6.38 vExp(v14) & vAval(v13) & vYN(v12) & vYN(v11) & vYN(v10)) | ? [v10: % 41.07/6.38 vnat] : ? [v11: vnat] : ? [v12: vnat] : ? [v13: vAval] : ? [v14: % 41.07/6.38 vExp] : (v6 = vsubop & vminus(v10, v11) = v12 & vsomeExp(v14) = v9 & % 41.07/6.38 vNum(v12) = v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 % 41.07/6.38 & vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 41.07/6.38 vAval(v13)) | (v9 = v5 & v6 = veqop & ~ (v8 = v7)) | (v9 = v2 & v8 = v7 % 41.07/6.38 & v6 = veqop) | (v9 = vnoExp & ~ (v6 = veqop) & ( ~ (v6 = vorop) | ! % 41.07/6.38 [v10: vYN] : ( ~ (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ % 41.07/6.38 (vB(v10) = v7) | ~ vYN(v10))) & ( ~ (v6 = vandop) | ! [v10: vYN] : % 41.07/6.38 ( ~ (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ (vB(v10) = v7) % 41.07/6.38 | ~ vYN(v10))) & ( ! [v10: vnat] : ( ~ (vNum(v10) = v8) | ~ % 41.07/6.38 vnat(v10)) | ! [v10: vnat] : ( ~ (vNum(v10) = v7) | ~ vnat(v10)) | % 41.07/6.38 ( ~ (v6 = vgtop) & ~ (v6 = vltop) & ~ (v6 = vaddop) & ~ (v6 = % 41.07/6.38 vmulop) & ~ (v6 = vdivop) & ~ (v6 = vsubop)))))) % 41.07/6.38 % 41.07/6.38 (evalUnOp-0) % 41.07/6.38 vUnOpT(vnotop) & ! [v0: vYN] : ! [v1: vYN] : ( ~ (vnot(v0) = v1) | ~ % 41.07/6.38 vYN(v0) | ? [v2: vAval] : ? [v3: vOptExp] : ? [v4: vAval] : ? [v5: vExp] % 41.07/6.38 : (vevalUnOp(vnotop, v2) = v3 & vsomeExp(v5) = v3 & vB(v1) = v4 & vB(v0) = % 41.07/6.38 v2 & vconstant(v4) = v5 & vOptExp(v3) & vExp(v5) & vAval(v4) & vAval(v2))) % 41.07/6.38 % 41.07/6.38 (evalUnOpPreservation) % 41.07/6.39 ! [v0: vExp] : ! [v1: vATMap] : ! [v2: vAType] : ! [v3: vAval] : ! [v4: % 41.07/6.39 vUnOpT] : ! [v5: vExp] : ! [v6: vExp] : ! [v7: vOptAType] : ! [v8: % 41.07/6.39 vOptExp] : ( ~ (vecheck(v1, v6) = v7) | ~ (vsomeExp(v0) = v8) | ~ % 41.07/6.39 (vsomeAType(v2) = v7) | ~ (vunop(v4, v5) = v6) | ~ (vconstant(v3) = v5) | % 41.07/6.39 ~ vAType(v2) | ~ vUnOpT(v4) | ~ vExp(v0) | ~ vAval(v3) | ~ vATMap(v1) | % 41.07/6.39 ? [v9: vOptExp] : ? [v10: vOptAType] : (vecheck(v1, v0) = v10 & % 41.07/6.39 vevalUnOp(v4, v3) = v9 & vOptExp(v9) & vOptAType(v10) & ( ~ (v9 = v8) | % 41.07/6.39 v10 = v7))) % 41.07/6.39 % 41.07/6.39 (evalUnOpProgress) % 41.07/6.39 ! [v0: vATMap] : ! [v1: vUnOpT] : ! [v2: vAval] : ! [v3: vAType] : ! [v4: % 41.07/6.39 vExp] : ! [v5: vExp] : ! [v6: vOptAType] : ( ~ (vecheck(v0, v5) = v6) | ~ % 41.07/6.39 (vsomeAType(v3) = v6) | ~ (vunop(v1, v4) = v5) | ~ (vconstant(v2) = v4) | % 41.07/6.39 ~ vAType(v3) | ~ vUnOpT(v1) | ~ vAval(v2) | ~ vATMap(v0) | ? [v7: % 41.07/6.39 vOptExp] : (vevalUnOp(v1, v2) = v7 & vOptExp(v7) & ? [v8: vExp] : % 41.07/6.39 (vsomeExp(v8) = v7 & vExp(v8)))) % 41.07/6.39 % 41.07/6.39 (expIsValue-1) % 41.07/6.39 ! [v0: vExp] : ( ~ (vexpIsValue(v0) = 0) | ~ vExp(v0) | ? [v1: vAval] : % 41.07/6.39 (vconstant(v1) = v0 & vAval(v1))) % 41.07/6.39 % 41.07/6.39 (expIsValue-true-INV) % 41.07/6.39 ! [v0: vExp] : ( ~ (vexpIsValue(v0) = 0) | ~ vExp(v0) | ? [v1: vAval] : % 41.07/6.39 (vconstant(v1) = v0 & vAval(v1))) % 41.07/6.39 % 41.07/6.39 (getExpValue-0) % 41.07/6.39 ! [v0: vAval] : ! [v1: vExp] : ( ~ (vconstant(v0) = v1) | ~ vAval(v0) | % 41.07/6.39 vgetExpValue(v1) = v0) % 41.07/6.39 % 41.07/6.39 (not-0) % 41.07/6.39 vnot(vyes) = vno & vYN(vno) & vYN(vyes) % 41.07/6.39 % 41.07/6.39 (not-1) % 41.07/6.39 vnot(vno) = vyes & vYN(vno) & vYN(vyes) % 41.07/6.39 % 41.07/6.39 (reduce-11) % 41.07/6.39 vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : (vB(vyes) = v0 & vconstant(v0) = % 41.07/6.39 v1 & vExp(v1) & vAval(v0) & ! [v2: vQuestionnaire] : ! [v3: % 41.07/6.39 vQuestionnaire] : ! [v4: vAnsMap] : ! [v5: vQMap] : ! [v6: % 41.07/6.39 vQuestionnaire] : ! [v7: vOptQConf] : ( ~ (vreduce(v6, v4, v5) = v7) | ~ % 41.07/6.39 (vqcond(v1, v2, v3) = v6) | ~ vQMap(v5) | ~ vAnsMap(v4) | ~ % 41.07/6.39 vQuestionnaire(v3) | ~ vQuestionnaire(v2) | ? [v8: vQConf] : (vQC(v4, % 41.07/6.39 v5, v2) = v8 & vsomeQConf(v8) = v7 & vOptQConf(v7) & vQConf(v8)))) % 41.07/6.39 % 41.07/6.39 (reduce-12) % 41.07/6.39 vYN(vno) & ? [v0: vAval] : ? [v1: vExp] : (vB(vno) = v0 & vconstant(v0) = v1 % 41.07/6.39 & vExp(v1) & vAval(v0) & ! [v2: vQuestionnaire] : ! [v3: vQuestionnaire] : % 41.07/6.39 ! [v4: vAnsMap] : ! [v5: vQMap] : ! [v6: vQuestionnaire] : ! [v7: % 41.07/6.39 vOptQConf] : ( ~ (vreduce(v6, v4, v5) = v7) | ~ (vqcond(v1, v2, v3) = v6) % 41.07/6.39 | ~ vQMap(v5) | ~ vAnsMap(v4) | ~ vQuestionnaire(v3) | ~ % 41.07/6.39 vQuestionnaire(v2) | ? [v8: vQConf] : (vQC(v4, v5, v3) = v8 & % 41.07/6.39 vsomeQConf(v8) = v7 & vOptQConf(v7) & vQConf(v8)))) % 41.07/6.39 % 41.07/6.39 (reduce-13) % 41.52/6.40 vYN(vno) & vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? % 41.52/6.40 [v3: vExp] : (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & % 41.52/6.40 vconstant(v0) = v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: % 41.52/6.40 vQMap] : ! [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : ! % 41.52/6.40 [v8: vQuestionnaire] : ! [v9: vOptExp] : ! [v10: vExp] : ! [v11: % 41.52/6.40 vQuestionnaire] : ! [v12: vQConf] : (v6 = v3 | v6 = v1 | ~ % 41.52/6.40 (vreduceExp(v6, v7) = v9) | ~ (vgetExp(v9) = v10) | ~ (vQC(v7, v4, v11) % 41.52/6.40 = v12) | ~ (vqcond(v10, v5, v8) = v11) | ~ vQMap(v4) | ~ vExp(v6) | % 41.52/6.40 ~ vAnsMap(v7) | ~ vQuestionnaire(v8) | ~ vQuestionnaire(v5) | ? [v13: % 41.52/6.40 any] : ? [v14: vQuestionnaire] : ? [v15: vOptQConf] : ? [v16: % 41.52/6.40 vOptQConf] : (vreduce(v14, v7, v4) = v15 & visSomeExp(v9) = v13 & % 41.52/6.40 vsomeQConf(v12) = v16 & vqcond(v6, v5, v8) = v14 & vOptQConf(v16) & % 41.52/6.40 vOptQConf(v15) & vQuestionnaire(v14) & ( ~ (v13 = 0) | v16 = v15)))) % 41.52/6.40 % 41.52/6.40 (reduce-14) % 41.52/6.40 vOptQConf(vnoQConf) & vYN(vno) & vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : % 41.52/6.40 ? [v2: vAval] : ? [v3: vExp] : (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) % 41.52/6.40 = v3 & vconstant(v0) = v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! % 41.52/6.40 [v4: vQMap] : ! [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : % 41.52/6.40 ! [v8: vQuestionnaire] : ! [v9: vQuestionnaire] : ! [v10: vOptQConf] : % 41.52/6.40 (v10 = vnoQConf | v6 = v3 | v6 = v1 | ~ (vreduce(v9, v7, v4) = v10) | ~ % 41.52/6.40 (vqcond(v6, v5, v8) = v9) | ~ vQMap(v4) | ~ vExp(v6) | ~ vAnsMap(v7) | % 41.52/6.40 ~ vQuestionnaire(v8) | ~ vQuestionnaire(v5) | ? [v11: vOptExp] : % 41.52/6.40 (vreduceExp(v6, v7) = v11 & visSomeExp(v11) = 0 & vOptExp(v11)))) % 41.52/6.40 % 41.52/6.40 (reduce-INV) % 41.52/6.41 vOptQConf(vnoQConf) & vQuestionnaire(vqempty) & vYN(vno) & vYN(vyes) & ? [v0: % 41.52/6.41 vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : (vB(vno) = v2 & % 41.52/6.41 vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = v1 & vExp(v3) & % 41.52/6.41 vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: vQuestionnaire] : ! [v5: % 41.52/6.41 vAnsMap] : ! [v6: vQMap] : ! [v7: vOptQConf] : ( ~ (vreduce(v4, v5, v6) % 41.52/6.41 = v7) | ~ vQMap(v6) | ~ vAnsMap(v5) | ~ vQuestionnaire(v4) | ? [v8: % 41.52/6.41 vAType] : ? [v9: vOptExp] : ? [v10: vQID] : ? [v11: vExp] : ? [v12: % 41.52/6.41 int] : ? [v13: vEntry] : ? [v14: vExp] : ? [v15: vEntry] : ? [v16: % 41.52/6.41 vQuestionnaire] : ? [v17: vQConf] : ( ~ (v12 = 0) & vreduceExp(v11, v5) % 41.52/6.41 = v9 & vexpIsValue(v11) = v12 & visSomeExp(v9) = 0 & vgetExp(v9) = v14 & % 41.52/6.41 vQC(v5, v6, v16) = v17 & vsomeQConf(v17) = v7 & vqsingle(v15) = v16 & % 41.52/6.41 vqsingle(v13) = v4 & vvalue(v10, v8, v14) = v15 & vvalue(v10, v8, v11) = % 41.52/6.41 v13 & vAType(v8) & vOptExp(v9) & vQID(v10) & vExp(v14) & vExp(v11) & % 41.52/6.41 vOptQConf(v7) & vQConf(v17) & vQuestionnaire(v16) & vEntry(v15) & % 41.52/6.41 vEntry(v13)) | ? [v8: vQID] : ? [v9: vOptQuestion] : ? [v10: vEntry] % 41.52/6.41 : ? [v11: vLabel] : ? [v12: vAType] : ? [v13: vEntry] : ? [v14: % 41.52/6.41 vQuestionnaire] : ? [v15: vQConf] : (vlookupQMap(v8, v6) = v9 & % 41.52/6.41 visSomeQuestion(v9) = 0 & vgetQuestionAType(v9) = v12 & % 41.52/6.41 vgetQuestionLabel(v9) = v11 & vQC(v5, v6, v14) = v15 & vsomeQConf(v15) = % 41.52/6.41 v7 & vqsingle(v13) = v14 & vqsingle(v10) = v4 & vask(v8) = v10 & % 41.52/6.41 vquestion(v8, v11, v12) = v13 & vAType(v12) & vLabel(v11) & vQID(v8) & % 41.52/6.41 vOptQuestion(v9) & vOptQConf(v7) & vQConf(v15) & vQuestionnaire(v14) & % 41.52/6.41 vEntry(v13) & vEntry(v10)) | ? [v8: vAType] : ? [v9: vOptExp] : ? % 41.52/6.41 [v10: vQID] : ? [v11: vExp] : ? [v12: int] : ? [v13: int] : ? [v14: % 41.52/6.41 vEntry] : (v7 = vnoQConf & ~ (v13 = 0) & ~ (v12 = 0) & vreduceExp(v11, % 41.52/6.41 v5) = v9 & vexpIsValue(v11) = v12 & visSomeExp(v9) = v13 & % 41.52/6.41 vqsingle(v14) = v4 & vvalue(v10, v8, v11) = v14 & vAType(v8) & % 41.52/6.41 vOptExp(v9) & vQID(v10) & vExp(v11) & vEntry(v14)) | ? [v8: vOptExp] : % 41.52/6.41 ? [v9: vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : ? % 41.52/6.41 [v12: vExp] : ? [v13: vQuestionnaire] : ? [v14: vQConf] : ( ~ (v10 = v3) % 41.52/6.41 & ~ (v10 = v1) & vreduceExp(v10, v5) = v8 & visSomeExp(v8) = 0 & % 41.52/6.41 vgetExp(v8) = v12 & vQC(v5, v6, v13) = v14 & vsomeQConf(v14) = v7 & % 41.52/6.41 vqcond(v12, v9, v11) = v13 & vqcond(v10, v9, v11) = v4 & vOptExp(v8) & % 41.52/6.41 vExp(v12) & vExp(v10) & vOptQConf(v7) & vQConf(v14) & % 41.52/6.41 vQuestionnaire(v13) & vQuestionnaire(v11) & vQuestionnaire(v9)) | ? % 41.52/6.41 [v8: vAType] : ? [v9: vLabel] : ? [v10: vAval] : ? [v11: vQID] : ? % 41.52/6.41 [v12: vEntry] : ? [v13: vAnsMap] : ? [v14: vQConf] : (vgetAnswer(v9, v8) % 41.52/6.41 = v10 & vQC(v13, v6, vqempty) = v14 & vabind(v11, v10, v5) = v13 & % 41.52/6.41 vsomeQConf(v14) = v7 & vqsingle(v12) = v4 & vquestion(v11, v9, v8) = v12 % 41.52/6.41 & vAType(v8) & vLabel(v9) & vQID(v11) & vAnsMap(v13) & vOptQConf(v7) & % 41.52/6.41 vAval(v10) & vQConf(v14) & vEntry(v12)) | ? [v8: vAType] : ? [v9: % 41.52/6.41 vQID] : ? [v10: vExp] : ? [v11: vEntry] : ? [v12: vAval] : ? [v13: % 41.52/6.41 vAnsMap] : ? [v14: vQConf] : (vexpIsValue(v10) = 0 & vgetExpValue(v10) % 41.52/6.41 = v12 & vQC(v13, v6, vqempty) = v14 & vabind(v9, v12, v5) = v13 & % 41.52/6.41 vsomeQConf(v14) = v7 & vqsingle(v11) = v4 & vvalue(v9, v8, v10) = v11 & % 41.52/6.41 vAType(v8) & vQID(v9) & vExp(v10) & vAnsMap(v13) & vOptQConf(v7) & % 41.52/6.41 vAval(v12) & vQConf(v14) & vEntry(v11)) | ? [v8: vAType] : ? [v9: % 41.52/6.41 vLabel] : ? [v10: vQID] : ? [v11: vEntry] : ? [v12: vQMap] : ? [v13: % 41.52/6.41 vQConf] : (vQC(v5, v12, vqempty) = v13 & vsomeQConf(v13) = v7 & % 41.52/6.41 vqsingle(v11) = v4 & vqmbind(v10, v9, v8, v6) = v12 & vdefquestion(v10, % 41.52/6.41 v9, v8) = v11 & vAType(v8) & vLabel(v9) & vQID(v10) & vQMap(v12) & % 41.52/6.41 vOptQConf(v7) & vQConf(v13) & vEntry(v11)) | ? [v8: vOptExp] : ? [v9: % 41.52/6.41 vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : ? [v12: % 41.52/6.41 int] : (v7 = vnoQConf & ~ (v12 = 0) & ~ (v10 = v3) & ~ (v10 = v1) & % 41.52/6.41 vreduceExp(v10, v5) = v8 & visSomeExp(v8) = v12 & vqcond(v10, v9, v11) = % 41.52/6.41 v4 & vOptExp(v8) & vExp(v10) & vQuestionnaire(v11) & vQuestionnaire(v9)) % 41.52/6.41 | ? [v8: vQuestionnaire] : ? [v9: vQuestionnaire] : ? [v10: vOptQConf] % 41.52/6.41 : ? [v11: vQConf] : ? [v12: vQConf] : ( ~ (v8 = vqempty) & vreduce(v8, % 41.52/6.41 v5, v6) = v10 & vqcappend(v11, v9) = v12 & visSomeQC(v10) = 0 & % 41.52/6.41 vgetQC(v10) = v11 & vsomeQConf(v12) = v7 & vqseq(v8, v9) = v4 & % 41.52/6.41 vOptQConf(v10) & vOptQConf(v7) & vQConf(v12) & vQConf(v11) & % 41.52/6.41 vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? % 41.52/6.41 [v9: vQuestionnaire] : ? [v10: vOptQConf] : ? [v11: int] : (v7 = % 41.52/6.41 vnoQConf & ~ (v11 = 0) & ~ (v8 = vqempty) & vreduce(v8, v5, v6) = v10 % 41.52/6.41 & visSomeQC(v10) = v11 & vqseq(v8, v9) = v4 & vOptQConf(v10) & % 41.52/6.41 vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: vQID] : ? [v9: % 41.52/6.41 vOptQuestion] : ? [v10: int] : ? [v11: vEntry] : (v7 = vnoQConf & ~ % 41.52/6.41 (v10 = 0) & vlookupQMap(v8, v6) = v9 & visSomeQuestion(v9) = v10 & % 41.52/6.41 vqsingle(v11) = v4 & vask(v8) = v11 & vQID(v8) & vOptQuestion(v9) & % 41.52/6.41 vEntry(v11)) | ? [v8: vGID] : ? [v9: vQuestionnaire] : ? [v10: % 41.52/6.41 vQConf] : (vQC(v5, v6, v9) = v10 & vsomeQConf(v10) = v7 & vqgroup(v8, % 41.52/6.41 v9) = v4 & vGID(v8) & vOptQConf(v7) & vQConf(v10) & % 41.52/6.41 vQuestionnaire(v9)) | ? [v8: vQuestionnaire] : ? [v9: vQuestionnaire] % 41.52/6.41 : ? [v10: vQConf] : (vQC(v5, v6, v9) = v10 & vsomeQConf(v10) = v7 & % 41.52/6.41 vqcond(v3, v8, v9) = v4 & vOptQConf(v7) & vQConf(v10) & % 41.52/6.42 vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? % 41.52/6.42 [v9: vQuestionnaire] : ? [v10: vQConf] : (vQC(v5, v6, v8) = v10 & % 41.52/6.42 vsomeQConf(v10) = v7 & vqcond(v1, v8, v9) = v4 & vOptQConf(v7) & % 41.52/6.42 vQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: % 41.52/6.42 vQuestionnaire] : ? [v9: vQConf] : (vQC(v5, v6, v8) = v9 & % 41.52/6.42 vsomeQConf(v9) = v7 & vqseq(vqempty, v8) = v4 & vOptQConf(v7) & % 41.52/6.42 vQConf(v9) & vQuestionnaire(v8)) | (v7 = vnoQConf & v4 = vqempty))) % 41.52/6.42 % 41.52/6.42 (reduceExp-8) % 41.52/6.42 ! [v0: vExp] : ! [v1: vUnOpT] : ! [v2: vAnsMap] : ! [v3: vExp] : ! [v4: % 41.52/6.42 vOptExp] : ( ~ (vreduceExp(v3, v2) = v4) | ~ (vunop(v1, v0) = v3) | ~ % 41.52/6.42 vUnOpT(v1) | ~ vExp(v0) | ~ vAnsMap(v2) | ? [v5: any] : ? [v6: vAval] : % 41.52/6.42 ? [v7: vOptExp] : (vevalUnOp(v1, v6) = v7 & vexpIsValue(v0) = v5 & % 41.52/6.42 vgetExpValue(v0) = v6 & vOptExp(v7) & vAval(v6) & ( ~ (v5 = 0) | v7 = % 41.52/6.42 v4))) % 41.52/6.42 % 41.52/6.42 (reduceExpPreservation-unop-IH0) % 41.52/6.42 vExp(ve1) & ! [v0: vAnsMap] : ! [v1: vAType] : ! [v2: vExp] : ! [v3: % 41.52/6.42 vATMap] : ! [v4: vOptAType] : ! [v5: vOptAType] : (v5 = v4 | ~ % 41.52/6.42 (vecheck(v3, v2) = v5) | ~ (vtypeAM(v0) = v3) | ~ (vsomeAType(v1) = v4) | % 41.52/6.42 ~ vAType(v1) | ~ vExp(v2) | ~ vAnsMap(v0) | ? [v6: vOptAType] : ? [v7: % 41.52/6.42 vOptExp] : ? [v8: vOptExp] : (vecheck(v3, ve1) = v6 & vreduceExp(ve1, v0) % 41.52/6.42 = v7 & vsomeExp(v2) = v8 & vOptExp(v8) & vOptExp(v7) & vOptAType(v6) & ( ~ % 41.52/6.42 (v8 = v7) | ~ (v6 = v4)))) % 41.52/6.42 % 41.52/6.42 (reduceExpPreservation-unop-expIsValue-True) % 41.52/6.42 vExp(ve1) & ? [v0: any] : (vexpIsValue(ve1) = v0 & ? [v1: vAnsMap] : ? [v2: % 41.52/6.42 vUnOpT] : ? [v3: vAType] : ? [v4: vExp] : ? [v5: vATMap] : ? [v6: % 41.52/6.42 vExp] : ? [v7: vOptAType] : ? [v8: vOptExp] : ? [v9: vOptAType] : (v0 = % 41.52/6.42 0 & ~ (v9 = v7) & vecheck(v5, v6) = v7 & vecheck(v5, v4) = v9 & % 41.52/6.42 vtypeAM(v1) = v5 & vreduceExp(v6, v1) = v8 & vsomeExp(v4) = v8 & % 41.52/6.42 vsomeAType(v3) = v7 & vunop(v2, ve1) = v6 & vAType(v3) & vUnOpT(v2) & % 41.52/6.42 vOptExp(v8) & vExp(v6) & vExp(v4) & vAnsMap(v1) & vATMap(v5) & % 41.52/6.42 vOptAType(v9) & vOptAType(v7))) % 41.52/6.42 % 41.52/6.42 (function-axioms) % 41.52/6.44 ! [v0: vQMap] : ! [v1: vQMap] : ! [v2: vQMap] : ! [v3: vAType] : ! [v4: % 41.52/6.44 vLabel] : ! [v5: vQID] : (v1 = v0 | ~ (vqmbind(v5, v4, v3, v2) = v1) | ~ % 41.52/6.44 (vqmbind(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.52/6.44 MultipleValueBool] : ! [v2: vMapConf] : ! [v3: vQuestionnaire] : ! [v4: % 41.52/6.44 vMapConf] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, % 41.52/6.44 v2) = v0)) & ! [v0: vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : % 41.52/6.44 ! [v3: vAType] : ! [v4: vBinOpT] : (v1 = v0 | ~ (vcheckBinOp(v4, v3, v2) = % 41.52/6.44 v1) | ~ (vcheckBinOp(v4, v3, v2) = v0)) & ! [v0: vOptQConf] : ! [v1: % 41.52/6.44 vOptQConf] : ! [v2: vQMap] : ! [v3: vAnsMap] : ! [v4: vQuestionnaire] : % 41.52/6.44 (v1 = v0 | ~ (vreduce(v4, v3, v2) = v1) | ~ (vreduce(v4, v3, v2) = v0)) & ! % 41.52/6.44 [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vAval] : ! [v4: % 41.52/6.44 vBinOpT] : (v1 = v0 | ~ (vevalBinOp(v4, v3, v2) = v1) | ~ (vevalBinOp(v4, % 41.52/6.44 v3, v2) = v0)) & ! [v0: vQConf] : ! [v1: vQConf] : ! [v2: % 41.52/6.44 vQuestionnaire] : ! [v3: vQMap] : ! [v4: vAnsMap] : (v1 = v0 | ~ (vQC(v4, % 41.52/6.44 v3, v2) = v1) | ~ (vQC(v4, v3, v2) = v0)) & ! [v0: vATMap] : ! [v1: % 41.52/6.44 vATMap] : ! [v2: vATMap] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ % 41.52/6.44 (vatmbind(v4, v3, v2) = v1) | ~ (vatmbind(v4, v3, v2) = v0)) & ! [v0: % 41.52/6.44 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vAType] : ! [v3: vLabel] : % 41.52/6.44 ! [v4: vQID] : (v1 = v0 | ~ (vsomeQuestion(v4, v3, v2) = v1) | ~ % 41.52/6.44 (vsomeQuestion(v4, v3, v2) = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! % 41.52/6.44 [v2: vAnsMap] : ! [v3: vAval] : ! [v4: vQID] : (v1 = v0 | ~ (vabind(v4, v3, % 41.52/6.44 v2) = v1) | ~ (vabind(v4, v3, v2) = v0)) & ! [v0: vQuestionnaire] : ! % 41.52/6.44 [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! [v3: vQuestionnaire] : ! % 41.52/6.44 [v4: vExp] : (v1 = v0 | ~ (vqcond(v4, v3, v2) = v1) | ~ (vqcond(v4, v3, v2) % 41.52/6.44 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: vBinOpT] % 41.52/6.44 : ! [v4: vExp] : (v1 = v0 | ~ (vbinop(v4, v3, v2) = v1) | ~ (vbinop(v4, v3, % 41.52/6.44 v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! [v2: vAType] : ! % 41.52/6.44 [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ (vdefquestion(v4, v3, v2) = v1) | % 41.52/6.44 ~ (vdefquestion(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! % 41.52/6.44 [v2: vExp] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ (vvalue(v4, v3, % 41.52/6.44 v2) = v1) | ~ (vvalue(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: % 41.52/6.44 vEntry] : ! [v2: vAType] : ! [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ % 41.52/6.44 (vquestion(v4, v3, v2) = v1) | ~ (vquestion(v4, v3, v2) = v0)) & ! [v0: % 41.52/6.44 vOptAType] : ! [v1: vOptAType] : ! [v2: vExp] : ! [v3: vATMap] : (v1 = v0 % 41.52/6.44 | ~ (vecheck(v3, v2) = v1) | ~ (vecheck(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : ! [v3: vUnOpT] : (v1 = % 41.52/6.44 v0 | ~ (vcheckUnOp(v3, v2) = v1) | ~ (vcheckUnOp(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 41.52/6.44 ~ (vintersectATM(v3, v2) = v1) | ~ (vintersectATM(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 41.52/6.44 ~ (vappendATMap(v3, v2) = v1) | ~ (vappendATMap(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vOptAType] : ! [v1: vOptAType] : ! [v2: vATMap] : ! [v3: vQID] : (v1 = v0 % 41.52/6.44 | ~ (vlookupATMap(v3, v2) = v1) | ~ (vlookupATMap(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vOptExp] : ! [v1: vOptExp] : ! [v2: vAnsMap] : ! [v3: vExp] : (v1 = v0 | % 41.52/6.44 ~ (vreduceExp(v3, v2) = v1) | ~ (vreduceExp(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vUnOpT] : (v1 = v0 | % 41.52/6.44 ~ (vevalUnOp(v3, v2) = v1) | ~ (vevalUnOp(v3, v2) = v0)) & ! [v0: vAval] : % 41.52/6.44 ! [v1: vAval] : ! [v2: vAType] : ! [v3: vLabel] : (v1 = v0 | ~ % 41.52/6.44 (vgetAnswer(v3, v2) = v1) | ~ (vgetAnswer(v3, v2) = v0)) & ! [v0: vQConf] % 41.52/6.44 : ! [v1: vQConf] : ! [v2: vQuestionnaire] : ! [v3: vQConf] : (v1 = v0 | ~ % 41.52/6.44 (vqcappend(v3, v2) = v1) | ~ (vqcappend(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vQMap] : ! [v3: vQID] : (v1 % 41.52/6.44 = v0 | ~ (vlookupQMap(v3, v2) = v1) | ~ (vlookupQMap(v3, v2) = v0)) & ! % 41.52/6.44 [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vAnsMap] : ! [v3: vAnsMap] : (v1 = % 41.52/6.44 v0 | ~ (vappendAnsMap(v3, v2) = v1) | ~ (vappendAnsMap(v3, v2) = v0)) & ! % 41.52/6.44 [v0: vOptAval] : ! [v1: vOptAval] : ! [v2: vAnsMap] : ! [v3: vQID] : (v1 = % 41.52/6.44 v0 | ~ (vlookupAnsMap(v3, v2) = v1) | ~ (vlookupAnsMap(v3, v2) = v0)) & ! % 41.52/6.44 [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vATList] : (v1 = % 41.52/6.44 v0 | ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vnat] % 41.52/6.44 : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vdivide(v3, % 41.52/6.44 v2) = v1) | ~ (vdivide(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : % 41.52/6.44 ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vmultiply(v3, v2) = v1) | ~ % 41.52/6.44 (vmultiply(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : % 41.52/6.44 ! [v3: vnat] : (v1 = v0 | ~ (vminus(v3, v2) = v1) | ~ (vminus(v3, v2) = v0)) % 41.52/6.44 & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | % 41.52/6.44 ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: % 41.52/6.44 vYN] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 41.52/6.44 (vlt(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vnat] : ! [v3: % 41.52/6.44 vnat] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vYN] : ! [v1: vYN] : ! [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vor(v3, % 41.52/6.44 v2) = v1) | ~ (vor(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! % 41.52/6.44 [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vand(v3, v2) = v1) | ~ (vand(v3, % 41.52/6.44 v2) = v0)) & ! [v0: vstring] : ! [v1: vstring] : ! [v2: vstring] : ! % 41.52/6.44 [v3: vchar] : (v1 = v0 | ~ (vscons(v3, v2) = v1) | ~ (vscons(v3, v2) = v0)) % 41.52/6.44 & ! [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vAType] : % 41.52/6.44 (v1 = v0 | ~ (vatcons(v3, v2) = v1) | ~ (vatcons(v3, v2) = v0)) & ! [v0: % 41.52/6.44 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! % 41.52/6.44 [v3: vGID] : (v1 = v0 | ~ (vqgroup(v3, v2) = v1) | ~ (vqgroup(v3, v2) = v0)) % 41.52/6.44 & ! [v0: vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] % 41.52/6.44 : ! [v3: vQuestionnaire] : (v1 = v0 | ~ (vqseq(v3, v2) = v1) | ~ (vqseq(v3, % 41.52/6.45 v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: % 41.52/6.45 vUnOpT] : (v1 = v0 | ~ (vunop(v3, v2) = v1) | ~ (vunop(v3, v2) = v0)) & ! % 41.52/6.45 [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = % 41.52/6.45 v0 | ~ (vMC(v3, v2) = v1) | ~ (vMC(v3, v2) = v0)) & ! [v0: vATMap] : ! % 41.52/6.45 [v1: vATMap] : ! [v2: vQMap] : (v1 = v0 | ~ (vtypeQM(v2) = v1) | ~ % 41.52/6.45 (vtypeQM(v2) = v0)) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vAnsMap] : % 41.52/6.45 (v1 = v0 | ~ (vtypeAM(v2) = v1) | ~ (vtypeAM(v2) = v0)) & ! [v0: % 41.52/6.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptMapConf] : (v1 % 41.52/6.45 = v0 | ~ (visSomeMapConf(v2) = v1) | ~ (visSomeMapConf(v2) = v0)) & ! % 41.52/6.45 [v0: vstring] : ! [v1: vstring] : ! [v2: vLabel] : (v1 = v0 | ~ % 41.52/6.45 (vaskText(v2) = v1) | ~ (vaskText(v2) = v0)) & ! [v0: vnat] : ! [v1: % 41.52/6.45 vnat] : ! [v2: vLabel] : (v1 = v0 | ~ (vaskNumber(v2) = v1) | ~ % 41.52/6.45 (vaskNumber(v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vLabel] : (v1 % 41.52/6.45 = v0 | ~ (vaskYesNo(v2) = v1) | ~ (vaskYesNo(v2) = v0)) & ! [v0: % 41.52/6.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] : (v1 = v0 | % 41.52/6.45 ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) & ! [v0: % 41.52/6.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptExp] : (v1 = % 41.52/6.45 v0 | ~ (visSomeExp(v2) = v1) | ~ (visSomeExp(v2) = v0)) & ! [v0: % 41.52/6.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQConf] : (v1 = % 41.52/6.45 v0 | ~ (visSomeQC(v2) = v1) | ~ (visSomeQC(v2) = v0)) & ! [v0: % 41.52/6.45 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuestionnaire] : % 41.52/6.45 (v1 = v0 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 41.52/6.45 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQConf] : (v1 = v0 | ~ % 41.52/6.45 (vgetQuest(v2) = v1) | ~ (vgetQuest(v2) = v0)) & ! [v0: vQMap] : ! [v1: % 41.52/6.45 vQMap] : ! [v2: vQConf] : (v1 = v0 | ~ (vgetQM(v2) = v1) | ~ (vgetQM(v2) % 41.52/6.45 = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vQConf] : (v1 = v0 % 41.52/6.45 | ~ (vgetAM(v2) = v1) | ~ (vgetAM(v2) = v0)) & ! [v0: MultipleValueBool] % 41.52/6.45 : ! [v1: MultipleValueBool] : ! [v2: vOptQuestion] : (v1 = v0 | ~ % 41.52/6.45 (visSomeQuestion(v2) = v1) | ~ (visSomeQuestion(v2) = v0)) & ! [v0: % 41.52/6.45 vAType] : ! [v1: vAType] : ! [v2: vAval] : (v1 = v0 | ~ (vtypeOf(v2) = % 41.52/6.45 v1) | ~ (vtypeOf(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.52/6.45 MultipleValueBool] : ! [v2: vOptAType] : (v1 = v0 | ~ (visSomeAType(v2) = % 41.52/6.45 v1) | ~ (visSomeAType(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.52/6.45 MultipleValueBool] : ! [v2: vOptAval] : (v1 = v0 | ~ (visSomeAval(v2) = % 41.52/6.45 v1) | ~ (visSomeAval(v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: % 41.52/6.45 vnat] : (v1 = v0 | ~ (vpred(v2) = v1) | ~ (vpred(v2) = v0)) & ! [v0: vYN] % 41.52/6.45 : ! [v1: vYN] : ! [v2: vYN] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) = % 41.52/6.45 v0)) & ! [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vOptMapConf] : (v1 % 41.52/6.45 = v0 | ~ (vgetMapConf(v2) = v1) | ~ (vgetMapConf(v2) = v0)) & ! [v0: % 41.52/6.45 vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ (vgetExpValue(v2) = % 41.52/6.45 v1) | ~ (vgetExpValue(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 41.52/6.45 [v2: vOptExp] : (v1 = v0 | ~ (vgetExp(v2) = v1) | ~ (vgetExp(v2) = v0)) & ! % 41.52/6.45 [v0: vQConf] : ! [v1: vQConf] : ! [v2: vOptQConf] : (v1 = v0 | ~ % 41.52/6.45 (vgetQC(v2) = v1) | ~ (vgetQC(v2) = v0)) & ! [v0: vAType] : ! [v1: % 41.52/6.45 vAType] : ! [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionAType(v2) = v1) % 41.52/6.45 | ~ (vgetQuestionAType(v2) = v0)) & ! [v0: vLabel] : ! [v1: vLabel] : ! % 41.52/6.45 [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionLabel(v2) = v1) | ~ % 41.52/6.45 (vgetQuestionLabel(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: % 41.52/6.45 vOptQuestion] : (v1 = v0 | ~ (vgetQuestionQID(v2) = v1) | ~ % 41.52/6.45 (vgetQuestionQID(v2) = v0)) & ! [v0: vAType] : ! [v1: vAType] : ! [v2: % 41.52/6.45 vOptAType] : (v1 = v0 | ~ (vgetAType(v2) = v1) | ~ (vgetAType(v2) = v0)) & % 41.52/6.45 ! [v0: vAval] : ! [v1: vAval] : ! [v2: vOptAval] : (v1 = v0 | ~ % 41.52/6.45 (vgetAval(v2) = v1) | ~ (vgetAval(v2) = v0)) & ! [v0: vOptAval] : ! [v1: % 41.52/6.45 vOptAval] : ! [v2: vAval] : (v1 = v0 | ~ (vsomeAval(v2) = v1) | ~ % 41.52/6.45 (vsomeAval(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: vQID] : (v1 % 41.52/6.45 = v0 | ~ (venumQID(v2) = v1) | ~ (venumQID(v2) = v0)) & ! [v0: % 41.52/6.45 vOptMapConf] : ! [v1: vOptMapConf] : ! [v2: vMapConf] : (v1 = v0 | ~ % 41.52/6.45 (vsomeMapConf(v2) = v1) | ~ (vsomeMapConf(v2) = v0)) & ! [v0: vGID] : ! % 41.52/6.45 [v1: vGID] : ! [v2: vGID] : (v1 = v0 | ~ (venumGID(v2) = v1) | ~ % 41.52/6.45 (venumGID(v2) = v0)) & ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vExp] : % 41.52/6.45 (v1 = v0 | ~ (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) & ! [v0: vAval] : % 41.52/6.45 ! [v1: vAval] : ! [v2: vstring] : (v1 = v0 | ~ (vT(v2) = v1) | ~ (vT(v2) = % 41.52/6.45 v0)) & ! [v0: vAval] : ! [v1: vAval] : ! [v2: vnat] : (v1 = v0 | ~ % 41.52/6.45 (vNum(v2) = v1) | ~ (vNum(v2) = v0)) & ! [v0: vAval] : ! [v1: vAval] : ! % 41.52/6.45 [v2: vYN] : (v1 = v0 | ~ (vB(v2) = v1) | ~ (vB(v2) = v0)) & ! [v0: % 41.52/6.45 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : (v1 = v0 | ~ % 41.52/6.45 (vsomeAType(v2) = v1) | ~ (vsomeAType(v2) = v0)) & ! [v0: vOptQConf] : ! % 41.52/6.45 [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | ~ (vsomeQConf(v2) = v1) | ~ % 41.52/6.45 (vsomeQConf(v2) = v0)) & ! [v0: vchar] : ! [v1: vchar] : ! [v2: vchar] : % 41.52/6.45 (v1 = v0 | ~ (venumchar(v2) = v1) | ~ (venumchar(v2) = v0)) & ! [v0: % 41.52/6.45 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vEntry] : (v1 = v0 | ~ % 41.52/6.45 (vqsingle(v2) = v1) | ~ (vqsingle(v2) = v0)) & ! [v0: vnat] : ! [v1: % 41.52/6.45 vnat] : ! [v2: vnat] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = % 41.52/6.45 v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vQID] : (v1 = v0 | ~ % 41.52/6.45 (vqvar(v2) = v1) | ~ (vqvar(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 41.52/6.45 [v2: vAval] : (v1 = v0 | ~ (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & % 41.52/6.45 ! [v0: vLabel] : ! [v1: vLabel] : ! [v2: vLabel] : (v1 = v0 | ~ % 41.52/6.45 (venumLabel(v2) = v1) | ~ (venumLabel(v2) = v0)) & ! [v0: vEntry] : ! % 41.52/6.45 [v1: vEntry] : ! [v2: vQID] : (v1 = v0 | ~ (vask(v2) = v1) | ~ (vask(v2) = % 41.52/6.45 v0)) % 41.52/6.45 % 41.52/6.45 Further assumptions not needed in the proof: % 41.52/6.45 -------------------------------------------- % 41.52/6.45 DIFF-B-Num, DIFF-B-T, DIFF-Num-T, DIFF-Number-Text, DIFF-YesNo-Number, % 41.52/6.45 DIFF-YesNo-Text, DIFF-addop-andop, DIFF-addop-divop, DIFF-addop-eqop, % 41.52/6.45 DIFF-addop-gtop, DIFF-addop-ltop, DIFF-addop-mulop, DIFF-addop-orop, % 41.52/6.45 DIFF-addop-subop, DIFF-aempty-abind, DIFF-andop-orop, DIFF-atempty-atcons, % 41.52/6.45 DIFF-atmempty-atmbind, DIFF-binop-unop, DIFF-constant-binop, DIFF-constant-qvar, % 41.52/6.45 DIFF-constant-unop, DIFF-defquestion-ask, DIFF-divop-andop, DIFF-divop-eqop, % 41.52/6.45 DIFF-divop-gtop, DIFF-divop-ltop, DIFF-divop-orop, DIFF-eqop-andop, % 41.52/6.45 DIFF-eqop-gtop, DIFF-eqop-ltop, DIFF-eqop-orop, DIFF-gtop-andop, DIFF-gtop-ltop, % 41.52/6.45 DIFF-gtop-orop, DIFF-initGID-enumGID, DIFF-initLabel-enumLabel, % 41.52/6.45 DIFF-initQID-enumQID, DIFF-initchar-enumchar, DIFF-ltop-andop, DIFF-ltop-orop, % 41.52/6.45 DIFF-mulop-andop, DIFF-mulop-divop, DIFF-mulop-eqop, DIFF-mulop-gtop, % 41.52/6.45 DIFF-mulop-ltop, DIFF-mulop-orop, DIFF-noAType-someAType, DIFF-noAval-someAval, % 41.52/6.45 DIFF-noExp-someExp, DIFF-noMapConf-someMapConf, DIFF-noQConf-someQConf, % 41.52/6.45 DIFF-noQuestion-someQuestion, DIFF-qcond-qgroup, DIFF-qempty-qcond, % 41.52/6.45 DIFF-qempty-qgroup, DIFF-qempty-qseq, DIFF-qempty-qsingle, DIFF-qmempty-qmbind, % 41.52/6.45 DIFF-qseq-qcond, DIFF-qseq-qgroup, DIFF-qsingle-qcond, DIFF-qsingle-qgroup, % 41.52/6.45 DIFF-qsingle-qseq, DIFF-question-ask, DIFF-question-defquestion, % 41.52/6.45 DIFF-question-value, DIFF-qvar-binop, DIFF-qvar-unop, DIFF-sempty-scons, % 41.52/6.45 DIFF-subop-andop, DIFF-subop-divop, DIFF-subop-eqop, DIFF-subop-gtop, % 41.52/6.45 DIFF-subop-ltop, DIFF-subop-mulop, DIFF-subop-orop, DIFF-value-ask, % 41.52/6.45 DIFF-value-defquestion, DIFF-yes-no, DIFF-zero-succ, EQ-B, EQ-MC, EQ-Num, EQ-QC, % 41.52/6.45 EQ-T, EQ-abind, EQ-ask, EQ-atcons, EQ-atmbind, EQ-binop, EQ-constant, % 41.52/6.45 EQ-defquestion, EQ-enumGID, EQ-enumLabel, EQ-enumQID, EQ-enumchar, EQ-qcond, % 41.52/6.45 EQ-qgroup, EQ-qmbind, EQ-qseq, EQ-qsingle, EQ-question, EQ-qvar, EQ-scons, % 41.52/6.45 EQ-someAType, EQ-someAval, EQ-someExp, EQ-someMapConf, EQ-someQConf, % 41.52/6.45 EQ-someQuestion, EQ-succ, EQ-unop, EQ-value, Task, Task_inv1, Task_inv2, % 41.52/6.45 Task_inv3, Task_inv4, Tdefquestion, Tdefquestion_inv1, Tdefquestion_inv2, % 41.52/6.45 Tdefquestion_inv3, Tqcond, Tqcond_inv1, Tqcond_inv2, Tqcond_inv3, Tqcond_inv4, % 41.52/6.45 Tqcond_inv5, Tqcond_inv6, Tqcond_inv7, Tqempty, Tqempty_inv1, Tqempty_inv2, % 41.52/6.45 Tqgroup, Tqgroup_inv, Tqseq, Tqseq_inv1, Tqseq_inv2, Tqseq_inv3, Tqseq_inv4, % 41.52/6.45 Tquestion, Tquestion_inv1, Tquestion_inv2, Tquestion_inv3, Tvalue, Tvalue_inv1, % 41.52/6.45 Tvalue_inv2, Tvalue_inv3, Tvalue_inv4, and-0, and-1, and-INV, append-0, % 41.52/6.45 append-1, append-INV, appendATMap-0, appendATMap-1, appendATMap-INV, % 41.52/6.45 appendAnsMap-0, appendAnsMap-1, appendAnsMap-INV, checkBinOp-0, checkBinOp-1, % 41.52/6.45 checkBinOp-2, checkBinOp-3, checkBinOp-4, checkBinOp-5, checkBinOp-6, % 41.52/6.45 checkBinOp-7, checkBinOp-8, checkBinOp-9, checkBinOp-INV, checkUnOp-0, % 41.52/6.45 checkUnOp-1, checkUnOp-INV, divide-0, divide-1, divide-INV, dom-ATList, % 41.52/6.45 dom-ATMap, dom-AType, dom-AnsMap, dom-Aval, dom-BinOpT, dom-Entry, dom-Exp, % 41.52/6.45 dom-MapConf, dom-OptAType, dom-OptAval, dom-OptExp, dom-OptMapConf, % 41.52/6.45 dom-OptQConf, dom-OptQuestion, dom-QConf, dom-QMap, dom-Questionnaire, % 41.52/6.45 dom-UnOpT, dom-YN, dom-nat, dom-string, echeck-0, echeck-1, echeck-2, echeck-3, % 41.52/6.45 echeck-4, echeck-5, echeck-6, echeck-7, echeck-INV, evalBinOp-0, evalBinOp-1, % 41.52/6.45 evalBinOp-10, evalBinOp-2, evalBinOp-3, evalBinOp-4, evalBinOp-5, evalBinOp-6, % 41.52/6.45 evalBinOp-7, evalUnOp-1, evalUnOp-INV, expIsValue-0, expIsValue-false-INV, % 41.52/6.45 getAM-0, getAM-INV, getAType-0, getAnswer-0, getAnswer-1, getAnswer-2, % 41.52/6.45 getAnswer-INV, getAval-0, getExp-0, getMapConf-0, getQC-0, getQM-0, getQM-INV, % 41.52/6.45 getQuest-0, getQuest-INV, getQuestionAType-0, getQuestionLabel-0, % 41.52/6.45 getQuestionQID-0, gt-0, gt-1, gt-2, gt-INV, intersectATM-0, intersectATM-1, % 41.52/6.45 intersectATM-2, intersectATM-INV, isSomeAType-0, isSomeAType-1, % 41.52/6.45 isSomeAType-false-INV, isSomeAType-true-INV, isSomeAval-0, isSomeAval-1, % 41.52/6.45 isSomeAval-false-INV, isSomeAval-true-INV, isSomeExp-0, isSomeExp-1, % 41.52/6.45 isSomeExp-false-INV, isSomeExp-true-INV, isSomeMapConf-0, isSomeMapConf-1, % 41.52/6.45 isSomeMapConf-false-INV, isSomeMapConf-true-INV, isSomeQC-0, isSomeQC-1, % 41.52/6.45 isSomeQC-false-INV, isSomeQC-true-INV, isSomeQuestion-0, isSomeQuestion-1, % 41.52/6.45 isSomeQuestion-false-INV, isSomeQuestion-true-INV, isValue-0, isValue-1, % 41.52/6.45 isValue-false-INV, isValue-true-INV, lookupATMap-0, lookupATMap-1, % 41.52/6.45 lookupATMap-2, lookupATMap-INV, lookupAnsMap-0, lookupAnsMap-1, lookupAnsMap-2, % 41.52/6.45 lookupAnsMap-INV, lookupQMap-0, lookupQMap-1, lookupQMap-2, lookupQMap-INV, % 41.52/6.45 lt-0, lt-1, lt-2, lt-INV, minus-0, minus-1, minus-INV, multiply-0, multiply-1, % 41.52/6.45 multiply-INV, not-INV, or-0, or-1, or-INV, plus-0, plus-1, plus-INV, pred-0, % 41.52/6.45 pred-1, pred-INV, qcappend-0, qcappend-INV, reduce-0, reduce-1, reduce-10, % 41.52/6.45 reduce-15, reduce-2, reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, reduce-8, % 41.52/6.45 reduce-9, reduceExp-0, reduceExp-1, reduceExp-10, reduceExp-2, reduceExp-3, % 41.52/6.45 reduceExp-4, reduceExp-5, reduceExp-6, reduceExp-7, reduceExp-9, reduceExp-INV, % 41.52/6.45 typeAM-0, typeAM-1, typeAM-INV, typeOf-0, typeOf-1, typeOf-2, typeOf-INV, % 41.52/6.45 typeQM-0, typeQM-1, typeQM-INV % 41.52/6.45 % 41.52/6.45 Those formulas are unsatisfiable: % 41.52/6.45 --------------------------------- % 41.52/6.45 % 41.52/6.45 Begin of proof % 41.52/6.45 | % 41.52/6.45 | ALPHA: (not-0) implies: % 41.52/6.45 | (1) vnot(vyes) = vno % 41.52/6.45 | % 41.52/6.45 | ALPHA: (not-1) implies: % 41.52/6.45 | (2) vnot(vno) = vyes % 41.52/6.45 | % 41.52/6.45 | ALPHA: (evalBinOp-8) implies: % 41.52/6.45 | (3) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] : (vsomeExp(v1) = v2 % 41.52/6.45 | & vB(vyes) = v0 & vconstant(v0) = v1 & vOptExp(v2) & vExp(v1) & % 41.52/6.45 | vAval(v0) & ! [v3: vAval] : ! [v4: vOptExp] : (v4 = v2 | ~ % 41.52/6.45 | (vevalBinOp(veqop, v3, v3) = v4) | ~ vAval(v3))) % 41.52/6.45 | % 41.52/6.45 | ALPHA: (evalBinOp-9) implies: % 41.52/6.45 | (4) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] : (vsomeExp(v1) = v2 % 41.52/6.45 | & vB(vno) = v0 & vconstant(v0) = v1 & vOptExp(v2) & vExp(v1) & % 41.52/6.45 | vAval(v0) & ! [v3: vAval] : ! [v4: vAval] : ! [v5: vOptExp] : (v5 % 41.52/6.45 | = v2 | v4 = v3 | ~ (vevalBinOp(veqop, v3, v4) = v5) | ~ vAval(v4) % 41.52/6.45 | | ~ vAval(v3))) % 41.52/6.45 | % 41.52/6.45 | ALPHA: (evalBinOp-INV) implies: % 41.52/6.46 | (5) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] : ? [v3: vAval] : ? % 41.52/6.46 | [v4: vExp] : ? [v5: vOptExp] : (vsomeExp(v4) = v5 & vsomeExp(v1) = v2 % 41.52/6.46 | & vB(vno) = v3 & vB(vyes) = v0 & vconstant(v3) = v4 & vconstant(v0) = % 41.52/6.46 | v1 & vOptExp(v5) & vOptExp(v2) & vExp(v4) & vExp(v1) & vAval(v3) & % 41.52/6.46 | vAval(v0) & ! [v6: vBinOpT] : ! [v7: vAval] : ! [v8: vAval] : ! % 41.52/6.46 | [v9: vOptExp] : ( ~ (vevalBinOp(v6, v7, v8) = v9) | ~ vBinOpT(v6) | % 41.52/6.46 | ~ vAval(v8) | ~ vAval(v7) | ? [v10: vnat] : ? [v11: vnat] : ? % 41.52/6.46 | [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] : (v6 = vgtop & % 41.52/6.46 | vgt(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v11) = v8 & % 41.52/6.46 | vNum(v10) = v7 & vB(v12) = v13 & vconstant(v13) = v14 & % 41.52/6.46 | vOptExp(v9) & vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13) & % 41.52/6.46 | vYN(v12)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vYN] : ? % 41.52/6.46 | [v13: vAval] : ? [v14: vExp] : (v6 = vltop & vlt(v10, v11) = v12 & % 41.52/6.46 | vsomeExp(v14) = v9 & vNum(v11) = v8 & vNum(v10) = v7 & vB(v12) = % 41.52/6.46 | v13 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v11) & vnat(v10) % 41.52/6.46 | & vExp(v14) & vAval(v13) & vYN(v12)) | ? [v10: vnat] : ? [v11: % 41.52/6.46 | vnat] : ? [v12: vnat] : ? [v13: vAval] : ? [v14: vExp] : (v6 = % 41.52/6.46 | vaddop & vplus(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v12) = % 41.52/6.46 | v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 & % 41.52/6.46 | vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 41.52/6.46 | vAval(v13)) | ? [v10: vYN] : ? [v11: vYN] : ? [v12: vYN] : ? % 41.52/6.46 | [v13: vAval] : ? [v14: vExp] : (v6 = vorop & vor(v10, v11) = v12 & % 41.52/6.46 | vsomeExp(v14) = v9 & vB(v12) = v13 & vB(v11) = v8 & vB(v10) = v7 % 41.52/6.46 | & vconstant(v13) = v14 & vOptExp(v9) & vExp(v14) & vAval(v13) & % 41.52/6.46 | vYN(v12) & vYN(v11) & vYN(v10)) | ? [v10: vnat] : ? [v11: vnat] % 41.52/6.46 | : ? [v12: vnat] : ? [v13: vAval] : ? [v14: vExp] : (v6 = vmulop % 41.52/6.46 | & vmultiply(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v12) = % 41.52/6.46 | v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 & % 41.52/6.46 | vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 41.52/6.46 | vAval(v13)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] : % 41.52/6.46 | ? [v13: vAval] : ? [v14: vExp] : (v6 = vdivop & vdivide(v10, v11) % 41.52/6.46 | = v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & vNum(v11) = v8 & % 41.52/6.46 | vNum(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v12) & % 41.52/6.46 | vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13)) | ? [v10: vYN] : % 41.52/6.46 | ? [v11: vYN] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] : % 41.52/6.46 | (v6 = vandop & vand(v10, v11) = v12 & vsomeExp(v14) = v9 & vB(v12) % 41.52/6.46 | = v13 & vB(v11) = v8 & vB(v10) = v7 & vconstant(v13) = v14 & % 41.52/6.46 | vOptExp(v9) & vExp(v14) & vAval(v13) & vYN(v12) & vYN(v11) & % 41.52/6.46 | vYN(v10)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] : ? % 41.52/6.46 | [v13: vAval] : ? [v14: vExp] : (v6 = vsubop & vminus(v10, v11) = % 41.52/6.46 | v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & vNum(v11) = v8 & % 41.52/6.46 | vNum(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v12) & % 41.52/6.46 | vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13)) | (v9 = v5 & v6 = % 41.52/6.46 | veqop & ~ (v8 = v7)) | (v9 = v2 & v8 = v7 & v6 = veqop) | (v9 = % 41.52/6.46 | vnoExp & ~ (v6 = veqop) & ( ~ (v6 = vorop) | ! [v10: vYN] : ( ~ % 41.52/6.46 | (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ (vB(v10) % 41.52/6.46 | = v7) | ~ vYN(v10))) & ( ~ (v6 = vandop) | ! [v10: vYN] : % 41.52/6.46 | ( ~ (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ % 41.52/6.46 | (vB(v10) = v7) | ~ vYN(v10))) & ( ! [v10: vnat] : ( ~ % 41.52/6.46 | (vNum(v10) = v8) | ~ vnat(v10)) | ! [v10: vnat] : ( ~ % 41.52/6.46 | (vNum(v10) = v7) | ~ vnat(v10)) | ( ~ (v6 = vgtop) & ~ (v6 % 41.52/6.46 | = vltop) & ~ (v6 = vaddop) & ~ (v6 = vmulop) & ~ (v6 = % 41.52/6.46 | vdivop) & ~ (v6 = vsubop)))))) % 41.52/6.46 | % 41.52/6.46 | ALPHA: (evalUnOp-0) implies: % 41.52/6.46 | (6) ! [v0: vYN] : ! [v1: vYN] : ( ~ (vnot(v0) = v1) | ~ vYN(v0) | ? % 41.52/6.46 | [v2: vAval] : ? [v3: vOptExp] : ? [v4: vAval] : ? [v5: vExp] : % 41.52/6.46 | (vevalUnOp(vnotop, v2) = v3 & vsomeExp(v5) = v3 & vB(v1) = v4 & % 41.52/6.46 | vB(v0) = v2 & vconstant(v4) = v5 & vOptExp(v3) & vExp(v5) & % 41.52/6.46 | vAval(v4) & vAval(v2))) % 41.52/6.46 | % 41.52/6.46 | ALPHA: (reduce-11) implies: % 41.52/6.47 | (7) ? [v0: vAval] : ? [v1: vExp] : (vB(vyes) = v0 & vconstant(v0) = v1 & % 41.52/6.47 | vExp(v1) & vAval(v0) & ! [v2: vQuestionnaire] : ! [v3: % 41.52/6.47 | vQuestionnaire] : ! [v4: vAnsMap] : ! [v5: vQMap] : ! [v6: % 41.52/6.47 | vQuestionnaire] : ! [v7: vOptQConf] : ( ~ (vreduce(v6, v4, v5) = % 41.52/6.47 | v7) | ~ (vqcond(v1, v2, v3) = v6) | ~ vQMap(v5) | ~ % 41.52/6.47 | vAnsMap(v4) | ~ vQuestionnaire(v3) | ~ vQuestionnaire(v2) | ? % 41.52/6.47 | [v8: vQConf] : (vQC(v4, v5, v2) = v8 & vsomeQConf(v8) = v7 & % 41.52/6.47 | vOptQConf(v7) & vQConf(v8)))) % 41.52/6.47 | % 41.52/6.47 | ALPHA: (reduce-12) implies: % 41.52/6.47 | (8) ? [v0: vAval] : ? [v1: vExp] : (vB(vno) = v0 & vconstant(v0) = v1 & % 41.52/6.47 | vExp(v1) & vAval(v0) & ! [v2: vQuestionnaire] : ! [v3: % 41.52/6.47 | vQuestionnaire] : ! [v4: vAnsMap] : ! [v5: vQMap] : ! [v6: % 41.52/6.47 | vQuestionnaire] : ! [v7: vOptQConf] : ( ~ (vreduce(v6, v4, v5) = % 41.52/6.47 | v7) | ~ (vqcond(v1, v2, v3) = v6) | ~ vQMap(v5) | ~ % 41.52/6.47 | vAnsMap(v4) | ~ vQuestionnaire(v3) | ~ vQuestionnaire(v2) | ? % 41.52/6.47 | [v8: vQConf] : (vQC(v4, v5, v3) = v8 & vsomeQConf(v8) = v7 & % 41.52/6.47 | vOptQConf(v7) & vQConf(v8)))) % 41.52/6.47 | % 41.52/6.47 | ALPHA: (reduce-13) implies: % 41.52/6.47 | (9) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.52/6.47 | (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = v1 % 41.52/6.47 | & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: vQMap] : ! % 41.52/6.47 | [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : ! [v8: % 41.52/6.47 | vQuestionnaire] : ! [v9: vOptExp] : ! [v10: vExp] : ! [v11: % 41.52/6.47 | vQuestionnaire] : ! [v12: vQConf] : (v6 = v3 | v6 = v1 | ~ % 41.52/6.47 | (vreduceExp(v6, v7) = v9) | ~ (vgetExp(v9) = v10) | ~ (vQC(v7, % 41.52/6.47 | v4, v11) = v12) | ~ (vqcond(v10, v5, v8) = v11) | ~ vQMap(v4) % 41.52/6.47 | | ~ vExp(v6) | ~ vAnsMap(v7) | ~ vQuestionnaire(v8) | ~ % 41.52/6.47 | vQuestionnaire(v5) | ? [v13: any] : ? [v14: vQuestionnaire] : ? % 41.52/6.47 | [v15: vOptQConf] : ? [v16: vOptQConf] : (vreduce(v14, v7, v4) = % 41.52/6.47 | v15 & visSomeExp(v9) = v13 & vsomeQConf(v12) = v16 & vqcond(v6, % 41.52/6.47 | v5, v8) = v14 & vOptQConf(v16) & vOptQConf(v15) & % 41.52/6.47 | vQuestionnaire(v14) & ( ~ (v13 = 0) | v16 = v15)))) % 41.52/6.47 | % 41.52/6.47 | ALPHA: (reduce-14) implies: % 41.52/6.47 | (10) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.52/6.47 | (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = % 41.52/6.47 | v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: vQMap] : % 41.52/6.47 | ! [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : ! [v8: % 41.52/6.47 | vQuestionnaire] : ! [v9: vQuestionnaire] : ! [v10: vOptQConf] : % 41.52/6.47 | (v10 = vnoQConf | v6 = v3 | v6 = v1 | ~ (vreduce(v9, v7, v4) = v10) % 41.52/6.47 | | ~ (vqcond(v6, v5, v8) = v9) | ~ vQMap(v4) | ~ vExp(v6) | ~ % 41.52/6.47 | vAnsMap(v7) | ~ vQuestionnaire(v8) | ~ vQuestionnaire(v5) | ? % 41.52/6.47 | [v11: vOptExp] : (vreduceExp(v6, v7) = v11 & visSomeExp(v11) = 0 & % 41.52/6.47 | vOptExp(v11)))) % 41.52/6.47 | % 41.52/6.47 | ALPHA: (reduce-INV) implies: % 41.52/6.47 | (11) vYN(vyes) % 41.52/6.47 | (12) vYN(vno) % 41.52/6.48 | (13) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.52/6.48 | (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = % 41.52/6.48 | v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: % 41.52/6.48 | vQuestionnaire] : ! [v5: vAnsMap] : ! [v6: vQMap] : ! [v7: % 41.52/6.48 | vOptQConf] : ( ~ (vreduce(v4, v5, v6) = v7) | ~ vQMap(v6) | ~ % 41.52/6.48 | vAnsMap(v5) | ~ vQuestionnaire(v4) | ? [v8: vAType] : ? [v9: % 41.52/6.48 | vOptExp] : ? [v10: vQID] : ? [v11: vExp] : ? [v12: int] : ? % 41.52/6.48 | [v13: vEntry] : ? [v14: vExp] : ? [v15: vEntry] : ? [v16: % 41.52/6.48 | vQuestionnaire] : ? [v17: vQConf] : ( ~ (v12 = 0) & % 41.52/6.48 | vreduceExp(v11, v5) = v9 & vexpIsValue(v11) = v12 & % 41.52/6.48 | visSomeExp(v9) = 0 & vgetExp(v9) = v14 & vQC(v5, v6, v16) = v17 % 41.52/6.48 | & vsomeQConf(v17) = v7 & vqsingle(v15) = v16 & vqsingle(v13) = % 41.52/6.48 | v4 & vvalue(v10, v8, v14) = v15 & vvalue(v10, v8, v11) = v13 & % 41.52/6.48 | vAType(v8) & vOptExp(v9) & vQID(v10) & vExp(v14) & vExp(v11) & % 41.52/6.48 | vOptQConf(v7) & vQConf(v17) & vQuestionnaire(v16) & vEntry(v15) % 41.52/6.48 | & vEntry(v13)) | ? [v8: vQID] : ? [v9: vOptQuestion] : ? % 41.52/6.48 | [v10: vEntry] : ? [v11: vLabel] : ? [v12: vAType] : ? [v13: % 41.52/6.48 | vEntry] : ? [v14: vQuestionnaire] : ? [v15: vQConf] : % 41.52/6.48 | (vlookupQMap(v8, v6) = v9 & visSomeQuestion(v9) = 0 & % 41.52/6.48 | vgetQuestionAType(v9) = v12 & vgetQuestionLabel(v9) = v11 & % 41.52/6.48 | vQC(v5, v6, v14) = v15 & vsomeQConf(v15) = v7 & vqsingle(v13) = % 41.52/6.48 | v14 & vqsingle(v10) = v4 & vask(v8) = v10 & vquestion(v8, v11, % 41.52/6.48 | v12) = v13 & vAType(v12) & vLabel(v11) & vQID(v8) & % 41.52/6.48 | vOptQuestion(v9) & vOptQConf(v7) & vQConf(v15) & % 41.52/6.48 | vQuestionnaire(v14) & vEntry(v13) & vEntry(v10)) | ? [v8: % 41.52/6.48 | vAType] : ? [v9: vOptExp] : ? [v10: vQID] : ? [v11: vExp] : % 41.52/6.48 | ? [v12: int] : ? [v13: int] : ? [v14: vEntry] : (v7 = vnoQConf & % 41.52/6.48 | ~ (v13 = 0) & ~ (v12 = 0) & vreduceExp(v11, v5) = v9 & % 41.52/6.48 | vexpIsValue(v11) = v12 & visSomeExp(v9) = v13 & vqsingle(v14) = % 41.52/6.48 | v4 & vvalue(v10, v8, v11) = v14 & vAType(v8) & vOptExp(v9) & % 41.52/6.48 | vQID(v10) & vExp(v11) & vEntry(v14)) | ? [v8: vOptExp] : ? % 41.52/6.48 | [v9: vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : % 41.52/6.48 | ? [v12: vExp] : ? [v13: vQuestionnaire] : ? [v14: vQConf] : ( ~ % 41.52/6.48 | (v10 = v3) & ~ (v10 = v1) & vreduceExp(v10, v5) = v8 & % 41.52/6.48 | visSomeExp(v8) = 0 & vgetExp(v8) = v12 & vQC(v5, v6, v13) = v14 % 41.52/6.48 | & vsomeQConf(v14) = v7 & vqcond(v12, v9, v11) = v13 & % 41.52/6.48 | vqcond(v10, v9, v11) = v4 & vOptExp(v8) & vExp(v12) & vExp(v10) % 41.52/6.48 | & vOptQConf(v7) & vQConf(v14) & vQuestionnaire(v13) & % 41.52/6.48 | vQuestionnaire(v11) & vQuestionnaire(v9)) | ? [v8: vAType] : ? % 41.52/6.48 | [v9: vLabel] : ? [v10: vAval] : ? [v11: vQID] : ? [v12: vEntry] % 41.52/6.48 | : ? [v13: vAnsMap] : ? [v14: vQConf] : (vgetAnswer(v9, v8) = v10 % 41.52/6.48 | & vQC(v13, v6, vqempty) = v14 & vabind(v11, v10, v5) = v13 & % 41.52/6.48 | vsomeQConf(v14) = v7 & vqsingle(v12) = v4 & vquestion(v11, v9, % 41.52/6.48 | v8) = v12 & vAType(v8) & vLabel(v9) & vQID(v11) & vAnsMap(v13) % 41.52/6.48 | & vOptQConf(v7) & vAval(v10) & vQConf(v14) & vEntry(v12)) | ? % 41.52/6.48 | [v8: vAType] : ? [v9: vQID] : ? [v10: vExp] : ? [v11: vEntry] : % 41.52/6.48 | ? [v12: vAval] : ? [v13: vAnsMap] : ? [v14: vQConf] : % 41.52/6.48 | (vexpIsValue(v10) = 0 & vgetExpValue(v10) = v12 & vQC(v13, v6, % 41.52/6.48 | vqempty) = v14 & vabind(v9, v12, v5) = v13 & vsomeQConf(v14) = % 41.52/6.48 | v7 & vqsingle(v11) = v4 & vvalue(v9, v8, v10) = v11 & vAType(v8) % 41.52/6.48 | & vQID(v9) & vExp(v10) & vAnsMap(v13) & vOptQConf(v7) & % 41.52/6.48 | vAval(v12) & vQConf(v14) & vEntry(v11)) | ? [v8: vAType] : ? % 41.52/6.48 | [v9: vLabel] : ? [v10: vQID] : ? [v11: vEntry] : ? [v12: vQMap] % 41.52/6.48 | : ? [v13: vQConf] : (vQC(v5, v12, vqempty) = v13 & % 41.52/6.48 | vsomeQConf(v13) = v7 & vqsingle(v11) = v4 & vqmbind(v10, v9, v8, % 41.52/6.48 | v6) = v12 & vdefquestion(v10, v9, v8) = v11 & vAType(v8) & % 41.52/6.48 | vLabel(v9) & vQID(v10) & vQMap(v12) & vOptQConf(v7) & % 41.52/6.48 | vQConf(v13) & vEntry(v11)) | ? [v8: vOptExp] : ? [v9: % 41.52/6.48 | vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : ? % 41.52/6.48 | [v12: int] : (v7 = vnoQConf & ~ (v12 = 0) & ~ (v10 = v3) & ~ % 41.52/6.48 | (v10 = v1) & vreduceExp(v10, v5) = v8 & visSomeExp(v8) = v12 & % 41.52/6.48 | vqcond(v10, v9, v11) = v4 & vOptExp(v8) & vExp(v10) & % 41.52/6.48 | vQuestionnaire(v11) & vQuestionnaire(v9)) | ? [v8: % 41.52/6.48 | vQuestionnaire] : ? [v9: vQuestionnaire] : ? [v10: vOptQConf] % 41.52/6.48 | : ? [v11: vQConf] : ? [v12: vQConf] : ( ~ (v8 = vqempty) & % 41.52/6.48 | vreduce(v8, v5, v6) = v10 & vqcappend(v11, v9) = v12 & % 41.52/6.48 | visSomeQC(v10) = 0 & vgetQC(v10) = v11 & vsomeQConf(v12) = v7 & % 41.52/6.48 | vqseq(v8, v9) = v4 & vOptQConf(v10) & vOptQConf(v7) & % 41.52/6.48 | vQConf(v12) & vQConf(v11) & vQuestionnaire(v9) & % 41.52/6.48 | vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? [v9: % 41.52/6.48 | vQuestionnaire] : ? [v10: vOptQConf] : ? [v11: int] : (v7 = % 41.52/6.48 | vnoQConf & ~ (v11 = 0) & ~ (v8 = vqempty) & vreduce(v8, v5, % 41.52/6.48 | v6) = v10 & visSomeQC(v10) = v11 & vqseq(v8, v9) = v4 & % 41.52/6.48 | vOptQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v8)) | ? % 41.52/6.48 | [v8: vQID] : ? [v9: vOptQuestion] : ? [v10: int] : ? [v11: % 41.52/6.48 | vEntry] : (v7 = vnoQConf & ~ (v10 = 0) & vlookupQMap(v8, v6) = % 41.52/6.48 | v9 & visSomeQuestion(v9) = v10 & vqsingle(v11) = v4 & vask(v8) = % 41.52/6.48 | v11 & vQID(v8) & vOptQuestion(v9) & vEntry(v11)) | ? [v8: vGID] % 41.52/6.48 | : ? [v9: vQuestionnaire] : ? [v10: vQConf] : (vQC(v5, v6, v9) = % 41.52/6.48 | v10 & vsomeQConf(v10) = v7 & vqgroup(v8, v9) = v4 & vGID(v8) & % 41.52/6.48 | vOptQConf(v7) & vQConf(v10) & vQuestionnaire(v9)) | ? [v8: % 41.52/6.48 | vQuestionnaire] : ? [v9: vQuestionnaire] : ? [v10: vQConf] : % 41.52/6.48 | (vQC(v5, v6, v9) = v10 & vsomeQConf(v10) = v7 & vqcond(v3, v8, v9) % 41.52/6.48 | = v4 & vOptQConf(v7) & vQConf(v10) & vQuestionnaire(v9) & % 41.52/6.48 | vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? [v9: % 41.52/6.48 | vQuestionnaire] : ? [v10: vQConf] : (vQC(v5, v6, v8) = v10 & % 41.52/6.48 | vsomeQConf(v10) = v7 & vqcond(v1, v8, v9) = v4 & vOptQConf(v7) & % 41.52/6.48 | vQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: % 41.52/6.48 | vQuestionnaire] : ? [v9: vQConf] : (vQC(v5, v6, v8) = v9 & % 41.52/6.48 | vsomeQConf(v9) = v7 & vqseq(vqempty, v8) = v4 & vOptQConf(v7) & % 41.52/6.48 | vQConf(v9) & vQuestionnaire(v8)) | (v7 = vnoQConf & v4 = % 41.52/6.48 | vqempty))) % 41.52/6.48 | % 41.52/6.48 | ALPHA: (reduceExpPreservation-unop-IH0) implies: % 41.52/6.48 | (14) ! [v0: vAnsMap] : ! [v1: vAType] : ! [v2: vExp] : ! [v3: vATMap] : % 41.52/6.48 | ! [v4: vOptAType] : ! [v5: vOptAType] : (v5 = v4 | ~ (vecheck(v3, % 41.52/6.48 | v2) = v5) | ~ (vtypeAM(v0) = v3) | ~ (vsomeAType(v1) = v4) | % 41.52/6.48 | ~ vAType(v1) | ~ vExp(v2) | ~ vAnsMap(v0) | ? [v6: vOptAType] : % 41.52/6.48 | ? [v7: vOptExp] : ? [v8: vOptExp] : (vecheck(v3, ve1) = v6 & % 41.52/6.48 | vreduceExp(ve1, v0) = v7 & vsomeExp(v2) = v8 & vOptExp(v8) & % 41.52/6.48 | vOptExp(v7) & vOptAType(v6) & ( ~ (v8 = v7) | ~ (v6 = v4)))) % 41.52/6.48 | % 41.52/6.48 | ALPHA: (reduceExpPreservation-unop-expIsValue-True) implies: % 41.52/6.48 | (15) vExp(ve1) % 41.52/6.48 | (16) ? [v0: any] : (vexpIsValue(ve1) = v0 & ? [v1: vAnsMap] : ? [v2: % 41.52/6.48 | vUnOpT] : ? [v3: vAType] : ? [v4: vExp] : ? [v5: vATMap] : ? % 41.52/6.48 | [v6: vExp] : ? [v7: vOptAType] : ? [v8: vOptExp] : ? [v9: % 41.52/6.48 | vOptAType] : (v0 = 0 & ~ (v9 = v7) & vecheck(v5, v6) = v7 & % 41.52/6.48 | vecheck(v5, v4) = v9 & vtypeAM(v1) = v5 & vreduceExp(v6, v1) = v8 % 41.52/6.48 | & vsomeExp(v4) = v8 & vsomeAType(v3) = v7 & vunop(v2, ve1) = v6 & % 41.52/6.48 | vAType(v3) & vUnOpT(v2) & vOptExp(v8) & vExp(v6) & vExp(v4) & % 41.52/6.48 | vAnsMap(v1) & vATMap(v5) & vOptAType(v9) & vOptAType(v7))) % 41.52/6.48 | % 41.52/6.48 | ALPHA: (function-axioms) implies: % 41.52/6.48 | (17) ! [v0: vExp] : ! [v1: vExp] : ! [v2: vAval] : (v1 = v0 | ~ % 41.52/6.48 | (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) % 41.52/6.48 | (18) ! [v0: vAval] : ! [v1: vAval] : ! [v2: vYN] : (v1 = v0 | ~ (vB(v2) % 41.52/6.48 | = v1) | ~ (vB(v2) = v0)) % 41.52/6.48 | (19) ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vExp] : (v1 = v0 | ~ % 41.52/6.48 | (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) % 41.52/6.49 | (20) ! [v0: vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ % 41.52/6.49 | (vgetExpValue(v2) = v1) | ~ (vgetExpValue(v2) = v0)) % 41.52/6.49 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 41.52/6.49 | vExp] : (v1 = v0 | ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = % 41.52/6.49 | v0)) % 41.52/6.49 | (22) ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vUnOpT] % 41.52/6.49 | : (v1 = v0 | ~ (vevalUnOp(v3, v2) = v1) | ~ (vevalUnOp(v3, v2) = % 41.52/6.49 | v0)) % 41.52/6.49 | (23) ! [v0: vOptAType] : ! [v1: vOptAType] : ! [v2: vExp] : ! [v3: % 41.52/6.49 | vATMap] : (v1 = v0 | ~ (vecheck(v3, v2) = v1) | ~ (vecheck(v3, v2) % 41.52/6.49 | = v0)) % 41.52/6.49 | % 41.52/6.49 | DELTA: instantiating (3) with fresh symbols all_376_0, all_376_1, all_376_2 % 41.52/6.49 | gives: % 41.52/6.49 | (24) vsomeExp(all_376_1) = all_376_0 & vB(vyes) = all_376_2 & % 41.52/6.49 | vconstant(all_376_2) = all_376_1 & vOptExp(all_376_0) & % 41.52/6.49 | vExp(all_376_1) & vAval(all_376_2) & ! [v0: vAval] : ! [v1: int] : % 41.52/6.49 | (v1 = all_376_0 | ~ (vevalBinOp(veqop, v0, v0) = v1) | ~ vAval(v0)) % 41.52/6.49 | % 41.52/6.49 | ALPHA: (24) implies: % 41.52/6.49 | (25) vconstant(all_376_2) = all_376_1 % 41.52/6.49 | (26) vB(vyes) = all_376_2 % 41.52/6.49 | (27) vsomeExp(all_376_1) = all_376_0 % 41.52/6.49 | % 41.52/6.49 | DELTA: instantiating (4) with fresh symbols all_380_0, all_380_1, all_380_2 % 41.52/6.49 | gives: % 41.52/6.49 | (28) vsomeExp(all_380_1) = all_380_0 & vB(vno) = all_380_2 & % 41.52/6.49 | vconstant(all_380_2) = all_380_1 & vOptExp(all_380_0) & % 41.52/6.49 | vExp(all_380_1) & vAval(all_380_2) & ! [v0: vAval] : ! [v1: vAval] : % 41.52/6.49 | ! [v2: int] : (v2 = all_380_0 | v1 = v0 | ~ (vevalBinOp(veqop, v0, % 41.52/6.49 | v1) = v2) | ~ vAval(v1) | ~ vAval(v0)) % 41.52/6.49 | % 41.52/6.49 | ALPHA: (28) implies: % 41.52/6.49 | (29) vconstant(all_380_2) = all_380_1 % 41.52/6.49 | (30) vB(vno) = all_380_2 % 41.52/6.49 | (31) vsomeExp(all_380_1) = all_380_0 % 41.52/6.49 | % 41.52/6.49 | DELTA: instantiating (7) with fresh symbols all_387_0, all_387_1 gives: % 41.52/6.49 | (32) vB(vyes) = all_387_1 & vconstant(all_387_1) = all_387_0 & % 41.52/6.49 | vExp(all_387_0) & vAval(all_387_1) & ! [v0: vQuestionnaire] : ! [v1: % 41.52/6.49 | vQuestionnaire] : ! [v2: vAnsMap] : ! [v3: vQMap] : ! [v4: % 41.52/6.49 | vQuestionnaire] : ! [v5: vOptQConf] : ( ~ (vreduce(v4, v2, v3) = % 41.52/6.49 | v5) | ~ (vqcond(all_387_0, v0, v1) = v4) | ~ vQMap(v3) | ~ % 41.52/6.49 | vAnsMap(v2) | ~ vQuestionnaire(v1) | ~ vQuestionnaire(v0) | ? % 41.52/6.49 | [v6: vQConf] : (vQC(v2, v3, v0) = v6 & vsomeQConf(v6) = v5 & % 41.52/6.49 | vOptQConf(v5) & vQConf(v6))) % 41.52/6.49 | % 41.52/6.49 | ALPHA: (32) implies: % 41.52/6.49 | (33) vconstant(all_387_1) = all_387_0 % 41.52/6.49 | (34) vB(vyes) = all_387_1 % 41.52/6.49 | % 41.52/6.49 | DELTA: instantiating (8) with fresh symbols all_393_0, all_393_1 gives: % 41.52/6.49 | (35) vB(vno) = all_393_1 & vconstant(all_393_1) = all_393_0 & % 41.52/6.49 | vExp(all_393_0) & vAval(all_393_1) & ! [v0: vQuestionnaire] : ! [v1: % 41.52/6.49 | vQuestionnaire] : ! [v2: vAnsMap] : ! [v3: vQMap] : ! [v4: % 41.52/6.49 | vQuestionnaire] : ! [v5: vOptQConf] : ( ~ (vreduce(v4, v2, v3) = % 41.52/6.49 | v5) | ~ (vqcond(all_393_0, v0, v1) = v4) | ~ vQMap(v3) | ~ % 41.52/6.49 | vAnsMap(v2) | ~ vQuestionnaire(v1) | ~ vQuestionnaire(v0) | ? % 41.52/6.49 | [v6: vQConf] : (vQC(v2, v3, v1) = v6 & vsomeQConf(v6) = v5 & % 41.52/6.49 | vOptQConf(v5) & vQConf(v6))) % 41.52/6.49 | % 41.52/6.49 | ALPHA: (35) implies: % 41.52/6.49 | (36) vconstant(all_393_1) = all_393_0 % 41.52/6.49 | (37) vB(vno) = all_393_1 % 41.52/6.49 | % 41.52/6.49 | DELTA: instantiating (16) with fresh symbol all_398_0 gives: % 41.52/6.49 | (38) vexpIsValue(ve1) = all_398_0 & ? [v0: vAnsMap] : ? [v1: vUnOpT] : ? % 41.52/6.49 | [v2: vAType] : ? [v3: vExp] : ? [v4: vATMap] : ? [v5: vExp] : ? % 41.52/6.49 | [v6: vOptAType] : ? [v7: vOptExp] : ? [v8: vOptAType] : (all_398_0 = % 41.52/6.49 | 0 & ~ (v8 = v6) & vecheck(v4, v5) = v6 & vecheck(v4, v3) = v8 & % 41.52/6.49 | vtypeAM(v0) = v4 & vreduceExp(v5, v0) = v7 & vsomeExp(v3) = v7 & % 41.52/6.49 | vsomeAType(v2) = v6 & vunop(v1, ve1) = v5 & vAType(v2) & vUnOpT(v1) % 41.52/6.49 | & vOptExp(v7) & vExp(v5) & vExp(v3) & vAnsMap(v0) & vATMap(v4) & % 41.52/6.49 | vOptAType(v8) & vOptAType(v6)) % 41.52/6.49 | % 41.52/6.49 | ALPHA: (38) implies: % 41.52/6.49 | (39) vexpIsValue(ve1) = all_398_0 % 41.52/6.49 | (40) ? [v0: vAnsMap] : ? [v1: vUnOpT] : ? [v2: vAType] : ? [v3: vExp] : % 41.52/6.49 | ? [v4: vATMap] : ? [v5: vExp] : ? [v6: vOptAType] : ? [v7: % 41.52/6.49 | vOptExp] : ? [v8: vOptAType] : (all_398_0 = 0 & ~ (v8 = v6) & % 41.52/6.49 | vecheck(v4, v5) = v6 & vecheck(v4, v3) = v8 & vtypeAM(v0) = v4 & % 41.52/6.49 | vreduceExp(v5, v0) = v7 & vsomeExp(v3) = v7 & vsomeAType(v2) = v6 & % 41.52/6.49 | vunop(v1, ve1) = v5 & vAType(v2) & vUnOpT(v1) & vOptExp(v7) & % 41.52/6.49 | vExp(v5) & vExp(v3) & vAnsMap(v0) & vATMap(v4) & vOptAType(v8) & % 41.52/6.49 | vOptAType(v6)) % 41.52/6.49 | % 41.52/6.49 | DELTA: instantiating (10) with fresh symbols all_403_0, all_403_1, all_403_2, % 41.52/6.49 | all_403_3 gives: % 41.52/6.49 | (41) vB(vno) = all_403_1 & vB(vyes) = all_403_3 & vconstant(all_403_1) = % 41.52/6.49 | all_403_0 & vconstant(all_403_3) = all_403_2 & vExp(all_403_0) & % 41.52/6.49 | vExp(all_403_2) & vAval(all_403_1) & vAval(all_403_3) & ! [v0: vQMap] % 41.52/6.49 | : ! [v1: vQuestionnaire] : ! [v2: any] : ! [v3: vAnsMap] : ! [v4: % 41.52/6.49 | vQuestionnaire] : ! [v5: vQuestionnaire] : ! [v6: vOptQConf] : (v6 % 41.52/6.49 | = vnoQConf | v2 = all_403_0 | v2 = all_403_2 | ~ (vreduce(v5, v3, % 41.52/6.49 | v0) = v6) | ~ (vqcond(v2, v1, v4) = v5) | ~ vQMap(v0) | ~ % 41.52/6.49 | vExp(v2) | ~ vAnsMap(v3) | ~ vQuestionnaire(v4) | ~ % 41.52/6.49 | vQuestionnaire(v1) | ? [v7: vOptExp] : (vreduceExp(v2, v3) = v7 & % 41.52/6.49 | visSomeExp(v7) = 0 & vOptExp(v7))) % 41.52/6.49 | % 41.52/6.49 | ALPHA: (41) implies: % 41.52/6.49 | (42) vconstant(all_403_3) = all_403_2 % 41.52/6.50 | (43) vconstant(all_403_1) = all_403_0 % 41.52/6.50 | (44) vB(vyes) = all_403_3 % 41.52/6.50 | (45) vB(vno) = all_403_1 % 41.52/6.50 | % 41.52/6.50 | DELTA: instantiating (9) with fresh symbols all_406_0, all_406_1, all_406_2, % 41.52/6.50 | all_406_3 gives: % 42.01/6.50 | (46) vB(vno) = all_406_1 & vB(vyes) = all_406_3 & vconstant(all_406_1) = % 42.01/6.50 | all_406_0 & vconstant(all_406_3) = all_406_2 & vExp(all_406_0) & % 42.01/6.50 | vExp(all_406_2) & vAval(all_406_1) & vAval(all_406_3) & ! [v0: vQMap] % 42.01/6.50 | : ! [v1: vQuestionnaire] : ! [v2: any] : ! [v3: vAnsMap] : ! [v4: % 42.01/6.50 | vQuestionnaire] : ! [v5: vOptExp] : ! [v6: vExp] : ! [v7: % 42.01/6.50 | vQuestionnaire] : ! [v8: vQConf] : (v2 = all_406_0 | v2 = all_406_2 % 42.01/6.50 | | ~ (vreduceExp(v2, v3) = v5) | ~ (vgetExp(v5) = v6) | ~ (vQC(v3, % 42.01/6.50 | v0, v7) = v8) | ~ (vqcond(v6, v1, v4) = v7) | ~ vQMap(v0) | ~ % 42.01/6.50 | vExp(v2) | ~ vAnsMap(v3) | ~ vQuestionnaire(v4) | ~ % 42.01/6.50 | vQuestionnaire(v1) | ? [v9: any] : ? [v10: vQuestionnaire] : ? % 42.01/6.50 | [v11: vOptQConf] : ? [v12: vOptQConf] : (vreduce(v10, v3, v0) = v11 % 42.01/6.50 | & visSomeExp(v5) = v9 & vsomeQConf(v8) = v12 & vqcond(v2, v1, v4) % 42.01/6.50 | = v10 & vOptQConf(v12) & vOptQConf(v11) & vQuestionnaire(v10) & ( % 42.01/6.50 | ~ (v9 = 0) | v12 = v11))) % 42.01/6.50 | % 42.01/6.50 | ALPHA: (46) implies: % 42.01/6.50 | (47) vconstant(all_406_3) = all_406_2 % 42.01/6.50 | (48) vconstant(all_406_1) = all_406_0 % 42.01/6.50 | (49) vB(vyes) = all_406_3 % 42.01/6.50 | (50) vB(vno) = all_406_1 % 42.01/6.50 | % 42.01/6.50 | DELTA: instantiating (5) with fresh symbols all_415_0, all_415_1, all_415_2, % 42.01/6.50 | all_415_3, all_415_4, all_415_5 gives: % 42.01/6.50 | (51) vsomeExp(all_415_1) = all_415_0 & vsomeExp(all_415_4) = all_415_3 & % 42.01/6.50 | vB(vno) = all_415_2 & vB(vyes) = all_415_5 & vconstant(all_415_2) = % 42.01/6.50 | all_415_1 & vconstant(all_415_5) = all_415_4 & vOptExp(all_415_0) & % 42.01/6.50 | vOptExp(all_415_3) & vExp(all_415_1) & vExp(all_415_4) & % 42.01/6.50 | vAval(all_415_2) & vAval(all_415_5) & ! [v0: vBinOpT] : ! [v1: % 42.01/6.50 | vAval] : ! [v2: vAval] : ! [v3: vOptExp] : ( ~ (vevalBinOp(v0, v1, % 42.01/6.50 | v2) = v3) | ~ vBinOpT(v0) | ~ vAval(v2) | ~ vAval(v1) | ? % 42.01/6.50 | [v4: vnat] : ? [v5: vnat] : ? [v6: vYN] : ? [v7: vAval] : ? [v8: % 42.01/6.50 | vExp] : (v0 = vgtop & vgt(v4, v5) = v6 & vsomeExp(v8) = v3 & % 42.01/6.50 | vNum(v5) = v2 & vNum(v4) = v1 & vB(v6) = v7 & vconstant(v7) = v8 & % 42.01/6.50 | vOptExp(v3) & vnat(v5) & vnat(v4) & vExp(v8) & vAval(v7) & % 42.01/6.50 | vYN(v6)) | ? [v4: vnat] : ? [v5: vnat] : ? [v6: vYN] : ? [v7: % 42.01/6.50 | vAval] : ? [v8: vExp] : (v0 = vltop & vlt(v4, v5) = v6 & % 42.01/6.50 | vsomeExp(v8) = v3 & vNum(v5) = v2 & vNum(v4) = v1 & vB(v6) = v7 & % 42.01/6.50 | vconstant(v7) = v8 & vOptExp(v3) & vnat(v5) & vnat(v4) & vExp(v8) % 42.01/6.50 | & vAval(v7) & vYN(v6)) | ? [v4: vnat] : ? [v5: vnat] : ? [v6: % 42.01/6.50 | vnat] : ? [v7: vAval] : ? [v8: vExp] : (v0 = vaddop & vplus(v4, % 42.01/6.50 | v5) = v6 & vsomeExp(v8) = v3 & vNum(v6) = v7 & vNum(v5) = v2 & % 42.01/6.50 | vNum(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & vnat(v6) & % 42.01/6.50 | vnat(v5) & vnat(v4) & vExp(v8) & vAval(v7)) | ? [v4: vYN] : ? % 42.01/6.50 | [v5: vYN] : ? [v6: vYN] : ? [v7: vAval] : ? [v8: vExp] : (v0 = % 42.01/6.50 | vorop & vor(v4, v5) = v6 & vsomeExp(v8) = v3 & vB(v6) = v7 & % 42.01/6.50 | vB(v5) = v2 & vB(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & % 42.01/6.50 | vExp(v8) & vAval(v7) & vYN(v6) & vYN(v5) & vYN(v4)) | ? [v4: % 42.01/6.50 | vnat] : ? [v5: vnat] : ? [v6: vnat] : ? [v7: vAval] : ? [v8: % 42.01/6.50 | vExp] : (v0 = vmulop & vmultiply(v4, v5) = v6 & vsomeExp(v8) = v3 % 42.01/6.50 | & vNum(v6) = v7 & vNum(v5) = v2 & vNum(v4) = v1 & vconstant(v7) = % 42.01/6.50 | v8 & vOptExp(v3) & vnat(v6) & vnat(v5) & vnat(v4) & vExp(v8) & % 42.01/6.50 | vAval(v7)) | ? [v4: vnat] : ? [v5: vnat] : ? [v6: vnat] : ? % 42.01/6.50 | [v7: vAval] : ? [v8: vExp] : (v0 = vdivop & vdivide(v4, v5) = v6 & % 42.01/6.50 | vsomeExp(v8) = v3 & vNum(v6) = v7 & vNum(v5) = v2 & vNum(v4) = v1 % 42.01/6.50 | & vconstant(v7) = v8 & vOptExp(v3) & vnat(v6) & vnat(v5) & % 42.01/6.50 | vnat(v4) & vExp(v8) & vAval(v7)) | ? [v4: vYN] : ? [v5: vYN] : % 42.01/6.50 | ? [v6: vYN] : ? [v7: vAval] : ? [v8: vExp] : (v0 = vandop & % 42.01/6.50 | vand(v4, v5) = v6 & vsomeExp(v8) = v3 & vB(v6) = v7 & vB(v5) = v2 % 42.01/6.50 | & vB(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & vExp(v8) & % 42.01/6.50 | vAval(v7) & vYN(v6) & vYN(v5) & vYN(v4)) | ? [v4: vnat] : ? [v5: % 42.01/6.50 | vnat] : ? [v6: vnat] : ? [v7: vAval] : ? [v8: vExp] : (v0 = % 42.01/6.50 | vsubop & vminus(v4, v5) = v6 & vsomeExp(v8) = v3 & vNum(v6) = v7 & % 42.01/6.50 | vNum(v5) = v2 & vNum(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & % 42.01/6.50 | vnat(v6) & vnat(v5) & vnat(v4) & vExp(v8) & vAval(v7)) | (v3 = % 42.01/6.50 | all_415_0 & v0 = veqop & ~ (v2 = v1)) | (v3 = all_415_3 & v2 = v1 % 42.01/6.50 | & v0 = veqop) | (v3 = vnoExp & ~ (v0 = veqop) & ( ~ (v0 = vorop) % 42.01/6.50 | | ! [v4: vYN] : ( ~ (vB(v4) = v2) | ~ vYN(v4)) | ! [v4: vYN] % 42.01/6.50 | : ( ~ (vB(v4) = v1) | ~ vYN(v4))) & ( ~ (v0 = vandop) | ! [v4: % 42.01/6.50 | vYN] : ( ~ (vB(v4) = v2) | ~ vYN(v4)) | ! [v4: vYN] : ( ~ % 42.01/6.50 | (vB(v4) = v1) | ~ vYN(v4))) & ( ! [v4: vnat] : ( ~ (vNum(v4) % 42.01/6.50 | = v2) | ~ vnat(v4)) | ! [v4: vnat] : ( ~ (vNum(v4) = v1) | % 42.01/6.50 | ~ vnat(v4)) | ( ~ (v0 = vgtop) & ~ (v0 = vltop) & ~ (v0 = % 42.01/6.50 | vaddop) & ~ (v0 = vmulop) & ~ (v0 = vdivop) & ~ (v0 = % 42.01/6.50 | vsubop))))) % 42.01/6.50 | % 42.01/6.50 | ALPHA: (51) implies: % 42.01/6.50 | (52) vconstant(all_415_5) = all_415_4 % 42.01/6.50 | (53) vconstant(all_415_2) = all_415_1 % 42.01/6.50 | (54) vB(vyes) = all_415_5 % 42.01/6.50 | (55) vB(vno) = all_415_2 % 42.01/6.50 | (56) vsomeExp(all_415_4) = all_415_3 % 42.01/6.50 | (57) vsomeExp(all_415_1) = all_415_0 % 42.01/6.50 | % 42.01/6.50 | DELTA: instantiating (13) with fresh symbols all_418_0, all_418_1, all_418_2, % 42.01/6.50 | all_418_3 gives: % 42.01/6.51 | (58) vB(vno) = all_418_1 & vB(vyes) = all_418_3 & vconstant(all_418_1) = % 42.01/6.51 | all_418_0 & vconstant(all_418_3) = all_418_2 & vExp(all_418_0) & % 42.01/6.51 | vExp(all_418_2) & vAval(all_418_1) & vAval(all_418_3) & ! [v0: % 42.01/6.51 | vQuestionnaire] : ! [v1: vAnsMap] : ! [v2: vQMap] : ! [v3: % 42.01/6.51 | vOptQConf] : ( ~ (vreduce(v0, v1, v2) = v3) | ~ vQMap(v2) | ~ % 42.01/6.51 | vAnsMap(v1) | ~ vQuestionnaire(v0) | ? [v4: vAType] : ? [v5: % 42.01/6.51 | vOptExp] : ? [v6: vQID] : ? [v7: vExp] : ? [v8: int] : ? [v9: % 42.01/6.51 | vEntry] : ? [v10: vExp] : ? [v11: vEntry] : ? [v12: % 42.01/6.51 | vQuestionnaire] : ? [v13: vQConf] : ( ~ (v8 = 0) & vreduceExp(v7, % 42.01/6.51 | v1) = v5 & vexpIsValue(v7) = v8 & visSomeExp(v5) = 0 & % 42.01/6.51 | vgetExp(v5) = v10 & vQC(v1, v2, v12) = v13 & vsomeQConf(v13) = v3 % 42.01/6.51 | & vqsingle(v11) = v12 & vqsingle(v9) = v0 & vvalue(v6, v4, v10) = % 42.01/6.51 | v11 & vvalue(v6, v4, v7) = v9 & vAType(v4) & vOptExp(v5) & % 42.01/6.51 | vQID(v6) & vExp(v10) & vExp(v7) & vOptQConf(v3) & vQConf(v13) & % 42.01/6.51 | vQuestionnaire(v12) & vEntry(v11) & vEntry(v9)) | ? [v4: vQID] : % 42.01/6.51 | ? [v5: vOptQuestion] : ? [v6: vEntry] : ? [v7: vLabel] : ? [v8: % 42.01/6.51 | vAType] : ? [v9: vEntry] : ? [v10: vQuestionnaire] : ? [v11: % 42.01/6.51 | vQConf] : (vlookupQMap(v4, v2) = v5 & visSomeQuestion(v5) = 0 & % 42.01/6.51 | vgetQuestionAType(v5) = v8 & vgetQuestionLabel(v5) = v7 & vQC(v1, % 42.01/6.51 | v2, v10) = v11 & vsomeQConf(v11) = v3 & vqsingle(v9) = v10 & % 42.01/6.51 | vqsingle(v6) = v0 & vask(v4) = v6 & vquestion(v4, v7, v8) = v9 & % 42.01/6.51 | vAType(v8) & vLabel(v7) & vQID(v4) & vOptQuestion(v5) & % 42.01/6.51 | vOptQConf(v3) & vQConf(v11) & vQuestionnaire(v10) & vEntry(v9) & % 42.01/6.51 | vEntry(v6)) | ? [v4: vAType] : ? [v5: vOptExp] : ? [v6: vQID] : % 42.01/6.51 | ? [v7: vExp] : ? [v8: int] : ? [v9: int] : ? [v10: vEntry] : (v3 % 42.01/6.51 | = vnoQConf & ~ (v9 = 0) & ~ (v8 = 0) & vreduceExp(v7, v1) = v5 & % 42.01/6.51 | vexpIsValue(v7) = v8 & visSomeExp(v5) = v9 & vqsingle(v10) = v0 & % 42.01/6.51 | vvalue(v6, v4, v7) = v10 & vAType(v4) & vOptExp(v5) & vQID(v6) & % 42.01/6.51 | vExp(v7) & vEntry(v10)) | ? [v4: vOptExp] : ? [v5: % 42.01/6.51 | vQuestionnaire] : ? [v6: any] : ? [v7: vQuestionnaire] : ? [v8: % 42.01/6.51 | vExp] : ? [v9: vQuestionnaire] : ? [v10: vQConf] : ( ~ (v6 = % 42.01/6.51 | all_418_0) & ~ (v6 = all_418_2) & vreduceExp(v6, v1) = v4 & % 42.01/6.51 | visSomeExp(v4) = 0 & vgetExp(v4) = v8 & vQC(v1, v2, v9) = v10 & % 42.01/6.51 | vsomeQConf(v10) = v3 & vqcond(v8, v5, v7) = v9 & vqcond(v6, v5, % 42.01/6.51 | v7) = v0 & vOptExp(v4) & vExp(v8) & vExp(v6) & vOptQConf(v3) & % 42.01/6.51 | vQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v7) & % 42.01/6.51 | vQuestionnaire(v5)) | ? [v4: vAType] : ? [v5: vLabel] : ? [v6: % 42.01/6.51 | vAval] : ? [v7: vQID] : ? [v8: vEntry] : ? [v9: vAnsMap] : ? % 42.01/6.51 | [v10: vQConf] : (vgetAnswer(v5, v4) = v6 & vQC(v9, v2, vqempty) = % 42.01/6.51 | v10 & vabind(v7, v6, v1) = v9 & vsomeQConf(v10) = v3 & % 42.01/6.51 | vqsingle(v8) = v0 & vquestion(v7, v5, v4) = v8 & vAType(v4) & % 42.01/6.51 | vLabel(v5) & vQID(v7) & vAnsMap(v9) & vOptQConf(v3) & vAval(v6) & % 42.01/6.51 | vQConf(v10) & vEntry(v8)) | ? [v4: vAType] : ? [v5: vQID] : ? % 42.01/6.51 | [v6: vExp] : ? [v7: vEntry] : ? [v8: vAval] : ? [v9: vAnsMap] : % 42.01/6.51 | ? [v10: vQConf] : (vexpIsValue(v6) = 0 & vgetExpValue(v6) = v8 & % 42.01/6.51 | vQC(v9, v2, vqempty) = v10 & vabind(v5, v8, v1) = v9 & % 42.01/6.51 | vsomeQConf(v10) = v3 & vqsingle(v7) = v0 & vvalue(v5, v4, v6) = v7 % 42.01/6.51 | & vAType(v4) & vQID(v5) & vExp(v6) & vAnsMap(v9) & vOptQConf(v3) & % 42.01/6.51 | vAval(v8) & vQConf(v10) & vEntry(v7)) | ? [v4: vAType] : ? [v5: % 42.01/6.51 | vLabel] : ? [v6: vQID] : ? [v7: vEntry] : ? [v8: vQMap] : ? % 42.01/6.51 | [v9: vQConf] : (vQC(v1, v8, vqempty) = v9 & vsomeQConf(v9) = v3 & % 42.01/6.51 | vqsingle(v7) = v0 & vqmbind(v6, v5, v4, v2) = v8 & % 42.01/6.51 | vdefquestion(v6, v5, v4) = v7 & vAType(v4) & vLabel(v5) & vQID(v6) % 42.01/6.51 | & vQMap(v8) & vOptQConf(v3) & vQConf(v9) & vEntry(v7)) | ? [v4: % 42.01/6.51 | vOptExp] : ? [v5: vQuestionnaire] : ? [v6: any] : ? [v7: % 42.01/6.51 | vQuestionnaire] : ? [v8: int] : (v3 = vnoQConf & ~ (v8 = 0) & ~ % 42.01/6.51 | (v6 = all_418_0) & ~ (v6 = all_418_2) & vreduceExp(v6, v1) = v4 & % 42.01/6.51 | visSomeExp(v4) = v8 & vqcond(v6, v5, v7) = v0 & vOptExp(v4) & % 42.01/6.51 | vExp(v6) & vQuestionnaire(v7) & vQuestionnaire(v5)) | ? [v4: % 42.01/6.51 | vQuestionnaire] : ? [v5: vQuestionnaire] : ? [v6: vOptQConf] : % 42.01/6.51 | ? [v7: vQConf] : ? [v8: vQConf] : ( ~ (v4 = vqempty) & vreduce(v4, % 42.01/6.51 | v1, v2) = v6 & vqcappend(v7, v5) = v8 & visSomeQC(v6) = 0 & % 42.01/6.51 | vgetQC(v6) = v7 & vsomeQConf(v8) = v3 & vqseq(v4, v5) = v0 & % 42.01/6.51 | vOptQConf(v6) & vOptQConf(v3) & vQConf(v8) & vQConf(v7) & % 42.01/6.51 | vQuestionnaire(v5) & vQuestionnaire(v4)) | ? [v4: vQuestionnaire] % 42.01/6.51 | : ? [v5: vQuestionnaire] : ? [v6: vOptQConf] : ? [v7: int] : (v3 % 42.01/6.51 | = vnoQConf & ~ (v7 = 0) & ~ (v4 = vqempty) & vreduce(v4, v1, v2) % 42.01/6.51 | = v6 & visSomeQC(v6) = v7 & vqseq(v4, v5) = v0 & vOptQConf(v6) & % 42.01/6.51 | vQuestionnaire(v5) & vQuestionnaire(v4)) | ? [v4: vQID] : ? [v5: % 42.01/6.51 | vOptQuestion] : ? [v6: int] : ? [v7: vEntry] : (v3 = vnoQConf & % 42.01/6.51 | ~ (v6 = 0) & vlookupQMap(v4, v2) = v5 & visSomeQuestion(v5) = v6 & % 42.01/6.51 | vqsingle(v7) = v0 & vask(v4) = v7 & vQID(v4) & vOptQuestion(v5) & % 42.01/6.51 | vEntry(v7)) | ? [v4: vGID] : ? [v5: vQuestionnaire] : ? [v6: % 42.01/6.51 | vQConf] : (vQC(v1, v2, v5) = v6 & vsomeQConf(v6) = v3 & % 42.01/6.51 | vqgroup(v4, v5) = v0 & vGID(v4) & vOptQConf(v3) & vQConf(v6) & % 42.01/6.51 | vQuestionnaire(v5)) | ? [v4: vQuestionnaire] : ? [v5: % 42.01/6.51 | vQuestionnaire] : ? [v6: vQConf] : (vQC(v1, v2, v5) = v6 & % 42.01/6.51 | vsomeQConf(v6) = v3 & vqcond(all_418_0, v4, v5) = v0 & % 42.01/6.51 | vOptQConf(v3) & vQConf(v6) & vQuestionnaire(v5) & % 42.01/6.51 | vQuestionnaire(v4)) | ? [v4: vQuestionnaire] : ? [v5: % 42.01/6.51 | vQuestionnaire] : ? [v6: vQConf] : (vQC(v1, v2, v4) = v6 & % 42.01/6.51 | vsomeQConf(v6) = v3 & vqcond(all_418_2, v4, v5) = v0 & % 42.01/6.51 | vOptQConf(v3) & vQConf(v6) & vQuestionnaire(v5) & % 42.01/6.51 | vQuestionnaire(v4)) | ? [v4: vQuestionnaire] : ? [v5: vQConf] : % 42.01/6.51 | (vQC(v1, v2, v4) = v5 & vsomeQConf(v5) = v3 & vqseq(vqempty, v4) = % 42.01/6.51 | v0 & vOptQConf(v3) & vQConf(v5) & vQuestionnaire(v4)) | (v3 = % 42.01/6.51 | vnoQConf & v0 = vqempty)) % 42.01/6.51 | % 42.01/6.51 | ALPHA: (58) implies: % 42.01/6.51 | (59) vconstant(all_418_3) = all_418_2 % 42.01/6.51 | (60) vconstant(all_418_1) = all_418_0 % 42.01/6.51 | (61) vB(vyes) = all_418_3 % 42.01/6.51 | (62) vB(vno) = all_418_1 % 42.01/6.51 | % 42.01/6.51 | DELTA: instantiating (40) with fresh symbols all_421_0, all_421_1, all_421_2, % 42.01/6.51 | all_421_3, all_421_4, all_421_5, all_421_6, all_421_7, all_421_8 gives: % 42.01/6.51 | (63) all_398_0 = 0 & ~ (all_421_0 = all_421_2) & vecheck(all_421_4, % 42.01/6.51 | all_421_3) = all_421_2 & vecheck(all_421_4, all_421_5) = all_421_0 & % 42.01/6.51 | vtypeAM(all_421_8) = all_421_4 & vreduceExp(all_421_3, all_421_8) = % 42.01/6.51 | all_421_1 & vsomeExp(all_421_5) = all_421_1 & vsomeAType(all_421_6) = % 42.01/6.51 | all_421_2 & vunop(all_421_7, ve1) = all_421_3 & vAType(all_421_6) & % 42.01/6.51 | vUnOpT(all_421_7) & vOptExp(all_421_1) & vExp(all_421_3) & % 42.01/6.51 | vExp(all_421_5) & vAnsMap(all_421_8) & vATMap(all_421_4) & % 42.01/6.51 | vOptAType(all_421_0) & vOptAType(all_421_2) % 42.01/6.51 | % 42.01/6.51 | ALPHA: (63) implies: % 42.01/6.52 | (64) all_398_0 = 0 % 42.01/6.52 | (65) ~ (all_421_0 = all_421_2) % 42.01/6.52 | (66) vATMap(all_421_4) % 42.01/6.52 | (67) vAnsMap(all_421_8) % 42.01/6.52 | (68) vExp(all_421_5) % 42.01/6.52 | (69) vUnOpT(all_421_7) % 42.01/6.52 | (70) vAType(all_421_6) % 42.01/6.52 | (71) vunop(all_421_7, ve1) = all_421_3 % 42.01/6.52 | (72) vsomeAType(all_421_6) = all_421_2 % 42.01/6.52 | (73) vsomeExp(all_421_5) = all_421_1 % 42.01/6.52 | (74) vreduceExp(all_421_3, all_421_8) = all_421_1 % 42.01/6.52 | (75) vtypeAM(all_421_8) = all_421_4 % 42.01/6.52 | (76) vecheck(all_421_4, all_421_5) = all_421_0 % 42.01/6.52 | (77) vecheck(all_421_4, all_421_3) = all_421_2 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (39), (64) imply: % 42.01/6.52 | (78) vexpIsValue(ve1) = 0 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_403_3, all_415_5, vyes, simplifying % 42.01/6.52 | with (44), (54) gives: % 42.01/6.52 | (79) all_415_5 = all_403_3 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_415_5, all_418_3, vyes, simplifying % 42.01/6.52 | with (54), (61) gives: % 42.01/6.52 | (80) all_418_3 = all_415_5 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_406_3, all_418_3, vyes, simplifying % 42.01/6.52 | with (49), (61) gives: % 42.01/6.52 | (81) all_418_3 = all_406_3 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_387_1, all_418_3, vyes, simplifying % 42.01/6.52 | with (34), (61) gives: % 42.01/6.52 | (82) all_418_3 = all_387_1 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_376_2, all_418_3, vyes, simplifying % 42.01/6.52 | with (26), (61) gives: % 42.01/6.52 | (83) all_418_3 = all_376_2 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_393_1, all_406_1, vno, simplifying % 42.01/6.52 | with (37), (50) gives: % 42.01/6.52 | (84) all_406_1 = all_393_1 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_406_1, all_415_2, vno, simplifying % 42.01/6.52 | with (50), (55) gives: % 42.01/6.52 | (85) all_415_2 = all_406_1 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_403_1, all_415_2, vno, simplifying % 42.01/6.52 | with (45), (55) gives: % 42.01/6.52 | (86) all_415_2 = all_403_1 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_415_2, all_418_1, vno, simplifying % 42.01/6.52 | with (55), (62) gives: % 42.01/6.52 | (87) all_418_1 = all_415_2 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (18) with all_380_2, all_418_1, vno, simplifying % 42.01/6.52 | with (30), (62) gives: % 42.01/6.52 | (88) all_418_1 = all_380_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (87), (88) imply: % 42.01/6.52 | (89) all_415_2 = all_380_2 % 42.01/6.52 | % 42.01/6.52 | SIMP: (89) implies: % 42.01/6.52 | (90) all_415_2 = all_380_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (80), (81) imply: % 42.01/6.52 | (91) all_415_5 = all_406_3 % 42.01/6.52 | % 42.01/6.52 | SIMP: (91) implies: % 42.01/6.52 | (92) all_415_5 = all_406_3 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (81), (82) imply: % 42.01/6.52 | (93) all_406_3 = all_387_1 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (81), (83) imply: % 42.01/6.52 | (94) all_406_3 = all_376_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (85), (86) imply: % 42.01/6.52 | (95) all_406_1 = all_403_1 % 42.01/6.52 | % 42.01/6.52 | SIMP: (95) implies: % 42.01/6.52 | (96) all_406_1 = all_403_1 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (86), (90) imply: % 42.01/6.52 | (97) all_403_1 = all_380_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (79), (92) imply: % 42.01/6.52 | (98) all_406_3 = all_403_3 % 42.01/6.52 | % 42.01/6.52 | SIMP: (98) implies: % 42.01/6.52 | (99) all_406_3 = all_403_3 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (84), (96) imply: % 42.01/6.52 | (100) all_403_1 = all_393_1 % 42.01/6.52 | % 42.01/6.52 | SIMP: (100) implies: % 42.01/6.52 | (101) all_403_1 = all_393_1 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (93), (99) imply: % 42.01/6.52 | (102) all_403_3 = all_387_1 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (94), (99) imply: % 42.01/6.52 | (103) all_403_3 = all_376_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (97), (101) imply: % 42.01/6.52 | (104) all_393_1 = all_380_2 % 42.01/6.52 | % 42.01/6.52 | SIMP: (104) implies: % 42.01/6.52 | (105) all_393_1 = all_380_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (102), (103) imply: % 42.01/6.52 | (106) all_387_1 = all_376_2 % 42.01/6.52 | % 42.01/6.52 | SIMP: (106) implies: % 42.01/6.52 | (107) all_387_1 = all_376_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (84), (105) imply: % 42.01/6.52 | (108) all_406_1 = all_380_2 % 42.01/6.52 | % 42.01/6.52 | COMBINE_EQS: (79), (103) imply: % 42.01/6.52 | (109) all_415_5 = all_376_2 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (60), (88) imply: % 42.01/6.52 | (110) vconstant(all_380_2) = all_418_0 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (59), (83) imply: % 42.01/6.52 | (111) vconstant(all_376_2) = all_418_2 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (53), (90) imply: % 42.01/6.52 | (112) vconstant(all_380_2) = all_415_1 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (52), (109) imply: % 42.01/6.52 | (113) vconstant(all_376_2) = all_415_4 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (48), (108) imply: % 42.01/6.52 | (114) vconstant(all_380_2) = all_406_0 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (47), (94) imply: % 42.01/6.52 | (115) vconstant(all_376_2) = all_406_2 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (43), (97) imply: % 42.01/6.52 | (116) vconstant(all_380_2) = all_403_0 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (42), (103) imply: % 42.01/6.52 | (117) vconstant(all_376_2) = all_403_2 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (36), (105) imply: % 42.01/6.52 | (118) vconstant(all_380_2) = all_393_0 % 42.01/6.52 | % 42.01/6.52 | REDUCE: (33), (107) imply: % 42.01/6.52 | (119) vconstant(all_376_2) = all_387_0 % 42.01/6.52 | % 42.01/6.52 | GROUND_INST: instantiating (17) with all_403_2, all_415_4, all_376_2, % 42.01/6.52 | simplifying with (113), (117) gives: % 42.01/6.53 | (120) all_415_4 = all_403_2 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_387_0, all_415_4, all_376_2, % 42.01/6.53 | simplifying with (113), (119) gives: % 42.01/6.53 | (121) all_415_4 = all_387_0 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_376_1, all_418_2, all_376_2, % 42.01/6.53 | simplifying with (25), (111) gives: % 42.01/6.53 | (122) all_418_2 = all_376_1 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_406_2, all_418_2, all_376_2, % 42.01/6.53 | simplifying with (111), (115) gives: % 42.01/6.53 | (123) all_418_2 = all_406_2 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_403_2, all_418_2, all_376_2, % 42.01/6.53 | simplifying with (111), (117) gives: % 42.01/6.53 | (124) all_418_2 = all_403_2 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_380_1, all_403_0, all_380_2, % 42.01/6.53 | simplifying with (29), (116) gives: % 42.01/6.53 | (125) all_403_0 = all_380_1 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_406_0, all_415_1, all_380_2, % 42.01/6.53 | simplifying with (112), (114) gives: % 42.01/6.53 | (126) all_415_1 = all_406_0 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_403_0, all_415_1, all_380_2, % 42.01/6.53 | simplifying with (112), (116) gives: % 42.01/6.53 | (127) all_415_1 = all_403_0 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_415_1, all_418_0, all_380_2, % 42.01/6.53 | simplifying with (110), (112) gives: % 42.01/6.53 | (128) all_418_0 = all_415_1 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (17) with all_393_0, all_418_0, all_380_2, % 42.01/6.53 | simplifying with (110), (118) gives: % 42.01/6.53 | (129) all_418_0 = all_393_0 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (128), (129) imply: % 42.01/6.53 | (130) all_415_1 = all_393_0 % 42.01/6.53 | % 42.01/6.53 | SIMP: (130) implies: % 42.01/6.53 | (131) all_415_1 = all_393_0 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (123), (124) imply: % 42.01/6.53 | (132) all_406_2 = all_403_2 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (122), (123) imply: % 42.01/6.53 | (133) all_406_2 = all_376_1 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (126), (127) imply: % 42.01/6.53 | (134) all_406_0 = all_403_0 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (126), (131) imply: % 42.01/6.53 | (135) all_406_0 = all_393_0 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (120), (121) imply: % 42.01/6.53 | (136) all_403_2 = all_387_0 % 42.01/6.53 | % 42.01/6.53 | SIMP: (136) implies: % 42.01/6.53 | (137) all_403_2 = all_387_0 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (134), (135) imply: % 42.01/6.53 | (138) all_403_0 = all_393_0 % 42.01/6.53 | % 42.01/6.53 | SIMP: (138) implies: % 42.01/6.53 | (139) all_403_0 = all_393_0 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (132), (133) imply: % 42.01/6.53 | (140) all_403_2 = all_376_1 % 42.01/6.53 | % 42.01/6.53 | SIMP: (140) implies: % 42.01/6.53 | (141) all_403_2 = all_376_1 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (125), (139) imply: % 42.01/6.53 | (142) all_393_0 = all_380_1 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (137), (141) imply: % 42.01/6.53 | (143) all_387_0 = all_376_1 % 42.01/6.53 | % 42.01/6.53 | SIMP: (143) implies: % 42.01/6.53 | (144) all_387_0 = all_376_1 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (135), (142) imply: % 42.01/6.53 | (145) all_406_0 = all_380_1 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (121), (144) imply: % 42.01/6.53 | (146) all_415_4 = all_376_1 % 42.01/6.53 | % 42.01/6.53 | COMBINE_EQS: (126), (145) imply: % 42.01/6.53 | (147) all_415_1 = all_380_1 % 42.01/6.53 | % 42.01/6.53 | REDUCE: (57), (147) imply: % 42.01/6.53 | (148) vsomeExp(all_380_1) = all_415_0 % 42.01/6.53 | % 42.01/6.53 | REDUCE: (56), (146) imply: % 42.01/6.53 | (149) vsomeExp(all_376_1) = all_415_3 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (19) with all_376_0, all_415_3, all_376_1, % 42.01/6.53 | simplifying with (27), (149) gives: % 42.01/6.53 | (150) all_415_3 = all_376_0 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (19) with all_380_0, all_415_0, all_380_1, % 42.01/6.53 | simplifying with (31), (148) gives: % 42.01/6.53 | (151) all_415_0 = all_380_0 % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (6) with vyes, vno, simplifying with (1), (11) % 42.01/6.53 | gives: % 42.01/6.53 | (152) ? [v0: vAval] : ? [v1: vOptExp] : ? [v2: vAval] : ? [v3: vExp] : % 42.01/6.53 | (vevalUnOp(vnotop, v0) = v1 & vsomeExp(v3) = v1 & vB(vno) = v2 & % 42.01/6.53 | vB(vyes) = v0 & vconstant(v2) = v3 & vOptExp(v1) & vExp(v3) & % 42.01/6.53 | vAval(v2) & vAval(v0)) % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (6) with vno, vyes, simplifying with (2), (12) % 42.01/6.53 | gives: % 42.01/6.53 | (153) ? [v0: vAval] : ? [v1: vOptExp] : ? [v2: vAval] : ? [v3: vExp] : % 42.01/6.53 | (vevalUnOp(vnotop, v0) = v1 & vsomeExp(v3) = v1 & vB(vno) = v0 & % 42.01/6.53 | vB(vyes) = v2 & vconstant(v2) = v3 & vOptExp(v1) & vExp(v3) & % 42.01/6.53 | vAval(v2) & vAval(v0)) % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (expIsValue-true-INV) with ve1, simplifying with % 42.01/6.53 | (15), (78) gives: % 42.01/6.53 | (154) ? [v0: vAval] : (vconstant(v0) = ve1 & vAval(v0)) % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (reduceExp-8) with ve1, all_421_7, all_421_8, % 42.01/6.53 | all_421_3, all_421_1, simplifying with (15), (67), (69), (71), % 42.01/6.53 | (74) gives: % 42.01/6.53 | (155) ? [v0: any] : ? [v1: vAval] : ? [v2: vOptExp] : % 42.01/6.53 | (vevalUnOp(all_421_7, v1) = v2 & vexpIsValue(ve1) = v0 & % 42.01/6.53 | vgetExpValue(ve1) = v1 & vOptExp(v2) & vAval(v1) & ( ~ (v0 = 0) | % 42.01/6.53 | v2 = all_421_1)) % 42.01/6.53 | % 42.01/6.53 | GROUND_INST: instantiating (14) with all_421_8, all_421_6, all_421_5, % 42.01/6.53 | all_421_4, all_421_2, all_421_0, simplifying with (67), (68), % 42.01/6.53 | (70), (72), (75), (76) gives: % 42.01/6.53 | (156) all_421_0 = all_421_2 | ? [v0: vOptAType] : ? [v1: vOptExp] : ? % 42.01/6.53 | [v2: vOptExp] : (vecheck(all_421_4, ve1) = v0 & vreduceExp(ve1, % 42.01/6.53 | all_421_8) = v1 & vsomeExp(all_421_5) = v2 & vOptExp(v2) & % 42.01/6.53 | vOptExp(v1) & vOptAType(v0) & ( ~ (v2 = v1) | ~ (v0 = all_421_2))) % 42.01/6.53 | % 42.01/6.53 | DELTA: instantiating (154) with fresh symbol all_441_0 gives: % 42.01/6.53 | (157) vconstant(all_441_0) = ve1 & vAval(all_441_0) % 42.01/6.53 | % 42.01/6.53 | ALPHA: (157) implies: % 42.01/6.53 | (158) vAval(all_441_0) % 42.01/6.53 | (159) vconstant(all_441_0) = ve1 % 42.01/6.53 | % 42.01/6.53 | DELTA: instantiating (155) with fresh symbols all_443_0, all_443_1, all_443_2 % 42.01/6.53 | gives: % 42.01/6.53 | (160) vevalUnOp(all_421_7, all_443_1) = all_443_0 & vexpIsValue(ve1) = % 42.01/6.53 | all_443_2 & vgetExpValue(ve1) = all_443_1 & vOptExp(all_443_0) & % 42.01/6.53 | vAval(all_443_1) & ( ~ (all_443_2 = 0) | all_443_0 = all_421_1) % 42.01/6.53 | % 42.01/6.53 | ALPHA: (160) implies: % 42.01/6.53 | (161) vgetExpValue(ve1) = all_443_1 % 42.01/6.53 | (162) vexpIsValue(ve1) = all_443_2 % 42.01/6.53 | (163) vevalUnOp(all_421_7, all_443_1) = all_443_0 % 42.01/6.53 | (164) ~ (all_443_2 = 0) | all_443_0 = all_421_1 % 42.01/6.53 | % 42.01/6.53 | DELTA: instantiating (153) with fresh symbols all_445_0, all_445_1, all_445_2, % 42.01/6.53 | all_445_3 gives: % 42.01/6.54 | (165) vevalUnOp(vnotop, all_445_3) = all_445_2 & vsomeExp(all_445_0) = % 42.01/6.54 | all_445_2 & vB(vno) = all_445_3 & vB(vyes) = all_445_1 & % 42.01/6.54 | vconstant(all_445_1) = all_445_0 & vOptExp(all_445_2) & % 42.01/6.54 | vExp(all_445_0) & vAval(all_445_1) & vAval(all_445_3) % 42.01/6.54 | % 42.01/6.54 | ALPHA: (165) implies: % 42.01/6.54 | (166) vExp(all_445_0) % 42.01/6.54 | (167) vconstant(all_445_1) = all_445_0 % 42.01/6.54 | (168) vB(vyes) = all_445_1 % 42.01/6.54 | (169) vB(vno) = all_445_3 % 42.01/6.54 | (170) vsomeExp(all_445_0) = all_445_2 % 42.01/6.54 | % 42.01/6.54 | DELTA: instantiating (152) with fresh symbols all_447_0, all_447_1, all_447_2, % 42.01/6.54 | all_447_3 gives: % 42.01/6.54 | (171) vevalUnOp(vnotop, all_447_3) = all_447_2 & vsomeExp(all_447_0) = % 42.01/6.54 | all_447_2 & vB(vno) = all_447_1 & vB(vyes) = all_447_3 & % 42.01/6.54 | vconstant(all_447_1) = all_447_0 & vOptExp(all_447_2) & % 42.01/6.54 | vExp(all_447_0) & vAval(all_447_1) & vAval(all_447_3) % 42.01/6.54 | % 42.01/6.54 | ALPHA: (171) implies: % 42.01/6.54 | (172) vExp(all_447_0) % 42.01/6.54 | (173) vconstant(all_447_1) = all_447_0 % 42.01/6.54 | (174) vB(vyes) = all_447_3 % 42.01/6.54 | (175) vB(vno) = all_447_1 % 42.01/6.54 | (176) vsomeExp(all_447_0) = all_447_2 % 42.01/6.54 | % 42.01/6.54 | BETA: splitting (156) gives: % 42.01/6.54 | % 42.01/6.54 | Case 1: % 42.01/6.54 | | % 42.01/6.54 | | (177) all_421_0 = all_421_2 % 42.01/6.54 | | % 42.01/6.54 | | REDUCE: (65), (177) imply: % 42.01/6.54 | | (178) $false % 42.01/6.54 | | % 42.01/6.54 | | CLOSE: (178) is inconsistent. % 42.01/6.54 | | % 42.01/6.54 | Case 2: % 42.01/6.54 | | % 42.01/6.54 | | (179) ? [v0: vOptAType] : ? [v1: vOptExp] : ? [v2: vOptExp] : % 42.01/6.54 | | (vecheck(all_421_4, ve1) = v0 & vreduceExp(ve1, all_421_8) = v1 & % 42.01/6.54 | | vsomeExp(all_421_5) = v2 & vOptExp(v2) & vOptExp(v1) & % 42.01/6.54 | | vOptAType(v0) & ( ~ (v2 = v1) | ~ (v0 = all_421_2))) % 42.01/6.54 | | % 42.01/6.54 | | DELTA: instantiating (179) with fresh symbols all_453_0, all_453_1, % 42.01/6.54 | | all_453_2 gives: % 42.01/6.54 | | (180) vecheck(all_421_4, ve1) = all_453_2 & vreduceExp(ve1, all_421_8) = % 42.01/6.54 | | all_453_1 & vsomeExp(all_421_5) = all_453_0 & vOptExp(all_453_0) & % 42.01/6.54 | | vOptExp(all_453_1) & vOptAType(all_453_2) & ( ~ (all_453_0 = % 42.01/6.54 | | all_453_1) | ~ (all_453_2 = all_421_2)) % 42.01/6.54 | | % 42.01/6.54 | | ALPHA: (180) implies: % 42.01/6.54 | | (181) vsomeExp(all_421_5) = all_453_0 % 42.01/6.54 | | % 42.01/6.54 | | GROUND_INST: instantiating (18) with all_376_2, all_447_3, vyes, simplifying % 42.01/6.54 | | with (26), (174) gives: % 42.01/6.54 | | (182) all_447_3 = all_376_2 % 42.01/6.54 | | % 42.01/6.54 | | GROUND_INST: instantiating (18) with all_445_1, all_447_3, vyes, simplifying % 42.01/6.54 | | with (168), (174) gives: % 42.01/6.54 | | (183) all_447_3 = all_445_1 % 42.01/6.54 | | % 42.01/6.54 | | GROUND_INST: instantiating (18) with all_380_2, all_447_1, vno, simplifying % 42.01/6.54 | | with (30), (175) gives: % 42.01/6.54 | | (184) all_447_1 = all_380_2 % 42.01/6.54 | | % 42.01/6.54 | | GROUND_INST: instantiating (18) with all_445_3, all_447_1, vno, simplifying % 42.01/6.54 | | with (169), (175) gives: % 42.01/6.54 | | (185) all_447_1 = all_445_3 % 42.01/6.54 | | % 42.01/6.54 | | GROUND_INST: instantiating (19) with all_421_1, all_453_0, all_421_5, % 42.01/6.54 | | simplifying with (73), (181) gives: % 42.01/6.54 | | (186) all_453_0 = all_421_1 % 42.01/6.54 | | % 42.01/6.54 | | GROUND_INST: instantiating (21) with 0, all_443_2, ve1, simplifying with % 42.01/6.54 | | (78), (162) gives: % 42.01/6.54 | | (187) all_443_2 = 0 % 42.01/6.54 | | % 42.01/6.54 | | COMBINE_EQS: (184), (185) imply: % 42.01/6.54 | | (188) all_445_3 = all_380_2 % 42.01/6.54 | | % 42.01/6.54 | | COMBINE_EQS: (182), (183) imply: % 42.01/6.54 | | (189) all_445_1 = all_376_2 % 42.01/6.54 | | % 42.01/6.54 | | REDUCE: (173), (184) imply: % 42.01/6.54 | | (190) vconstant(all_380_2) = all_447_0 % 42.01/6.54 | | % 42.01/6.54 | | REDUCE: (167), (189) imply: % 42.01/6.54 | | (191) vconstant(all_376_2) = all_445_0 % 42.01/6.54 | | % 42.01/6.54 | | BETA: splitting (164) gives: % 42.01/6.54 | | % 42.01/6.54 | | Case 1: % 42.01/6.54 | | | % 42.01/6.54 | | | (192) ~ (all_443_2 = 0) % 42.01/6.54 | | | % 42.01/6.54 | | | REDUCE: (187), (192) imply: % 42.01/6.54 | | | (193) $false % 42.01/6.54 | | | % 42.01/6.54 | | | CLOSE: (193) is inconsistent. % 42.01/6.54 | | | % 42.01/6.54 | | Case 2: % 42.01/6.54 | | | % 42.01/6.54 | | | (194) all_443_0 = all_421_1 % 42.01/6.54 | | | % 42.01/6.54 | | | REDUCE: (163), (194) imply: % 42.01/6.54 | | | (195) vevalUnOp(all_421_7, all_443_1) = all_421_1 % 42.01/6.54 | | | % 42.01/6.54 | | | GROUND_INST: instantiating (17) with all_376_1, all_445_0, all_376_2, % 42.01/6.54 | | | simplifying with (25), (191) gives: % 42.01/6.54 | | | (196) all_445_0 = all_376_1 % 42.01/6.54 | | | % 42.01/6.54 | | | GROUND_INST: instantiating (17) with all_380_1, all_447_0, all_380_2, % 42.01/6.54 | | | simplifying with (29), (190) gives: % 42.01/6.54 | | | (197) all_447_0 = all_380_1 % 42.01/6.54 | | | % 42.01/6.54 | | | REDUCE: (176), (197) imply: % 42.01/6.54 | | | (198) vsomeExp(all_380_1) = all_447_2 % 42.01/6.54 | | | % 42.01/6.54 | | | REDUCE: (170), (196) imply: % 42.01/6.54 | | | (199) vsomeExp(all_376_1) = all_445_2 % 42.01/6.54 | | | % 42.01/6.54 | | | REDUCE: (172), (197) imply: % 42.01/6.54 | | | (200) vExp(all_380_1) % 42.01/6.54 | | | % 42.01/6.54 | | | REDUCE: (166), (196) imply: % 42.01/6.54 | | | (201) vExp(all_376_1) % 42.01/6.54 | | | % 42.01/6.54 | | | GROUND_INST: instantiating (19) with all_376_0, all_445_2, all_376_1, % 42.01/6.54 | | | simplifying with (27), (199) gives: % 42.01/6.54 | | | (202) all_445_2 = all_376_0 % 42.01/6.54 | | | % 42.01/6.54 | | | GROUND_INST: instantiating (19) with all_380_0, all_447_2, all_380_1, % 42.01/6.54 | | | simplifying with (31), (198) gives: % 42.01/6.54 | | | (203) all_447_2 = all_380_0 % 42.01/6.54 | | | % 42.01/6.54 | | | GROUND_INST: instantiating (evalUnOpPreservation) with all_421_5, % 42.01/6.54 | | | all_421_4, all_421_6, all_441_0, all_421_7, ve1, all_421_3, % 42.01/6.54 | | | all_421_2, all_421_1, simplifying with (66), (68), (69), % 42.01/6.54 | | | (70), (71), (72), (73), (77), (158), (159) gives: % 42.01/6.54 | | | (204) ? [v0: vOptExp] : ? [v1: vOptAType] : (vecheck(all_421_4, % 42.01/6.54 | | | all_421_5) = v1 & vevalUnOp(all_421_7, all_441_0) = v0 & % 42.01/6.54 | | | vOptExp(v0) & vOptAType(v1) & ( ~ (v0 = all_421_1) | v1 = % 42.01/6.54 | | | all_421_2)) % 42.01/6.54 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (evalUnOpPreservation) with all_380_1, % 42.01/6.55 | | | all_421_4, all_421_6, all_441_0, all_421_7, ve1, all_421_3, % 42.01/6.55 | | | all_421_2, all_380_0, simplifying with (31), (66), (69), % 42.01/6.55 | | | (70), (71), (72), (77), (158), (159), (200) gives: % 42.01/6.55 | | | (205) ? [v0: vOptExp] : ? [v1: vOptAType] : (vecheck(all_421_4, % 42.01/6.55 | | | all_380_1) = v1 & vevalUnOp(all_421_7, all_441_0) = v0 & % 42.01/6.55 | | | vOptExp(v0) & vOptAType(v1) & ( ~ (v0 = all_380_0) | v1 = % 42.01/6.55 | | | all_421_2)) % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (evalUnOpPreservation) with all_376_1, % 42.01/6.55 | | | all_421_4, all_421_6, all_441_0, all_421_7, ve1, all_421_3, % 42.01/6.55 | | | all_421_2, all_376_0, simplifying with (27), (66), (69), % 42.01/6.55 | | | (70), (71), (72), (77), (158), (159), (201) gives: % 42.01/6.55 | | | (206) ? [v0: vOptExp] : ? [v1: vOptAType] : (vecheck(all_421_4, % 42.01/6.55 | | | all_376_1) = v1 & vevalUnOp(all_421_7, all_441_0) = v0 & % 42.01/6.55 | | | vOptExp(v0) & vOptAType(v1) & ( ~ (v0 = all_376_0) | v1 = % 42.01/6.55 | | | all_421_2)) % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (evalUnOpProgress) with all_421_4, all_421_7, % 42.01/6.55 | | | all_441_0, all_421_6, ve1, all_421_3, all_421_2, simplifying % 42.01/6.55 | | | with (66), (69), (70), (71), (72), (77), (158), (159) gives: % 42.01/6.55 | | | (207) ? [v0: vOptExp] : (vevalUnOp(all_421_7, all_441_0) = v0 & % 42.01/6.55 | | | vOptExp(v0) & ? [v1: vExp] : (vsomeExp(v1) = v0 & vExp(v1))) % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (getExpValue-0) with all_441_0, ve1, % 42.01/6.55 | | | simplifying with (158), (159) gives: % 42.01/6.55 | | | (208) vgetExpValue(ve1) = all_441_0 % 42.01/6.55 | | | % 42.01/6.55 | | | DELTA: instantiating (207) with fresh symbol all_507_0 gives: % 42.01/6.55 | | | (209) vevalUnOp(all_421_7, all_441_0) = all_507_0 & vOptExp(all_507_0) % 42.01/6.55 | | | & ? [v0: vExp] : (vsomeExp(v0) = all_507_0 & vExp(v0)) % 42.01/6.55 | | | % 42.01/6.55 | | | ALPHA: (209) implies: % 42.01/6.55 | | | (210) vevalUnOp(all_421_7, all_441_0) = all_507_0 % 42.01/6.55 | | | % 42.01/6.55 | | | DELTA: instantiating (206) with fresh symbols all_509_0, all_509_1 gives: % 42.01/6.55 | | | (211) vecheck(all_421_4, all_376_1) = all_509_0 & vevalUnOp(all_421_7, % 42.01/6.55 | | | all_441_0) = all_509_1 & vOptExp(all_509_1) & % 42.01/6.55 | | | vOptAType(all_509_0) & ( ~ (all_509_1 = all_376_0) | all_509_0 = % 42.01/6.55 | | | all_421_2) % 42.01/6.55 | | | % 42.01/6.55 | | | ALPHA: (211) implies: % 42.01/6.55 | | | (212) vevalUnOp(all_421_7, all_441_0) = all_509_1 % 42.01/6.55 | | | % 42.01/6.55 | | | DELTA: instantiating (205) with fresh symbols all_511_0, all_511_1 gives: % 42.01/6.55 | | | (213) vecheck(all_421_4, all_380_1) = all_511_0 & vevalUnOp(all_421_7, % 42.01/6.55 | | | all_441_0) = all_511_1 & vOptExp(all_511_1) & % 42.01/6.55 | | | vOptAType(all_511_0) & ( ~ (all_511_1 = all_380_0) | all_511_0 = % 42.01/6.55 | | | all_421_2) % 42.01/6.55 | | | % 42.01/6.55 | | | ALPHA: (213) implies: % 42.01/6.55 | | | (214) vevalUnOp(all_421_7, all_441_0) = all_511_1 % 42.01/6.55 | | | % 42.01/6.55 | | | DELTA: instantiating (204) with fresh symbols all_513_0, all_513_1 gives: % 42.01/6.55 | | | (215) vecheck(all_421_4, all_421_5) = all_513_0 & vevalUnOp(all_421_7, % 42.01/6.55 | | | all_441_0) = all_513_1 & vOptExp(all_513_1) & % 42.01/6.55 | | | vOptAType(all_513_0) & ( ~ (all_513_1 = all_421_1) | all_513_0 = % 42.01/6.55 | | | all_421_2) % 42.01/6.55 | | | % 42.01/6.55 | | | ALPHA: (215) implies: % 42.01/6.55 | | | (216) vevalUnOp(all_421_7, all_441_0) = all_513_1 % 42.01/6.55 | | | (217) vecheck(all_421_4, all_421_5) = all_513_0 % 42.01/6.55 | | | (218) ~ (all_513_1 = all_421_1) | all_513_0 = all_421_2 % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (20) with all_443_1, all_441_0, ve1, % 42.01/6.55 | | | simplifying with (161), (208) gives: % 42.01/6.55 | | | (219) all_443_1 = all_441_0 % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (22) with all_507_0, all_511_1, all_441_0, % 42.01/6.55 | | | all_421_7, simplifying with (210), (214) gives: % 42.01/6.55 | | | (220) all_511_1 = all_507_0 % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (22) with all_511_1, all_513_1, all_441_0, % 42.01/6.55 | | | all_421_7, simplifying with (214), (216) gives: % 42.01/6.55 | | | (221) all_513_1 = all_511_1 % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (22) with all_509_1, all_513_1, all_441_0, % 42.01/6.55 | | | all_421_7, simplifying with (212), (216) gives: % 42.01/6.55 | | | (222) all_513_1 = all_509_1 % 42.01/6.55 | | | % 42.01/6.55 | | | GROUND_INST: instantiating (23) with all_421_0, all_513_0, all_421_5, % 42.01/6.55 | | | all_421_4, simplifying with (76), (217) gives: % 42.01/6.55 | | | (223) all_513_0 = all_421_0 % 42.01/6.55 | | | % 42.01/6.55 | | | COMBINE_EQS: (221), (222) imply: % 42.01/6.55 | | | (224) all_511_1 = all_509_1 % 42.01/6.55 | | | % 42.01/6.55 | | | SIMP: (224) implies: % 42.01/6.55 | | | (225) all_511_1 = all_509_1 % 42.01/6.55 | | | % 42.01/6.55 | | | COMBINE_EQS: (220), (225) imply: % 42.01/6.55 | | | (226) all_509_1 = all_507_0 % 42.01/6.55 | | | % 42.01/6.55 | | | SIMP: (226) implies: % 42.01/6.55 | | | (227) all_509_1 = all_507_0 % 42.01/6.55 | | | % 42.01/6.55 | | | COMBINE_EQS: (222), (227) imply: % 42.01/6.55 | | | (228) all_513_1 = all_507_0 % 42.01/6.55 | | | % 42.01/6.55 | | | REDUCE: (195), (219) imply: % 42.01/6.55 | | | (229) vevalUnOp(all_421_7, all_441_0) = all_421_1 % 42.01/6.55 | | | % 42.01/6.55 | | | BETA: splitting (218) gives: % 42.01/6.55 | | | % 42.01/6.55 | | | Case 1: % 42.01/6.55 | | | | % 42.01/6.55 | | | | (230) ~ (all_513_1 = all_421_1) % 42.01/6.55 | | | | % 42.01/6.55 | | | | REDUCE: (228), (230) imply: % 42.01/6.55 | | | | (231) ~ (all_507_0 = all_421_1) % 42.01/6.55 | | | | % 42.01/6.55 | | | | GROUND_INST: instantiating (22) with all_507_0, all_421_1, all_441_0, % 42.01/6.55 | | | | all_421_7, simplifying with (210), (229) gives: % 42.01/6.55 | | | | (232) all_507_0 = all_421_1 % 42.01/6.55 | | | | % 42.01/6.55 | | | | REDUCE: (231), (232) imply: % 42.01/6.55 | | | | (233) $false % 42.01/6.55 | | | | % 42.01/6.55 | | | | CLOSE: (233) is inconsistent. % 42.01/6.55 | | | | % 42.01/6.55 | | | Case 2: % 42.01/6.55 | | | | % 42.01/6.55 | | | | (234) all_513_0 = all_421_2 % 42.01/6.55 | | | | % 42.01/6.55 | | | | COMBINE_EQS: (223), (234) imply: % 42.01/6.55 | | | | (235) all_421_0 = all_421_2 % 42.01/6.55 | | | | % 42.01/6.55 | | | | REDUCE: (65), (235) imply: % 42.01/6.55 | | | | (236) $false % 42.01/6.55 | | | | % 42.01/6.55 | | | | CLOSE: (236) is inconsistent. % 42.01/6.55 | | | | % 42.01/6.55 | | | End of split % 42.01/6.55 | | | % 42.01/6.55 | | End of split % 42.01/6.55 | | % 42.01/6.55 | End of split % 42.01/6.55 | % 42.01/6.55 End of proof % 42.01/6.55 % SZS output end Proof for theBenchmark % 42.01/6.55 % 42.01/6.55 5947ms %------------------------------------------------------------------------------