%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM276_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 29.82s 4.66s % Output : Proof 41.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.15 % Problem : COM276_1 : TPTP v9.3.0. Released v9.3.0. % 0.08/0.16 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.17/0.40 % Computer : n023.cluster.edu % 0.17/0.40 % Model : x86_64 x86_64 % 0.17/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.40 % Memory : 8042.1875MB % 0.17/0.40 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.40 % CPULimit : 300 % 0.17/0.40 % WCLimit : 300 % 0.17/0.40 % DateTime : Mon May 4 20:10:53 EDT 2026 % 0.17/0.40 % CPUTime : % 0.54/0.66 ________ _____ % 0.54/0.66 ___ __ \_________(_)________________________________ % 0.54/0.66 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.54/0.66 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.54/0.66 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.54/0.66 % 0.54/0.66 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.54/0.66 (2023-06-19) % 0.54/0.66 % 0.54/0.66 (c) Philipp Rümmer, 2009-2023 % 0.54/0.66 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.54/0.66 Amanda Stjerna. % 0.54/0.66 Free software under BSD-3-Clause. % 0.54/0.66 % 0.54/0.66 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.54/0.66 % 0.54/0.66 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.54/0.68 Running up to 7 provers in parallel. % 0.54/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.54/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.54/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.54/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.54/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.54/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.54/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.56/2.09 Prover 4: Preprocessing ... % 9.56/2.11 Prover 1: Preprocessing ... % 10.35/2.13 Prover 0: Preprocessing ... % 10.35/2.13 Prover 2: Preprocessing ... % 10.35/2.13 Prover 5: Preprocessing ... % 10.35/2.13 Prover 3: Preprocessing ... % 10.35/2.13 Prover 6: Preprocessing ... % 24.35/3.94 Prover 1: Warning: ignoring some quantifiers % 24.35/3.95 Prover 3: Warning: ignoring some quantifiers % 25.23/4.03 Prover 3: Constructing countermodel ... % 25.23/4.04 Prover 6: Proving ... % 25.23/4.05 Prover 1: Constructing countermodel ... % 28.25/4.42 Prover 5: Proving ... % 29.04/4.56 Prover 4: Warning: ignoring some quantifiers % 29.82/4.66 Prover 3: proved (3973ms) % 29.82/4.66 % 29.82/4.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 29.82/4.66 % 29.82/4.66 Prover 5: stopped % 29.82/4.66 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.82/4.66 Prover 6: stopped % 29.82/4.68 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 29.82/4.68 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.82/4.68 Prover 4: Constructing countermodel ... % 31.38/4.87 Prover 0: Proving ... % 31.38/4.87 Prover 0: stopped % 31.38/4.87 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 34.52/5.29 Prover 10: Preprocessing ... % 35.31/5.30 Prover 7: Preprocessing ... % 35.31/5.33 Prover 8: Preprocessing ... % 35.31/5.39 Prover 11: Preprocessing ... % 36.86/5.59 Prover 2: Proving ... % 36.86/5.59 Prover 2: stopped % 37.66/5.60 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 37.66/5.65 Prover 1: Found proof (size 115) % 37.66/5.65 Prover 1: proved (4966ms) % 37.66/5.65 Prover 4: stopped % 37.66/5.67 Prover 7: stopped % 37.66/5.68 Prover 10: stopped % 38.45/5.73 Prover 11: stopped % 39.00/5.87 Prover 13: Preprocessing ... % 39.50/6.00 Prover 8: Warning: ignoring some quantifiers % 40.10/6.04 Prover 8: Constructing countermodel ... % 40.10/6.05 Prover 8: stopped % 40.10/6.07 Prover 13: stopped % 40.10/6.07 % 40.10/6.07 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 40.10/6.07 % 40.60/6.14 % SZS output start Proof for theBenchmark % 40.60/6.17 Assumptions after simplification: % 40.60/6.17 --------------------------------- % 40.60/6.17 % 40.60/6.17 (DIFF-YesNo-Number) % 40.60/6.18 ~ (vYesNo = vNumber) & vAType(vYesNo) & vAType(vNumber) % 40.60/6.18 % 40.60/6.18 (DIFF-YesNo-Text) % 40.60/6.18 ~ (vText = vYesNo) & vAType(vText) & vAType(vYesNo) % 40.60/6.18 % 40.60/6.18 (evalBinOp-8) % 40.97/6.20 vBinOpT(veqop) & vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] % 40.97/6.20 : (vsomeExp(v1) = v2 & vB(vyes) = v0 & vconstant(v0) = v1 & vOptExp(v2) & % 40.97/6.20 vExp(v1) & vAval(v0) & ! [v3: vAval] : ! [v4: vOptExp] : (v4 = v2 | ~ % 40.97/6.20 (vevalBinOp(veqop, v3, v3) = v4) | ~ vAval(v3))) % 40.97/6.20 % 40.97/6.20 (evalBinOp-INV) % 40.97/6.22 vBinOpT(vgtop) & vBinOpT(vltop) & vBinOpT(vaddop) & vBinOpT(veqop) & % 40.97/6.22 vBinOpT(vorop) & vBinOpT(vmulop) & vBinOpT(vdivop) & vBinOpT(vandop) & % 40.97/6.22 vBinOpT(vsubop) & vOptExp(vnoExp) & vYN(vno) & vYN(vyes) & ? [v0: vAval] : ? % 40.97/6.22 [v1: vExp] : ? [v2: vOptExp] : ? [v3: vAval] : ? [v4: vExp] : ? [v5: % 40.97/6.22 vOptExp] : (vsomeExp(v4) = v5 & vsomeExp(v1) = v2 & vB(vno) = v3 & vB(vyes) % 40.97/6.22 = v0 & vconstant(v3) = v4 & vconstant(v0) = v1 & vOptExp(v5) & vOptExp(v2) & % 40.97/6.22 vExp(v4) & vExp(v1) & vAval(v3) & vAval(v0) & ! [v6: vBinOpT] : ! [v7: % 40.97/6.22 vAval] : ! [v8: vAval] : ! [v9: vOptExp] : ( ~ (vevalBinOp(v6, v7, v8) = % 40.97/6.22 v9) | ~ vBinOpT(v6) | ~ vAval(v8) | ~ vAval(v7) | ? [v10: vnat] : ? % 40.97/6.22 [v11: vnat] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] : (v6 = % 40.97/6.22 vgtop & vgt(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v11) = v8 & % 40.97/6.22 vNum(v10) = v7 & vB(v12) = v13 & vconstant(v13) = v14 & vOptExp(v9) & % 40.97/6.22 vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13) & vYN(v12)) | ? [v10: % 40.97/6.22 vnat] : ? [v11: vnat] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: % 40.97/6.22 vExp] : (v6 = vltop & vlt(v10, v11) = v12 & vsomeExp(v14) = v9 & % 40.97/6.22 vNum(v11) = v8 & vNum(v10) = v7 & vB(v12) = v13 & vconstant(v13) = v14 & % 40.97/6.22 vOptExp(v9) & vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13) & vYN(v12)) % 40.97/6.22 | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] : ? [v13: vAval] : ? % 40.97/6.22 [v14: vExp] : (v6 = vaddop & vplus(v10, v11) = v12 & vsomeExp(v14) = v9 & % 40.97/6.22 vNum(v12) = v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 % 40.97/6.22 & vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 40.97/6.22 vAval(v13)) | ? [v10: vYN] : ? [v11: vYN] : ? [v12: vYN] : ? [v13: % 40.97/6.22 vAval] : ? [v14: vExp] : (v6 = vorop & vor(v10, v11) = v12 & % 40.97/6.22 vsomeExp(v14) = v9 & vB(v12) = v13 & vB(v11) = v8 & vB(v10) = v7 & % 40.97/6.22 vconstant(v13) = v14 & vOptExp(v9) & vExp(v14) & vAval(v13) & vYN(v12) & % 40.97/6.22 vYN(v11) & vYN(v10)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] % 40.97/6.22 : ? [v13: vAval] : ? [v14: vExp] : (v6 = vmulop & vmultiply(v10, v11) = % 40.97/6.22 v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & vNum(v11) = v8 & vNum(v10) % 40.97/6.22 = v7 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v12) & vnat(v11) & % 40.97/6.22 vnat(v10) & vExp(v14) & vAval(v13)) | ? [v10: vnat] : ? [v11: vnat] : % 40.97/6.22 ? [v12: vnat] : ? [v13: vAval] : ? [v14: vExp] : (v6 = vdivop & % 40.97/6.22 vdivide(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & % 40.97/6.22 vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & % 40.97/6.22 vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13)) | ? [v10: % 40.97/6.22 vYN] : ? [v11: vYN] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] % 40.97/6.22 : (v6 = vandop & vand(v10, v11) = v12 & vsomeExp(v14) = v9 & vB(v12) = v13 % 40.97/6.22 & vB(v11) = v8 & vB(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & % 40.97/6.22 vExp(v14) & vAval(v13) & vYN(v12) & vYN(v11) & vYN(v10)) | ? [v10: % 40.97/6.22 vnat] : ? [v11: vnat] : ? [v12: vnat] : ? [v13: vAval] : ? [v14: % 40.97/6.22 vExp] : (v6 = vsubop & vminus(v10, v11) = v12 & vsomeExp(v14) = v9 & % 40.97/6.22 vNum(v12) = v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 % 40.97/6.22 & vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 40.97/6.22 vAval(v13)) | (v9 = v5 & v6 = veqop & ~ (v8 = v7)) | (v9 = v2 & v8 = v7 % 40.97/6.22 & v6 = veqop) | (v9 = vnoExp & ~ (v6 = veqop) & ( ~ (v6 = vorop) | ! % 40.97/6.22 [v10: vYN] : ( ~ (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ % 40.97/6.22 (vB(v10) = v7) | ~ vYN(v10))) & ( ~ (v6 = vandop) | ! [v10: vYN] : % 40.97/6.22 ( ~ (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ (vB(v10) = v7) % 40.97/6.22 | ~ vYN(v10))) & ( ! [v10: vnat] : ( ~ (vNum(v10) = v8) | ~ % 40.97/6.22 vnat(v10)) | ! [v10: vnat] : ( ~ (vNum(v10) = v7) | ~ vnat(v10)) | % 40.97/6.23 ( ~ (v6 = vgtop) & ~ (v6 = vltop) & ~ (v6 = vaddop) & ~ (v6 = % 40.97/6.23 vmulop) & ~ (v6 = vdivop) & ~ (v6 = vsubop)))))) % 40.97/6.23 % 40.97/6.23 (evalBinOpProgress) % 40.97/6.23 ! [v0: vBinOpT] : ! [v1: vAval] : ! [v2: vATMap] : ! [v3: vAval] : ! [v4: % 40.97/6.23 vAType] : ! [v5: vExp] : ! [v6: vExp] : ! [v7: vExp] : ! [v8: vOptAType] % 40.97/6.23 : ( ~ (vecheck(v2, v7) = v8) | ~ (vsomeAType(v4) = v8) | ~ (vbinop(v5, v0, % 40.97/6.23 v6) = v7) | ~ (vconstant(v3) = v6) | ~ (vconstant(v1) = v5) | ~ % 40.97/6.23 vAType(v4) | ~ vBinOpT(v0) | ~ vAval(v3) | ~ vAval(v1) | ~ vATMap(v2) | % 40.97/6.23 ? [v9: vOptExp] : (vevalBinOp(v0, v1, v3) = v9 & vOptExp(v9) & ? [v10: % 40.97/6.23 vExp] : (vsomeExp(v10) = v9 & vExp(v10)))) % 40.97/6.23 % 40.97/6.23 (evalUnOp-0) % 40.97/6.23 vUnOpT(vnotop) & ! [v0: vYN] : ! [v1: vYN] : ( ~ (vnot(v0) = v1) | ~ % 40.97/6.23 vYN(v0) | ? [v2: vAval] : ? [v3: vOptExp] : ? [v4: vAval] : ? [v5: vExp] % 40.97/6.23 : (vevalUnOp(vnotop, v2) = v3 & vsomeExp(v5) = v3 & vB(v1) = v4 & vB(v0) = % 40.97/6.23 v2 & vconstant(v4) = v5 & vOptExp(v3) & vExp(v5) & vAval(v4) & vAval(v2))) % 40.97/6.23 % 40.97/6.23 (expIsValue-1) % 40.97/6.23 ! [v0: vExp] : ( ~ (vexpIsValue(v0) = 0) | ~ vExp(v0) | ? [v1: vAval] : % 40.97/6.23 (vconstant(v1) = v0 & vAval(v1))) % 40.97/6.23 % 40.97/6.23 (expIsValue-true-INV) % 40.97/6.23 ! [v0: vExp] : ( ~ (vexpIsValue(v0) = 0) | ~ vExp(v0) | ? [v1: vAval] : % 40.97/6.23 (vconstant(v1) = v0 & vAval(v1))) % 40.97/6.23 % 40.97/6.23 (getExpValue-0) % 40.97/6.23 ! [v0: vAval] : ! [v1: vExp] : ( ~ (vconstant(v0) = v1) | ~ vAval(v0) | % 40.97/6.23 vgetExpValue(v1) = v0) % 40.97/6.23 % 40.97/6.23 (not-0) % 40.97/6.23 vnot(vyes) = vno & vYN(vno) & vYN(vyes) % 40.97/6.23 % 40.97/6.23 (not-1) % 40.97/6.23 vnot(vno) = vyes & vYN(vno) & vYN(vyes) % 40.97/6.23 % 40.97/6.23 (reduce-11) % 40.97/6.23 vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : (vB(vyes) = v0 & vconstant(v0) = % 40.97/6.23 v1 & vExp(v1) & vAval(v0) & ! [v2: vQuestionnaire] : ! [v3: % 40.97/6.23 vQuestionnaire] : ! [v4: vAnsMap] : ! [v5: vQMap] : ! [v6: % 40.97/6.23 vQuestionnaire] : ! [v7: vOptQConf] : ( ~ (vreduce(v6, v4, v5) = v7) | ~ % 40.97/6.23 (vqcond(v1, v2, v3) = v6) | ~ vQMap(v5) | ~ vAnsMap(v4) | ~ % 40.97/6.23 vQuestionnaire(v3) | ~ vQuestionnaire(v2) | ? [v8: vQConf] : (vQC(v4, % 40.97/6.23 v5, v2) = v8 & vsomeQConf(v8) = v7 & vOptQConf(v7) & vQConf(v8)))) % 40.97/6.23 % 40.97/6.23 (reduce-13) % 40.97/6.24 vYN(vno) & vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? % 40.97/6.24 [v3: vExp] : (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & % 40.97/6.24 vconstant(v0) = v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: % 40.97/6.24 vQMap] : ! [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : ! % 40.97/6.24 [v8: vQuestionnaire] : ! [v9: vOptExp] : ! [v10: vExp] : ! [v11: % 40.97/6.24 vQuestionnaire] : ! [v12: vQConf] : (v6 = v3 | v6 = v1 | ~ % 40.97/6.24 (vreduceExp(v6, v7) = v9) | ~ (vgetExp(v9) = v10) | ~ (vQC(v7, v4, v11) % 40.97/6.24 = v12) | ~ (vqcond(v10, v5, v8) = v11) | ~ vQMap(v4) | ~ vExp(v6) | % 40.97/6.24 ~ vAnsMap(v7) | ~ vQuestionnaire(v8) | ~ vQuestionnaire(v5) | ? [v13: % 40.97/6.24 any] : ? [v14: vQuestionnaire] : ? [v15: vOptQConf] : ? [v16: % 40.97/6.24 vOptQConf] : (vreduce(v14, v7, v4) = v15 & visSomeExp(v9) = v13 & % 40.97/6.24 vsomeQConf(v12) = v16 & vqcond(v6, v5, v8) = v14 & vOptQConf(v16) & % 40.97/6.24 vOptQConf(v15) & vQuestionnaire(v14) & ( ~ (v13 = 0) | v16 = v15)))) % 40.97/6.24 % 40.97/6.24 (reduce-14) % 40.97/6.24 vOptQConf(vnoQConf) & vYN(vno) & vYN(vyes) & ? [v0: vAval] : ? [v1: vExp] : % 40.97/6.24 ? [v2: vAval] : ? [v3: vExp] : (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) % 40.97/6.24 = v3 & vconstant(v0) = v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! % 40.97/6.24 [v4: vQMap] : ! [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : % 40.97/6.24 ! [v8: vQuestionnaire] : ! [v9: vQuestionnaire] : ! [v10: vOptQConf] : % 40.97/6.24 (v10 = vnoQConf | v6 = v3 | v6 = v1 | ~ (vreduce(v9, v7, v4) = v10) | ~ % 40.97/6.24 (vqcond(v6, v5, v8) = v9) | ~ vQMap(v4) | ~ vExp(v6) | ~ vAnsMap(v7) | % 40.97/6.24 ~ vQuestionnaire(v8) | ~ vQuestionnaire(v5) | ? [v11: vOptExp] : % 40.97/6.24 (vreduceExp(v6, v7) = v11 & visSomeExp(v11) = 0 & vOptExp(v11)))) % 40.97/6.24 % 40.97/6.24 (reduce-INV) % 40.97/6.25 vOptQConf(vnoQConf) & vQuestionnaire(vqempty) & vYN(vno) & vYN(vyes) & ? [v0: % 40.97/6.25 vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : (vB(vno) = v2 & % 40.97/6.25 vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = v1 & vExp(v3) & % 40.97/6.25 vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: vQuestionnaire] : ! [v5: % 40.97/6.25 vAnsMap] : ! [v6: vQMap] : ! [v7: vOptQConf] : ( ~ (vreduce(v4, v5, v6) % 40.97/6.25 = v7) | ~ vQMap(v6) | ~ vAnsMap(v5) | ~ vQuestionnaire(v4) | ? [v8: % 40.97/6.25 vAType] : ? [v9: vOptExp] : ? [v10: vQID] : ? [v11: vExp] : ? [v12: % 40.97/6.26 int] : ? [v13: vEntry] : ? [v14: vExp] : ? [v15: vEntry] : ? [v16: % 40.97/6.26 vQuestionnaire] : ? [v17: vQConf] : ( ~ (v12 = 0) & vreduceExp(v11, v5) % 40.97/6.26 = v9 & vexpIsValue(v11) = v12 & visSomeExp(v9) = 0 & vgetExp(v9) = v14 & % 40.97/6.26 vQC(v5, v6, v16) = v17 & vsomeQConf(v17) = v7 & vqsingle(v15) = v16 & % 40.97/6.26 vqsingle(v13) = v4 & vvalue(v10, v8, v14) = v15 & vvalue(v10, v8, v11) = % 40.97/6.26 v13 & vAType(v8) & vOptExp(v9) & vQID(v10) & vExp(v14) & vExp(v11) & % 40.97/6.26 vOptQConf(v7) & vQConf(v17) & vQuestionnaire(v16) & vEntry(v15) & % 40.97/6.26 vEntry(v13)) | ? [v8: vQID] : ? [v9: vOptQuestion] : ? [v10: vEntry] % 40.97/6.26 : ? [v11: vLabel] : ? [v12: vAType] : ? [v13: vEntry] : ? [v14: % 40.97/6.26 vQuestionnaire] : ? [v15: vQConf] : (vlookupQMap(v8, v6) = v9 & % 40.97/6.26 visSomeQuestion(v9) = 0 & vgetQuestionAType(v9) = v12 & % 40.97/6.26 vgetQuestionLabel(v9) = v11 & vQC(v5, v6, v14) = v15 & vsomeQConf(v15) = % 40.97/6.26 v7 & vqsingle(v13) = v14 & vqsingle(v10) = v4 & vask(v8) = v10 & % 40.97/6.26 vquestion(v8, v11, v12) = v13 & vAType(v12) & vLabel(v11) & vQID(v8) & % 40.97/6.26 vOptQuestion(v9) & vOptQConf(v7) & vQConf(v15) & vQuestionnaire(v14) & % 40.97/6.26 vEntry(v13) & vEntry(v10)) | ? [v8: vAType] : ? [v9: vOptExp] : ? % 40.97/6.26 [v10: vQID] : ? [v11: vExp] : ? [v12: int] : ? [v13: int] : ? [v14: % 40.97/6.26 vEntry] : (v7 = vnoQConf & ~ (v13 = 0) & ~ (v12 = 0) & vreduceExp(v11, % 40.97/6.26 v5) = v9 & vexpIsValue(v11) = v12 & visSomeExp(v9) = v13 & % 40.97/6.26 vqsingle(v14) = v4 & vvalue(v10, v8, v11) = v14 & vAType(v8) & % 40.97/6.26 vOptExp(v9) & vQID(v10) & vExp(v11) & vEntry(v14)) | ? [v8: vOptExp] : % 40.97/6.26 ? [v9: vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : ? % 40.97/6.26 [v12: vExp] : ? [v13: vQuestionnaire] : ? [v14: vQConf] : ( ~ (v10 = v3) % 40.97/6.26 & ~ (v10 = v1) & vreduceExp(v10, v5) = v8 & visSomeExp(v8) = 0 & % 40.97/6.26 vgetExp(v8) = v12 & vQC(v5, v6, v13) = v14 & vsomeQConf(v14) = v7 & % 40.97/6.26 vqcond(v12, v9, v11) = v13 & vqcond(v10, v9, v11) = v4 & vOptExp(v8) & % 40.97/6.26 vExp(v12) & vExp(v10) & vOptQConf(v7) & vQConf(v14) & % 40.97/6.26 vQuestionnaire(v13) & vQuestionnaire(v11) & vQuestionnaire(v9)) | ? % 40.97/6.26 [v8: vAType] : ? [v9: vLabel] : ? [v10: vAval] : ? [v11: vQID] : ? % 40.97/6.26 [v12: vEntry] : ? [v13: vAnsMap] : ? [v14: vQConf] : (vgetAnswer(v9, v8) % 40.97/6.26 = v10 & vQC(v13, v6, vqempty) = v14 & vabind(v11, v10, v5) = v13 & % 40.97/6.26 vsomeQConf(v14) = v7 & vqsingle(v12) = v4 & vquestion(v11, v9, v8) = v12 % 40.97/6.26 & vAType(v8) & vLabel(v9) & vQID(v11) & vAnsMap(v13) & vOptQConf(v7) & % 40.97/6.26 vAval(v10) & vQConf(v14) & vEntry(v12)) | ? [v8: vAType] : ? [v9: % 40.97/6.26 vQID] : ? [v10: vExp] : ? [v11: vEntry] : ? [v12: vAval] : ? [v13: % 40.97/6.26 vAnsMap] : ? [v14: vQConf] : (vexpIsValue(v10) = 0 & vgetExpValue(v10) % 40.97/6.26 = v12 & vQC(v13, v6, vqempty) = v14 & vabind(v9, v12, v5) = v13 & % 40.97/6.26 vsomeQConf(v14) = v7 & vqsingle(v11) = v4 & vvalue(v9, v8, v10) = v11 & % 40.97/6.26 vAType(v8) & vQID(v9) & vExp(v10) & vAnsMap(v13) & vOptQConf(v7) & % 40.97/6.26 vAval(v12) & vQConf(v14) & vEntry(v11)) | ? [v8: vAType] : ? [v9: % 40.97/6.26 vLabel] : ? [v10: vQID] : ? [v11: vEntry] : ? [v12: vQMap] : ? [v13: % 40.97/6.26 vQConf] : (vQC(v5, v12, vqempty) = v13 & vsomeQConf(v13) = v7 & % 40.97/6.26 vqsingle(v11) = v4 & vqmbind(v10, v9, v8, v6) = v12 & vdefquestion(v10, % 40.97/6.26 v9, v8) = v11 & vAType(v8) & vLabel(v9) & vQID(v10) & vQMap(v12) & % 40.97/6.26 vOptQConf(v7) & vQConf(v13) & vEntry(v11)) | ? [v8: vOptExp] : ? [v9: % 40.97/6.26 vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : ? [v12: % 40.97/6.26 int] : (v7 = vnoQConf & ~ (v12 = 0) & ~ (v10 = v3) & ~ (v10 = v1) & % 40.97/6.26 vreduceExp(v10, v5) = v8 & visSomeExp(v8) = v12 & vqcond(v10, v9, v11) = % 40.97/6.26 v4 & vOptExp(v8) & vExp(v10) & vQuestionnaire(v11) & vQuestionnaire(v9)) % 40.97/6.26 | ? [v8: vQuestionnaire] : ? [v9: vQuestionnaire] : ? [v10: vOptQConf] % 40.97/6.26 : ? [v11: vQConf] : ? [v12: vQConf] : ( ~ (v8 = vqempty) & vreduce(v8, % 40.97/6.26 v5, v6) = v10 & vqcappend(v11, v9) = v12 & visSomeQC(v10) = 0 & % 40.97/6.26 vgetQC(v10) = v11 & vsomeQConf(v12) = v7 & vqseq(v8, v9) = v4 & % 40.97/6.26 vOptQConf(v10) & vOptQConf(v7) & vQConf(v12) & vQConf(v11) & % 40.97/6.26 vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? % 40.97/6.26 [v9: vQuestionnaire] : ? [v10: vOptQConf] : ? [v11: int] : (v7 = % 40.97/6.26 vnoQConf & ~ (v11 = 0) & ~ (v8 = vqempty) & vreduce(v8, v5, v6) = v10 % 40.97/6.26 & visSomeQC(v10) = v11 & vqseq(v8, v9) = v4 & vOptQConf(v10) & % 40.97/6.26 vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: vQID] : ? [v9: % 40.97/6.26 vOptQuestion] : ? [v10: int] : ? [v11: vEntry] : (v7 = vnoQConf & ~ % 40.97/6.26 (v10 = 0) & vlookupQMap(v8, v6) = v9 & visSomeQuestion(v9) = v10 & % 40.97/6.26 vqsingle(v11) = v4 & vask(v8) = v11 & vQID(v8) & vOptQuestion(v9) & % 40.97/6.26 vEntry(v11)) | ? [v8: vGID] : ? [v9: vQuestionnaire] : ? [v10: % 40.97/6.26 vQConf] : (vQC(v5, v6, v9) = v10 & vsomeQConf(v10) = v7 & vqgroup(v8, % 40.97/6.26 v9) = v4 & vGID(v8) & vOptQConf(v7) & vQConf(v10) & % 40.97/6.26 vQuestionnaire(v9)) | ? [v8: vQuestionnaire] : ? [v9: vQuestionnaire] % 40.97/6.26 : ? [v10: vQConf] : (vQC(v5, v6, v9) = v10 & vsomeQConf(v10) = v7 & % 40.97/6.26 vqcond(v3, v8, v9) = v4 & vOptQConf(v7) & vQConf(v10) & % 40.97/6.26 vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? % 40.97/6.26 [v9: vQuestionnaire] : ? [v10: vQConf] : (vQC(v5, v6, v8) = v10 & % 40.97/6.26 vsomeQConf(v10) = v7 & vqcond(v1, v8, v9) = v4 & vOptQConf(v7) & % 40.97/6.26 vQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: % 40.97/6.26 vQuestionnaire] : ? [v9: vQConf] : (vQC(v5, v6, v8) = v9 & % 40.97/6.26 vsomeQConf(v9) = v7 & vqseq(vqempty, v8) = v4 & vOptQConf(v7) & % 40.97/6.26 vQConf(v9) & vQuestionnaire(v8)) | (v7 = vnoQConf & v4 = vqempty))) % 40.97/6.26 % 40.97/6.26 (reduceExp-3) % 40.97/6.26 ! [v0: vExp] : ! [v1: vExp] : ! [v2: vBinOpT] : ! [v3: vAnsMap] : ! [v4: % 40.97/6.26 vExp] : ! [v5: vOptExp] : ( ~ (vreduceExp(v4, v3) = v5) | ~ (vbinop(v0, % 40.97/6.26 v2, v1) = v4) | ~ vBinOpT(v2) | ~ vExp(v1) | ~ vExp(v0) | ~ % 40.97/6.26 vAnsMap(v3) | ? [v6: any] : ? [v7: any] : ? [v8: vAval] : ? [v9: vAval] % 40.97/6.26 : ? [v10: vOptExp] : (vevalBinOp(v2, v8, v9) = v10 & vexpIsValue(v1) = v7 & % 40.97/6.26 vexpIsValue(v0) = v6 & vgetExpValue(v1) = v9 & vgetExpValue(v0) = v8 & % 40.97/6.26 vOptExp(v10) & vAval(v9) & vAval(v8) & ( ~ (v7 = 0) | ~ (v6 = 0) | v10 = % 40.97/6.26 v5))) % 40.97/6.26 % 40.97/6.26 (reduceExpProgress-binop-IH0) % 40.97/6.26 vExp(ve1) & ? [v0: any] : (vexpIsValue(ve1) = v0 & ! [v1: vAnsMap] : ! [v2: % 40.97/6.26 vAType] : ! [v3: vOptAType] : ! [v4: vOptExp] : (v0 = 0 | ~ % 40.97/6.26 (vreduceExp(ve1, v1) = v4) | ~ (vsomeAType(v2) = v3) | ~ vAType(v2) | ~ % 40.97/6.26 vAnsMap(v1) | ? [v5: vATMap] : ? [v6: vOptAType] : ( ~ (v6 = v3) & % 40.97/6.26 vecheck(v5, ve1) = v6 & vtypeAM(v1) = v5 & vATMap(v5) & vOptAType(v6)) | % 40.97/6.26 ? [v5: vExp] : (vsomeExp(v5) = v4 & vOptExp(v4) & vExp(v5)))) % 40.97/6.26 % 40.97/6.26 (reduceExpProgress-binop-IH1) % 40.97/6.26 vExp(ve2) & ? [v0: any] : (vexpIsValue(ve2) = v0 & ! [v1: vAnsMap] : ! [v2: % 40.97/6.26 vAType] : ! [v3: vOptAType] : ! [v4: vOptExp] : (v0 = 0 | ~ % 40.97/6.26 (vreduceExp(ve2, v1) = v4) | ~ (vsomeAType(v2) = v3) | ~ vAType(v2) | ~ % 40.97/6.26 vAnsMap(v1) | ? [v5: vATMap] : ? [v6: vOptAType] : ( ~ (v6 = v3) & % 40.97/6.26 vecheck(v5, ve2) = v6 & vtypeAM(v1) = v5 & vATMap(v5) & vOptAType(v6)) | % 40.97/6.26 ? [v5: vExp] : (vsomeExp(v5) = v4 & vOptExp(v4) & vExp(v5)))) % 40.97/6.26 % 40.97/6.26 (reduceExpProgress-binop-expIsValue-True-expIsValue-True) % 40.97/6.26 vExp(ve2) & vExp(ve1) & ? [v0: any] : ? [v1: any] : (vexpIsValue(ve2) = v0 & % 40.97/6.26 vexpIsValue(ve1) = v1 & ? [v2: vBinOpT] : ? [v3: vAnsMap] : ? [v4: % 40.97/6.26 vAType] : ? [v5: vExp] : ? [v6: int] : ? [v7: vATMap] : ? [v8: % 40.97/6.26 vOptAType] : ? [v9: vOptExp] : (v1 = 0 & v0 = 0 & ~ (v6 = 0) & % 40.97/6.26 vecheck(v7, v5) = v8 & vtypeAM(v3) = v7 & vreduceExp(v5, v3) = v9 & % 40.97/6.26 vexpIsValue(v5) = v6 & vsomeAType(v4) = v8 & vbinop(ve1, v2, ve2) = v5 & % 40.97/6.26 vAType(v4) & vBinOpT(v2) & vOptExp(v9) & vExp(v5) & vAnsMap(v3) & % 40.97/6.26 vATMap(v7) & vOptAType(v8) & ! [v10: vExp] : ( ~ (vsomeExp(v10) = v9) | % 40.97/6.26 ~ vExp(v10)))) % 40.97/6.26 % 40.97/6.26 (typeOf-0) % 40.97/6.26 vAType(vYesNo) & ! [v0: vYN] : ! [v1: vAval] : ( ~ (vB(v0) = v1) | ~ % 40.97/6.26 vYN(v0) | vtypeOf(v1) = vYesNo) % 40.97/6.26 % 40.97/6.26 (typeOf-INV) % 40.97/6.27 vAType(vText) & vAType(vYesNo) & vAType(vNumber) & ! [v0: vAval] : ! [v1: % 40.97/6.27 vAType] : ( ~ (vtypeOf(v0) = v1) | ~ vAval(v0) | ? [v2: vstring] : (v1 = % 40.97/6.27 vText & vT(v2) = v0 & vstring(v2)) | ? [v2: vYN] : (v1 = vYesNo & vB(v2) % 40.97/6.27 = v0 & vYN(v2)) | ? [v2: vnat] : (v1 = vNumber & vNum(v2) = v0 & % 40.97/6.27 vnat(v2))) % 40.97/6.27 % 40.97/6.27 (function-axioms) % 40.97/6.29 ! [v0: vQMap] : ! [v1: vQMap] : ! [v2: vQMap] : ! [v3: vAType] : ! [v4: % 40.97/6.29 vLabel] : ! [v5: vQID] : (v1 = v0 | ~ (vqmbind(v5, v4, v3, v2) = v1) | ~ % 40.97/6.29 (vqmbind(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 40.97/6.29 MultipleValueBool] : ! [v2: vMapConf] : ! [v3: vQuestionnaire] : ! [v4: % 40.97/6.29 vMapConf] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, % 40.97/6.29 v2) = v0)) & ! [v0: vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : % 40.97/6.29 ! [v3: vAType] : ! [v4: vBinOpT] : (v1 = v0 | ~ (vcheckBinOp(v4, v3, v2) = % 40.97/6.29 v1) | ~ (vcheckBinOp(v4, v3, v2) = v0)) & ! [v0: vOptQConf] : ! [v1: % 40.97/6.29 vOptQConf] : ! [v2: vQMap] : ! [v3: vAnsMap] : ! [v4: vQuestionnaire] : % 40.97/6.29 (v1 = v0 | ~ (vreduce(v4, v3, v2) = v1) | ~ (vreduce(v4, v3, v2) = v0)) & ! % 40.97/6.29 [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vAval] : ! [v4: % 40.97/6.29 vBinOpT] : (v1 = v0 | ~ (vevalBinOp(v4, v3, v2) = v1) | ~ (vevalBinOp(v4, % 40.97/6.29 v3, v2) = v0)) & ! [v0: vQConf] : ! [v1: vQConf] : ! [v2: % 40.97/6.29 vQuestionnaire] : ! [v3: vQMap] : ! [v4: vAnsMap] : (v1 = v0 | ~ (vQC(v4, % 40.97/6.29 v3, v2) = v1) | ~ (vQC(v4, v3, v2) = v0)) & ! [v0: vATMap] : ! [v1: % 40.97/6.29 vATMap] : ! [v2: vATMap] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ % 40.97/6.29 (vatmbind(v4, v3, v2) = v1) | ~ (vatmbind(v4, v3, v2) = v0)) & ! [v0: % 40.97/6.29 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vAType] : ! [v3: vLabel] : % 40.97/6.29 ! [v4: vQID] : (v1 = v0 | ~ (vsomeQuestion(v4, v3, v2) = v1) | ~ % 40.97/6.29 (vsomeQuestion(v4, v3, v2) = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! % 40.97/6.29 [v2: vAnsMap] : ! [v3: vAval] : ! [v4: vQID] : (v1 = v0 | ~ (vabind(v4, v3, % 40.97/6.29 v2) = v1) | ~ (vabind(v4, v3, v2) = v0)) & ! [v0: vQuestionnaire] : ! % 40.97/6.29 [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! [v3: vQuestionnaire] : ! % 40.97/6.29 [v4: vExp] : (v1 = v0 | ~ (vqcond(v4, v3, v2) = v1) | ~ (vqcond(v4, v3, v2) % 40.97/6.29 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: vBinOpT] % 40.97/6.29 : ! [v4: vExp] : (v1 = v0 | ~ (vbinop(v4, v3, v2) = v1) | ~ (vbinop(v4, v3, % 40.97/6.29 v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! [v2: vAType] : ! % 40.97/6.29 [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ (vdefquestion(v4, v3, v2) = v1) | % 40.97/6.29 ~ (vdefquestion(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! % 40.97/6.29 [v2: vExp] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ (vvalue(v4, v3, % 40.97/6.29 v2) = v1) | ~ (vvalue(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: % 40.97/6.29 vEntry] : ! [v2: vAType] : ! [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ % 40.97/6.29 (vquestion(v4, v3, v2) = v1) | ~ (vquestion(v4, v3, v2) = v0)) & ! [v0: % 40.97/6.29 vOptAType] : ! [v1: vOptAType] : ! [v2: vExp] : ! [v3: vATMap] : (v1 = v0 % 40.97/6.29 | ~ (vecheck(v3, v2) = v1) | ~ (vecheck(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : ! [v3: vUnOpT] : (v1 = % 40.97/6.29 v0 | ~ (vcheckUnOp(v3, v2) = v1) | ~ (vcheckUnOp(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 40.97/6.29 ~ (vintersectATM(v3, v2) = v1) | ~ (vintersectATM(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 40.97/6.29 ~ (vappendATMap(v3, v2) = v1) | ~ (vappendATMap(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vOptAType] : ! [v1: vOptAType] : ! [v2: vATMap] : ! [v3: vQID] : (v1 = v0 % 40.97/6.29 | ~ (vlookupATMap(v3, v2) = v1) | ~ (vlookupATMap(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vOptExp] : ! [v1: vOptExp] : ! [v2: vAnsMap] : ! [v3: vExp] : (v1 = v0 | % 40.97/6.29 ~ (vreduceExp(v3, v2) = v1) | ~ (vreduceExp(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vUnOpT] : (v1 = v0 | % 40.97/6.29 ~ (vevalUnOp(v3, v2) = v1) | ~ (vevalUnOp(v3, v2) = v0)) & ! [v0: vAval] : % 40.97/6.29 ! [v1: vAval] : ! [v2: vAType] : ! [v3: vLabel] : (v1 = v0 | ~ % 40.97/6.29 (vgetAnswer(v3, v2) = v1) | ~ (vgetAnswer(v3, v2) = v0)) & ! [v0: vQConf] % 40.97/6.29 : ! [v1: vQConf] : ! [v2: vQuestionnaire] : ! [v3: vQConf] : (v1 = v0 | ~ % 40.97/6.29 (vqcappend(v3, v2) = v1) | ~ (vqcappend(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vQMap] : ! [v3: vQID] : (v1 % 40.97/6.29 = v0 | ~ (vlookupQMap(v3, v2) = v1) | ~ (vlookupQMap(v3, v2) = v0)) & ! % 40.97/6.29 [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vAnsMap] : ! [v3: vAnsMap] : (v1 = % 40.97/6.29 v0 | ~ (vappendAnsMap(v3, v2) = v1) | ~ (vappendAnsMap(v3, v2) = v0)) & ! % 40.97/6.29 [v0: vOptAval] : ! [v1: vOptAval] : ! [v2: vAnsMap] : ! [v3: vQID] : (v1 = % 40.97/6.29 v0 | ~ (vlookupAnsMap(v3, v2) = v1) | ~ (vlookupAnsMap(v3, v2) = v0)) & ! % 40.97/6.29 [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vATList] : (v1 = % 40.97/6.29 v0 | ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vnat] % 40.97/6.29 : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vdivide(v3, % 40.97/6.29 v2) = v1) | ~ (vdivide(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : % 40.97/6.29 ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vmultiply(v3, v2) = v1) | ~ % 40.97/6.29 (vmultiply(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : % 40.97/6.29 ! [v3: vnat] : (v1 = v0 | ~ (vminus(v3, v2) = v1) | ~ (vminus(v3, v2) = v0)) % 40.97/6.29 & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | % 40.97/6.29 ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: % 40.97/6.29 vYN] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 40.97/6.29 (vlt(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vnat] : ! [v3: % 40.97/6.29 vnat] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vYN] : ! [v1: vYN] : ! [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vor(v3, % 40.97/6.29 v2) = v1) | ~ (vor(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! % 40.97/6.29 [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vand(v3, v2) = v1) | ~ (vand(v3, % 40.97/6.29 v2) = v0)) & ! [v0: vstring] : ! [v1: vstring] : ! [v2: vstring] : ! % 40.97/6.29 [v3: vchar] : (v1 = v0 | ~ (vscons(v3, v2) = v1) | ~ (vscons(v3, v2) = v0)) % 40.97/6.29 & ! [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vAType] : % 40.97/6.29 (v1 = v0 | ~ (vatcons(v3, v2) = v1) | ~ (vatcons(v3, v2) = v0)) & ! [v0: % 40.97/6.29 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! % 40.97/6.29 [v3: vGID] : (v1 = v0 | ~ (vqgroup(v3, v2) = v1) | ~ (vqgroup(v3, v2) = v0)) % 40.97/6.29 & ! [v0: vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] % 40.97/6.29 : ! [v3: vQuestionnaire] : (v1 = v0 | ~ (vqseq(v3, v2) = v1) | ~ (vqseq(v3, % 40.97/6.29 v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: % 40.97/6.29 vUnOpT] : (v1 = v0 | ~ (vunop(v3, v2) = v1) | ~ (vunop(v3, v2) = v0)) & ! % 40.97/6.29 [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = % 40.97/6.29 v0 | ~ (vMC(v3, v2) = v1) | ~ (vMC(v3, v2) = v0)) & ! [v0: vATMap] : ! % 40.97/6.29 [v1: vATMap] : ! [v2: vQMap] : (v1 = v0 | ~ (vtypeQM(v2) = v1) | ~ % 40.97/6.29 (vtypeQM(v2) = v0)) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vAnsMap] : % 40.97/6.29 (v1 = v0 | ~ (vtypeAM(v2) = v1) | ~ (vtypeAM(v2) = v0)) & ! [v0: % 40.97/6.29 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptMapConf] : (v1 % 40.97/6.29 = v0 | ~ (visSomeMapConf(v2) = v1) | ~ (visSomeMapConf(v2) = v0)) & ! % 40.97/6.29 [v0: vstring] : ! [v1: vstring] : ! [v2: vLabel] : (v1 = v0 | ~ % 40.97/6.29 (vaskText(v2) = v1) | ~ (vaskText(v2) = v0)) & ! [v0: vnat] : ! [v1: % 40.97/6.29 vnat] : ! [v2: vLabel] : (v1 = v0 | ~ (vaskNumber(v2) = v1) | ~ % 40.97/6.29 (vaskNumber(v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vLabel] : (v1 % 40.97/6.29 = v0 | ~ (vaskYesNo(v2) = v1) | ~ (vaskYesNo(v2) = v0)) & ! [v0: % 40.97/6.29 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] : (v1 = v0 | % 40.97/6.29 ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) & ! [v0: % 40.97/6.29 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptExp] : (v1 = % 40.97/6.29 v0 | ~ (visSomeExp(v2) = v1) | ~ (visSomeExp(v2) = v0)) & ! [v0: % 40.97/6.29 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQConf] : (v1 = % 40.97/6.29 v0 | ~ (visSomeQC(v2) = v1) | ~ (visSomeQC(v2) = v0)) & ! [v0: % 40.97/6.29 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuestionnaire] : % 40.97/6.29 (v1 = v0 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 40.97/6.29 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQConf] : (v1 = v0 | ~ % 40.97/6.29 (vgetQuest(v2) = v1) | ~ (vgetQuest(v2) = v0)) & ! [v0: vQMap] : ! [v1: % 40.97/6.29 vQMap] : ! [v2: vQConf] : (v1 = v0 | ~ (vgetQM(v2) = v1) | ~ (vgetQM(v2) % 40.97/6.29 = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vQConf] : (v1 = v0 % 40.97/6.29 | ~ (vgetAM(v2) = v1) | ~ (vgetAM(v2) = v0)) & ! [v0: MultipleValueBool] % 40.97/6.29 : ! [v1: MultipleValueBool] : ! [v2: vOptQuestion] : (v1 = v0 | ~ % 40.97/6.29 (visSomeQuestion(v2) = v1) | ~ (visSomeQuestion(v2) = v0)) & ! [v0: % 40.97/6.29 vAType] : ! [v1: vAType] : ! [v2: vAval] : (v1 = v0 | ~ (vtypeOf(v2) = % 40.97/6.29 v1) | ~ (vtypeOf(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 40.97/6.29 MultipleValueBool] : ! [v2: vOptAType] : (v1 = v0 | ~ (visSomeAType(v2) = % 40.97/6.29 v1) | ~ (visSomeAType(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 40.97/6.29 MultipleValueBool] : ! [v2: vOptAval] : (v1 = v0 | ~ (visSomeAval(v2) = % 40.97/6.29 v1) | ~ (visSomeAval(v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: % 40.97/6.29 vnat] : (v1 = v0 | ~ (vpred(v2) = v1) | ~ (vpred(v2) = v0)) & ! [v0: vYN] % 40.97/6.29 : ! [v1: vYN] : ! [v2: vYN] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) = % 40.97/6.29 v0)) & ! [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vOptMapConf] : (v1 % 40.97/6.29 = v0 | ~ (vgetMapConf(v2) = v1) | ~ (vgetMapConf(v2) = v0)) & ! [v0: % 40.97/6.29 vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ (vgetExpValue(v2) = % 40.97/6.29 v1) | ~ (vgetExpValue(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 40.97/6.29 [v2: vOptExp] : (v1 = v0 | ~ (vgetExp(v2) = v1) | ~ (vgetExp(v2) = v0)) & ! % 40.97/6.29 [v0: vQConf] : ! [v1: vQConf] : ! [v2: vOptQConf] : (v1 = v0 | ~ % 40.97/6.29 (vgetQC(v2) = v1) | ~ (vgetQC(v2) = v0)) & ! [v0: vAType] : ! [v1: % 40.97/6.29 vAType] : ! [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionAType(v2) = v1) % 40.97/6.29 | ~ (vgetQuestionAType(v2) = v0)) & ! [v0: vLabel] : ! [v1: vLabel] : ! % 40.97/6.29 [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionLabel(v2) = v1) | ~ % 40.97/6.29 (vgetQuestionLabel(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: % 40.97/6.29 vOptQuestion] : (v1 = v0 | ~ (vgetQuestionQID(v2) = v1) | ~ % 40.97/6.29 (vgetQuestionQID(v2) = v0)) & ! [v0: vAType] : ! [v1: vAType] : ! [v2: % 40.97/6.29 vOptAType] : (v1 = v0 | ~ (vgetAType(v2) = v1) | ~ (vgetAType(v2) = v0)) & % 40.97/6.29 ! [v0: vAval] : ! [v1: vAval] : ! [v2: vOptAval] : (v1 = v0 | ~ % 40.97/6.29 (vgetAval(v2) = v1) | ~ (vgetAval(v2) = v0)) & ! [v0: vOptAval] : ! [v1: % 40.97/6.29 vOptAval] : ! [v2: vAval] : (v1 = v0 | ~ (vsomeAval(v2) = v1) | ~ % 40.97/6.29 (vsomeAval(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: vQID] : (v1 % 40.97/6.29 = v0 | ~ (venumQID(v2) = v1) | ~ (venumQID(v2) = v0)) & ! [v0: % 40.97/6.29 vOptMapConf] : ! [v1: vOptMapConf] : ! [v2: vMapConf] : (v1 = v0 | ~ % 40.97/6.29 (vsomeMapConf(v2) = v1) | ~ (vsomeMapConf(v2) = v0)) & ! [v0: vGID] : ! % 40.97/6.29 [v1: vGID] : ! [v2: vGID] : (v1 = v0 | ~ (venumGID(v2) = v1) | ~ % 40.97/6.29 (venumGID(v2) = v0)) & ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vExp] : % 40.97/6.29 (v1 = v0 | ~ (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) & ! [v0: vAval] : % 40.97/6.29 ! [v1: vAval] : ! [v2: vstring] : (v1 = v0 | ~ (vT(v2) = v1) | ~ (vT(v2) = % 40.97/6.29 v0)) & ! [v0: vAval] : ! [v1: vAval] : ! [v2: vnat] : (v1 = v0 | ~ % 40.97/6.29 (vNum(v2) = v1) | ~ (vNum(v2) = v0)) & ! [v0: vAval] : ! [v1: vAval] : ! % 40.97/6.29 [v2: vYN] : (v1 = v0 | ~ (vB(v2) = v1) | ~ (vB(v2) = v0)) & ! [v0: % 40.97/6.29 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : (v1 = v0 | ~ % 40.97/6.29 (vsomeAType(v2) = v1) | ~ (vsomeAType(v2) = v0)) & ! [v0: vOptQConf] : ! % 40.97/6.29 [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | ~ (vsomeQConf(v2) = v1) | ~ % 40.97/6.29 (vsomeQConf(v2) = v0)) & ! [v0: vchar] : ! [v1: vchar] : ! [v2: vchar] : % 40.97/6.29 (v1 = v0 | ~ (venumchar(v2) = v1) | ~ (venumchar(v2) = v0)) & ! [v0: % 40.97/6.29 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vEntry] : (v1 = v0 | ~ % 40.97/6.29 (vqsingle(v2) = v1) | ~ (vqsingle(v2) = v0)) & ! [v0: vnat] : ! [v1: % 40.97/6.29 vnat] : ! [v2: vnat] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = % 40.97/6.29 v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vQID] : (v1 = v0 | ~ % 40.97/6.29 (vqvar(v2) = v1) | ~ (vqvar(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 40.97/6.29 [v2: vAval] : (v1 = v0 | ~ (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & % 40.97/6.29 ! [v0: vLabel] : ! [v1: vLabel] : ! [v2: vLabel] : (v1 = v0 | ~ % 40.97/6.29 (venumLabel(v2) = v1) | ~ (venumLabel(v2) = v0)) & ! [v0: vEntry] : ! % 40.97/6.29 [v1: vEntry] : ! [v2: vQID] : (v1 = v0 | ~ (vask(v2) = v1) | ~ (vask(v2) = % 40.97/6.29 v0)) % 40.97/6.29 % 40.97/6.29 Further assumptions not needed in the proof: % 40.97/6.29 -------------------------------------------- % 40.97/6.29 DIFF-B-Num, DIFF-B-T, DIFF-Num-T, DIFF-Number-Text, DIFF-addop-andop, % 40.97/6.29 DIFF-addop-divop, DIFF-addop-eqop, DIFF-addop-gtop, DIFF-addop-ltop, % 40.97/6.29 DIFF-addop-mulop, DIFF-addop-orop, DIFF-addop-subop, DIFF-aempty-abind, % 40.97/6.29 DIFF-andop-orop, DIFF-atempty-atcons, DIFF-atmempty-atmbind, DIFF-binop-unop, % 40.97/6.29 DIFF-constant-binop, DIFF-constant-qvar, DIFF-constant-unop, % 40.97/6.29 DIFF-defquestion-ask, DIFF-divop-andop, DIFF-divop-eqop, DIFF-divop-gtop, % 40.97/6.29 DIFF-divop-ltop, DIFF-divop-orop, DIFF-eqop-andop, DIFF-eqop-gtop, % 40.97/6.29 DIFF-eqop-ltop, DIFF-eqop-orop, DIFF-gtop-andop, DIFF-gtop-ltop, DIFF-gtop-orop, % 40.97/6.29 DIFF-initGID-enumGID, DIFF-initLabel-enumLabel, DIFF-initQID-enumQID, % 40.97/6.29 DIFF-initchar-enumchar, DIFF-ltop-andop, DIFF-ltop-orop, DIFF-mulop-andop, % 40.97/6.29 DIFF-mulop-divop, DIFF-mulop-eqop, DIFF-mulop-gtop, DIFF-mulop-ltop, % 40.97/6.29 DIFF-mulop-orop, DIFF-noAType-someAType, DIFF-noAval-someAval, % 40.97/6.29 DIFF-noExp-someExp, DIFF-noMapConf-someMapConf, DIFF-noQConf-someQConf, % 40.97/6.29 DIFF-noQuestion-someQuestion, DIFF-qcond-qgroup, DIFF-qempty-qcond, % 40.97/6.29 DIFF-qempty-qgroup, DIFF-qempty-qseq, DIFF-qempty-qsingle, DIFF-qmempty-qmbind, % 40.97/6.29 DIFF-qseq-qcond, DIFF-qseq-qgroup, DIFF-qsingle-qcond, DIFF-qsingle-qgroup, % 40.97/6.29 DIFF-qsingle-qseq, DIFF-question-ask, DIFF-question-defquestion, % 40.97/6.29 DIFF-question-value, DIFF-qvar-binop, DIFF-qvar-unop, DIFF-sempty-scons, % 40.97/6.29 DIFF-subop-andop, DIFF-subop-divop, DIFF-subop-eqop, DIFF-subop-gtop, % 40.97/6.29 DIFF-subop-ltop, DIFF-subop-mulop, DIFF-subop-orop, DIFF-value-ask, % 40.97/6.29 DIFF-value-defquestion, DIFF-yes-no, DIFF-zero-succ, EQ-B, EQ-MC, EQ-Num, EQ-QC, % 40.97/6.29 EQ-T, EQ-abind, EQ-ask, EQ-atcons, EQ-atmbind, EQ-binop, EQ-constant, % 40.97/6.29 EQ-defquestion, EQ-enumGID, EQ-enumLabel, EQ-enumQID, EQ-enumchar, EQ-qcond, % 40.97/6.29 EQ-qgroup, EQ-qmbind, EQ-qseq, EQ-qsingle, EQ-question, EQ-qvar, EQ-scons, % 40.97/6.29 EQ-someAType, EQ-someAval, EQ-someExp, EQ-someMapConf, EQ-someQConf, % 40.97/6.29 EQ-someQuestion, EQ-succ, EQ-unop, EQ-value, Task, Task_inv1, Task_inv2, % 40.97/6.29 Task_inv3, Task_inv4, Tdefquestion, Tdefquestion_inv1, Tdefquestion_inv2, % 40.97/6.29 Tdefquestion_inv3, Tqcond, Tqcond_inv1, Tqcond_inv2, Tqcond_inv3, Tqcond_inv4, % 40.97/6.29 Tqcond_inv5, Tqcond_inv6, Tqcond_inv7, Tqempty, Tqempty_inv1, Tqempty_inv2, % 40.97/6.29 Tqgroup, Tqgroup_inv, Tqseq, Tqseq_inv1, Tqseq_inv2, Tqseq_inv3, Tqseq_inv4, % 40.97/6.29 Tquestion, Tquestion_inv1, Tquestion_inv2, Tquestion_inv3, Tvalue, Tvalue_inv1, % 40.97/6.29 Tvalue_inv2, Tvalue_inv3, Tvalue_inv4, and-0, and-1, and-INV, append-0, % 40.97/6.29 append-1, append-INV, appendATMap-0, appendATMap-1, appendATMap-INV, % 40.97/6.29 appendAnsMap-0, appendAnsMap-1, appendAnsMap-INV, checkBinOp-0, checkBinOp-1, % 40.97/6.29 checkBinOp-2, checkBinOp-3, checkBinOp-4, checkBinOp-5, checkBinOp-6, % 40.97/6.29 checkBinOp-7, checkBinOp-8, checkBinOp-9, checkBinOp-INV, checkUnOp-0, % 40.97/6.29 checkUnOp-1, checkUnOp-INV, divide-0, divide-1, divide-INV, dom-ATList, % 40.97/6.29 dom-ATMap, dom-AType, dom-AnsMap, dom-Aval, dom-BinOpT, dom-Entry, dom-Exp, % 40.97/6.29 dom-MapConf, dom-OptAType, dom-OptAval, dom-OptExp, dom-OptMapConf, % 40.97/6.29 dom-OptQConf, dom-OptQuestion, dom-QConf, dom-QMap, dom-Questionnaire, % 40.97/6.29 dom-UnOpT, dom-YN, dom-nat, dom-string, echeck-0, echeck-1, echeck-2, echeck-3, % 40.97/6.29 echeck-4, echeck-5, echeck-6, echeck-7, echeck-INV, evalBinOp-0, evalBinOp-1, % 40.97/6.29 evalBinOp-10, evalBinOp-2, evalBinOp-3, evalBinOp-4, evalBinOp-5, evalBinOp-6, % 40.97/6.29 evalBinOp-7, evalBinOp-9, evalBinOpPreservation, evalUnOp-1, evalUnOp-INV, % 40.97/6.29 expIsValue-0, expIsValue-false-INV, getAM-0, getAM-INV, getAType-0, getAnswer-0, % 40.97/6.29 getAnswer-1, getAnswer-2, getAnswer-INV, getAval-0, getExp-0, getMapConf-0, % 40.97/6.29 getQC-0, getQM-0, getQM-INV, getQuest-0, getQuest-INV, getQuestionAType-0, % 40.97/6.29 getQuestionLabel-0, getQuestionQID-0, gt-0, gt-1, gt-2, gt-INV, intersectATM-0, % 40.97/6.29 intersectATM-1, intersectATM-2, intersectATM-INV, isSomeAType-0, isSomeAType-1, % 40.97/6.29 isSomeAType-false-INV, isSomeAType-true-INV, isSomeAval-0, isSomeAval-1, % 40.97/6.29 isSomeAval-false-INV, isSomeAval-true-INV, isSomeExp-0, isSomeExp-1, % 40.97/6.29 isSomeExp-false-INV, isSomeExp-true-INV, isSomeMapConf-0, isSomeMapConf-1, % 40.97/6.29 isSomeMapConf-false-INV, isSomeMapConf-true-INV, isSomeQC-0, isSomeQC-1, % 40.97/6.29 isSomeQC-false-INV, isSomeQC-true-INV, isSomeQuestion-0, isSomeQuestion-1, % 40.97/6.29 isSomeQuestion-false-INV, isSomeQuestion-true-INV, isValue-0, isValue-1, % 40.97/6.29 isValue-false-INV, isValue-true-INV, lookupATMap-0, lookupATMap-1, % 40.97/6.29 lookupATMap-2, lookupATMap-INV, lookupAnsMap-0, lookupAnsMap-1, lookupAnsMap-2, % 40.97/6.29 lookupAnsMap-INV, lookupQMap-0, lookupQMap-1, lookupQMap-2, lookupQMap-INV, % 40.97/6.29 lt-0, lt-1, lt-2, lt-INV, minus-0, minus-1, minus-INV, multiply-0, multiply-1, % 40.97/6.29 multiply-INV, not-INV, or-0, or-1, or-INV, plus-0, plus-1, plus-INV, pred-0, % 40.97/6.29 pred-1, pred-INV, qcappend-0, qcappend-INV, reduce-0, reduce-1, reduce-10, % 40.97/6.29 reduce-12, reduce-15, reduce-2, reduce-3, reduce-4, reduce-5, reduce-6, % 40.97/6.29 reduce-7, reduce-8, reduce-9, reduceExp-0, reduceExp-1, reduceExp-10, % 40.97/6.29 reduceExp-2, reduceExp-4, reduceExp-5, reduceExp-6, reduceExp-7, reduceExp-8, % 40.97/6.29 reduceExp-9, reduceExp-INV, typeAM-0, typeAM-1, typeAM-INV, typeOf-1, typeOf-2, % 40.97/6.29 typeQM-0, typeQM-1, typeQM-INV % 40.97/6.29 % 40.97/6.29 Those formulas are unsatisfiable: % 40.97/6.29 --------------------------------- % 40.97/6.29 % 40.97/6.29 Begin of proof % 40.97/6.29 | % 40.97/6.29 | ALPHA: (DIFF-YesNo-Number) implies: % 40.97/6.29 | (1) ~ (vYesNo = vNumber) % 40.97/6.29 | % 40.97/6.29 | ALPHA: (DIFF-YesNo-Text) implies: % 40.97/6.30 | (2) ~ (vText = vYesNo) % 40.97/6.30 | % 40.97/6.30 | ALPHA: (not-0) implies: % 40.97/6.30 | (3) vnot(vyes) = vno % 40.97/6.30 | % 40.97/6.30 | ALPHA: (not-1) implies: % 40.97/6.30 | (4) vnot(vno) = vyes % 40.97/6.30 | % 40.97/6.30 | ALPHA: (typeOf-0) implies: % 40.97/6.30 | (5) ! [v0: vYN] : ! [v1: vAval] : ( ~ (vB(v0) = v1) | ~ vYN(v0) | % 40.97/6.30 | vtypeOf(v1) = vYesNo) % 40.97/6.30 | % 40.97/6.30 | ALPHA: (typeOf-INV) implies: % 40.97/6.30 | (6) ! [v0: vAval] : ! [v1: vAType] : ( ~ (vtypeOf(v0) = v1) | ~ % 40.97/6.30 | vAval(v0) | ? [v2: vstring] : (v1 = vText & vT(v2) = v0 & % 40.97/6.30 | vstring(v2)) | ? [v2: vYN] : (v1 = vYesNo & vB(v2) = v0 & vYN(v2)) % 40.97/6.30 | | ? [v2: vnat] : (v1 = vNumber & vNum(v2) = v0 & vnat(v2))) % 40.97/6.30 | % 40.97/6.30 | ALPHA: (evalBinOp-8) implies: % 41.47/6.30 | (7) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] : (vsomeExp(v1) = v2 % 41.47/6.30 | & vB(vyes) = v0 & vconstant(v0) = v1 & vOptExp(v2) & vExp(v1) & % 41.47/6.30 | vAval(v0) & ! [v3: vAval] : ! [v4: vOptExp] : (v4 = v2 | ~ % 41.47/6.30 | (vevalBinOp(veqop, v3, v3) = v4) | ~ vAval(v3))) % 41.47/6.30 | % 41.47/6.30 | ALPHA: (evalBinOp-INV) implies: % 41.47/6.31 | (8) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vOptExp] : ? [v3: vAval] : ? % 41.47/6.31 | [v4: vExp] : ? [v5: vOptExp] : (vsomeExp(v4) = v5 & vsomeExp(v1) = v2 % 41.47/6.31 | & vB(vno) = v3 & vB(vyes) = v0 & vconstant(v3) = v4 & vconstant(v0) = % 41.47/6.31 | v1 & vOptExp(v5) & vOptExp(v2) & vExp(v4) & vExp(v1) & vAval(v3) & % 41.47/6.31 | vAval(v0) & ! [v6: vBinOpT] : ! [v7: vAval] : ! [v8: vAval] : ! % 41.47/6.31 | [v9: vOptExp] : ( ~ (vevalBinOp(v6, v7, v8) = v9) | ~ vBinOpT(v6) | % 41.47/6.31 | ~ vAval(v8) | ~ vAval(v7) | ? [v10: vnat] : ? [v11: vnat] : ? % 41.47/6.31 | [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] : (v6 = vgtop & % 41.47/6.31 | vgt(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v11) = v8 & % 41.47/6.31 | vNum(v10) = v7 & vB(v12) = v13 & vconstant(v13) = v14 & % 41.47/6.31 | vOptExp(v9) & vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13) & % 41.47/6.31 | vYN(v12)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vYN] : ? % 41.47/6.31 | [v13: vAval] : ? [v14: vExp] : (v6 = vltop & vlt(v10, v11) = v12 & % 41.47/6.31 | vsomeExp(v14) = v9 & vNum(v11) = v8 & vNum(v10) = v7 & vB(v12) = % 41.47/6.31 | v13 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v11) & vnat(v10) % 41.47/6.31 | & vExp(v14) & vAval(v13) & vYN(v12)) | ? [v10: vnat] : ? [v11: % 41.47/6.31 | vnat] : ? [v12: vnat] : ? [v13: vAval] : ? [v14: vExp] : (v6 = % 41.47/6.31 | vaddop & vplus(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v12) = % 41.47/6.31 | v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 & % 41.47/6.31 | vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 41.47/6.31 | vAval(v13)) | ? [v10: vYN] : ? [v11: vYN] : ? [v12: vYN] : ? % 41.47/6.31 | [v13: vAval] : ? [v14: vExp] : (v6 = vorop & vor(v10, v11) = v12 & % 41.47/6.31 | vsomeExp(v14) = v9 & vB(v12) = v13 & vB(v11) = v8 & vB(v10) = v7 % 41.47/6.31 | & vconstant(v13) = v14 & vOptExp(v9) & vExp(v14) & vAval(v13) & % 41.47/6.31 | vYN(v12) & vYN(v11) & vYN(v10)) | ? [v10: vnat] : ? [v11: vnat] % 41.47/6.31 | : ? [v12: vnat] : ? [v13: vAval] : ? [v14: vExp] : (v6 = vmulop % 41.47/6.31 | & vmultiply(v10, v11) = v12 & vsomeExp(v14) = v9 & vNum(v12) = % 41.47/6.31 | v13 & vNum(v11) = v8 & vNum(v10) = v7 & vconstant(v13) = v14 & % 41.47/6.31 | vOptExp(v9) & vnat(v12) & vnat(v11) & vnat(v10) & vExp(v14) & % 41.47/6.31 | vAval(v13)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] : % 41.47/6.31 | ? [v13: vAval] : ? [v14: vExp] : (v6 = vdivop & vdivide(v10, v11) % 41.47/6.31 | = v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & vNum(v11) = v8 & % 41.47/6.31 | vNum(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v12) & % 41.47/6.31 | vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13)) | ? [v10: vYN] : % 41.47/6.31 | ? [v11: vYN] : ? [v12: vYN] : ? [v13: vAval] : ? [v14: vExp] : % 41.47/6.31 | (v6 = vandop & vand(v10, v11) = v12 & vsomeExp(v14) = v9 & vB(v12) % 41.47/6.31 | = v13 & vB(v11) = v8 & vB(v10) = v7 & vconstant(v13) = v14 & % 41.47/6.31 | vOptExp(v9) & vExp(v14) & vAval(v13) & vYN(v12) & vYN(v11) & % 41.47/6.31 | vYN(v10)) | ? [v10: vnat] : ? [v11: vnat] : ? [v12: vnat] : ? % 41.47/6.31 | [v13: vAval] : ? [v14: vExp] : (v6 = vsubop & vminus(v10, v11) = % 41.47/6.31 | v12 & vsomeExp(v14) = v9 & vNum(v12) = v13 & vNum(v11) = v8 & % 41.47/6.31 | vNum(v10) = v7 & vconstant(v13) = v14 & vOptExp(v9) & vnat(v12) & % 41.47/6.31 | vnat(v11) & vnat(v10) & vExp(v14) & vAval(v13)) | (v9 = v5 & v6 = % 41.47/6.31 | veqop & ~ (v8 = v7)) | (v9 = v2 & v8 = v7 & v6 = veqop) | (v9 = % 41.47/6.31 | vnoExp & ~ (v6 = veqop) & ( ~ (v6 = vorop) | ! [v10: vYN] : ( ~ % 41.47/6.31 | (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ (vB(v10) % 41.47/6.31 | = v7) | ~ vYN(v10))) & ( ~ (v6 = vandop) | ! [v10: vYN] : % 41.47/6.31 | ( ~ (vB(v10) = v8) | ~ vYN(v10)) | ! [v10: vYN] : ( ~ % 41.47/6.31 | (vB(v10) = v7) | ~ vYN(v10))) & ( ! [v10: vnat] : ( ~ % 41.47/6.31 | (vNum(v10) = v8) | ~ vnat(v10)) | ! [v10: vnat] : ( ~ % 41.47/6.31 | (vNum(v10) = v7) | ~ vnat(v10)) | ( ~ (v6 = vgtop) & ~ (v6 % 41.47/6.31 | = vltop) & ~ (v6 = vaddop) & ~ (v6 = vmulop) & ~ (v6 = % 41.47/6.31 | vdivop) & ~ (v6 = vsubop)))))) % 41.47/6.31 | % 41.47/6.31 | ALPHA: (evalUnOp-0) implies: % 41.47/6.31 | (9) ! [v0: vYN] : ! [v1: vYN] : ( ~ (vnot(v0) = v1) | ~ vYN(v0) | ? % 41.47/6.31 | [v2: vAval] : ? [v3: vOptExp] : ? [v4: vAval] : ? [v5: vExp] : % 41.47/6.31 | (vevalUnOp(vnotop, v2) = v3 & vsomeExp(v5) = v3 & vB(v1) = v4 & % 41.47/6.31 | vB(v0) = v2 & vconstant(v4) = v5 & vOptExp(v3) & vExp(v5) & % 41.47/6.31 | vAval(v4) & vAval(v2))) % 41.47/6.31 | % 41.47/6.31 | ALPHA: (reduce-11) implies: % 41.47/6.31 | (10) ? [v0: vAval] : ? [v1: vExp] : (vB(vyes) = v0 & vconstant(v0) = v1 & % 41.47/6.31 | vExp(v1) & vAval(v0) & ! [v2: vQuestionnaire] : ! [v3: % 41.47/6.31 | vQuestionnaire] : ! [v4: vAnsMap] : ! [v5: vQMap] : ! [v6: % 41.47/6.31 | vQuestionnaire] : ! [v7: vOptQConf] : ( ~ (vreduce(v6, v4, v5) = % 41.47/6.31 | v7) | ~ (vqcond(v1, v2, v3) = v6) | ~ vQMap(v5) | ~ % 41.47/6.31 | vAnsMap(v4) | ~ vQuestionnaire(v3) | ~ vQuestionnaire(v2) | ? % 41.47/6.31 | [v8: vQConf] : (vQC(v4, v5, v2) = v8 & vsomeQConf(v8) = v7 & % 41.47/6.31 | vOptQConf(v7) & vQConf(v8)))) % 41.47/6.31 | % 41.47/6.31 | ALPHA: (reduce-13) implies: % 41.47/6.31 | (11) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.47/6.31 | (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = % 41.47/6.31 | v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: vQMap] : % 41.47/6.31 | ! [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : ! [v8: % 41.47/6.31 | vQuestionnaire] : ! [v9: vOptExp] : ! [v10: vExp] : ! [v11: % 41.47/6.31 | vQuestionnaire] : ! [v12: vQConf] : (v6 = v3 | v6 = v1 | ~ % 41.47/6.31 | (vreduceExp(v6, v7) = v9) | ~ (vgetExp(v9) = v10) | ~ (vQC(v7, % 41.47/6.31 | v4, v11) = v12) | ~ (vqcond(v10, v5, v8) = v11) | ~ % 41.47/6.31 | vQMap(v4) | ~ vExp(v6) | ~ vAnsMap(v7) | ~ vQuestionnaire(v8) | % 41.47/6.31 | ~ vQuestionnaire(v5) | ? [v13: any] : ? [v14: vQuestionnaire] : % 41.47/6.31 | ? [v15: vOptQConf] : ? [v16: vOptQConf] : (vreduce(v14, v7, v4) % 41.47/6.31 | = v15 & visSomeExp(v9) = v13 & vsomeQConf(v12) = v16 & % 41.47/6.31 | vqcond(v6, v5, v8) = v14 & vOptQConf(v16) & vOptQConf(v15) & % 41.47/6.31 | vQuestionnaire(v14) & ( ~ (v13 = 0) | v16 = v15)))) % 41.47/6.31 | % 41.47/6.31 | ALPHA: (reduce-14) implies: % 41.47/6.31 | (12) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.47/6.31 | (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = % 41.47/6.31 | v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: vQMap] : % 41.47/6.31 | ! [v5: vQuestionnaire] : ! [v6: vExp] : ! [v7: vAnsMap] : ! [v8: % 41.47/6.31 | vQuestionnaire] : ! [v9: vQuestionnaire] : ! [v10: vOptQConf] : % 41.47/6.31 | (v10 = vnoQConf | v6 = v3 | v6 = v1 | ~ (vreduce(v9, v7, v4) = v10) % 41.47/6.31 | | ~ (vqcond(v6, v5, v8) = v9) | ~ vQMap(v4) | ~ vExp(v6) | ~ % 41.47/6.31 | vAnsMap(v7) | ~ vQuestionnaire(v8) | ~ vQuestionnaire(v5) | ? % 41.47/6.31 | [v11: vOptExp] : (vreduceExp(v6, v7) = v11 & visSomeExp(v11) = 0 & % 41.47/6.31 | vOptExp(v11)))) % 41.47/6.31 | % 41.47/6.31 | ALPHA: (reduce-INV) implies: % 41.47/6.31 | (13) vYN(vyes) % 41.47/6.31 | (14) vYN(vno) % 41.47/6.32 | (15) ? [v0: vAval] : ? [v1: vExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.47/6.32 | (vB(vno) = v2 & vB(vyes) = v0 & vconstant(v2) = v3 & vconstant(v0) = % 41.47/6.32 | v1 & vExp(v3) & vExp(v1) & vAval(v2) & vAval(v0) & ! [v4: % 41.47/6.32 | vQuestionnaire] : ! [v5: vAnsMap] : ! [v6: vQMap] : ! [v7: % 41.47/6.32 | vOptQConf] : ( ~ (vreduce(v4, v5, v6) = v7) | ~ vQMap(v6) | ~ % 41.47/6.32 | vAnsMap(v5) | ~ vQuestionnaire(v4) | ? [v8: vAType] : ? [v9: % 41.47/6.32 | vOptExp] : ? [v10: vQID] : ? [v11: vExp] : ? [v12: int] : ? % 41.47/6.32 | [v13: vEntry] : ? [v14: vExp] : ? [v15: vEntry] : ? [v16: % 41.47/6.32 | vQuestionnaire] : ? [v17: vQConf] : ( ~ (v12 = 0) & % 41.47/6.32 | vreduceExp(v11, v5) = v9 & vexpIsValue(v11) = v12 & % 41.47/6.32 | visSomeExp(v9) = 0 & vgetExp(v9) = v14 & vQC(v5, v6, v16) = v17 % 41.47/6.32 | & vsomeQConf(v17) = v7 & vqsingle(v15) = v16 & vqsingle(v13) = % 41.47/6.32 | v4 & vvalue(v10, v8, v14) = v15 & vvalue(v10, v8, v11) = v13 & % 41.47/6.32 | vAType(v8) & vOptExp(v9) & vQID(v10) & vExp(v14) & vExp(v11) & % 41.47/6.32 | vOptQConf(v7) & vQConf(v17) & vQuestionnaire(v16) & vEntry(v15) % 41.47/6.32 | & vEntry(v13)) | ? [v8: vQID] : ? [v9: vOptQuestion] : ? % 41.47/6.32 | [v10: vEntry] : ? [v11: vLabel] : ? [v12: vAType] : ? [v13: % 41.47/6.32 | vEntry] : ? [v14: vQuestionnaire] : ? [v15: vQConf] : % 41.47/6.32 | (vlookupQMap(v8, v6) = v9 & visSomeQuestion(v9) = 0 & % 41.47/6.32 | vgetQuestionAType(v9) = v12 & vgetQuestionLabel(v9) = v11 & % 41.47/6.32 | vQC(v5, v6, v14) = v15 & vsomeQConf(v15) = v7 & vqsingle(v13) = % 41.47/6.32 | v14 & vqsingle(v10) = v4 & vask(v8) = v10 & vquestion(v8, v11, % 41.47/6.32 | v12) = v13 & vAType(v12) & vLabel(v11) & vQID(v8) & % 41.47/6.32 | vOptQuestion(v9) & vOptQConf(v7) & vQConf(v15) & % 41.47/6.32 | vQuestionnaire(v14) & vEntry(v13) & vEntry(v10)) | ? [v8: % 41.47/6.32 | vAType] : ? [v9: vOptExp] : ? [v10: vQID] : ? [v11: vExp] : % 41.47/6.32 | ? [v12: int] : ? [v13: int] : ? [v14: vEntry] : (v7 = vnoQConf & % 41.47/6.32 | ~ (v13 = 0) & ~ (v12 = 0) & vreduceExp(v11, v5) = v9 & % 41.47/6.32 | vexpIsValue(v11) = v12 & visSomeExp(v9) = v13 & vqsingle(v14) = % 41.47/6.32 | v4 & vvalue(v10, v8, v11) = v14 & vAType(v8) & vOptExp(v9) & % 41.47/6.32 | vQID(v10) & vExp(v11) & vEntry(v14)) | ? [v8: vOptExp] : ? % 41.47/6.32 | [v9: vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : % 41.47/6.32 | ? [v12: vExp] : ? [v13: vQuestionnaire] : ? [v14: vQConf] : ( ~ % 41.47/6.32 | (v10 = v3) & ~ (v10 = v1) & vreduceExp(v10, v5) = v8 & % 41.47/6.32 | visSomeExp(v8) = 0 & vgetExp(v8) = v12 & vQC(v5, v6, v13) = v14 % 41.47/6.32 | & vsomeQConf(v14) = v7 & vqcond(v12, v9, v11) = v13 & % 41.47/6.32 | vqcond(v10, v9, v11) = v4 & vOptExp(v8) & vExp(v12) & vExp(v10) % 41.47/6.32 | & vOptQConf(v7) & vQConf(v14) & vQuestionnaire(v13) & % 41.47/6.32 | vQuestionnaire(v11) & vQuestionnaire(v9)) | ? [v8: vAType] : ? % 41.47/6.32 | [v9: vLabel] : ? [v10: vAval] : ? [v11: vQID] : ? [v12: vEntry] % 41.47/6.32 | : ? [v13: vAnsMap] : ? [v14: vQConf] : (vgetAnswer(v9, v8) = v10 % 41.47/6.32 | & vQC(v13, v6, vqempty) = v14 & vabind(v11, v10, v5) = v13 & % 41.47/6.32 | vsomeQConf(v14) = v7 & vqsingle(v12) = v4 & vquestion(v11, v9, % 41.47/6.32 | v8) = v12 & vAType(v8) & vLabel(v9) & vQID(v11) & vAnsMap(v13) % 41.47/6.32 | & vOptQConf(v7) & vAval(v10) & vQConf(v14) & vEntry(v12)) | ? % 41.47/6.32 | [v8: vAType] : ? [v9: vQID] : ? [v10: vExp] : ? [v11: vEntry] : % 41.47/6.32 | ? [v12: vAval] : ? [v13: vAnsMap] : ? [v14: vQConf] : % 41.47/6.32 | (vexpIsValue(v10) = 0 & vgetExpValue(v10) = v12 & vQC(v13, v6, % 41.47/6.32 | vqempty) = v14 & vabind(v9, v12, v5) = v13 & vsomeQConf(v14) = % 41.47/6.32 | v7 & vqsingle(v11) = v4 & vvalue(v9, v8, v10) = v11 & vAType(v8) % 41.47/6.32 | & vQID(v9) & vExp(v10) & vAnsMap(v13) & vOptQConf(v7) & % 41.47/6.32 | vAval(v12) & vQConf(v14) & vEntry(v11)) | ? [v8: vAType] : ? % 41.47/6.32 | [v9: vLabel] : ? [v10: vQID] : ? [v11: vEntry] : ? [v12: vQMap] % 41.47/6.32 | : ? [v13: vQConf] : (vQC(v5, v12, vqempty) = v13 & % 41.47/6.32 | vsomeQConf(v13) = v7 & vqsingle(v11) = v4 & vqmbind(v10, v9, v8, % 41.47/6.32 | v6) = v12 & vdefquestion(v10, v9, v8) = v11 & vAType(v8) & % 41.47/6.32 | vLabel(v9) & vQID(v10) & vQMap(v12) & vOptQConf(v7) & % 41.47/6.32 | vQConf(v13) & vEntry(v11)) | ? [v8: vOptExp] : ? [v9: % 41.47/6.32 | vQuestionnaire] : ? [v10: vExp] : ? [v11: vQuestionnaire] : ? % 41.47/6.32 | [v12: int] : (v7 = vnoQConf & ~ (v12 = 0) & ~ (v10 = v3) & ~ % 41.47/6.32 | (v10 = v1) & vreduceExp(v10, v5) = v8 & visSomeExp(v8) = v12 & % 41.47/6.32 | vqcond(v10, v9, v11) = v4 & vOptExp(v8) & vExp(v10) & % 41.47/6.32 | vQuestionnaire(v11) & vQuestionnaire(v9)) | ? [v8: % 41.47/6.32 | vQuestionnaire] : ? [v9: vQuestionnaire] : ? [v10: vOptQConf] % 41.47/6.32 | : ? [v11: vQConf] : ? [v12: vQConf] : ( ~ (v8 = vqempty) & % 41.47/6.32 | vreduce(v8, v5, v6) = v10 & vqcappend(v11, v9) = v12 & % 41.47/6.32 | visSomeQC(v10) = 0 & vgetQC(v10) = v11 & vsomeQConf(v12) = v7 & % 41.47/6.32 | vqseq(v8, v9) = v4 & vOptQConf(v10) & vOptQConf(v7) & % 41.47/6.32 | vQConf(v12) & vQConf(v11) & vQuestionnaire(v9) & % 41.47/6.32 | vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? [v9: % 41.47/6.32 | vQuestionnaire] : ? [v10: vOptQConf] : ? [v11: int] : (v7 = % 41.47/6.32 | vnoQConf & ~ (v11 = 0) & ~ (v8 = vqempty) & vreduce(v8, v5, % 41.47/6.32 | v6) = v10 & visSomeQC(v10) = v11 & vqseq(v8, v9) = v4 & % 41.47/6.32 | vOptQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v8)) | ? % 41.47/6.32 | [v8: vQID] : ? [v9: vOptQuestion] : ? [v10: int] : ? [v11: % 41.47/6.32 | vEntry] : (v7 = vnoQConf & ~ (v10 = 0) & vlookupQMap(v8, v6) = % 41.47/6.32 | v9 & visSomeQuestion(v9) = v10 & vqsingle(v11) = v4 & vask(v8) = % 41.47/6.32 | v11 & vQID(v8) & vOptQuestion(v9) & vEntry(v11)) | ? [v8: vGID] % 41.47/6.32 | : ? [v9: vQuestionnaire] : ? [v10: vQConf] : (vQC(v5, v6, v9) = % 41.47/6.32 | v10 & vsomeQConf(v10) = v7 & vqgroup(v8, v9) = v4 & vGID(v8) & % 41.47/6.32 | vOptQConf(v7) & vQConf(v10) & vQuestionnaire(v9)) | ? [v8: % 41.47/6.32 | vQuestionnaire] : ? [v9: vQuestionnaire] : ? [v10: vQConf] : % 41.47/6.32 | (vQC(v5, v6, v9) = v10 & vsomeQConf(v10) = v7 & vqcond(v3, v8, v9) % 41.47/6.32 | = v4 & vOptQConf(v7) & vQConf(v10) & vQuestionnaire(v9) & % 41.47/6.32 | vQuestionnaire(v8)) | ? [v8: vQuestionnaire] : ? [v9: % 41.47/6.32 | vQuestionnaire] : ? [v10: vQConf] : (vQC(v5, v6, v8) = v10 & % 41.47/6.32 | vsomeQConf(v10) = v7 & vqcond(v1, v8, v9) = v4 & vOptQConf(v7) & % 41.47/6.32 | vQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v8)) | ? [v8: % 41.47/6.32 | vQuestionnaire] : ? [v9: vQConf] : (vQC(v5, v6, v8) = v9 & % 41.47/6.32 | vsomeQConf(v9) = v7 & vqseq(vqempty, v8) = v4 & vOptQConf(v7) & % 41.47/6.32 | vQConf(v9) & vQuestionnaire(v8)) | (v7 = vnoQConf & v4 = % 41.47/6.32 | vqempty))) % 41.47/6.32 | % 41.47/6.32 | ALPHA: (reduceExpProgress-binop-IH0) implies: % 41.47/6.32 | (16) ? [v0: any] : (vexpIsValue(ve1) = v0 & ! [v1: vAnsMap] : ! [v2: % 41.47/6.32 | vAType] : ! [v3: vOptAType] : ! [v4: vOptExp] : (v0 = 0 | ~ % 41.47/6.32 | (vreduceExp(ve1, v1) = v4) | ~ (vsomeAType(v2) = v3) | ~ % 41.47/6.32 | vAType(v2) | ~ vAnsMap(v1) | ? [v5: vATMap] : ? [v6: vOptAType] % 41.47/6.32 | : ( ~ (v6 = v3) & vecheck(v5, ve1) = v6 & vtypeAM(v1) = v5 & % 41.47/6.32 | vATMap(v5) & vOptAType(v6)) | ? [v5: vExp] : (vsomeExp(v5) = v4 % 41.47/6.32 | & vOptExp(v4) & vExp(v5)))) % 41.47/6.32 | % 41.47/6.32 | ALPHA: (reduceExpProgress-binop-IH1) implies: % 41.47/6.32 | (17) ? [v0: any] : (vexpIsValue(ve2) = v0 & ! [v1: vAnsMap] : ! [v2: % 41.47/6.32 | vAType] : ! [v3: vOptAType] : ! [v4: vOptExp] : (v0 = 0 | ~ % 41.47/6.32 | (vreduceExp(ve2, v1) = v4) | ~ (vsomeAType(v2) = v3) | ~ % 41.47/6.32 | vAType(v2) | ~ vAnsMap(v1) | ? [v5: vATMap] : ? [v6: vOptAType] % 41.47/6.32 | : ( ~ (v6 = v3) & vecheck(v5, ve2) = v6 & vtypeAM(v1) = v5 & % 41.47/6.32 | vATMap(v5) & vOptAType(v6)) | ? [v5: vExp] : (vsomeExp(v5) = v4 % 41.47/6.32 | & vOptExp(v4) & vExp(v5)))) % 41.47/6.32 | % 41.47/6.32 | ALPHA: (reduceExpProgress-binop-expIsValue-True-expIsValue-True) implies: % 41.47/6.32 | (18) vExp(ve1) % 41.47/6.32 | (19) vExp(ve2) % 41.47/6.33 | (20) ? [v0: any] : ? [v1: any] : (vexpIsValue(ve2) = v0 & % 41.47/6.33 | vexpIsValue(ve1) = v1 & ? [v2: vBinOpT] : ? [v3: vAnsMap] : ? % 41.47/6.33 | [v4: vAType] : ? [v5: vExp] : ? [v6: int] : ? [v7: vATMap] : ? % 41.47/6.33 | [v8: vOptAType] : ? [v9: vOptExp] : (v1 = 0 & v0 = 0 & ~ (v6 = 0) % 41.47/6.33 | & vecheck(v7, v5) = v8 & vtypeAM(v3) = v7 & vreduceExp(v5, v3) = % 41.47/6.33 | v9 & vexpIsValue(v5) = v6 & vsomeAType(v4) = v8 & vbinop(ve1, v2, % 41.47/6.33 | ve2) = v5 & vAType(v4) & vBinOpT(v2) & vOptExp(v9) & vExp(v5) & % 41.47/6.33 | vAnsMap(v3) & vATMap(v7) & vOptAType(v8) & ! [v10: vExp] : ( ~ % 41.47/6.33 | (vsomeExp(v10) = v9) | ~ vExp(v10)))) % 41.47/6.33 | % 41.47/6.33 | ALPHA: (function-axioms) implies: % 41.47/6.33 | (21) ! [v0: vAval] : ! [v1: vAval] : ! [v2: vYN] : (v1 = v0 | ~ (vB(v2) % 41.47/6.33 | = v1) | ~ (vB(v2) = v0)) % 41.47/6.33 | (22) ! [v0: vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ % 41.47/6.33 | (vgetExpValue(v2) = v1) | ~ (vgetExpValue(v2) = v0)) % 41.47/6.33 | (23) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 41.47/6.33 | vExp] : (v1 = v0 | ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = % 41.47/6.33 | v0)) % 41.47/6.33 | (24) ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vAval] % 41.47/6.33 | : ! [v4: vBinOpT] : (v1 = v0 | ~ (vevalBinOp(v4, v3, v2) = v1) | ~ % 41.47/6.33 | (vevalBinOp(v4, v3, v2) = v0)) % 41.47/6.33 | % 41.47/6.33 | DELTA: instantiating (7) with fresh symbols all_375_0, all_375_1, all_375_2 % 41.47/6.33 | gives: % 41.47/6.33 | (25) vsomeExp(all_375_1) = all_375_0 & vB(vyes) = all_375_2 & % 41.47/6.33 | vconstant(all_375_2) = all_375_1 & vOptExp(all_375_0) & % 41.47/6.33 | vExp(all_375_1) & vAval(all_375_2) & ! [v0: vAval] : ! [v1: int] : % 41.47/6.33 | (v1 = all_375_0 | ~ (vevalBinOp(veqop, v0, v0) = v1) | ~ vAval(v0)) % 41.47/6.33 | % 41.47/6.33 | ALPHA: (25) implies: % 41.47/6.33 | (26) vB(vyes) = all_375_2 % 41.47/6.33 | % 41.47/6.33 | DELTA: instantiating (16) with fresh symbol all_386_0 gives: % 41.47/6.33 | (27) vexpIsValue(ve1) = all_386_0 & ! [v0: vAnsMap] : ! [v1: vAType] : ! % 41.47/6.33 | [v2: vOptAType] : ! [v3: vOptExp] : (all_386_0 = 0 | ~ % 41.47/6.33 | (vreduceExp(ve1, v0) = v3) | ~ (vsomeAType(v1) = v2) | ~ % 41.47/6.33 | vAType(v1) | ~ vAnsMap(v0) | ? [v4: vATMap] : ? [v5: vOptAType] : % 41.47/6.33 | ( ~ (v5 = v2) & vecheck(v4, ve1) = v5 & vtypeAM(v0) = v4 & % 41.47/6.33 | vATMap(v4) & vOptAType(v5)) | ? [v4: vExp] : (vsomeExp(v4) = v3 & % 41.47/6.33 | vOptExp(v3) & vExp(v4))) % 41.47/6.33 | % 41.47/6.33 | ALPHA: (27) implies: % 41.47/6.33 | (28) vexpIsValue(ve1) = all_386_0 % 41.47/6.33 | % 41.47/6.33 | DELTA: instantiating (10) with fresh symbols all_392_0, all_392_1 gives: % 41.47/6.33 | (29) vB(vyes) = all_392_1 & vconstant(all_392_1) = all_392_0 & % 41.47/6.33 | vExp(all_392_0) & vAval(all_392_1) & ! [v0: vQuestionnaire] : ! [v1: % 41.47/6.33 | vQuestionnaire] : ! [v2: vAnsMap] : ! [v3: vQMap] : ! [v4: % 41.47/6.33 | vQuestionnaire] : ! [v5: vOptQConf] : ( ~ (vreduce(v4, v2, v3) = % 41.47/6.33 | v5) | ~ (vqcond(all_392_0, v0, v1) = v4) | ~ vQMap(v3) | ~ % 41.47/6.33 | vAnsMap(v2) | ~ vQuestionnaire(v1) | ~ vQuestionnaire(v0) | ? % 41.47/6.33 | [v6: vQConf] : (vQC(v2, v3, v0) = v6 & vsomeQConf(v6) = v5 & % 41.47/6.33 | vOptQConf(v5) & vQConf(v6))) % 41.47/6.33 | % 41.47/6.33 | ALPHA: (29) implies: % 41.47/6.33 | (30) vB(vyes) = all_392_1 % 41.47/6.33 | % 41.47/6.33 | DELTA: instantiating (17) with fresh symbol all_398_0 gives: % 41.47/6.33 | (31) vexpIsValue(ve2) = all_398_0 & ! [v0: vAnsMap] : ! [v1: vAType] : ! % 41.47/6.33 | [v2: vOptAType] : ! [v3: vOptExp] : (all_398_0 = 0 | ~ % 41.47/6.33 | (vreduceExp(ve2, v0) = v3) | ~ (vsomeAType(v1) = v2) | ~ % 41.47/6.33 | vAType(v1) | ~ vAnsMap(v0) | ? [v4: vATMap] : ? [v5: vOptAType] : % 41.47/6.33 | ( ~ (v5 = v2) & vecheck(v4, ve2) = v5 & vtypeAM(v0) = v4 & % 41.47/6.33 | vATMap(v4) & vOptAType(v5)) | ? [v4: vExp] : (vsomeExp(v4) = v3 & % 41.47/6.33 | vOptExp(v3) & vExp(v4))) % 41.47/6.33 | % 41.47/6.33 | ALPHA: (31) implies: % 41.47/6.33 | (32) vexpIsValue(ve2) = all_398_0 % 41.47/6.33 | % 41.47/6.33 | DELTA: instantiating (20) with fresh symbols all_403_0, all_403_1 gives: % 41.47/6.33 | (33) vexpIsValue(ve2) = all_403_1 & vexpIsValue(ve1) = all_403_0 & ? [v0: % 41.47/6.33 | vBinOpT] : ? [v1: vAnsMap] : ? [v2: vAType] : ? [v3: vExp] : ? % 41.47/6.33 | [v4: int] : ? [v5: vATMap] : ? [v6: vOptAType] : ? [v7: vOptExp] : % 41.47/6.33 | (all_403_0 = 0 & all_403_1 = 0 & ~ (v4 = 0) & vecheck(v5, v3) = v6 & % 41.47/6.33 | vtypeAM(v1) = v5 & vreduceExp(v3, v1) = v7 & vexpIsValue(v3) = v4 & % 41.47/6.33 | vsomeAType(v2) = v6 & vbinop(ve1, v0, ve2) = v3 & vAType(v2) & % 41.47/6.33 | vBinOpT(v0) & vOptExp(v7) & vExp(v3) & vAnsMap(v1) & vATMap(v5) & % 41.47/6.33 | vOptAType(v6) & ! [v8: vExp] : ( ~ (vsomeExp(v8) = v7) | ~ % 41.47/6.33 | vExp(v8))) % 41.47/6.33 | % 41.47/6.33 | ALPHA: (33) implies: % 41.47/6.33 | (34) vexpIsValue(ve1) = all_403_0 % 41.47/6.33 | (35) vexpIsValue(ve2) = all_403_1 % 41.47/6.34 | (36) ? [v0: vBinOpT] : ? [v1: vAnsMap] : ? [v2: vAType] : ? [v3: vExp] % 41.47/6.34 | : ? [v4: int] : ? [v5: vATMap] : ? [v6: vOptAType] : ? [v7: % 41.47/6.34 | vOptExp] : (all_403_0 = 0 & all_403_1 = 0 & ~ (v4 = 0) & % 41.47/6.34 | vecheck(v5, v3) = v6 & vtypeAM(v1) = v5 & vreduceExp(v3, v1) = v7 & % 41.47/6.34 | vexpIsValue(v3) = v4 & vsomeAType(v2) = v6 & vbinop(ve1, v0, ve2) = % 41.47/6.34 | v3 & vAType(v2) & vBinOpT(v0) & vOptExp(v7) & vExp(v3) & vAnsMap(v1) % 41.47/6.34 | & vATMap(v5) & vOptAType(v6) & ! [v8: vExp] : ( ~ (vsomeExp(v8) = % 41.47/6.34 | v7) | ~ vExp(v8))) % 41.47/6.34 | % 41.47/6.34 | DELTA: instantiating (12) with fresh symbols all_408_0, all_408_1, all_408_2, % 41.47/6.34 | all_408_3 gives: % 41.47/6.34 | (37) vB(vno) = all_408_1 & vB(vyes) = all_408_3 & vconstant(all_408_1) = % 41.47/6.34 | all_408_0 & vconstant(all_408_3) = all_408_2 & vExp(all_408_0) & % 41.47/6.34 | vExp(all_408_2) & vAval(all_408_1) & vAval(all_408_3) & ! [v0: vQMap] % 41.47/6.34 | : ! [v1: vQuestionnaire] : ! [v2: any] : ! [v3: vAnsMap] : ! [v4: % 41.47/6.34 | vQuestionnaire] : ! [v5: vQuestionnaire] : ! [v6: vOptQConf] : (v6 % 41.47/6.34 | = vnoQConf | v2 = all_408_0 | v2 = all_408_2 | ~ (vreduce(v5, v3, % 41.47/6.34 | v0) = v6) | ~ (vqcond(v2, v1, v4) = v5) | ~ vQMap(v0) | ~ % 41.47/6.34 | vExp(v2) | ~ vAnsMap(v3) | ~ vQuestionnaire(v4) | ~ % 41.47/6.34 | vQuestionnaire(v1) | ? [v7: vOptExp] : (vreduceExp(v2, v3) = v7 & % 41.47/6.34 | visSomeExp(v7) = 0 & vOptExp(v7))) % 41.47/6.34 | % 41.47/6.34 | ALPHA: (37) implies: % 41.47/6.34 | (38) vB(vyes) = all_408_3 % 41.47/6.34 | % 41.47/6.34 | DELTA: instantiating (11) with fresh symbols all_411_0, all_411_1, all_411_2, % 41.47/6.34 | all_411_3 gives: % 41.47/6.34 | (39) vB(vno) = all_411_1 & vB(vyes) = all_411_3 & vconstant(all_411_1) = % 41.47/6.34 | all_411_0 & vconstant(all_411_3) = all_411_2 & vExp(all_411_0) & % 41.47/6.34 | vExp(all_411_2) & vAval(all_411_1) & vAval(all_411_3) & ! [v0: vQMap] % 41.47/6.34 | : ! [v1: vQuestionnaire] : ! [v2: any] : ! [v3: vAnsMap] : ! [v4: % 41.47/6.34 | vQuestionnaire] : ! [v5: vOptExp] : ! [v6: vExp] : ! [v7: % 41.47/6.34 | vQuestionnaire] : ! [v8: vQConf] : (v2 = all_411_0 | v2 = all_411_2 % 41.47/6.34 | | ~ (vreduceExp(v2, v3) = v5) | ~ (vgetExp(v5) = v6) | ~ (vQC(v3, % 41.47/6.34 | v0, v7) = v8) | ~ (vqcond(v6, v1, v4) = v7) | ~ vQMap(v0) | ~ % 41.47/6.34 | vExp(v2) | ~ vAnsMap(v3) | ~ vQuestionnaire(v4) | ~ % 41.47/6.34 | vQuestionnaire(v1) | ? [v9: any] : ? [v10: vQuestionnaire] : ? % 41.47/6.34 | [v11: vOptQConf] : ? [v12: vOptQConf] : (vreduce(v10, v3, v0) = v11 % 41.47/6.34 | & visSomeExp(v5) = v9 & vsomeQConf(v8) = v12 & vqcond(v2, v1, v4) % 41.47/6.34 | = v10 & vOptQConf(v12) & vOptQConf(v11) & vQuestionnaire(v10) & ( % 41.47/6.34 | ~ (v9 = 0) | v12 = v11))) % 41.47/6.34 | % 41.47/6.34 | ALPHA: (39) implies: % 41.47/6.34 | (40) vB(vyes) = all_411_3 % 41.47/6.34 | % 41.47/6.34 | DELTA: instantiating (8) with fresh symbols all_420_0, all_420_1, all_420_2, % 41.47/6.34 | all_420_3, all_420_4, all_420_5 gives: % 41.47/6.35 | (41) vsomeExp(all_420_1) = all_420_0 & vsomeExp(all_420_4) = all_420_3 & % 41.47/6.35 | vB(vno) = all_420_2 & vB(vyes) = all_420_5 & vconstant(all_420_2) = % 41.47/6.35 | all_420_1 & vconstant(all_420_5) = all_420_4 & vOptExp(all_420_0) & % 41.47/6.35 | vOptExp(all_420_3) & vExp(all_420_1) & vExp(all_420_4) & % 41.47/6.35 | vAval(all_420_2) & vAval(all_420_5) & ! [v0: vBinOpT] : ! [v1: % 41.47/6.35 | vAval] : ! [v2: vAval] : ! [v3: vOptExp] : ( ~ (vevalBinOp(v0, v1, % 41.47/6.35 | v2) = v3) | ~ vBinOpT(v0) | ~ vAval(v2) | ~ vAval(v1) | ? % 41.47/6.35 | [v4: vnat] : ? [v5: vnat] : ? [v6: vYN] : ? [v7: vAval] : ? [v8: % 41.47/6.35 | vExp] : (v0 = vgtop & vgt(v4, v5) = v6 & vsomeExp(v8) = v3 & % 41.47/6.35 | vNum(v5) = v2 & vNum(v4) = v1 & vB(v6) = v7 & vconstant(v7) = v8 & % 41.47/6.35 | vOptExp(v3) & vnat(v5) & vnat(v4) & vExp(v8) & vAval(v7) & % 41.47/6.35 | vYN(v6)) | ? [v4: vnat] : ? [v5: vnat] : ? [v6: vYN] : ? [v7: % 41.47/6.35 | vAval] : ? [v8: vExp] : (v0 = vltop & vlt(v4, v5) = v6 & % 41.47/6.35 | vsomeExp(v8) = v3 & vNum(v5) = v2 & vNum(v4) = v1 & vB(v6) = v7 & % 41.47/6.35 | vconstant(v7) = v8 & vOptExp(v3) & vnat(v5) & vnat(v4) & vExp(v8) % 41.47/6.35 | & vAval(v7) & vYN(v6)) | ? [v4: vnat] : ? [v5: vnat] : ? [v6: % 41.47/6.35 | vnat] : ? [v7: vAval] : ? [v8: vExp] : (v0 = vaddop & vplus(v4, % 41.47/6.35 | v5) = v6 & vsomeExp(v8) = v3 & vNum(v6) = v7 & vNum(v5) = v2 & % 41.47/6.35 | vNum(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & vnat(v6) & % 41.47/6.35 | vnat(v5) & vnat(v4) & vExp(v8) & vAval(v7)) | ? [v4: vYN] : ? % 41.47/6.35 | [v5: vYN] : ? [v6: vYN] : ? [v7: vAval] : ? [v8: vExp] : (v0 = % 41.47/6.35 | vorop & vor(v4, v5) = v6 & vsomeExp(v8) = v3 & vB(v6) = v7 & % 41.47/6.35 | vB(v5) = v2 & vB(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & % 41.47/6.35 | vExp(v8) & vAval(v7) & vYN(v6) & vYN(v5) & vYN(v4)) | ? [v4: % 41.47/6.35 | vnat] : ? [v5: vnat] : ? [v6: vnat] : ? [v7: vAval] : ? [v8: % 41.47/6.35 | vExp] : (v0 = vmulop & vmultiply(v4, v5) = v6 & vsomeExp(v8) = v3 % 41.47/6.35 | & vNum(v6) = v7 & vNum(v5) = v2 & vNum(v4) = v1 & vconstant(v7) = % 41.47/6.35 | v8 & vOptExp(v3) & vnat(v6) & vnat(v5) & vnat(v4) & vExp(v8) & % 41.47/6.35 | vAval(v7)) | ? [v4: vnat] : ? [v5: vnat] : ? [v6: vnat] : ? % 41.47/6.35 | [v7: vAval] : ? [v8: vExp] : (v0 = vdivop & vdivide(v4, v5) = v6 & % 41.47/6.35 | vsomeExp(v8) = v3 & vNum(v6) = v7 & vNum(v5) = v2 & vNum(v4) = v1 % 41.47/6.35 | & vconstant(v7) = v8 & vOptExp(v3) & vnat(v6) & vnat(v5) & % 41.47/6.35 | vnat(v4) & vExp(v8) & vAval(v7)) | ? [v4: vYN] : ? [v5: vYN] : % 41.47/6.35 | ? [v6: vYN] : ? [v7: vAval] : ? [v8: vExp] : (v0 = vandop & % 41.47/6.35 | vand(v4, v5) = v6 & vsomeExp(v8) = v3 & vB(v6) = v7 & vB(v5) = v2 % 41.47/6.35 | & vB(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & vExp(v8) & % 41.47/6.35 | vAval(v7) & vYN(v6) & vYN(v5) & vYN(v4)) | ? [v4: vnat] : ? [v5: % 41.47/6.35 | vnat] : ? [v6: vnat] : ? [v7: vAval] : ? [v8: vExp] : (v0 = % 41.47/6.35 | vsubop & vminus(v4, v5) = v6 & vsomeExp(v8) = v3 & vNum(v6) = v7 & % 41.47/6.35 | vNum(v5) = v2 & vNum(v4) = v1 & vconstant(v7) = v8 & vOptExp(v3) & % 41.47/6.35 | vnat(v6) & vnat(v5) & vnat(v4) & vExp(v8) & vAval(v7)) | (v3 = % 41.47/6.35 | all_420_0 & v0 = veqop & ~ (v2 = v1)) | (v3 = all_420_3 & v2 = v1 % 41.47/6.35 | & v0 = veqop) | (v3 = vnoExp & ~ (v0 = veqop) & ( ~ (v0 = vorop) % 41.47/6.35 | | ! [v4: vYN] : ( ~ (vB(v4) = v2) | ~ vYN(v4)) | ! [v4: vYN] % 41.47/6.35 | : ( ~ (vB(v4) = v1) | ~ vYN(v4))) & ( ~ (v0 = vandop) | ! [v4: % 41.47/6.35 | vYN] : ( ~ (vB(v4) = v2) | ~ vYN(v4)) | ! [v4: vYN] : ( ~ % 41.47/6.35 | (vB(v4) = v1) | ~ vYN(v4))) & ( ! [v4: vnat] : ( ~ (vNum(v4) % 41.47/6.35 | = v2) | ~ vnat(v4)) | ! [v4: vnat] : ( ~ (vNum(v4) = v1) | % 41.47/6.35 | ~ vnat(v4)) | ( ~ (v0 = vgtop) & ~ (v0 = vltop) & ~ (v0 = % 41.47/6.35 | vaddop) & ~ (v0 = vmulop) & ~ (v0 = vdivop) & ~ (v0 = % 41.47/6.35 | vsubop))))) % 41.47/6.35 | % 41.47/6.35 | ALPHA: (41) implies: % 41.47/6.35 | (42) vB(vyes) = all_420_5 % 41.47/6.35 | % 41.47/6.35 | DELTA: instantiating (15) with fresh symbols all_423_0, all_423_1, all_423_2, % 41.47/6.35 | all_423_3 gives: % 41.47/6.35 | (43) vB(vno) = all_423_1 & vB(vyes) = all_423_3 & vconstant(all_423_1) = % 41.47/6.35 | all_423_0 & vconstant(all_423_3) = all_423_2 & vExp(all_423_0) & % 41.47/6.35 | vExp(all_423_2) & vAval(all_423_1) & vAval(all_423_3) & ! [v0: % 41.47/6.35 | vQuestionnaire] : ! [v1: vAnsMap] : ! [v2: vQMap] : ! [v3: % 41.47/6.35 | vOptQConf] : ( ~ (vreduce(v0, v1, v2) = v3) | ~ vQMap(v2) | ~ % 41.47/6.35 | vAnsMap(v1) | ~ vQuestionnaire(v0) | ? [v4: vAType] : ? [v5: % 41.47/6.35 | vOptExp] : ? [v6: vQID] : ? [v7: vExp] : ? [v8: int] : ? [v9: % 41.47/6.35 | vEntry] : ? [v10: vExp] : ? [v11: vEntry] : ? [v12: % 41.47/6.35 | vQuestionnaire] : ? [v13: vQConf] : ( ~ (v8 = 0) & vreduceExp(v7, % 41.47/6.35 | v1) = v5 & vexpIsValue(v7) = v8 & visSomeExp(v5) = 0 & % 41.47/6.35 | vgetExp(v5) = v10 & vQC(v1, v2, v12) = v13 & vsomeQConf(v13) = v3 % 41.47/6.35 | & vqsingle(v11) = v12 & vqsingle(v9) = v0 & vvalue(v6, v4, v10) = % 41.47/6.35 | v11 & vvalue(v6, v4, v7) = v9 & vAType(v4) & vOptExp(v5) & % 41.47/6.35 | vQID(v6) & vExp(v10) & vExp(v7) & vOptQConf(v3) & vQConf(v13) & % 41.47/6.35 | vQuestionnaire(v12) & vEntry(v11) & vEntry(v9)) | ? [v4: vQID] : % 41.47/6.36 | ? [v5: vOptQuestion] : ? [v6: vEntry] : ? [v7: vLabel] : ? [v8: % 41.47/6.36 | vAType] : ? [v9: vEntry] : ? [v10: vQuestionnaire] : ? [v11: % 41.47/6.36 | vQConf] : (vlookupQMap(v4, v2) = v5 & visSomeQuestion(v5) = 0 & % 41.47/6.36 | vgetQuestionAType(v5) = v8 & vgetQuestionLabel(v5) = v7 & vQC(v1, % 41.47/6.36 | v2, v10) = v11 & vsomeQConf(v11) = v3 & vqsingle(v9) = v10 & % 41.47/6.36 | vqsingle(v6) = v0 & vask(v4) = v6 & vquestion(v4, v7, v8) = v9 & % 41.47/6.36 | vAType(v8) & vLabel(v7) & vQID(v4) & vOptQuestion(v5) & % 41.47/6.36 | vOptQConf(v3) & vQConf(v11) & vQuestionnaire(v10) & vEntry(v9) & % 41.47/6.36 | vEntry(v6)) | ? [v4: vAType] : ? [v5: vOptExp] : ? [v6: vQID] : % 41.47/6.36 | ? [v7: vExp] : ? [v8: int] : ? [v9: int] : ? [v10: vEntry] : (v3 % 41.47/6.36 | = vnoQConf & ~ (v9 = 0) & ~ (v8 = 0) & vreduceExp(v7, v1) = v5 & % 41.47/6.36 | vexpIsValue(v7) = v8 & visSomeExp(v5) = v9 & vqsingle(v10) = v0 & % 41.47/6.36 | vvalue(v6, v4, v7) = v10 & vAType(v4) & vOptExp(v5) & vQID(v6) & % 41.47/6.36 | vExp(v7) & vEntry(v10)) | ? [v4: vOptExp] : ? [v5: % 41.47/6.36 | vQuestionnaire] : ? [v6: any] : ? [v7: vQuestionnaire] : ? [v8: % 41.47/6.36 | vExp] : ? [v9: vQuestionnaire] : ? [v10: vQConf] : ( ~ (v6 = % 41.47/6.36 | all_423_0) & ~ (v6 = all_423_2) & vreduceExp(v6, v1) = v4 & % 41.47/6.36 | visSomeExp(v4) = 0 & vgetExp(v4) = v8 & vQC(v1, v2, v9) = v10 & % 41.47/6.36 | vsomeQConf(v10) = v3 & vqcond(v8, v5, v7) = v9 & vqcond(v6, v5, % 41.47/6.36 | v7) = v0 & vOptExp(v4) & vExp(v8) & vExp(v6) & vOptQConf(v3) & % 41.47/6.36 | vQConf(v10) & vQuestionnaire(v9) & vQuestionnaire(v7) & % 41.47/6.36 | vQuestionnaire(v5)) | ? [v4: vAType] : ? [v5: vLabel] : ? [v6: % 41.47/6.36 | vAval] : ? [v7: vQID] : ? [v8: vEntry] : ? [v9: vAnsMap] : ? % 41.47/6.36 | [v10: vQConf] : (vgetAnswer(v5, v4) = v6 & vQC(v9, v2, vqempty) = % 41.47/6.36 | v10 & vabind(v7, v6, v1) = v9 & vsomeQConf(v10) = v3 & % 41.47/6.36 | vqsingle(v8) = v0 & vquestion(v7, v5, v4) = v8 & vAType(v4) & % 41.47/6.36 | vLabel(v5) & vQID(v7) & vAnsMap(v9) & vOptQConf(v3) & vAval(v6) & % 41.47/6.36 | vQConf(v10) & vEntry(v8)) | ? [v4: vAType] : ? [v5: vQID] : ? % 41.47/6.36 | [v6: vExp] : ? [v7: vEntry] : ? [v8: vAval] : ? [v9: vAnsMap] : % 41.47/6.36 | ? [v10: vQConf] : (vexpIsValue(v6) = 0 & vgetExpValue(v6) = v8 & % 41.47/6.36 | vQC(v9, v2, vqempty) = v10 & vabind(v5, v8, v1) = v9 & % 41.47/6.36 | vsomeQConf(v10) = v3 & vqsingle(v7) = v0 & vvalue(v5, v4, v6) = v7 % 41.47/6.36 | & vAType(v4) & vQID(v5) & vExp(v6) & vAnsMap(v9) & vOptQConf(v3) & % 41.47/6.36 | vAval(v8) & vQConf(v10) & vEntry(v7)) | ? [v4: vAType] : ? [v5: % 41.47/6.36 | vLabel] : ? [v6: vQID] : ? [v7: vEntry] : ? [v8: vQMap] : ? % 41.47/6.36 | [v9: vQConf] : (vQC(v1, v8, vqempty) = v9 & vsomeQConf(v9) = v3 & % 41.47/6.36 | vqsingle(v7) = v0 & vqmbind(v6, v5, v4, v2) = v8 & % 41.47/6.36 | vdefquestion(v6, v5, v4) = v7 & vAType(v4) & vLabel(v5) & vQID(v6) % 41.47/6.36 | & vQMap(v8) & vOptQConf(v3) & vQConf(v9) & vEntry(v7)) | ? [v4: % 41.47/6.36 | vOptExp] : ? [v5: vQuestionnaire] : ? [v6: any] : ? [v7: % 41.47/6.36 | vQuestionnaire] : ? [v8: int] : (v3 = vnoQConf & ~ (v8 = 0) & ~ % 41.47/6.36 | (v6 = all_423_0) & ~ (v6 = all_423_2) & vreduceExp(v6, v1) = v4 & % 41.47/6.36 | visSomeExp(v4) = v8 & vqcond(v6, v5, v7) = v0 & vOptExp(v4) & % 41.47/6.36 | vExp(v6) & vQuestionnaire(v7) & vQuestionnaire(v5)) | ? [v4: % 41.47/6.36 | vQuestionnaire] : ? [v5: vQuestionnaire] : ? [v6: vOptQConf] : % 41.47/6.36 | ? [v7: vQConf] : ? [v8: vQConf] : ( ~ (v4 = vqempty) & vreduce(v4, % 41.47/6.36 | v1, v2) = v6 & vqcappend(v7, v5) = v8 & visSomeQC(v6) = 0 & % 41.47/6.36 | vgetQC(v6) = v7 & vsomeQConf(v8) = v3 & vqseq(v4, v5) = v0 & % 41.47/6.36 | vOptQConf(v6) & vOptQConf(v3) & vQConf(v8) & vQConf(v7) & % 41.47/6.36 | vQuestionnaire(v5) & vQuestionnaire(v4)) | ? [v4: vQuestionnaire] % 41.47/6.36 | : ? [v5: vQuestionnaire] : ? [v6: vOptQConf] : ? [v7: int] : (v3 % 41.47/6.36 | = vnoQConf & ~ (v7 = 0) & ~ (v4 = vqempty) & vreduce(v4, v1, v2) % 41.47/6.36 | = v6 & visSomeQC(v6) = v7 & vqseq(v4, v5) = v0 & vOptQConf(v6) & % 41.47/6.36 | vQuestionnaire(v5) & vQuestionnaire(v4)) | ? [v4: vQID] : ? [v5: % 41.47/6.36 | vOptQuestion] : ? [v6: int] : ? [v7: vEntry] : (v3 = vnoQConf & % 41.47/6.36 | ~ (v6 = 0) & vlookupQMap(v4, v2) = v5 & visSomeQuestion(v5) = v6 & % 41.47/6.36 | vqsingle(v7) = v0 & vask(v4) = v7 & vQID(v4) & vOptQuestion(v5) & % 41.47/6.36 | vEntry(v7)) | ? [v4: vGID] : ? [v5: vQuestionnaire] : ? [v6: % 41.47/6.36 | vQConf] : (vQC(v1, v2, v5) = v6 & vsomeQConf(v6) = v3 & % 41.47/6.36 | vqgroup(v4, v5) = v0 & vGID(v4) & vOptQConf(v3) & vQConf(v6) & % 41.47/6.36 | vQuestionnaire(v5)) | ? [v4: vQuestionnaire] : ? [v5: % 41.47/6.36 | vQuestionnaire] : ? [v6: vQConf] : (vQC(v1, v2, v5) = v6 & % 41.47/6.36 | vsomeQConf(v6) = v3 & vqcond(all_423_0, v4, v5) = v0 & % 41.47/6.36 | vOptQConf(v3) & vQConf(v6) & vQuestionnaire(v5) & % 41.47/6.36 | vQuestionnaire(v4)) | ? [v4: vQuestionnaire] : ? [v5: % 41.47/6.36 | vQuestionnaire] : ? [v6: vQConf] : (vQC(v1, v2, v4) = v6 & % 41.47/6.36 | vsomeQConf(v6) = v3 & vqcond(all_423_2, v4, v5) = v0 & % 41.47/6.36 | vOptQConf(v3) & vQConf(v6) & vQuestionnaire(v5) & % 41.47/6.36 | vQuestionnaire(v4)) | ? [v4: vQuestionnaire] : ? [v5: vQConf] : % 41.47/6.36 | (vQC(v1, v2, v4) = v5 & vsomeQConf(v5) = v3 & vqseq(vqempty, v4) = % 41.47/6.36 | v0 & vOptQConf(v3) & vQConf(v5) & vQuestionnaire(v4)) | (v3 = % 41.47/6.36 | vnoQConf & v0 = vqempty)) % 41.47/6.36 | % 41.47/6.36 | ALPHA: (43) implies: % 41.47/6.36 | (44) vB(vyes) = all_423_3 % 41.47/6.36 | % 41.47/6.36 | DELTA: instantiating (36) with fresh symbols all_426_0, all_426_1, all_426_2, % 41.47/6.36 | all_426_3, all_426_4, all_426_5, all_426_6, all_426_7 gives: % 41.47/6.36 | (45) all_403_0 = 0 & all_403_1 = 0 & ~ (all_426_3 = 0) & % 41.47/6.36 | vecheck(all_426_2, all_426_4) = all_426_1 & vtypeAM(all_426_6) = % 41.47/6.36 | all_426_2 & vreduceExp(all_426_4, all_426_6) = all_426_0 & % 41.47/6.36 | vexpIsValue(all_426_4) = all_426_3 & vsomeAType(all_426_5) = all_426_1 % 41.47/6.36 | & vbinop(ve1, all_426_7, ve2) = all_426_4 & vAType(all_426_5) & % 41.47/6.36 | vBinOpT(all_426_7) & vOptExp(all_426_0) & vExp(all_426_4) & % 41.47/6.36 | vAnsMap(all_426_6) & vATMap(all_426_2) & vOptAType(all_426_1) & ! % 41.47/6.36 | [v0: vExp] : ( ~ (vsomeExp(v0) = all_426_0) | ~ vExp(v0)) % 41.47/6.36 | % 41.47/6.36 | ALPHA: (45) implies: % 41.47/6.36 | (46) all_403_1 = 0 % 41.47/6.36 | (47) all_403_0 = 0 % 41.47/6.36 | (48) vATMap(all_426_2) % 41.47/6.36 | (49) vAnsMap(all_426_6) % 41.47/6.36 | (50) vBinOpT(all_426_7) % 41.47/6.36 | (51) vAType(all_426_5) % 41.47/6.36 | (52) vbinop(ve1, all_426_7, ve2) = all_426_4 % 41.47/6.36 | (53) vsomeAType(all_426_5) = all_426_1 % 41.47/6.36 | (54) vreduceExp(all_426_4, all_426_6) = all_426_0 % 41.47/6.36 | (55) vecheck(all_426_2, all_426_4) = all_426_1 % 41.47/6.36 | (56) ! [v0: vExp] : ( ~ (vsomeExp(v0) = all_426_0) | ~ vExp(v0)) % 41.47/6.36 | % 41.47/6.36 | REDUCE: (35), (46) imply: % 41.47/6.36 | (57) vexpIsValue(ve2) = 0 % 41.47/6.36 | % 41.47/6.36 | REDUCE: (34), (47) imply: % 41.47/6.36 | (58) vexpIsValue(ve1) = 0 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (21) with all_411_3, all_420_5, vyes, simplifying % 41.47/6.36 | with (40), (42) gives: % 41.47/6.36 | (59) all_420_5 = all_411_3 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (21) with all_408_3, all_420_5, vyes, simplifying % 41.47/6.36 | with (38), (42) gives: % 41.47/6.36 | (60) all_420_5 = all_408_3 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (21) with all_392_1, all_420_5, vyes, simplifying % 41.47/6.36 | with (30), (42) gives: % 41.47/6.36 | (61) all_420_5 = all_392_1 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (21) with all_411_3, all_423_3, vyes, simplifying % 41.47/6.36 | with (40), (44) gives: % 41.47/6.36 | (62) all_423_3 = all_411_3 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (21) with all_375_2, all_423_3, vyes, simplifying % 41.47/6.36 | with (26), (44) gives: % 41.47/6.36 | (63) all_423_3 = all_375_2 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (23) with 0, all_386_0, ve1, simplifying with (28), % 41.47/6.36 | (58) gives: % 41.47/6.36 | (64) all_386_0 = 0 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (23) with 0, all_398_0, ve2, simplifying with (32), % 41.47/6.36 | (57) gives: % 41.47/6.36 | (65) all_398_0 = 0 % 41.47/6.36 | % 41.47/6.36 | COMBINE_EQS: (62), (63) imply: % 41.47/6.36 | (66) all_411_3 = all_375_2 % 41.47/6.36 | % 41.47/6.36 | SIMP: (66) implies: % 41.47/6.36 | (67) all_411_3 = all_375_2 % 41.47/6.36 | % 41.47/6.36 | COMBINE_EQS: (60), (61) imply: % 41.47/6.36 | (68) all_408_3 = all_392_1 % 41.47/6.36 | % 41.47/6.36 | COMBINE_EQS: (59), (60) imply: % 41.47/6.36 | (69) all_411_3 = all_408_3 % 41.47/6.36 | % 41.47/6.36 | SIMP: (69) implies: % 41.47/6.36 | (70) all_411_3 = all_408_3 % 41.47/6.36 | % 41.47/6.36 | COMBINE_EQS: (67), (70) imply: % 41.47/6.36 | (71) all_408_3 = all_375_2 % 41.47/6.36 | % 41.47/6.36 | SIMP: (71) implies: % 41.47/6.36 | (72) all_408_3 = all_375_2 % 41.47/6.36 | % 41.47/6.36 | COMBINE_EQS: (68), (72) imply: % 41.47/6.36 | (73) all_392_1 = all_375_2 % 41.47/6.36 | % 41.47/6.36 | SIMP: (73) implies: % 41.47/6.36 | (74) all_392_1 = all_375_2 % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (5) with vyes, all_375_2, simplifying with (13), % 41.47/6.36 | (26) gives: % 41.47/6.36 | (75) vtypeOf(all_375_2) = vYesNo % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (9) with vyes, vno, simplifying with (3), (13) % 41.47/6.36 | gives: % 41.47/6.36 | (76) ? [v0: vAval] : ? [v1: vOptExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.47/6.36 | (vevalUnOp(vnotop, v0) = v1 & vsomeExp(v3) = v1 & vB(vno) = v2 & % 41.47/6.36 | vB(vyes) = v0 & vconstant(v2) = v3 & vOptExp(v1) & vExp(v3) & % 41.47/6.36 | vAval(v2) & vAval(v0)) % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (9) with vno, vyes, simplifying with (4), (14) % 41.47/6.36 | gives: % 41.47/6.36 | (77) ? [v0: vAval] : ? [v1: vOptExp] : ? [v2: vAval] : ? [v3: vExp] : % 41.47/6.36 | (vevalUnOp(vnotop, v0) = v1 & vsomeExp(v3) = v1 & vB(vno) = v0 & % 41.47/6.36 | vB(vyes) = v2 & vconstant(v2) = v3 & vOptExp(v1) & vExp(v3) & % 41.47/6.36 | vAval(v2) & vAval(v0)) % 41.47/6.36 | % 41.47/6.36 | GROUND_INST: instantiating (expIsValue-true-INV) with ve1, simplifying with % 41.47/6.36 | (18), (58) gives: % 41.47/6.37 | (78) ? [v0: vAval] : (vconstant(v0) = ve1 & vAval(v0)) % 41.47/6.37 | % 41.47/6.37 | GROUND_INST: instantiating (expIsValue-true-INV) with ve2, simplifying with % 41.47/6.37 | (19), (57) gives: % 41.47/6.37 | (79) ? [v0: vAval] : (vconstant(v0) = ve2 & vAval(v0)) % 41.47/6.37 | % 41.47/6.37 | GROUND_INST: instantiating (reduceExp-3) with ve1, ve2, all_426_7, all_426_6, % 41.47/6.37 | all_426_4, all_426_0, simplifying with (18), (19), (49), (50), % 41.47/6.37 | (52), (54) gives: % 41.47/6.37 | (80) ? [v0: any] : ? [v1: any] : ? [v2: vAval] : ? [v3: vAval] : ? % 41.47/6.37 | [v4: vOptExp] : (vevalBinOp(all_426_7, v2, v3) = v4 & vexpIsValue(ve2) % 41.47/6.37 | = v1 & vexpIsValue(ve1) = v0 & vgetExpValue(ve2) = v3 & % 41.47/6.37 | vgetExpValue(ve1) = v2 & vOptExp(v4) & vAval(v3) & vAval(v2) & ( ~ % 41.47/6.37 | (v1 = 0) | ~ (v0 = 0) | v4 = all_426_0)) % 41.47/6.37 | % 41.47/6.37 | DELTA: instantiating (79) with fresh symbol all_447_0 gives: % 41.47/6.37 | (81) vconstant(all_447_0) = ve2 & vAval(all_447_0) % 41.47/6.37 | % 41.47/6.37 | ALPHA: (81) implies: % 41.47/6.37 | (82) vAval(all_447_0) % 41.47/6.37 | (83) vconstant(all_447_0) = ve2 % 41.47/6.37 | % 41.47/6.37 | DELTA: instantiating (78) with fresh symbol all_449_0 gives: % 41.47/6.37 | (84) vconstant(all_449_0) = ve1 & vAval(all_449_0) % 41.47/6.37 | % 41.47/6.37 | ALPHA: (84) implies: % 41.47/6.37 | (85) vAval(all_449_0) % 41.47/6.37 | (86) vconstant(all_449_0) = ve1 % 41.47/6.37 | % 41.47/6.37 | DELTA: instantiating (77) with fresh symbols all_451_0, all_451_1, all_451_2, % 41.47/6.37 | all_451_3 gives: % 41.47/6.37 | (87) vevalUnOp(vnotop, all_451_3) = all_451_2 & vsomeExp(all_451_0) = % 41.47/6.37 | all_451_2 & vB(vno) = all_451_3 & vB(vyes) = all_451_1 & % 41.47/6.37 | vconstant(all_451_1) = all_451_0 & vOptExp(all_451_2) & % 41.47/6.37 | vExp(all_451_0) & vAval(all_451_1) & vAval(all_451_3) % 41.47/6.37 | % 41.47/6.37 | ALPHA: (87) implies: % 41.47/6.37 | (88) vAval(all_451_1) % 41.47/6.37 | (89) vB(vyes) = all_451_1 % 41.47/6.37 | % 41.47/6.37 | DELTA: instantiating (76) with fresh symbols all_453_0, all_453_1, all_453_2, % 41.47/6.37 | all_453_3 gives: % 41.47/6.37 | (90) vevalUnOp(vnotop, all_453_3) = all_453_2 & vsomeExp(all_453_0) = % 41.47/6.37 | all_453_2 & vB(vno) = all_453_1 & vB(vyes) = all_453_3 & % 41.47/6.37 | vconstant(all_453_1) = all_453_0 & vOptExp(all_453_2) & % 41.47/6.37 | vExp(all_453_0) & vAval(all_453_1) & vAval(all_453_3) % 41.47/6.37 | % 41.47/6.37 | ALPHA: (90) implies: % 41.47/6.37 | (91) vB(vyes) = all_453_3 % 41.47/6.37 | % 41.47/6.37 | DELTA: instantiating (80) with fresh symbols all_455_0, all_455_1, all_455_2, % 41.47/6.37 | all_455_3, all_455_4 gives: % 41.47/6.37 | (92) vevalBinOp(all_426_7, all_455_2, all_455_1) = all_455_0 & % 41.47/6.37 | vexpIsValue(ve2) = all_455_3 & vexpIsValue(ve1) = all_455_4 & % 41.47/6.37 | vgetExpValue(ve2) = all_455_1 & vgetExpValue(ve1) = all_455_2 & % 41.47/6.37 | vOptExp(all_455_0) & vAval(all_455_1) & vAval(all_455_2) & ( ~ % 41.47/6.37 | (all_455_3 = 0) | ~ (all_455_4 = 0) | all_455_0 = all_426_0) % 41.47/6.37 | % 41.47/6.37 | ALPHA: (92) implies: % 41.47/6.37 | (93) vgetExpValue(ve1) = all_455_2 % 41.47/6.37 | (94) vgetExpValue(ve2) = all_455_1 % 41.47/6.37 | (95) vexpIsValue(ve1) = all_455_4 % 41.47/6.37 | (96) vexpIsValue(ve2) = all_455_3 % 41.47/6.37 | (97) vevalBinOp(all_426_7, all_455_2, all_455_1) = all_455_0 % 41.47/6.37 | (98) ~ (all_455_3 = 0) | ~ (all_455_4 = 0) | all_455_0 = all_426_0 % 41.47/6.37 | % 41.47/6.37 | GROUND_INST: instantiating (21) with all_375_2, all_453_3, vyes, simplifying % 41.47/6.37 | with (26), (91) gives: % 41.47/6.37 | (99) all_453_3 = all_375_2 % 41.47/6.37 | % 41.47/6.37 | GROUND_INST: instantiating (21) with all_451_1, all_453_3, vyes, simplifying % 41.47/6.37 | with (89), (91) gives: % 41.47/6.37 | (100) all_453_3 = all_451_1 % 41.47/6.37 | % 41.47/6.37 | GROUND_INST: instantiating (23) with 0, all_455_4, ve1, simplifying with (58), % 41.47/6.37 | (95) gives: % 41.47/6.37 | (101) all_455_4 = 0 % 41.47/6.37 | % 41.47/6.37 | GROUND_INST: instantiating (23) with 0, all_455_3, ve2, simplifying with (57), % 41.47/6.37 | (96) gives: % 41.47/6.37 | (102) all_455_3 = 0 % 41.47/6.37 | % 41.47/6.37 | COMBINE_EQS: (99), (100) imply: % 41.47/6.37 | (103) all_451_1 = all_375_2 % 41.47/6.37 | % 41.47/6.37 | REDUCE: (88), (103) imply: % 41.47/6.37 | (104) vAval(all_375_2) % 41.47/6.37 | % 41.47/6.37 | BETA: splitting (98) gives: % 41.47/6.37 | % 41.47/6.37 | Case 1: % 41.47/6.37 | | % 41.47/6.37 | | (105) ~ (all_455_3 = 0) % 41.47/6.37 | | % 41.47/6.37 | | REDUCE: (102), (105) imply: % 41.47/6.37 | | (106) $false % 41.47/6.37 | | % 41.47/6.37 | | CLOSE: (106) is inconsistent. % 41.47/6.37 | | % 41.47/6.37 | Case 2: % 41.47/6.37 | | % 41.47/6.37 | | (107) ~ (all_455_4 = 0) | all_455_0 = all_426_0 % 41.47/6.37 | | % 41.47/6.37 | | BETA: splitting (107) gives: % 41.47/6.37 | | % 41.47/6.37 | | Case 1: % 41.47/6.37 | | | % 41.47/6.37 | | | (108) ~ (all_455_4 = 0) % 41.47/6.37 | | | % 41.47/6.37 | | | REDUCE: (101), (108) imply: % 41.47/6.37 | | | (109) $false % 41.47/6.37 | | | % 41.47/6.37 | | | CLOSE: (109) is inconsistent. % 41.47/6.37 | | | % 41.47/6.37 | | Case 2: % 41.47/6.37 | | | % 41.47/6.37 | | | (110) all_455_0 = all_426_0 % 41.47/6.37 | | | % 41.47/6.37 | | | REDUCE: (97), (110) imply: % 41.47/6.37 | | | (111) vevalBinOp(all_426_7, all_455_2, all_455_1) = all_426_0 % 41.47/6.37 | | | % 41.47/6.37 | | | GROUND_INST: instantiating (getExpValue-0) with all_447_0, ve2, % 41.47/6.37 | | | simplifying with (82), (83) gives: % 41.47/6.37 | | | (112) vgetExpValue(ve2) = all_447_0 % 41.47/6.37 | | | % 41.47/6.37 | | | GROUND_INST: instantiating (evalBinOpProgress) with all_426_7, all_449_0, % 41.47/6.37 | | | all_426_2, all_447_0, all_426_5, ve1, ve2, all_426_4, % 41.47/6.37 | | | all_426_1, simplifying with (48), (50), (51), (52), (53), % 41.47/6.37 | | | (55), (82), (83), (85), (86) gives: % 41.47/6.38 | | | (113) ? [v0: vOptExp] : (vevalBinOp(all_426_7, all_449_0, all_447_0) = % 41.47/6.38 | | | v0 & vOptExp(v0) & ? [v1: vExp] : (vsomeExp(v1) = v0 & % 41.47/6.38 | | | vExp(v1))) % 41.47/6.38 | | | % 41.47/6.38 | | | GROUND_INST: instantiating (getExpValue-0) with all_449_0, ve1, % 41.47/6.38 | | | simplifying with (85), (86) gives: % 41.47/6.38 | | | (114) vgetExpValue(ve1) = all_449_0 % 41.47/6.38 | | | % 41.47/6.38 | | | GROUND_INST: instantiating (6) with all_375_2, vYesNo, simplifying with % 41.47/6.38 | | | (75), (104) gives: % 41.47/6.38 | | | (115) ? [v0: vstring] : (vText = vYesNo & vT(v0) = all_375_2 & % 41.47/6.38 | | | vstring(v0)) | ? [v0: vnat] : (vYesNo = vNumber & vNum(v0) = % 41.47/6.38 | | | all_375_2 & vnat(v0)) | ? [v0: vYN] : (vB(v0) = all_375_2 & % 41.47/6.38 | | | vYN(v0)) % 41.47/6.38 | | | % 41.47/6.38 | | | DELTA: instantiating (113) with fresh symbol all_516_0 gives: % 41.47/6.38 | | | (116) vevalBinOp(all_426_7, all_449_0, all_447_0) = all_516_0 & % 41.47/6.38 | | | vOptExp(all_516_0) & ? [v0: vExp] : (vsomeExp(v0) = all_516_0 & % 41.47/6.38 | | | vExp(v0)) % 41.47/6.38 | | | % 41.47/6.38 | | | ALPHA: (116) implies: % 41.47/6.38 | | | (117) vevalBinOp(all_426_7, all_449_0, all_447_0) = all_516_0 % 41.47/6.38 | | | (118) ? [v0: vExp] : (vsomeExp(v0) = all_516_0 & vExp(v0)) % 41.47/6.38 | | | % 41.47/6.38 | | | DELTA: instantiating (118) with fresh symbol all_518_0 gives: % 41.47/6.38 | | | (119) vsomeExp(all_518_0) = all_516_0 & vExp(all_518_0) % 41.47/6.38 | | | % 41.47/6.38 | | | ALPHA: (119) implies: % 41.47/6.38 | | | (120) vExp(all_518_0) % 41.47/6.38 | | | (121) vsomeExp(all_518_0) = all_516_0 % 41.47/6.38 | | | % 41.47/6.38 | | | BETA: splitting (115) gives: % 41.47/6.38 | | | % 41.47/6.38 | | | Case 1: % 41.47/6.38 | | | | % 41.47/6.38 | | | | (122) ? [v0: vstring] : (vText = vYesNo & vT(v0) = all_375_2 & % 41.47/6.38 | | | | vstring(v0)) % 41.47/6.38 | | | | % 41.47/6.38 | | | | DELTA: instantiating (122) with fresh symbol all_523_0 gives: % 41.47/6.38 | | | | (123) vText = vYesNo & vT(all_523_0) = all_375_2 & vstring(all_523_0) % 41.47/6.38 | | | | % 41.47/6.38 | | | | ALPHA: (123) implies: % 41.47/6.38 | | | | (124) vText = vYesNo % 41.47/6.38 | | | | % 41.47/6.38 | | | | REDUCE: (2), (124) imply: % 41.47/6.38 | | | | (125) $false % 41.47/6.38 | | | | % 41.47/6.38 | | | | CLOSE: (125) is inconsistent. % 41.47/6.38 | | | | % 41.47/6.38 | | | Case 2: % 41.47/6.38 | | | | % 41.47/6.38 | | | | (126) ? [v0: vnat] : (vYesNo = vNumber & vNum(v0) = all_375_2 & % 41.47/6.38 | | | | vnat(v0)) | ? [v0: vYN] : (vB(v0) = all_375_2 & vYN(v0)) % 41.47/6.38 | | | | % 41.47/6.38 | | | | BETA: splitting (126) gives: % 41.47/6.38 | | | | % 41.47/6.38 | | | | Case 1: % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | (127) ? [v0: vnat] : (vYesNo = vNumber & vNum(v0) = all_375_2 & % 41.47/6.38 | | | | | vnat(v0)) % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | DELTA: instantiating (127) with fresh symbol all_523_0 gives: % 41.47/6.38 | | | | | (128) vYesNo = vNumber & vNum(all_523_0) = all_375_2 & % 41.47/6.38 | | | | | vnat(all_523_0) % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | ALPHA: (128) implies: % 41.47/6.38 | | | | | (129) vYesNo = vNumber % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | REDUCE: (1), (129) imply: % 41.47/6.38 | | | | | (130) $false % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | CLOSE: (130) is inconsistent. % 41.47/6.38 | | | | | % 41.47/6.38 | | | | Case 2: % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | GROUND_INST: instantiating (22) with all_455_2, all_449_0, ve1, % 41.47/6.38 | | | | | simplifying with (93), (114) gives: % 41.47/6.38 | | | | | (131) all_455_2 = all_449_0 % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | GROUND_INST: instantiating (22) with all_455_1, all_447_0, ve2, % 41.47/6.38 | | | | | simplifying with (94), (112) gives: % 41.47/6.38 | | | | | (132) all_455_1 = all_447_0 % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | REDUCE: (111), (131), (132) imply: % 41.47/6.38 | | | | | (133) vevalBinOp(all_426_7, all_449_0, all_447_0) = all_426_0 % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | GROUND_INST: instantiating (24) with all_516_0, all_426_0, all_447_0, % 41.47/6.38 | | | | | all_449_0, all_426_7, simplifying with (117), (133) % 41.47/6.38 | | | | | gives: % 41.47/6.38 | | | | | (134) all_516_0 = all_426_0 % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | REDUCE: (121), (134) imply: % 41.47/6.38 | | | | | (135) vsomeExp(all_518_0) = all_426_0 % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | GROUND_INST: instantiating (56) with all_518_0, simplifying with % 41.47/6.38 | | | | | (120), (135) gives: % 41.47/6.38 | | | | | (136) $false % 41.47/6.38 | | | | | % 41.47/6.38 | | | | | CLOSE: (136) is inconsistent. % 41.47/6.38 | | | | | % 41.47/6.38 | | | | End of split % 41.47/6.38 | | | | % 41.47/6.38 | | | End of split % 41.47/6.38 | | | % 41.47/6.38 | | End of split % 41.47/6.38 | | % 41.47/6.38 | End of split % 41.47/6.38 | % 41.47/6.38 End of proof % 41.47/6.38 % SZS output end Proof for theBenchmark % 41.47/6.38 % 41.47/6.38 5716ms %------------------------------------------------------------------------------