%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM219_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 : n004.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:35 PM UTC 2026 % Result : Theorem 16.56s 2.91s % Output : Proof 28.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM219_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.33 % Computer : n004.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 4 19:01:47 EDT 2026 % 0.15/0.33 % CPUTime : % 0.66/0.63 ________ _____ % 0.66/0.63 ___ __ \_________(_)________________________________ % 0.66/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.66/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.66/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.66/0.63 % 0.66/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.66/0.63 (2023-06-19) % 0.66/0.63 % 0.66/0.63 (c) Philipp Rümmer, 2009-2023 % 0.66/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.66/0.63 Amanda Stjerna. % 0.66/0.63 Free software under BSD-3-Clause. % 0.66/0.63 % 0.66/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.66/0.63 % 0.66/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.66/0.65 Running up to 7 provers in parallel. % 0.66/0.67 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.66/0.67 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.66/0.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.66/0.67 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.66/0.67 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.66/0.67 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.66/0.67 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.90/1.52 Prover 1: Preprocessing ... % 5.90/1.52 Prover 4: Preprocessing ... % 5.90/1.55 Prover 3: Preprocessing ... % 5.90/1.55 Prover 5: Preprocessing ... % 5.90/1.55 Prover 2: Preprocessing ... % 5.90/1.55 Prover 6: Preprocessing ... % 5.90/1.55 Prover 0: Preprocessing ... % 12.69/2.45 Prover 1: Warning: ignoring some quantifiers % 12.69/2.46 Prover 3: Warning: ignoring some quantifiers % 13.47/2.50 Prover 3: Constructing countermodel ... % 13.47/2.50 Prover 1: Constructing countermodel ... % 13.47/2.53 Prover 6: Proving ... % 14.23/2.62 Prover 5: Proving ... % 14.23/2.66 Prover 4: Warning: ignoring some quantifiers % 15.01/2.75 Prover 4: Constructing countermodel ... % 15.01/2.78 Prover 0: Proving ... % 16.56/2.91 Prover 3: proved (2246ms) % 16.56/2.91 % 16.56/2.91 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.56/2.91 % 16.56/2.91 Prover 2: Proving ... % 16.56/2.91 Prover 6: stopped % 16.56/2.92 Prover 2: stopped % 16.56/2.93 Prover 0: stopped % 16.56/2.94 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 16.56/2.94 Prover 5: stopped % 16.56/2.94 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.56/2.94 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 16.56/2.94 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 16.56/2.95 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 18.79/3.24 Prover 11: Preprocessing ... % 18.79/3.24 Prover 13: Preprocessing ... % 18.79/3.25 Prover 8: Preprocessing ... % 18.79/3.27 Prover 10: Preprocessing ... % 18.79/3.27 Prover 7: Preprocessing ... % 21.12/3.50 Prover 8: Warning: ignoring some quantifiers % 21.12/3.53 Prover 8: Constructing countermodel ... % 21.90/3.62 Prover 7: Warning: ignoring some quantifiers % 21.90/3.62 Prover 10: Warning: ignoring some quantifiers % 21.90/3.64 Prover 10: Constructing countermodel ... % 21.90/3.66 Prover 7: Constructing countermodel ... % 21.90/3.69 Prover 13: Warning: ignoring some quantifiers % 22.70/3.70 Prover 11: Warning: ignoring some quantifiers % 22.70/3.71 Prover 13: Constructing countermodel ... % 22.70/3.72 Prover 11: Constructing countermodel ... % 27.38/4.33 Prover 4: Found proof (size 299) % 27.38/4.33 Prover 4: proved (3670ms) % 27.38/4.33 Prover 1: stopped % 27.38/4.33 Prover 7: stopped % 27.38/4.33 Prover 11: stopped % 27.38/4.33 Prover 13: stopped % 27.38/4.33 Prover 8: stopped % 27.38/4.33 Prover 10: stopped % 27.38/4.33 % 27.38/4.33 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.38/4.33 % 27.38/4.38 % SZS output start Proof for theBenchmark % 27.38/4.38 Assumptions after simplification: % 27.38/4.38 --------------------------------- % 27.38/4.38 % 27.38/4.38 (Preservation-Iszero-IH0) % 27.91/4.41 vTerm(vt1) & ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: % 27.91/4.41 vTy] : ! [v2: vTerm] : ! [v3: int] : (v3 = 0 | ~ (vptchecksimple(v2, % 27.91/4.41 v1) = v3) | ~ vTy(v1) | ~ vTerm(v2) | ? [v4: any] : ? [v5: % 27.91/4.41 vOptTerm] : (vptchecksimple(vt1, v1) = v4 & vsomeTerm(v2) = v5 & % 27.91/4.41 vOptTerm(v5) & ( ~ (v5 = v0) | ~ (v4 = 0))))) % 27.91/4.41 % 27.91/4.41 (Preservation-Iszero-Succ-isNV-False) % 27.91/4.41 vTerm(vt1) & vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: % 27.91/4.41 vTerm] : ? [v3: vTy] : ? [v4: vTerm] : ? [v5: int] : ? [v6: int] : ( ~ % 27.91/4.41 (v6 = 0) & ~ (v5 = 0) & ~ (vt1 = vZero) & vptchecksimple(v4, v3) = v6 & % 27.91/4.41 vptchecksimple(v0, v3) = 0 & vreduce(v0) = v1 & visNV(v2) = v5 & % 27.91/4.41 vsomeTerm(v4) = v1 & vIszero(vt1) = v0 & vSucc(v2) = vt1 & vTy(v3) & % 27.91/4.41 vOptTerm(v1) & vTerm(v4) & vTerm(v2) & vTerm(v0)) % 27.91/4.41 % 27.91/4.41 (Preservation-Iszero-Succ-isNV-False-isSomeTerm-False) % 27.91/4.42 vTerm(vt1) & vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) % 27.91/4.42 = v1 & vIszero(vt1) = v0 & vOptTerm(v1) & vTerm(v0) & ! [v2: vTerm] : ! % 27.91/4.42 [v3: vTy] : ! [v4: vTerm] : ! [v5: vOptTerm] : ! [v6: int] : ! [v7: int] % 27.91/4.42 : (v7 = 0 | v6 = 0 | vt1 = vZero | ~ (vptchecksimple(v4, v3) = v7) | ~ % 27.91/4.42 (vreduce(vt1) = v5) | ~ (visSomeTerm(v5) = v6) | ~ (vSucc(v2) = vt1) | % 27.91/4.42 ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v8: any] : ? [v9: any] : ? % 27.91/4.42 [v10: vOptTerm] : (vptchecksimple(v0, v3) = v9 & visNV(v2) = v8 & % 27.91/4.42 vsomeTerm(v4) = v10 & vOptTerm(v10) & ( ~ (v10 = v1) | ~ (v9 = 0) | v8 % 27.91/4.42 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] : ! [v5: int] % 27.91/4.42 : ! [v6: int] : (v6 = 0 | v5 = 0 | vt1 = vZero | ~ (vptchecksimple(v4, v3) % 27.91/4.42 = v6) | ~ (visNV(v2) = v5) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | % 27.91/4.42 ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: any] : ? [v10: any] : ? % 27.91/4.42 [v11: vOptTerm] : (vptchecksimple(v0, v3) = v10 & vreduce(v7) = v8 & % 27.91/4.42 visSomeTerm(v8) = v9 & vsomeTerm(v4) = v11 & vSucc(v2) = v7 & % 27.91/4.42 vOptTerm(v11) & vOptTerm(v8) & vTerm(v7) & ( ~ (v11 = v1) | ~ (v10 = 0) % 27.91/4.42 | ~ (v7 = vt1) | v9 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: % 27.91/4.42 vTerm] : ! [v5: vOptTerm] : ! [v6: int] : (v6 = 0 | vt1 = vZero | ~ % 27.91/4.42 (vptchecksimple(v0, v3) = 0) | ~ (vreduce(vt1) = v5) | ~ % 27.91/4.42 (visSomeTerm(v5) = v6) | ~ (vsomeTerm(v4) = v1) | ~ (vSucc(v2) = vt1) | % 27.91/4.42 ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v7: any] : ? [v8: any] : % 27.91/4.42 (vptchecksimple(v4, v3) = v8 & visNV(v2) = v7 & (v8 = 0 | v7 = 0))) & ! % 27.91/4.42 [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] : ! [v5: int] : (v5 = 0 | vt1 = % 27.91/4.42 vZero | ~ (vptchecksimple(v4, v3) = v5) | ~ (vSucc(v2) = vt1) | ~ % 27.91/4.42 vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v6: vOptTerm] : ? [v7: any] : % 27.91/4.42 ? [v8: any] : ? [v9: any] : ? [v10: vOptTerm] : (vptchecksimple(v0, v3) % 27.91/4.42 = v9 & vreduce(vt1) = v6 & visSomeTerm(v6) = v7 & visNV(v2) = v8 & % 27.91/4.42 vsomeTerm(v4) = v10 & vOptTerm(v10) & vOptTerm(v6) & ( ~ (v10 = v1) | ~ % 27.91/4.42 (v9 = 0) | v8 = 0 | v7 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! % 27.91/4.42 [v4: vTerm] : ! [v5: int] : (v5 = 0 | vt1 = vZero | ~ (vptchecksimple(v0, % 27.91/4.42 v3) = 0) | ~ (visNV(v2) = v5) | ~ (vsomeTerm(v4) = v1) | ~ vTy(v3) % 27.91/4.42 | ~ vTerm(v4) | ~ vTerm(v2) | ? [v6: vTerm] : ? [v7: vOptTerm] : ? % 27.91/4.42 [v8: any] : ? [v9: any] : (vptchecksimple(v4, v3) = v9 & vreduce(v6) = v7 % 27.91/4.42 & visSomeTerm(v7) = v8 & vSucc(v2) = v6 & vOptTerm(v7) & vTerm(v6) & ( ~ % 27.91/4.42 (v6 = vt1) | v9 = 0 | v8 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! % 27.91/4.42 [v4: vTerm] : (vt1 = vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ % 27.91/4.42 (vsomeTerm(v4) = v1) | ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ vTerm(v4) | % 27.91/4.42 ~ vTerm(v2) | ? [v5: vOptTerm] : ? [v6: any] : ? [v7: any] : ? [v8: % 27.91/4.42 any] : (vptchecksimple(v4, v3) = v8 & vreduce(vt1) = v5 & % 27.91/4.42 visSomeTerm(v5) = v6 & visNV(v2) = v7 & vOptTerm(v5) & (v8 = 0 | v7 = 0 % 27.91/4.42 | v6 = 0)))) % 27.91/4.42 % 27.91/4.42 (Preservation-Iszero-Succ-isNV-False-isSomeTerm-True) % 27.91/4.43 vTerm(vt1) & vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) % 27.91/4.43 = v1 & vIszero(vt1) = v0 & vOptTerm(v1) & vTerm(v0) & ! [v2: vTerm] : ! % 27.91/4.43 [v3: vTy] : ! [v4: vTerm] : ! [v5: int] : ! [v6: int] : (v6 = 0 | v5 = 0 % 27.91/4.43 | vt1 = vZero | ~ (vptchecksimple(v4, v3) = v6) | ~ (visNV(v2) = v5) | % 27.91/4.43 ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v7: vTerm] : ? [v8: % 27.91/4.43 vOptTerm] : ? [v9: any] : ? [v10: any] : ? [v11: vOptTerm] : % 27.91/4.43 (vptchecksimple(v0, v3) = v10 & vreduce(v7) = v8 & visSomeTerm(v8) = v9 & % 27.91/4.43 vsomeTerm(v4) = v11 & vSucc(v2) = v7 & vOptTerm(v11) & vOptTerm(v8) & % 27.91/4.43 vTerm(v7) & ( ~ (v11 = v1) | ~ (v10 = 0) | ~ (v9 = 0) | ~ (v7 = % 27.91/4.43 vt1)))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] : ! [v5: % 27.91/4.43 vOptTerm] : ! [v6: int] : (v6 = 0 | vt1 = vZero | ~ (vptchecksimple(v4, % 27.91/4.43 v3) = v6) | ~ (vreduce(vt1) = v5) | ~ (visSomeTerm(v5) = 0) | ~ % 27.91/4.43 (vSucc(v2) = vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v7: % 27.91/4.43 any] : ? [v8: any] : ? [v9: vOptTerm] : (vptchecksimple(v0, v3) = v8 & % 27.91/4.43 visNV(v2) = v7 & vsomeTerm(v4) = v9 & vOptTerm(v9) & ( ~ (v9 = v1) | ~ % 27.91/4.43 (v8 = 0) | v7 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] % 27.91/4.43 : ! [v5: int] : (v5 = 0 | vt1 = vZero | ~ (vptchecksimple(v4, v3) = v5) | % 27.91/4.43 ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v6: % 27.91/4.43 vOptTerm] : ? [v7: any] : ? [v8: any] : ? [v9: any] : ? [v10: % 27.91/4.43 vOptTerm] : (vptchecksimple(v0, v3) = v9 & vreduce(vt1) = v6 & % 27.91/4.43 visSomeTerm(v6) = v7 & visNV(v2) = v8 & vsomeTerm(v4) = v10 & % 27.91/4.43 vOptTerm(v10) & vOptTerm(v6) & ( ~ (v10 = v1) | ~ (v9 = 0) | ~ (v7 = % 27.91/4.43 0) | v8 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] : ! % 27.91/4.43 [v5: int] : (v5 = 0 | vt1 = vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ % 27.91/4.43 (visNV(v2) = v5) | ~ (vsomeTerm(v4) = v1) | ~ vTy(v3) | ~ vTerm(v4) | % 27.91/4.43 ~ vTerm(v2) | ? [v6: vTerm] : ? [v7: vOptTerm] : ? [v8: any] : ? [v9: % 27.91/4.43 any] : (vptchecksimple(v4, v3) = v9 & vreduce(v6) = v7 & visSomeTerm(v7) % 27.91/4.43 = v8 & vSucc(v2) = v6 & vOptTerm(v7) & vTerm(v6) & ( ~ (v8 = 0) | ~ (v6 % 27.91/4.43 = vt1) | v9 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] % 27.91/4.43 : ! [v5: vOptTerm] : (vt1 = vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ % 27.91/4.43 (vreduce(vt1) = v5) | ~ (visSomeTerm(v5) = 0) | ~ (vsomeTerm(v4) = v1) | % 27.91/4.43 ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v6: % 27.91/4.43 any] : ? [v7: any] : (vptchecksimple(v4, v3) = v7 & visNV(v2) = v6 & % 27.91/4.43 (v7 = 0 | v6 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] : % 27.91/4.43 (vt1 = vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ (vsomeTerm(v4) = v1) | % 27.91/4.43 ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v5: % 27.91/4.43 vOptTerm] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 27.91/4.43 (vptchecksimple(v4, v3) = v8 & vreduce(vt1) = v5 & visSomeTerm(v5) = v6 & % 27.91/4.43 visNV(v2) = v7 & vOptTerm(v5) & ( ~ (v6 = 0) | v8 = 0 | v7 = 0)))) % 27.91/4.43 % 27.91/4.43 (Tiszero) % 27.91/4.43 vTy(vB) & vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) % 27.91/4.43 | ~ vTerm(v0) | ? [v2: any] : ? [v3: any] : (vptchecksimple(v1, vB) = v3 % 27.91/4.43 & vptchecksimple(v0, vNat) = v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: % 27.91/4.43 vTerm] : ( ~ (vptchecksimple(v0, vNat) = 0) | ~ vTerm(v0) | ? [v1: vTerm] % 27.91/4.43 : (vptchecksimple(v1, vB) = 0 & vIszero(v0) = v1 & vTerm(v1))) % 27.91/4.43 % 27.91/4.43 (Tiszero_inv1) % 27.91/4.43 vTy(vB) & vTy(vNat) & ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ % 27.91/4.43 (vptchecksimple(v0, vNat) = v1) | ~ vTerm(v0) | ? [v2: vTerm] : ? [v3: % 27.91/4.43 int] : ( ~ (v3 = 0) & vptchecksimple(v2, vB) = v3 & vIszero(v0) = v2 & % 27.91/4.43 vTerm(v2))) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) | % 27.91/4.43 ~ vTerm(v0) | ? [v2: any] : ? [v3: any] : (vptchecksimple(v1, vB) = v2 & % 27.91/4.43 vptchecksimple(v0, vNat) = v3 & ( ~ (v2 = 0) | v3 = 0))) % 27.91/4.43 % 27.91/4.43 (Tiszero_inv2) % 27.91/4.43 vTy(vB) & ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vB | ~ % 27.91/4.43 (vptchecksimple(v2, v1) = 0) | ~ (vIszero(v0) = v2) | ~ vTy(v1) | ~ % 27.91/4.43 vTerm(v0)) % 27.91/4.43 % 27.91/4.43 (isNV-1) % 27.91/4.44 ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = v1) | ~ vTerm(v0) | % 27.91/4.44 ? [v2: vTerm] : ? [v3: int] : ( ~ (v3 = 0) & visNV(v2) = v3 & vSucc(v0) = % 27.91/4.44 v2 & vTerm(v2))) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) % 27.91/4.44 | ~ vTerm(v0) | ? [v2: any] : ? [v3: any] : (visNV(v1) = v3 & visNV(v0) = % 27.91/4.44 v2 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ % 27.91/4.44 (vSucc(v0) = v1) | ~ vTerm(v0) | ? [v2: any] : ? [v3: any] : (visNV(v1) = % 27.91/4.44 v2 & visNV(v0) = v3 & ( ~ (v2 = 0) | v3 = 0))) & ! [v0: vTerm] : ( ~ % 27.91/4.44 (visNV(v0) = 0) | ~ vTerm(v0) | ? [v1: vTerm] : (visNV(v1) = 0 & vSucc(v0) % 27.91/4.44 = v1 & vTerm(v1))) % 27.91/4.44 % 27.91/4.44 (reduce-14) % 27.91/4.44 ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = v1) | ~ vTerm(v0) | % 27.91/4.44 ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : ? [v6: % 27.91/4.44 vOptTerm] : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : % 27.91/4.44 (vreduce(v5) = v6 & vreduce(v2) = v3 & visSomeTerm(v3) = v4 & vgetTerm(v3) = % 27.91/4.44 v7 & vsomeTerm(v8) = v9 & vIszero(v7) = v8 & vIszero(v2) = v5 & vSucc(v0) % 27.91/4.44 = v2 & vOptTerm(v9) & vOptTerm(v6) & vOptTerm(v3) & vTerm(v8) & vTerm(v7) % 27.91/4.44 & vTerm(v5) & vTerm(v2) & ( ~ (v4 = 0) | v9 = v6))) & ! [v0: vTerm] : ! % 27.91/4.44 [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | ? [v2: any] : ? [v3: % 27.91/4.44 vOptTerm] : ? [v4: any] : ? [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: % 27.91/4.44 vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : (vreduce(v5) = v6 & % 27.91/4.44 vreduce(v1) = v3 & visSomeTerm(v3) = v4 & visNV(v0) = v2 & vgetTerm(v3) = % 27.91/4.44 v7 & vsomeTerm(v8) = v9 & vIszero(v7) = v8 & vIszero(v1) = v5 & % 27.91/4.44 vOptTerm(v9) & vOptTerm(v6) & vOptTerm(v3) & vTerm(v8) & vTerm(v7) & % 27.91/4.44 vTerm(v5) & ( ~ (v4 = 0) | v9 = v6 | v2 = 0))) % 27.91/4.44 % 27.91/4.44 (reduce-15) % 27.91/4.44 vOptTerm(vnoTerm) & ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = % 27.91/4.44 v1) | ~ vTerm(v0) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: any] : % 27.91/4.44 ? [v5: vTerm] : ? [v6: vOptTerm] : (vreduce(v5) = v6 & vreduce(v2) = v3 & % 27.91/4.44 visSomeTerm(v3) = v4 & vIszero(v2) = v5 & vSucc(v0) = v2 & vOptTerm(v6) & % 27.91/4.44 vOptTerm(v3) & vTerm(v5) & vTerm(v2) & (v6 = vnoTerm | v4 = 0))) & ! [v0: % 27.91/4.44 vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | ? [v2: any] % 27.91/4.44 : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : ? [v6: vOptTerm] : % 27.91/4.44 (vreduce(v5) = v6 & vreduce(v1) = v3 & visSomeTerm(v3) = v4 & visNV(v0) = v2 % 27.91/4.44 & vIszero(v1) = v5 & vOptTerm(v6) & vOptTerm(v3) & vTerm(v5) & (v6 = % 27.91/4.44 vnoTerm | v4 = 0 | v2 = 0))) % 27.91/4.44 % 27.91/4.44 (reduce-4) % 27.91/4.44 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vreduce(v0) = v1) | ~ vTerm(v0) | % 27.91/4.44 ? [v2: any] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: % 27.91/4.44 vTerm] : ? [v7: vOptTerm] : (vreduce(v3) = v4 & visSomeTerm(v1) = v2 & % 27.91/4.44 vgetTerm(v1) = v5 & vsomeTerm(v6) = v7 & vSucc(v5) = v6 & vSucc(v0) = v3 & % 27.91/4.44 vOptTerm(v7) & vOptTerm(v4) & vTerm(v6) & vTerm(v5) & vTerm(v3) & ( ~ (v2 % 27.91/4.44 = 0) | v7 = v4))) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = % 27.91/4.44 v1) | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: any] : ? [v4: vOptTerm] % 27.91/4.44 : ? [v5: vTerm] : ? [v6: vTerm] : ? [v7: vOptTerm] : (vreduce(v1) = v4 & % 27.91/4.44 vreduce(v0) = v2 & visSomeTerm(v2) = v3 & vgetTerm(v2) = v5 & % 27.91/4.44 vsomeTerm(v6) = v7 & vSucc(v5) = v6 & vOptTerm(v7) & vOptTerm(v4) & % 27.91/4.44 vOptTerm(v2) & vTerm(v6) & vTerm(v5) & ( ~ (v3 = 0) | v7 = v4))) % 27.91/4.44 % 27.91/4.44 (reduce-5) % 27.91/4.45 vOptTerm(vnoTerm) & ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vreduce(v0) = % 27.91/4.45 v1) | ~ vTerm(v0) | ? [v2: any] : ? [v3: vTerm] : ? [v4: vOptTerm] : % 27.91/4.45 (vreduce(v3) = v4 & visSomeTerm(v1) = v2 & vSucc(v0) = v3 & vOptTerm(v4) & % 27.91/4.45 vTerm(v3) & (v4 = vnoTerm | v2 = 0))) & ! [v0: vTerm] : ! [v1: vTerm] : % 27.91/4.45 ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: any] : ? % 27.91/4.45 [v4: vOptTerm] : (vreduce(v1) = v4 & vreduce(v0) = v2 & visSomeTerm(v2) = v3 % 27.91/4.45 & vOptTerm(v4) & vOptTerm(v2) & (v4 = vnoTerm | v3 = 0))) % 27.91/4.45 % 27.91/4.45 (reduce-7) % 27.91/4.45 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vsomeTerm(v0) = v1) | ~ vTerm(v0) | % 27.91/4.45 ? [v2: any] : ? [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : % 27.91/4.45 (vreduce(v4) = v5 & visNV(v0) = v2 & vPred(v3) = v4 & vSucc(v0) = v3 & % 27.91/4.45 vOptTerm(v5) & vTerm(v4) & vTerm(v3) & ( ~ (v2 = 0) | v5 = v1))) & ! [v0: % 27.91/4.45 vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | ? [v2: any] % 27.91/4.45 : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vOptTerm] : (vreduce(v3) = v4 % 27.91/4.45 & visNV(v0) = v2 & vsomeTerm(v0) = v5 & vPred(v1) = v3 & vOptTerm(v5) & % 27.91/4.45 vOptTerm(v4) & vTerm(v3) & ( ~ (v2 = 0) | v5 = v4))) & ! [v0: vTerm] : ( % 27.91/4.45 ~ (visNV(v0) = 0) | ~ vTerm(v0) | ? [v1: vTerm] : ? [v2: vTerm] : ? [v3: % 27.91/4.45 vOptTerm] : (vreduce(v2) = v3 & vsomeTerm(v0) = v3 & vPred(v1) = v2 & % 27.91/4.45 vSucc(v0) = v1 & vOptTerm(v3) & vTerm(v2) & vTerm(v1))) % 27.91/4.45 % 27.91/4.45 (reduce-8) % 27.91/4.45 ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = v1) | ~ vTerm(v0) | % 27.91/4.45 ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : ? [v6: % 27.91/4.45 vOptTerm] : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : % 27.91/4.45 (vreduce(v5) = v6 & vreduce(v2) = v3 & visSomeTerm(v3) = v4 & vgetTerm(v3) = % 27.91/4.45 v7 & vsomeTerm(v8) = v9 & vPred(v7) = v8 & vPred(v2) = v5 & vSucc(v0) = v2 % 27.91/4.45 & vOptTerm(v9) & vOptTerm(v6) & vOptTerm(v3) & vTerm(v8) & vTerm(v7) & % 27.91/4.45 vTerm(v5) & vTerm(v2) & ( ~ (v4 = 0) | v9 = v6))) & ! [v0: vTerm] : ! % 27.91/4.45 [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | ? [v2: any] : ? [v3: % 27.91/4.45 vOptTerm] : ? [v4: any] : ? [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: % 27.91/4.45 vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : (vreduce(v5) = v6 & % 27.91/4.45 vreduce(v1) = v3 & visSomeTerm(v3) = v4 & visNV(v0) = v2 & vgetTerm(v3) = % 27.91/4.45 v7 & vsomeTerm(v8) = v9 & vPred(v7) = v8 & vPred(v1) = v5 & vOptTerm(v9) & % 27.91/4.45 vOptTerm(v6) & vOptTerm(v3) & vTerm(v8) & vTerm(v7) & vTerm(v5) & ( ~ (v4 % 27.91/4.45 = 0) | v9 = v6 | v2 = 0))) % 27.91/4.45 % 27.91/4.45 (reduce-9) % 27.91/4.45 vOptTerm(vnoTerm) & ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = % 27.91/4.45 v1) | ~ vTerm(v0) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: any] : % 27.91/4.45 ? [v5: vTerm] : ? [v6: vOptTerm] : (vreduce(v5) = v6 & vreduce(v2) = v3 & % 27.91/4.45 visSomeTerm(v3) = v4 & vPred(v2) = v5 & vSucc(v0) = v2 & vOptTerm(v6) & % 27.91/4.45 vOptTerm(v3) & vTerm(v5) & vTerm(v2) & (v6 = vnoTerm | v4 = 0))) & ! [v0: % 27.91/4.45 vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | ? [v2: any] % 27.91/4.45 : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : ? [v6: vOptTerm] : % 27.91/4.45 (vreduce(v5) = v6 & vreduce(v1) = v3 & visSomeTerm(v3) = v4 & visNV(v0) = v2 % 27.91/4.45 & vPred(v1) = v5 & vOptTerm(v6) & vOptTerm(v3) & vTerm(v5) & (v6 = vnoTerm % 27.91/4.45 | v4 = 0 | v2 = 0))) % 27.91/4.45 % 27.91/4.45 (function-axioms) % 27.91/4.46 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 27.91/4.46 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 27.91/4.46 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 27.91/4.46 vTy] : ! [v3: vTerm] : (v1 = v0 | ~ (vptchecksimple(v3, v2) = v1) | ~ % 27.91/4.46 (vptchecksimple(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: % 27.91/4.46 vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ % 27.91/4.46 (vplusop(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : % 27.91/4.46 ! [v3: vTerm] : (v1 = v0 | ~ (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) % 27.91/4.46 & ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 27.91/4.46 (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) & ! [v0: MultipleValueBool] : % 27.91/4.46 ! [v1: MultipleValueBool] : ! [v2: vOptTerm] : (v1 = v0 | ~ (visSomeTerm(v2) % 27.91/4.46 = v1) | ~ (visSomeTerm(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 27.91/4.46 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visValue(v2) = v1) | ~ % 27.91/4.46 (visValue(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 27.91/4.46 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visNV(v2) = v1) | ~ % 27.91/4.46 (visNV(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 27.91/4.46 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 27.91/4.46 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 27.91/4.46 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 27.91/4.46 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 27.91/4.46 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 27.91/4.46 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 27.91/4.46 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 27.91/4.46 % 27.91/4.46 Further assumptions not needed in the proof: % 27.91/4.46 -------------------------------------------- % 27.91/4.46 DIFF-B-Nat, DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, % 27.91/4.46 DIFF-False-Pred, DIFF-False-Succ, DIFF-False-Zero, DIFF-Ifelse-Iszero, % 27.91/4.46 DIFF-Ifelse-Plus, DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, % 27.91/4.46 DIFF-Iszero-Plus, DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, % 27.91/4.46 DIFF-Succ-Plus, DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, % 27.91/4.46 DIFF-True-Iszero, DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, % 27.91/4.46 DIFF-True-Zero, DIFF-Zero-Iszero, DIFF-Zero-Plus, DIFF-Zero-Pred, % 27.91/4.46 DIFF-Zero-Succ, DIFF-noTerm-someTerm, EQ-Ifelse, EQ-Iszero, EQ-Plus, EQ-Pred, % 27.91/4.46 EQ-Succ, EQ-someTerm, TPlus, TPlus_inv0, TPlus_inv1, TPlus_inv2, TPred, % 27.91/4.46 TPred_inv1, TPred_inv2, TSucc, TSucc_inv1, TSucc_inv2, TZero, TZero_inv, Tfalse, % 27.91/4.46 Tif, Tif_inv1, Tif_inv2, Tif_inv3, Ttrue, dom-OptTerm, dom-Term, dom-Ty, % 27.91/4.46 getTerm-0, isNV-0, isNV-2, isNV-false-INV, isNV-true-INV, isSomeTerm-0, % 27.91/4.46 isSomeTerm-1, isSomeTerm-false-INV, isSomeTerm-true-INV, isValue-0, isValue-1, % 27.91/4.46 isValue-2, isValue-false-INV, isValue-true-INV, plusop-0, plusop-1, plusop-2, % 27.91/4.46 plusop-INV, reduce-0, reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, % 27.91/4.46 reduce-16, reduce-17, reduce-18, reduce-19, reduce-2, reduce-20, reduce-21, % 27.91/4.46 reduce-22, reduce-23, reduce-3, reduce-6, reduce-INV % 27.91/4.46 % 27.91/4.46 Those formulas are unsatisfiable: % 27.91/4.46 --------------------------------- % 27.91/4.46 % 27.91/4.46 Begin of proof % 27.91/4.46 | % 27.91/4.46 | ALPHA: (isNV-1) implies: % 27.91/4.46 | (1) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | % 27.91/4.46 | ? [v2: any] : ? [v3: any] : (visNV(v1) = v2 & visNV(v0) = v3 & ( ~ % 27.91/4.46 | (v2 = 0) | v3 = 0))) % 27.91/4.46 | (2) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | % 27.91/4.46 | ? [v2: any] : ? [v3: any] : (visNV(v1) = v3 & visNV(v0) = v2 & ( ~ % 27.91/4.46 | (v2 = 0) | v3 = 0))) % 27.91/4.47 | (3) ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = v1) | ~ % 27.91/4.47 | vTerm(v0) | ? [v2: vTerm] : ? [v3: int] : ( ~ (v3 = 0) & visNV(v2) % 27.91/4.47 | = v3 & vSucc(v0) = v2 & vTerm(v2))) % 27.91/4.47 | % 27.91/4.47 | ALPHA: (reduce-4) implies: % 27.91/4.47 | (4) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | % 27.91/4.47 | ? [v2: vOptTerm] : ? [v3: any] : ? [v4: vOptTerm] : ? [v5: vTerm] % 27.91/4.47 | : ? [v6: vTerm] : ? [v7: vOptTerm] : (vreduce(v1) = v4 & % 27.91/4.47 | vreduce(v0) = v2 & visSomeTerm(v2) = v3 & vgetTerm(v2) = v5 & % 27.91/4.47 | vsomeTerm(v6) = v7 & vSucc(v5) = v6 & vOptTerm(v7) & vOptTerm(v4) & % 27.91/4.47 | vOptTerm(v2) & vTerm(v6) & vTerm(v5) & ( ~ (v3 = 0) | v7 = v4))) % 27.91/4.47 | (5) ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vreduce(v0) = v1) | ~ % 27.91/4.47 | vTerm(v0) | ? [v2: any] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? % 27.91/4.47 | [v5: vTerm] : ? [v6: vTerm] : ? [v7: vOptTerm] : (vreduce(v3) = v4 % 27.91/4.47 | & visSomeTerm(v1) = v2 & vgetTerm(v1) = v5 & vsomeTerm(v6) = v7 & % 27.91/4.47 | vSucc(v5) = v6 & vSucc(v0) = v3 & vOptTerm(v7) & vOptTerm(v4) & % 27.91/4.47 | vTerm(v6) & vTerm(v5) & vTerm(v3) & ( ~ (v2 = 0) | v7 = v4))) % 27.91/4.47 | % 27.91/4.47 | ALPHA: (reduce-5) implies: % 27.91/4.47 | (6) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | % 27.91/4.47 | ? [v2: vOptTerm] : ? [v3: any] : ? [v4: vOptTerm] : (vreduce(v1) = % 27.91/4.47 | v4 & vreduce(v0) = v2 & visSomeTerm(v2) = v3 & vOptTerm(v4) & % 27.91/4.47 | vOptTerm(v2) & (v4 = vnoTerm | v3 = 0))) % 27.91/4.47 | (7) ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vreduce(v0) = v1) | ~ % 27.91/4.47 | vTerm(v0) | ? [v2: any] : ? [v3: vTerm] : ? [v4: vOptTerm] : % 27.91/4.47 | (vreduce(v3) = v4 & visSomeTerm(v1) = v2 & vSucc(v0) = v3 & % 27.91/4.47 | vOptTerm(v4) & vTerm(v3) & (v4 = vnoTerm | v2 = 0))) % 27.91/4.47 | % 27.91/4.47 | ALPHA: (reduce-7) implies: % 27.91/4.47 | (8) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | % 27.91/4.47 | ? [v2: any] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vOptTerm] % 27.91/4.47 | : (vreduce(v3) = v4 & visNV(v0) = v2 & vsomeTerm(v0) = v5 & vPred(v1) % 27.91/4.47 | = v3 & vOptTerm(v5) & vOptTerm(v4) & vTerm(v3) & ( ~ (v2 = 0) | v5 % 27.91/4.47 | = v4))) % 27.91/4.47 | % 27.91/4.47 | ALPHA: (reduce-8) implies: % 27.91/4.47 | (9) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) | % 27.91/4.47 | ? [v2: any] : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : ? % 27.91/4.47 | [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] % 27.91/4.47 | : (vreduce(v5) = v6 & vreduce(v1) = v3 & visSomeTerm(v3) = v4 & % 27.91/4.47 | visNV(v0) = v2 & vgetTerm(v3) = v7 & vsomeTerm(v8) = v9 & vPred(v7) % 27.91/4.47 | = v8 & vPred(v1) = v5 & vOptTerm(v9) & vOptTerm(v6) & vOptTerm(v3) % 27.91/4.47 | & vTerm(v8) & vTerm(v7) & vTerm(v5) & ( ~ (v4 = 0) | v9 = v6 | v2 = % 27.91/4.47 | 0))) % 27.91/4.47 | (10) ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = v1) | ~ % 27.91/4.47 | vTerm(v0) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: any] : ? % 27.91/4.47 | [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: vTerm] : % 27.91/4.47 | ? [v9: vOptTerm] : (vreduce(v5) = v6 & vreduce(v2) = v3 & % 27.91/4.47 | visSomeTerm(v3) = v4 & vgetTerm(v3) = v7 & vsomeTerm(v8) = v9 & % 27.91/4.47 | vPred(v7) = v8 & vPred(v2) = v5 & vSucc(v0) = v2 & vOptTerm(v9) & % 27.91/4.47 | vOptTerm(v6) & vOptTerm(v3) & vTerm(v8) & vTerm(v7) & vTerm(v5) & % 27.91/4.47 | vTerm(v2) & ( ~ (v4 = 0) | v9 = v6))) % 27.91/4.47 | % 27.91/4.47 | ALPHA: (reduce-9) implies: % 27.91/4.48 | (11) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) % 27.91/4.48 | | ? [v2: any] : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : % 27.91/4.48 | ? [v6: vOptTerm] : (vreduce(v5) = v6 & vreduce(v1) = v3 & % 27.91/4.48 | visSomeTerm(v3) = v4 & visNV(v0) = v2 & vPred(v1) = v5 & % 27.91/4.48 | vOptTerm(v6) & vOptTerm(v3) & vTerm(v5) & (v6 = vnoTerm | v4 = 0 | % 27.91/4.48 | v2 = 0))) % 27.91/4.48 | (12) ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = v1) | ~ % 27.91/4.48 | vTerm(v0) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: any] : ? % 27.91/4.48 | [v5: vTerm] : ? [v6: vOptTerm] : (vreduce(v5) = v6 & vreduce(v2) = % 27.91/4.48 | v3 & visSomeTerm(v3) = v4 & vPred(v2) = v5 & vSucc(v0) = v2 & % 27.91/4.48 | vOptTerm(v6) & vOptTerm(v3) & vTerm(v5) & vTerm(v2) & (v6 = % 27.91/4.48 | vnoTerm | v4 = 0))) % 27.91/4.48 | % 27.91/4.48 | ALPHA: (reduce-14) implies: % 27.91/4.48 | (13) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) % 27.91/4.48 | | ? [v2: any] : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : % 27.91/4.48 | ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: % 27.91/4.48 | vOptTerm] : (vreduce(v5) = v6 & vreduce(v1) = v3 & visSomeTerm(v3) % 27.91/4.48 | = v4 & visNV(v0) = v2 & vgetTerm(v3) = v7 & vsomeTerm(v8) = v9 & % 27.91/4.48 | vIszero(v7) = v8 & vIszero(v1) = v5 & vOptTerm(v9) & vOptTerm(v6) % 27.91/4.48 | & vOptTerm(v3) & vTerm(v8) & vTerm(v7) & vTerm(v5) & ( ~ (v4 = 0) % 27.91/4.48 | | v9 = v6 | v2 = 0))) % 27.91/4.48 | % 27.91/4.48 | ALPHA: (reduce-15) implies: % 27.91/4.48 | (14) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vSucc(v0) = v1) | ~ vTerm(v0) % 27.91/4.48 | | ? [v2: any] : ? [v3: vOptTerm] : ? [v4: any] : ? [v5: vTerm] : % 27.91/4.48 | ? [v6: vOptTerm] : (vreduce(v5) = v6 & vreduce(v1) = v3 & % 27.91/4.48 | visSomeTerm(v3) = v4 & visNV(v0) = v2 & vIszero(v1) = v5 & % 27.91/4.48 | vOptTerm(v6) & vOptTerm(v3) & vTerm(v5) & (v6 = vnoTerm | v4 = 0 | % 27.91/4.48 | v2 = 0))) % 27.91/4.48 | (15) ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visNV(v0) = v1) | ~ % 27.91/4.48 | vTerm(v0) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: any] : ? % 27.91/4.48 | [v5: vTerm] : ? [v6: vOptTerm] : (vreduce(v5) = v6 & vreduce(v2) = % 27.91/4.48 | v3 & visSomeTerm(v3) = v4 & vIszero(v2) = v5 & vSucc(v0) = v2 & % 27.91/4.48 | vOptTerm(v6) & vOptTerm(v3) & vTerm(v5) & vTerm(v2) & (v6 = % 27.91/4.48 | vnoTerm | v4 = 0))) % 27.91/4.48 | % 27.91/4.48 | ALPHA: (Tiszero) implies: % 27.91/4.48 | (16) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) | ~ % 27.91/4.48 | vTerm(v0) | ? [v2: any] : ? [v3: any] : (vptchecksimple(v1, vB) = % 27.91/4.48 | v3 & vptchecksimple(v0, vNat) = v2 & ( ~ (v2 = 0) | v3 = 0))) % 27.91/4.48 | % 27.91/4.48 | ALPHA: (Tiszero_inv1) implies: % 27.91/4.48 | (17) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) | ~ % 27.91/4.48 | vTerm(v0) | ? [v2: any] : ? [v3: any] : (vptchecksimple(v1, vB) = % 27.91/4.48 | v2 & vptchecksimple(v0, vNat) = v3 & ( ~ (v2 = 0) | v3 = 0))) % 27.91/4.48 | % 27.91/4.48 | ALPHA: (Tiszero_inv2) implies: % 27.91/4.48 | (18) ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vB | ~ % 27.91/4.48 | (vptchecksimple(v2, v1) = 0) | ~ (vIszero(v0) = v2) | ~ vTy(v1) | % 27.91/4.48 | ~ vTerm(v0)) % 27.91/4.48 | % 27.91/4.48 | ALPHA: (Preservation-Iszero-IH0) implies: % 27.91/4.48 | (19) ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: vTy] : % 27.91/4.48 | ! [v2: vTerm] : ! [v3: int] : (v3 = 0 | ~ (vptchecksimple(v2, v1) % 27.91/4.48 | = v3) | ~ vTy(v1) | ~ vTerm(v2) | ? [v4: any] : ? [v5: % 27.91/4.48 | vOptTerm] : (vptchecksimple(vt1, v1) = v4 & vsomeTerm(v2) = v5 & % 27.91/4.48 | vOptTerm(v5) & ( ~ (v5 = v0) | ~ (v4 = 0))))) % 27.91/4.48 | % 27.91/4.48 | ALPHA: (Preservation-Iszero-Succ-isNV-False-isSomeTerm-True) implies: % 27.91/4.49 | (20) ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & vIszero(vt1) % 27.91/4.49 | = v0 & vOptTerm(v1) & vTerm(v0) & ! [v2: vTerm] : ! [v3: vTy] : ! % 27.91/4.49 | [v4: vTerm] : ! [v5: int] : ! [v6: int] : (v6 = 0 | v5 = 0 | vt1 = % 27.91/4.49 | vZero | ~ (vptchecksimple(v4, v3) = v6) | ~ (visNV(v2) = v5) | % 27.91/4.49 | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v7: vTerm] : ? [v8: % 27.91/4.49 | vOptTerm] : ? [v9: any] : ? [v10: any] : ? [v11: vOptTerm] : % 27.91/4.49 | (vptchecksimple(v0, v3) = v10 & vreduce(v7) = v8 & visSomeTerm(v8) % 27.91/4.49 | = v9 & vsomeTerm(v4) = v11 & vSucc(v2) = v7 & vOptTerm(v11) & % 27.91/4.49 | vOptTerm(v8) & vTerm(v7) & ( ~ (v11 = v1) | ~ (v10 = 0) | ~ % 27.91/4.49 | (v9 = 0) | ~ (v7 = vt1)))) & ! [v2: vTerm] : ! [v3: vTy] : % 27.91/4.49 | ! [v4: vTerm] : ! [v5: vOptTerm] : ! [v6: int] : (v6 = 0 | vt1 = % 27.91/4.49 | vZero | ~ (vptchecksimple(v4, v3) = v6) | ~ (vreduce(vt1) = v5) % 27.91/4.49 | | ~ (visSomeTerm(v5) = 0) | ~ (vSucc(v2) = vt1) | ~ vTy(v3) | % 27.91/4.49 | ~ vTerm(v4) | ~ vTerm(v2) | ? [v7: any] : ? [v8: any] : ? [v9: % 27.91/4.49 | vOptTerm] : (vptchecksimple(v0, v3) = v8 & visNV(v2) = v7 & % 27.91/4.49 | vsomeTerm(v4) = v9 & vOptTerm(v9) & ( ~ (v9 = v1) | ~ (v8 = 0) % 27.91/4.49 | | v7 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] : % 27.91/4.49 | ! [v5: int] : (v5 = 0 | vt1 = vZero | ~ (vptchecksimple(v4, v3) = % 27.91/4.49 | v5) | ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ % 27.91/4.49 | vTerm(v2) | ? [v6: vOptTerm] : ? [v7: any] : ? [v8: any] : ? % 27.91/4.49 | [v9: any] : ? [v10: vOptTerm] : (vptchecksimple(v0, v3) = v9 & % 27.91/4.49 | vreduce(vt1) = v6 & visSomeTerm(v6) = v7 & visNV(v2) = v8 & % 27.91/4.49 | vsomeTerm(v4) = v10 & vOptTerm(v10) & vOptTerm(v6) & ( ~ (v10 = % 27.91/4.49 | v1) | ~ (v9 = 0) | ~ (v7 = 0) | v8 = 0))) & ! [v2: vTerm] % 27.91/4.49 | : ! [v3: vTy] : ! [v4: vTerm] : ! [v5: int] : (v5 = 0 | vt1 = % 27.91/4.49 | vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ (visNV(v2) = v5) | ~ % 27.91/4.49 | (vsomeTerm(v4) = v1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | % 27.91/4.49 | ? [v6: vTerm] : ? [v7: vOptTerm] : ? [v8: any] : ? [v9: any] : % 27.91/4.49 | (vptchecksimple(v4, v3) = v9 & vreduce(v6) = v7 & visSomeTerm(v7) % 27.91/4.49 | = v8 & vSucc(v2) = v6 & vOptTerm(v7) & vTerm(v6) & ( ~ (v8 = 0) % 27.91/4.49 | | ~ (v6 = vt1) | v9 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : % 27.91/4.49 | ! [v4: vTerm] : ! [v5: vOptTerm] : (vt1 = vZero | ~ % 27.91/4.49 | (vptchecksimple(v0, v3) = 0) | ~ (vreduce(vt1) = v5) | ~ % 27.91/4.49 | (visSomeTerm(v5) = 0) | ~ (vsomeTerm(v4) = v1) | ~ (vSucc(v2) = % 27.91/4.49 | vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v6: any] : % 27.91/4.49 | ? [v7: any] : (vptchecksimple(v4, v3) = v7 & visNV(v2) = v6 & (v7 % 27.91/4.49 | = 0 | v6 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: % 27.91/4.49 | vTerm] : (vt1 = vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ % 27.91/4.49 | (vsomeTerm(v4) = v1) | ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ % 27.91/4.49 | vTerm(v4) | ~ vTerm(v2) | ? [v5: vOptTerm] : ? [v6: any] : ? % 27.91/4.49 | [v7: any] : ? [v8: any] : (vptchecksimple(v4, v3) = v8 & % 27.91/4.49 | vreduce(vt1) = v5 & visSomeTerm(v5) = v6 & visNV(v2) = v7 & % 27.91/4.49 | vOptTerm(v5) & ( ~ (v6 = 0) | v8 = 0 | v7 = 0)))) % 27.91/4.49 | % 27.91/4.49 | ALPHA: (Preservation-Iszero-Succ-isNV-False-isSomeTerm-False) implies: % 27.91/4.49 | (21) ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & vIszero(vt1) % 27.91/4.49 | = v0 & vOptTerm(v1) & vTerm(v0) & ! [v2: vTerm] : ! [v3: vTy] : ! % 27.91/4.49 | [v4: vTerm] : ! [v5: vOptTerm] : ! [v6: int] : ! [v7: int] : (v7 % 27.91/4.49 | = 0 | v6 = 0 | vt1 = vZero | ~ (vptchecksimple(v4, v3) = v7) | ~ % 27.91/4.49 | (vreduce(vt1) = v5) | ~ (visSomeTerm(v5) = v6) | ~ (vSucc(v2) = % 27.91/4.49 | vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? [v8: any] : % 27.91/4.49 | ? [v9: any] : ? [v10: vOptTerm] : (vptchecksimple(v0, v3) = v9 & % 27.91/4.49 | visNV(v2) = v8 & vsomeTerm(v4) = v10 & vOptTerm(v10) & ( ~ (v10 % 27.91/4.49 | = v1) | ~ (v9 = 0) | v8 = 0))) & ! [v2: vTerm] : ! [v3: % 27.91/4.49 | vTy] : ! [v4: vTerm] : ! [v5: int] : ! [v6: int] : (v6 = 0 | v5 % 27.91/4.49 | = 0 | vt1 = vZero | ~ (vptchecksimple(v4, v3) = v6) | ~ % 27.91/4.49 | (visNV(v2) = v5) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | ? % 27.91/4.49 | [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: any] : ? [v10: any] : % 27.91/4.49 | ? [v11: vOptTerm] : (vptchecksimple(v0, v3) = v10 & vreduce(v7) = % 27.91/4.49 | v8 & visSomeTerm(v8) = v9 & vsomeTerm(v4) = v11 & vSucc(v2) = v7 % 27.91/4.49 | & vOptTerm(v11) & vOptTerm(v8) & vTerm(v7) & ( ~ (v11 = v1) | ~ % 27.91/4.49 | (v10 = 0) | ~ (v7 = vt1) | v9 = 0))) & ! [v2: vTerm] : ! % 27.91/4.49 | [v3: vTy] : ! [v4: vTerm] : ! [v5: vOptTerm] : ! [v6: int] : (v6 % 27.91/4.49 | = 0 | vt1 = vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ % 27.91/4.49 | (vreduce(vt1) = v5) | ~ (visSomeTerm(v5) = v6) | ~ % 27.91/4.49 | (vsomeTerm(v4) = v1) | ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ % 27.91/4.49 | vTerm(v4) | ~ vTerm(v2) | ? [v7: any] : ? [v8: any] : % 27.91/4.49 | (vptchecksimple(v4, v3) = v8 & visNV(v2) = v7 & (v8 = 0 | v7 = % 27.91/4.49 | 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: vTerm] : ! % 27.91/4.49 | [v5: int] : (v5 = 0 | vt1 = vZero | ~ (vptchecksimple(v4, v3) = v5) % 27.91/4.49 | | ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) % 27.91/4.49 | | ? [v6: vOptTerm] : ? [v7: any] : ? [v8: any] : ? [v9: any] : % 27.91/4.49 | ? [v10: vOptTerm] : (vptchecksimple(v0, v3) = v9 & vreduce(vt1) = % 27.91/4.49 | v6 & visSomeTerm(v6) = v7 & visNV(v2) = v8 & vsomeTerm(v4) = v10 % 27.91/4.49 | & vOptTerm(v10) & vOptTerm(v6) & ( ~ (v10 = v1) | ~ (v9 = 0) | % 27.91/4.49 | v8 = 0 | v7 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : ! [v4: % 27.91/4.49 | vTerm] : ! [v5: int] : (v5 = 0 | vt1 = vZero | ~ % 27.91/4.49 | (vptchecksimple(v0, v3) = 0) | ~ (visNV(v2) = v5) | ~ % 27.91/4.49 | (vsomeTerm(v4) = v1) | ~ vTy(v3) | ~ vTerm(v4) | ~ vTerm(v2) | % 27.91/4.49 | ? [v6: vTerm] : ? [v7: vOptTerm] : ? [v8: any] : ? [v9: any] : % 27.91/4.49 | (vptchecksimple(v4, v3) = v9 & vreduce(v6) = v7 & visSomeTerm(v7) % 27.91/4.49 | = v8 & vSucc(v2) = v6 & vOptTerm(v7) & vTerm(v6) & ( ~ (v6 = % 27.91/4.49 | vt1) | v9 = 0 | v8 = 0))) & ! [v2: vTerm] : ! [v3: vTy] : % 27.91/4.49 | ! [v4: vTerm] : (vt1 = vZero | ~ (vptchecksimple(v0, v3) = 0) | ~ % 27.91/4.49 | (vsomeTerm(v4) = v1) | ~ (vSucc(v2) = vt1) | ~ vTy(v3) | ~ % 27.91/4.49 | vTerm(v4) | ~ vTerm(v2) | ? [v5: vOptTerm] : ? [v6: any] : ? % 27.91/4.49 | [v7: any] : ? [v8: any] : (vptchecksimple(v4, v3) = v8 & % 27.91/4.49 | vreduce(vt1) = v5 & visSomeTerm(v5) = v6 & visNV(v2) = v7 & % 27.91/4.49 | vOptTerm(v5) & (v8 = 0 | v7 = 0 | v6 = 0)))) % 27.91/4.49 | % 27.91/4.49 | ALPHA: (Preservation-Iszero-Succ-isNV-False) implies: % 27.91/4.49 | (22) vTerm(vt1) % 27.91/4.49 | (23) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vTy] : % 27.91/4.49 | ? [v4: vTerm] : ? [v5: int] : ? [v6: int] : ( ~ (v6 = 0) & ~ (v5 = % 27.91/4.49 | 0) & ~ (vt1 = vZero) & vptchecksimple(v4, v3) = v6 & % 27.91/4.49 | vptchecksimple(v0, v3) = 0 & vreduce(v0) = v1 & visNV(v2) = v5 & % 27.91/4.49 | vsomeTerm(v4) = v1 & vIszero(vt1) = v0 & vSucc(v2) = vt1 & vTy(v3) & % 27.91/4.49 | vOptTerm(v1) & vTerm(v4) & vTerm(v2) & vTerm(v0)) % 27.91/4.49 | % 27.91/4.49 | ALPHA: (function-axioms) implies: % 27.91/4.49 | (24) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 27.91/4.49 | (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 27.91/4.49 | (25) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 27.91/4.49 | (vIszero(v2) = v1) | ~ (vIszero(v2) = v0)) % 27.91/4.49 | (26) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 27.91/4.49 | (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) % 27.91/4.50 | (27) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 27.91/4.50 | vTerm] : (v1 = v0 | ~ (visNV(v2) = v1) | ~ (visNV(v2) = v0)) % 27.91/4.50 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 27.91/4.50 | vOptTerm] : (v1 = v0 | ~ (visSomeTerm(v2) = v1) | ~ % 27.91/4.50 | (visSomeTerm(v2) = v0)) % 27.91/4.50 | (29) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 27.91/4.50 | (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) % 27.91/4.50 | (30) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTy] % 27.91/4.50 | : ! [v3: vTerm] : (v1 = v0 | ~ (vptchecksimple(v3, v2) = v1) | ~ % 27.91/4.50 | (vptchecksimple(v3, v2) = v0)) % 27.91/4.50 | % 28.40/4.50 | DELTA: instantiating (19) with fresh symbol all_103_0 gives: % 28.40/4.50 | (31) vreduce(vt1) = all_103_0 & vOptTerm(all_103_0) & ! [v0: vTy] : ! % 28.40/4.50 | [v1: vTerm] : ! [v2: int] : (v2 = 0 | ~ (vptchecksimple(v1, v0) = % 28.40/4.50 | v2) | ~ vTy(v0) | ~ vTerm(v1) | ? [v3: any] : ? [v4: vOptTerm] % 28.40/4.50 | : (vptchecksimple(vt1, v0) = v3 & vsomeTerm(v1) = v4 & vOptTerm(v4) % 28.40/4.50 | & ( ~ (v4 = all_103_0) | ~ (v3 = 0)))) % 28.40/4.50 | % 28.40/4.50 | ALPHA: (31) implies: % 28.40/4.50 | (32) vreduce(vt1) = all_103_0 % 28.40/4.50 | (33) ! [v0: vTy] : ! [v1: vTerm] : ! [v2: int] : (v2 = 0 | ~ % 28.40/4.50 | (vptchecksimple(v1, v0) = v2) | ~ vTy(v0) | ~ vTerm(v1) | ? [v3: % 28.40/4.50 | any] : ? [v4: vOptTerm] : (vptchecksimple(vt1, v0) = v3 & % 28.40/4.50 | vsomeTerm(v1) = v4 & vOptTerm(v4) & ( ~ (v4 = all_103_0) | ~ (v3 % 28.40/4.50 | = 0)))) % 28.40/4.50 | % 28.40/4.50 | DELTA: instantiating (23) with fresh symbols all_106_0, all_106_1, all_106_2, % 28.40/4.50 | all_106_3, all_106_4, all_106_5, all_106_6 gives: % 28.40/4.50 | (34) ~ (all_106_0 = 0) & ~ (all_106_1 = 0) & ~ (vt1 = vZero) & % 28.40/4.50 | vptchecksimple(all_106_2, all_106_3) = all_106_0 & % 28.40/4.50 | vptchecksimple(all_106_6, all_106_3) = 0 & vreduce(all_106_6) = % 28.40/4.50 | all_106_5 & visNV(all_106_4) = all_106_1 & vsomeTerm(all_106_2) = % 28.40/4.50 | all_106_5 & vIszero(vt1) = all_106_6 & vSucc(all_106_4) = vt1 & % 28.40/4.50 | vTy(all_106_3) & vOptTerm(all_106_5) & vTerm(all_106_2) & % 28.40/4.50 | vTerm(all_106_4) & vTerm(all_106_6) % 28.40/4.50 | % 28.40/4.50 | ALPHA: (34) implies: % 28.40/4.50 | (35) ~ (vt1 = vZero) % 28.40/4.50 | (36) ~ (all_106_1 = 0) % 28.40/4.50 | (37) ~ (all_106_0 = 0) % 28.40/4.50 | (38) vTerm(all_106_4) % 28.40/4.50 | (39) vTerm(all_106_2) % 28.40/4.50 | (40) vTy(all_106_3) % 28.40/4.50 | (41) vSucc(all_106_4) = vt1 % 28.40/4.50 | (42) vIszero(vt1) = all_106_6 % 28.40/4.50 | (43) vsomeTerm(all_106_2) = all_106_5 % 28.40/4.50 | (44) visNV(all_106_4) = all_106_1 % 28.40/4.50 | (45) vreduce(all_106_6) = all_106_5 % 28.40/4.50 | (46) vptchecksimple(all_106_6, all_106_3) = 0 % 28.40/4.50 | (47) vptchecksimple(all_106_2, all_106_3) = all_106_0 % 28.40/4.50 | % 28.40/4.50 | DELTA: instantiating (20) with fresh symbols all_115_0, all_115_1 gives: % 28.40/4.51 | (48) vreduce(all_115_1) = all_115_0 & vIszero(vt1) = all_115_1 & % 28.40/4.51 | vOptTerm(all_115_0) & vTerm(all_115_1) & ! [v0: vTerm] : ! [v1: vTy] % 28.40/4.51 | : ! [v2: vTerm] : ! [v3: int] : ! [v4: int] : (v4 = 0 | v3 = 0 | % 28.40/4.51 | vt1 = vZero | ~ (vptchecksimple(v2, v1) = v4) | ~ (visNV(v0) = v3) % 28.40/4.51 | | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? [v5: vTerm] : ? % 28.40/4.51 | [v6: vOptTerm] : ? [v7: any] : ? [v8: any] : ? [v9: vOptTerm] : % 28.40/4.51 | (vptchecksimple(all_115_1, v1) = v8 & vreduce(v5) = v6 & % 28.40/4.51 | visSomeTerm(v6) = v7 & vsomeTerm(v2) = v9 & vSucc(v0) = v5 & % 28.40/4.51 | vOptTerm(v9) & vOptTerm(v6) & vTerm(v5) & ( ~ (v9 = all_115_0) | % 28.40/4.51 | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v5 = vt1)))) & ! [v0: vTerm] : % 28.40/4.51 | ! [v1: vTy] : ! [v2: vTerm] : ! [v3: vOptTerm] : ! [v4: int] : (v4 % 28.40/4.51 | = 0 | vt1 = vZero | ~ (vptchecksimple(v2, v1) = v4) | ~ % 28.40/4.51 | (vreduce(vt1) = v3) | ~ (visSomeTerm(v3) = 0) | ~ (vSucc(v0) = % 28.40/4.51 | vt1) | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? [v5: any] : % 28.40/4.51 | ? [v6: any] : ? [v7: vOptTerm] : (vptchecksimple(all_115_1, v1) = % 28.40/4.51 | v6 & visNV(v0) = v5 & vsomeTerm(v2) = v7 & vOptTerm(v7) & ( ~ (v7 % 28.40/4.51 | = all_115_0) | ~ (v6 = 0) | v5 = 0))) & ! [v0: vTerm] : ! % 28.40/4.51 | [v1: vTy] : ! [v2: vTerm] : ! [v3: int] : (v3 = 0 | vt1 = vZero | ~ % 28.40/4.51 | (vptchecksimple(v2, v1) = v3) | ~ (vSucc(v0) = vt1) | ~ vTy(v1) | % 28.40/4.51 | ~ vTerm(v2) | ~ vTerm(v0) | ? [v4: vOptTerm] : ? [v5: any] : ? % 28.40/4.51 | [v6: any] : ? [v7: any] : ? [v8: vOptTerm] : % 28.40/4.51 | (vptchecksimple(all_115_1, v1) = v7 & vreduce(vt1) = v4 & % 28.40/4.51 | visSomeTerm(v4) = v5 & visNV(v0) = v6 & vsomeTerm(v2) = v8 & % 28.40/4.51 | vOptTerm(v8) & vOptTerm(v4) & ( ~ (v8 = all_115_0) | ~ (v7 = 0) | % 28.40/4.51 | ~ (v5 = 0) | v6 = 0))) & ! [v0: vTerm] : ! [v1: vTy] : ! % 28.40/4.51 | [v2: vTerm] : ! [v3: int] : (v3 = 0 | vt1 = vZero | ~ % 28.40/4.51 | (vptchecksimple(all_115_1, v1) = 0) | ~ (visNV(v0) = v3) | ~ % 28.40/4.51 | (vsomeTerm(v2) = all_115_0) | ~ vTy(v1) | ~ vTerm(v2) | ~ % 28.40/4.51 | vTerm(v0) | ? [v4: vTerm] : ? [v5: vOptTerm] : ? [v6: any] : ? % 28.40/4.51 | [v7: any] : (vptchecksimple(v2, v1) = v7 & vreduce(v4) = v5 & % 28.40/4.51 | visSomeTerm(v5) = v6 & vSucc(v0) = v4 & vOptTerm(v5) & vTerm(v4) & % 28.40/4.51 | ( ~ (v6 = 0) | ~ (v4 = vt1) | v7 = 0))) & ! [v0: vTerm] : ! % 28.40/4.51 | [v1: vTy] : ! [v2: vTerm] : ! [v3: vOptTerm] : (vt1 = vZero | ~ % 28.40/4.51 | (vptchecksimple(all_115_1, v1) = 0) | ~ (vreduce(vt1) = v3) | ~ % 28.40/4.51 | (visSomeTerm(v3) = 0) | ~ (vsomeTerm(v2) = all_115_0) | ~ % 28.40/4.51 | (vSucc(v0) = vt1) | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? % 28.40/4.51 | [v4: any] : ? [v5: any] : (vptchecksimple(v2, v1) = v5 & visNV(v0) % 28.40/4.51 | = v4 & (v5 = 0 | v4 = 0))) & ! [v0: vTerm] : ! [v1: vTy] : ! % 28.40/4.51 | [v2: vTerm] : (vt1 = vZero | ~ (vptchecksimple(all_115_1, v1) = 0) | % 28.40/4.51 | ~ (vsomeTerm(v2) = all_115_0) | ~ (vSucc(v0) = vt1) | ~ vTy(v1) | % 28.40/4.51 | ~ vTerm(v2) | ~ vTerm(v0) | ? [v3: vOptTerm] : ? [v4: any] : ? % 28.40/4.51 | [v5: any] : ? [v6: any] : (vptchecksimple(v2, v1) = v6 & % 28.40/4.51 | vreduce(vt1) = v3 & visSomeTerm(v3) = v4 & visNV(v0) = v5 & % 28.40/4.51 | vOptTerm(v3) & ( ~ (v4 = 0) | v6 = 0 | v5 = 0))) % 28.40/4.51 | % 28.40/4.51 | ALPHA: (48) implies: % 28.40/4.51 | (49) vIszero(vt1) = all_115_1 % 28.40/4.51 | (50) vreduce(all_115_1) = all_115_0 % 28.40/4.51 | (51) ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : ! [v3: int] : (v3 = % 28.40/4.51 | 0 | vt1 = vZero | ~ (vptchecksimple(v2, v1) = v3) | ~ (vSucc(v0) = % 28.40/4.51 | vt1) | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? [v4: % 28.40/4.51 | vOptTerm] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 28.40/4.51 | vOptTerm] : (vptchecksimple(all_115_1, v1) = v7 & vreduce(vt1) = % 28.40/4.51 | v4 & visSomeTerm(v4) = v5 & visNV(v0) = v6 & vsomeTerm(v2) = v8 & % 28.40/4.51 | vOptTerm(v8) & vOptTerm(v4) & ( ~ (v8 = all_115_0) | ~ (v7 = 0) | % 28.40/4.51 | ~ (v5 = 0) | v6 = 0))) % 28.40/4.51 | (52) ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : ! [v3: int] : ! % 28.40/4.51 | [v4: int] : (v4 = 0 | v3 = 0 | vt1 = vZero | ~ (vptchecksimple(v2, % 28.40/4.51 | v1) = v4) | ~ (visNV(v0) = v3) | ~ vTy(v1) | ~ vTerm(v2) | ~ % 28.40/4.51 | vTerm(v0) | ? [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: any] : ? % 28.40/4.51 | [v8: any] : ? [v9: vOptTerm] : (vptchecksimple(all_115_1, v1) = v8 % 28.40/4.51 | & vreduce(v5) = v6 & visSomeTerm(v6) = v7 & vsomeTerm(v2) = v9 & % 28.40/4.51 | vSucc(v0) = v5 & vOptTerm(v9) & vOptTerm(v6) & vTerm(v5) & ( ~ (v9 % 28.40/4.51 | = all_115_0) | ~ (v8 = 0) | ~ (v7 = 0) | ~ (v5 = vt1)))) % 28.40/4.51 | % 28.40/4.51 | DELTA: instantiating (21) with fresh symbols all_118_0, all_118_1 gives: % 28.40/4.51 | (53) vreduce(all_118_1) = all_118_0 & vIszero(vt1) = all_118_1 & % 28.40/4.51 | vOptTerm(all_118_0) & vTerm(all_118_1) & ! [v0: vTerm] : ! [v1: vTy] % 28.40/4.51 | : ! [v2: vTerm] : ! [v3: vOptTerm] : ! [v4: int] : ! [v5: int] : % 28.40/4.51 | (v5 = 0 | v4 = 0 | vt1 = vZero | ~ (vptchecksimple(v2, v1) = v5) | ~ % 28.40/4.51 | (vreduce(vt1) = v3) | ~ (visSomeTerm(v3) = v4) | ~ (vSucc(v0) = % 28.40/4.51 | vt1) | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? [v6: any] : % 28.40/4.51 | ? [v7: any] : ? [v8: vOptTerm] : (vptchecksimple(all_118_1, v1) = % 28.40/4.51 | v7 & visNV(v0) = v6 & vsomeTerm(v2) = v8 & vOptTerm(v8) & ( ~ (v8 % 28.40/4.51 | = all_118_0) | ~ (v7 = 0) | v6 = 0))) & ! [v0: vTerm] : ! % 28.40/4.51 | [v1: vTy] : ! [v2: vTerm] : ! [v3: int] : ! [v4: int] : (v4 = 0 | % 28.40/4.51 | v3 = 0 | vt1 = vZero | ~ (vptchecksimple(v2, v1) = v4) | ~ % 28.40/4.51 | (visNV(v0) = v3) | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? % 28.40/4.51 | [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: any] : ? [v8: any] : ? % 28.40/4.51 | [v9: vOptTerm] : (vptchecksimple(all_118_1, v1) = v8 & vreduce(v5) = % 28.40/4.51 | v6 & visSomeTerm(v6) = v7 & vsomeTerm(v2) = v9 & vSucc(v0) = v5 & % 28.40/4.51 | vOptTerm(v9) & vOptTerm(v6) & vTerm(v5) & ( ~ (v9 = all_118_0) | % 28.40/4.51 | ~ (v8 = 0) | ~ (v5 = vt1) | v7 = 0))) & ! [v0: vTerm] : ! % 28.40/4.51 | [v1: vTy] : ! [v2: vTerm] : ! [v3: vOptTerm] : ! [v4: int] : (v4 = % 28.40/4.51 | 0 | vt1 = vZero | ~ (vptchecksimple(all_118_1, v1) = 0) | ~ % 28.40/4.51 | (vreduce(vt1) = v3) | ~ (visSomeTerm(v3) = v4) | ~ (vsomeTerm(v2) % 28.40/4.51 | = all_118_0) | ~ (vSucc(v0) = vt1) | ~ vTy(v1) | ~ vTerm(v2) | % 28.40/4.51 | ~ vTerm(v0) | ? [v5: any] : ? [v6: any] : (vptchecksimple(v2, v1) % 28.40/4.51 | = v6 & visNV(v0) = v5 & (v6 = 0 | v5 = 0))) & ! [v0: vTerm] : ! % 28.40/4.51 | [v1: vTy] : ! [v2: vTerm] : ! [v3: int] : (v3 = 0 | vt1 = vZero | ~ % 28.40/4.51 | (vptchecksimple(v2, v1) = v3) | ~ (vSucc(v0) = vt1) | ~ vTy(v1) | % 28.40/4.51 | ~ vTerm(v2) | ~ vTerm(v0) | ? [v4: vOptTerm] : ? [v5: any] : ? % 28.40/4.51 | [v6: any] : ? [v7: any] : ? [v8: vOptTerm] : % 28.40/4.51 | (vptchecksimple(all_118_1, v1) = v7 & vreduce(vt1) = v4 & % 28.40/4.51 | visSomeTerm(v4) = v5 & visNV(v0) = v6 & vsomeTerm(v2) = v8 & % 28.40/4.51 | vOptTerm(v8) & vOptTerm(v4) & ( ~ (v8 = all_118_0) | ~ (v7 = 0) | % 28.40/4.51 | v6 = 0 | v5 = 0))) & ! [v0: vTerm] : ! [v1: vTy] : ! [v2: % 28.40/4.51 | vTerm] : ! [v3: int] : (v3 = 0 | vt1 = vZero | ~ % 28.40/4.51 | (vptchecksimple(all_118_1, v1) = 0) | ~ (visNV(v0) = v3) | ~ % 28.40/4.51 | (vsomeTerm(v2) = all_118_0) | ~ vTy(v1) | ~ vTerm(v2) | ~ % 28.40/4.51 | vTerm(v0) | ? [v4: vTerm] : ? [v5: vOptTerm] : ? [v6: any] : ? % 28.40/4.51 | [v7: any] : (vptchecksimple(v2, v1) = v7 & vreduce(v4) = v5 & % 28.40/4.51 | visSomeTerm(v5) = v6 & vSucc(v0) = v4 & vOptTerm(v5) & vTerm(v4) & % 28.40/4.51 | ( ~ (v4 = vt1) | v7 = 0 | v6 = 0))) & ! [v0: vTerm] : ! [v1: % 28.40/4.51 | vTy] : ! [v2: vTerm] : (vt1 = vZero | ~ (vptchecksimple(all_118_1, % 28.40/4.51 | v1) = 0) | ~ (vsomeTerm(v2) = all_118_0) | ~ (vSucc(v0) = vt1) % 28.40/4.51 | | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? [v3: vOptTerm] : ? % 28.40/4.51 | [v4: any] : ? [v5: any] : ? [v6: any] : (vptchecksimple(v2, v1) = % 28.40/4.51 | v6 & vreduce(vt1) = v3 & visSomeTerm(v3) = v4 & visNV(v0) = v5 & % 28.40/4.51 | vOptTerm(v3) & (v6 = 0 | v5 = 0 | v4 = 0))) % 28.40/4.51 | % 28.40/4.51 | ALPHA: (53) implies: % 28.40/4.51 | (54) vIszero(vt1) = all_118_1 % 28.40/4.51 | (55) vreduce(all_118_1) = all_118_0 % 28.40/4.51 | (56) ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : ! [v3: int] : (v3 = % 28.40/4.51 | 0 | vt1 = vZero | ~ (vptchecksimple(v2, v1) = v3) | ~ (vSucc(v0) = % 28.40/4.51 | vt1) | ~ vTy(v1) | ~ vTerm(v2) | ~ vTerm(v0) | ? [v4: % 28.40/4.51 | vOptTerm] : ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: % 28.40/4.51 | vOptTerm] : (vptchecksimple(all_118_1, v1) = v7 & vreduce(vt1) = % 28.40/4.51 | v4 & visSomeTerm(v4) = v5 & visNV(v0) = v6 & vsomeTerm(v2) = v8 & % 28.40/4.51 | vOptTerm(v8) & vOptTerm(v4) & ( ~ (v8 = all_118_0) | ~ (v7 = 0) | % 28.40/4.51 | v6 = 0 | v5 = 0))) % 28.40/4.51 | % 28.40/4.52 | GROUND_INST: instantiating (25) with all_115_1, all_118_1, vt1, simplifying % 28.40/4.52 | with (49), (54) gives: % 28.40/4.52 | (57) all_118_1 = all_115_1 % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (25) with all_106_6, all_118_1, vt1, simplifying % 28.40/4.52 | with (42), (54) gives: % 28.40/4.52 | (58) all_118_1 = all_106_6 % 28.40/4.52 | % 28.40/4.52 | COMBINE_EQS: (57), (58) imply: % 28.40/4.52 | (59) all_115_1 = all_106_6 % 28.40/4.52 | % 28.40/4.52 | REDUCE: (55), (58) imply: % 28.40/4.52 | (60) vreduce(all_106_6) = all_118_0 % 28.40/4.52 | % 28.40/4.52 | REDUCE: (50), (59) imply: % 28.40/4.52 | (61) vreduce(all_106_6) = all_115_0 % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (29) with all_106_5, all_118_0, all_106_6, % 28.40/4.52 | simplifying with (45), (60) gives: % 28.40/4.52 | (62) all_118_0 = all_106_5 % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (29) with all_115_0, all_118_0, all_106_6, % 28.40/4.52 | simplifying with (60), (61) gives: % 28.40/4.52 | (63) all_118_0 = all_115_0 % 28.40/4.52 | % 28.40/4.52 | COMBINE_EQS: (62), (63) imply: % 28.40/4.52 | (64) all_115_0 = all_106_5 % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (13) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (65) ? [v0: any] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: vTerm] : ? % 28.40/4.52 | [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : ? [v7: vOptTerm] : % 28.40/4.52 | (vreduce(v3) = v4 & vreduce(vt1) = v1 & visSomeTerm(v1) = v2 & % 28.40/4.52 | visNV(all_106_4) = v0 & vgetTerm(v1) = v5 & vsomeTerm(v6) = v7 & % 28.40/4.52 | vIszero(v5) = v6 & vIszero(vt1) = v3 & vOptTerm(v7) & vOptTerm(v4) & % 28.40/4.52 | vOptTerm(v1) & vTerm(v6) & vTerm(v5) & vTerm(v3) & ( ~ (v2 = 0) | v7 % 28.40/4.52 | = v4 | v0 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (9) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (66) ? [v0: any] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: vTerm] : ? % 28.40/4.52 | [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : ? [v7: vOptTerm] : % 28.40/4.52 | (vreduce(v3) = v4 & vreduce(vt1) = v1 & visSomeTerm(v1) = v2 & % 28.40/4.52 | visNV(all_106_4) = v0 & vgetTerm(v1) = v5 & vsomeTerm(v6) = v7 & % 28.40/4.52 | vPred(v5) = v6 & vPred(vt1) = v3 & vOptTerm(v7) & vOptTerm(v4) & % 28.40/4.52 | vOptTerm(v1) & vTerm(v6) & vTerm(v5) & vTerm(v3) & ( ~ (v2 = 0) | v7 % 28.40/4.52 | = v4 | v0 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (4) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (67) ? [v0: vOptTerm] : ? [v1: any] : ? [v2: vOptTerm] : ? [v3: vTerm] % 28.40/4.52 | : ? [v4: vTerm] : ? [v5: vOptTerm] : (vreduce(all_106_4) = v0 & % 28.40/4.52 | vreduce(vt1) = v2 & visSomeTerm(v0) = v1 & vgetTerm(v0) = v3 & % 28.40/4.52 | vsomeTerm(v4) = v5 & vSucc(v3) = v4 & vOptTerm(v5) & vOptTerm(v2) & % 28.40/4.52 | vOptTerm(v0) & vTerm(v4) & vTerm(v3) & ( ~ (v1 = 0) | v5 = v2)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (14) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (68) ? [v0: any] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: vTerm] : ? % 28.40/4.52 | [v4: vOptTerm] : (vreduce(v3) = v4 & vreduce(vt1) = v1 & % 28.40/4.52 | visSomeTerm(v1) = v2 & visNV(all_106_4) = v0 & vIszero(vt1) = v3 & % 28.40/4.52 | vOptTerm(v4) & vOptTerm(v1) & vTerm(v3) & (v4 = vnoTerm | v2 = 0 | % 28.40/4.52 | v0 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (11) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (69) ? [v0: any] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: vTerm] : ? % 28.40/4.52 | [v4: vOptTerm] : (vreduce(v3) = v4 & vreduce(vt1) = v1 & % 28.40/4.52 | visSomeTerm(v1) = v2 & visNV(all_106_4) = v0 & vPred(vt1) = v3 & % 28.40/4.52 | vOptTerm(v4) & vOptTerm(v1) & vTerm(v3) & (v4 = vnoTerm | v2 = 0 | % 28.40/4.52 | v0 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (8) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (70) ? [v0: any] : ? [v1: vTerm] : ? [v2: vOptTerm] : ? [v3: vOptTerm] % 28.40/4.52 | : (vreduce(v1) = v2 & visNV(all_106_4) = v0 & vsomeTerm(all_106_4) = % 28.40/4.52 | v3 & vPred(vt1) = v1 & vOptTerm(v3) & vOptTerm(v2) & vTerm(v1) & ( ~ % 28.40/4.52 | (v0 = 0) | v3 = v2)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (6) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (71) ? [v0: vOptTerm] : ? [v1: any] : ? [v2: vOptTerm] : % 28.40/4.52 | (vreduce(all_106_4) = v0 & vreduce(vt1) = v2 & visSomeTerm(v0) = v1 & % 28.40/4.52 | vOptTerm(v2) & vOptTerm(v0) & (v2 = vnoTerm | v1 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (2) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (72) ? [v0: any] : ? [v1: any] : (visNV(all_106_4) = v0 & visNV(vt1) = v1 % 28.40/4.52 | & ( ~ (v0 = 0) | v1 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (1) with all_106_4, vt1, simplifying with (38), % 28.40/4.52 | (41) gives: % 28.40/4.52 | (73) ? [v0: any] : ? [v1: any] : (visNV(all_106_4) = v1 & visNV(vt1) = v0 % 28.40/4.52 | & ( ~ (v0 = 0) | v1 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (16) with vt1, all_106_6, simplifying with (22), % 28.40/4.52 | (42) gives: % 28.40/4.52 | (74) ? [v0: any] : ? [v1: any] : (vptchecksimple(all_106_6, vB) = v1 & % 28.40/4.52 | vptchecksimple(vt1, vNat) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 28.40/4.52 | % 28.40/4.52 | GROUND_INST: instantiating (17) with vt1, all_106_6, simplifying with (22), % 28.40/4.52 | (42) gives: % 28.40/4.53 | (75) ? [v0: any] : ? [v1: any] : (vptchecksimple(all_106_6, vB) = v0 & % 28.40/4.53 | vptchecksimple(vt1, vNat) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (10) with all_106_4, all_106_1, simplifying with % 28.40/4.53 | (38), (44) gives: % 28.40/4.53 | (76) all_106_1 = 0 | ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: any] : ? % 28.40/4.53 | [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : ? % 28.40/4.53 | [v7: vOptTerm] : (vreduce(v3) = v4 & vreduce(v0) = v1 & % 28.40/4.53 | visSomeTerm(v1) = v2 & vgetTerm(v1) = v5 & vsomeTerm(v6) = v7 & % 28.40/4.53 | vPred(v5) = v6 & vPred(v0) = v3 & vSucc(all_106_4) = v0 & % 28.40/4.53 | vOptTerm(v7) & vOptTerm(v4) & vOptTerm(v1) & vTerm(v6) & vTerm(v5) & % 28.40/4.53 | vTerm(v3) & vTerm(v0) & ( ~ (v2 = 0) | v7 = v4)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (15) with all_106_4, all_106_1, simplifying with % 28.40/4.53 | (38), (44) gives: % 28.40/4.53 | (77) all_106_1 = 0 | ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: any] : ? % 28.40/4.53 | [v3: vTerm] : ? [v4: vOptTerm] : (vreduce(v3) = v4 & vreduce(v0) = v1 % 28.40/4.53 | & visSomeTerm(v1) = v2 & vIszero(v0) = v3 & vSucc(all_106_4) = v0 & % 28.40/4.53 | vOptTerm(v4) & vOptTerm(v1) & vTerm(v3) & vTerm(v0) & (v4 = vnoTerm % 28.40/4.53 | | v2 = 0)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (12) with all_106_4, all_106_1, simplifying with % 28.40/4.53 | (38), (44) gives: % 28.40/4.53 | (78) all_106_1 = 0 | ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: any] : ? % 28.40/4.53 | [v3: vTerm] : ? [v4: vOptTerm] : (vreduce(v3) = v4 & vreduce(v0) = v1 % 28.40/4.53 | & visSomeTerm(v1) = v2 & vPred(v0) = v3 & vSucc(all_106_4) = v0 & % 28.40/4.53 | vOptTerm(v4) & vOptTerm(v1) & vTerm(v3) & vTerm(v0) & (v4 = vnoTerm % 28.40/4.53 | | v2 = 0)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (3) with all_106_4, all_106_1, simplifying with % 28.40/4.53 | (38), (44) gives: % 28.40/4.53 | (79) all_106_1 = 0 | ? [v0: vTerm] : ? [v1: int] : ( ~ (v1 = 0) & % 28.40/4.53 | visNV(v0) = v1 & vSucc(all_106_4) = v0 & vTerm(v0)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (5) with vt1, all_103_0, simplifying with (22), % 28.40/4.53 | (32) gives: % 28.40/4.53 | (80) ? [v0: any] : ? [v1: vTerm] : ? [v2: vOptTerm] : ? [v3: vTerm] : % 28.40/4.53 | ? [v4: vTerm] : ? [v5: vOptTerm] : (vreduce(v1) = v2 & % 28.40/4.53 | visSomeTerm(all_103_0) = v0 & vgetTerm(all_103_0) = v3 & % 28.40/4.53 | vsomeTerm(v4) = v5 & vSucc(v3) = v4 & vSucc(vt1) = v1 & vOptTerm(v5) % 28.40/4.53 | & vOptTerm(v2) & vTerm(v4) & vTerm(v3) & vTerm(v1) & ( ~ (v0 = 0) | % 28.40/4.53 | v5 = v2)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (7) with vt1, all_103_0, simplifying with (22), % 28.40/4.53 | (32) gives: % 28.40/4.53 | (81) ? [v0: any] : ? [v1: vTerm] : ? [v2: vOptTerm] : (vreduce(v1) = v2 % 28.40/4.53 | & visSomeTerm(all_103_0) = v0 & vSucc(vt1) = v1 & vOptTerm(v2) & % 28.40/4.53 | vTerm(v1) & (v2 = vnoTerm | v0 = 0)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (18) with vt1, all_106_3, all_106_6, simplifying % 28.40/4.53 | with (22), (40), (42), (46) gives: % 28.40/4.53 | (82) all_106_3 = vB % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (52) with all_106_4, all_106_3, all_106_2, % 28.40/4.53 | all_106_1, all_106_0, simplifying with (38), (39), (40), (44), % 28.40/4.53 | (47) gives: % 28.40/4.53 | (83) all_106_0 = 0 | all_106_1 = 0 | vt1 = vZero | ? [v0: vTerm] : ? [v1: % 28.40/4.53 | vOptTerm] : ? [v2: any] : ? [v3: any] : ? [v4: vOptTerm] : % 28.40/4.53 | (vptchecksimple(all_115_1, all_106_3) = v3 & vreduce(v0) = v1 & % 28.40/4.53 | visSomeTerm(v1) = v2 & vsomeTerm(all_106_2) = v4 & vSucc(all_106_4) % 28.40/4.53 | = v0 & vOptTerm(v4) & vOptTerm(v1) & vTerm(v0) & ( ~ (v4 = % 28.40/4.53 | all_115_0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v0 = vt1))) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (56) with all_106_4, all_106_3, all_106_2, % 28.40/4.53 | all_106_0, simplifying with (38), (39), (40), (41), (47) gives: % 28.40/4.53 | (84) all_106_0 = 0 | vt1 = vZero | ? [v0: vOptTerm] : ? [v1: any] : ? % 28.40/4.53 | [v2: any] : ? [v3: any] : ? [v4: vOptTerm] : % 28.40/4.53 | (vptchecksimple(all_118_1, all_106_3) = v3 & vreduce(vt1) = v0 & % 28.40/4.53 | visSomeTerm(v0) = v1 & visNV(all_106_4) = v2 & vsomeTerm(all_106_2) % 28.40/4.53 | = v4 & vOptTerm(v4) & vOptTerm(v0) & ( ~ (v4 = all_118_0) | ~ (v3 = % 28.40/4.53 | 0) | v2 = 0 | v1 = 0)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (51) with all_106_4, all_106_3, all_106_2, % 28.40/4.53 | all_106_0, simplifying with (38), (39), (40), (41), (47) gives: % 28.40/4.53 | (85) all_106_0 = 0 | vt1 = vZero | ? [v0: vOptTerm] : ? [v1: any] : ? % 28.40/4.53 | [v2: any] : ? [v3: any] : ? [v4: vOptTerm] : % 28.40/4.53 | (vptchecksimple(all_115_1, all_106_3) = v3 & vreduce(vt1) = v0 & % 28.40/4.53 | visSomeTerm(v0) = v1 & visNV(all_106_4) = v2 & vsomeTerm(all_106_2) % 28.40/4.53 | = v4 & vOptTerm(v4) & vOptTerm(v0) & ( ~ (v4 = all_115_0) | ~ (v3 = % 28.40/4.53 | 0) | ~ (v1 = 0) | v2 = 0)) % 28.40/4.53 | % 28.40/4.53 | GROUND_INST: instantiating (33) with all_106_3, all_106_2, all_106_0, % 28.40/4.53 | simplifying with (39), (40), (47) gives: % 28.40/4.53 | (86) all_106_0 = 0 | ? [v0: any] : ? [v1: vOptTerm] : % 28.40/4.53 | (vptchecksimple(vt1, all_106_3) = v0 & vsomeTerm(all_106_2) = v1 & % 28.40/4.53 | vOptTerm(v1) & ( ~ (v1 = all_103_0) | ~ (v0 = 0))) % 28.40/4.53 | % 28.40/4.53 | DELTA: instantiating (72) with fresh symbols all_148_0, all_148_1 gives: % 28.40/4.53 | (87) visNV(all_106_4) = all_148_1 & visNV(vt1) = all_148_0 & ( ~ (all_148_1 % 28.40/4.53 | = 0) | all_148_0 = 0) % 28.40/4.53 | % 28.40/4.53 | ALPHA: (87) implies: % 28.40/4.53 | (88) visNV(all_106_4) = all_148_1 % 28.40/4.53 | % 28.40/4.53 | DELTA: instantiating (75) with fresh symbols all_152_0, all_152_1 gives: % 28.40/4.53 | (89) vptchecksimple(all_106_6, vB) = all_152_1 & vptchecksimple(vt1, vNat) % 28.40/4.53 | = all_152_0 & ( ~ (all_152_1 = 0) | all_152_0 = 0) % 28.40/4.53 | % 28.40/4.53 | ALPHA: (89) implies: % 28.40/4.53 | (90) vptchecksimple(all_106_6, vB) = all_152_1 % 28.40/4.53 | % 28.40/4.53 | DELTA: instantiating (74) with fresh symbols all_154_0, all_154_1 gives: % 28.40/4.54 | (91) vptchecksimple(all_106_6, vB) = all_154_0 & vptchecksimple(vt1, vNat) % 28.40/4.54 | = all_154_1 & ( ~ (all_154_1 = 0) | all_154_0 = 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (91) implies: % 28.40/4.54 | (92) vptchecksimple(all_106_6, vB) = all_154_0 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (73) with fresh symbols all_156_0, all_156_1 gives: % 28.40/4.54 | (93) visNV(all_106_4) = all_156_0 & visNV(vt1) = all_156_1 & ( ~ (all_156_1 % 28.40/4.54 | = 0) | all_156_0 = 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (93) implies: % 28.40/4.54 | (94) visNV(all_106_4) = all_156_0 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (81) with fresh symbols all_170_0, all_170_1, all_170_2 % 28.40/4.54 | gives: % 28.40/4.54 | (95) vreduce(all_170_1) = all_170_0 & visSomeTerm(all_103_0) = all_170_2 & % 28.40/4.54 | vSucc(vt1) = all_170_1 & vOptTerm(all_170_0) & vTerm(all_170_1) & % 28.40/4.54 | (all_170_0 = vnoTerm | all_170_2 = 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (95) implies: % 28.40/4.54 | (96) visSomeTerm(all_103_0) = all_170_2 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (71) with fresh symbols all_172_0, all_172_1, all_172_2 % 28.40/4.54 | gives: % 28.40/4.54 | (97) vreduce(all_106_4) = all_172_2 & vreduce(vt1) = all_172_0 & % 28.40/4.54 | visSomeTerm(all_172_2) = all_172_1 & vOptTerm(all_172_0) & % 28.40/4.54 | vOptTerm(all_172_2) & (all_172_0 = vnoTerm | all_172_1 = 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (97) implies: % 28.40/4.54 | (98) vreduce(vt1) = all_172_0 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (70) with fresh symbols all_188_0, all_188_1, all_188_2, % 28.40/4.54 | all_188_3 gives: % 28.40/4.54 | (99) vreduce(all_188_2) = all_188_1 & visNV(all_106_4) = all_188_3 & % 28.40/4.54 | vsomeTerm(all_106_4) = all_188_0 & vPred(vt1) = all_188_2 & % 28.40/4.54 | vOptTerm(all_188_0) & vOptTerm(all_188_1) & vTerm(all_188_2) & ( ~ % 28.40/4.54 | (all_188_3 = 0) | all_188_0 = all_188_1) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (99) implies: % 28.40/4.54 | (100) visNV(all_106_4) = all_188_3 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (69) with fresh symbols all_190_0, all_190_1, all_190_2, % 28.40/4.54 | all_190_3, all_190_4 gives: % 28.40/4.54 | (101) vreduce(all_190_1) = all_190_0 & vreduce(vt1) = all_190_3 & % 28.40/4.54 | visSomeTerm(all_190_3) = all_190_2 & visNV(all_106_4) = all_190_4 & % 28.40/4.54 | vPred(vt1) = all_190_1 & vOptTerm(all_190_0) & vOptTerm(all_190_3) & % 28.40/4.54 | vTerm(all_190_1) & (all_190_0 = vnoTerm | all_190_2 = 0 | all_190_4 = % 28.40/4.54 | 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (101) implies: % 28.40/4.54 | (102) visNV(all_106_4) = all_190_4 % 28.40/4.54 | (103) visSomeTerm(all_190_3) = all_190_2 % 28.40/4.54 | (104) vreduce(vt1) = all_190_3 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (68) with fresh symbols all_192_0, all_192_1, all_192_2, % 28.40/4.54 | all_192_3, all_192_4 gives: % 28.40/4.54 | (105) vreduce(all_192_1) = all_192_0 & vreduce(vt1) = all_192_3 & % 28.40/4.54 | visSomeTerm(all_192_3) = all_192_2 & visNV(all_106_4) = all_192_4 & % 28.40/4.54 | vIszero(vt1) = all_192_1 & vOptTerm(all_192_0) & vOptTerm(all_192_3) % 28.40/4.54 | & vTerm(all_192_1) & (all_192_0 = vnoTerm | all_192_2 = 0 | all_192_4 % 28.40/4.54 | = 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (105) implies: % 28.40/4.54 | (106) visNV(all_106_4) = all_192_4 % 28.40/4.54 | (107) visSomeTerm(all_192_3) = all_192_2 % 28.40/4.54 | (108) vreduce(vt1) = all_192_3 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (80) with fresh symbols all_196_0, all_196_1, all_196_2, % 28.40/4.54 | all_196_3, all_196_4, all_196_5 gives: % 28.40/4.54 | (109) vreduce(all_196_4) = all_196_3 & visSomeTerm(all_103_0) = all_196_5 & % 28.40/4.54 | vgetTerm(all_103_0) = all_196_2 & vsomeTerm(all_196_1) = all_196_0 & % 28.40/4.54 | vSucc(all_196_2) = all_196_1 & vSucc(vt1) = all_196_4 & % 28.40/4.54 | vOptTerm(all_196_0) & vOptTerm(all_196_3) & vTerm(all_196_1) & % 28.40/4.54 | vTerm(all_196_2) & vTerm(all_196_4) & ( ~ (all_196_5 = 0) | all_196_0 % 28.40/4.54 | = all_196_3) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (109) implies: % 28.40/4.54 | (110) visSomeTerm(all_103_0) = all_196_5 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (67) with fresh symbols all_202_0, all_202_1, all_202_2, % 28.40/4.54 | all_202_3, all_202_4, all_202_5 gives: % 28.40/4.54 | (111) vreduce(all_106_4) = all_202_5 & vreduce(vt1) = all_202_3 & % 28.40/4.54 | visSomeTerm(all_202_5) = all_202_4 & vgetTerm(all_202_5) = all_202_2 % 28.40/4.54 | & vsomeTerm(all_202_1) = all_202_0 & vSucc(all_202_2) = all_202_1 & % 28.40/4.54 | vOptTerm(all_202_0) & vOptTerm(all_202_3) & vOptTerm(all_202_5) & % 28.40/4.54 | vTerm(all_202_1) & vTerm(all_202_2) & ( ~ (all_202_4 = 0) | all_202_0 % 28.40/4.54 | = all_202_3) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (111) implies: % 28.40/4.54 | (112) vreduce(vt1) = all_202_3 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (66) with fresh symbols all_204_0, all_204_1, all_204_2, % 28.40/4.54 | all_204_3, all_204_4, all_204_5, all_204_6, all_204_7 gives: % 28.40/4.54 | (113) vreduce(all_204_4) = all_204_3 & vreduce(vt1) = all_204_6 & % 28.40/4.54 | visSomeTerm(all_204_6) = all_204_5 & visNV(all_106_4) = all_204_7 & % 28.40/4.54 | vgetTerm(all_204_6) = all_204_2 & vsomeTerm(all_204_1) = all_204_0 & % 28.40/4.54 | vPred(all_204_2) = all_204_1 & vPred(vt1) = all_204_4 & % 28.40/4.54 | vOptTerm(all_204_0) & vOptTerm(all_204_3) & vOptTerm(all_204_6) & % 28.40/4.54 | vTerm(all_204_1) & vTerm(all_204_2) & vTerm(all_204_4) & ( ~ % 28.40/4.54 | (all_204_5 = 0) | all_204_0 = all_204_3 | all_204_7 = 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (113) implies: % 28.40/4.54 | (114) visNV(all_106_4) = all_204_7 % 28.40/4.54 | (115) visSomeTerm(all_204_6) = all_204_5 % 28.40/4.54 | (116) vreduce(vt1) = all_204_6 % 28.40/4.54 | % 28.40/4.54 | DELTA: instantiating (65) with fresh symbols all_206_0, all_206_1, all_206_2, % 28.40/4.54 | all_206_3, all_206_4, all_206_5, all_206_6, all_206_7 gives: % 28.40/4.54 | (117) vreduce(all_206_4) = all_206_3 & vreduce(vt1) = all_206_6 & % 28.40/4.54 | visSomeTerm(all_206_6) = all_206_5 & visNV(all_106_4) = all_206_7 & % 28.40/4.54 | vgetTerm(all_206_6) = all_206_2 & vsomeTerm(all_206_1) = all_206_0 & % 28.40/4.54 | vIszero(all_206_2) = all_206_1 & vIszero(vt1) = all_206_4 & % 28.40/4.54 | vOptTerm(all_206_0) & vOptTerm(all_206_3) & vOptTerm(all_206_6) & % 28.40/4.54 | vTerm(all_206_1) & vTerm(all_206_2) & vTerm(all_206_4) & ( ~ % 28.40/4.54 | (all_206_5 = 0) | all_206_0 = all_206_3 | all_206_7 = 0) % 28.40/4.54 | % 28.40/4.54 | ALPHA: (117) implies: % 28.40/4.54 | (118) visNV(all_106_4) = all_206_7 % 28.40/4.54 | (119) visSomeTerm(all_206_6) = all_206_5 % 28.40/4.54 | (120) vreduce(vt1) = all_206_6 % 28.40/4.54 | % 28.40/4.54 | REDUCE: (46), (82) imply: % 28.40/4.54 | (121) vptchecksimple(all_106_6, vB) = 0 % 28.40/4.54 | % 28.40/4.54 | BETA: splitting (79) gives: % 28.40/4.54 | % 28.40/4.54 | Case 1: % 28.40/4.54 | | % 28.40/4.54 | | (122) all_106_1 = 0 % 28.40/4.54 | | % 28.40/4.54 | | REDUCE: (36), (122) imply: % 28.40/4.54 | | (123) $false % 28.40/4.54 | | % 28.40/4.54 | | CLOSE: (123) is inconsistent. % 28.40/4.54 | | % 28.40/4.54 | Case 2: % 28.40/4.54 | | % 28.40/4.54 | | (124) ? [v0: vTerm] : ? [v1: int] : ( ~ (v1 = 0) & visNV(v0) = v1 & % 28.40/4.54 | | vSucc(all_106_4) = v0 & vTerm(v0)) % 28.40/4.54 | | % 28.40/4.54 | | DELTA: instantiating (124) with fresh symbols all_241_0, all_241_1 gives: % 28.40/4.54 | | (125) ~ (all_241_0 = 0) & visNV(all_241_1) = all_241_0 & % 28.40/4.54 | | vSucc(all_106_4) = all_241_1 & vTerm(all_241_1) % 28.40/4.54 | | % 28.40/4.54 | | ALPHA: (125) implies: % 28.40/4.54 | | (126) vSucc(all_106_4) = all_241_1 % 28.40/4.54 | | % 28.40/4.54 | | BETA: splitting (86) gives: % 28.40/4.54 | | % 28.40/4.54 | | Case 1: % 28.40/4.54 | | | % 28.40/4.55 | | | (127) all_106_0 = 0 % 28.40/4.55 | | | % 28.40/4.55 | | | REDUCE: (37), (127) imply: % 28.40/4.55 | | | (128) $false % 28.40/4.55 | | | % 28.40/4.55 | | | CLOSE: (128) is inconsistent. % 28.40/4.55 | | | % 28.40/4.55 | | Case 2: % 28.40/4.55 | | | % 28.40/4.55 | | | (129) ? [v0: any] : ? [v1: vOptTerm] : (vptchecksimple(vt1, % 28.40/4.55 | | | all_106_3) = v0 & vsomeTerm(all_106_2) = v1 & vOptTerm(v1) & % 28.40/4.55 | | | ( ~ (v1 = all_103_0) | ~ (v0 = 0))) % 28.40/4.55 | | | % 28.40/4.55 | | | DELTA: instantiating (129) with fresh symbols all_247_0, all_247_1 gives: % 28.40/4.55 | | | (130) vptchecksimple(vt1, all_106_3) = all_247_1 & vsomeTerm(all_106_2) % 28.40/4.55 | | | = all_247_0 & vOptTerm(all_247_0) & ( ~ (all_247_0 = all_103_0) | % 28.40/4.55 | | | ~ (all_247_1 = 0)) % 28.40/4.55 | | | % 28.40/4.55 | | | ALPHA: (130) implies: % 28.40/4.55 | | | (131) vsomeTerm(all_106_2) = all_247_0 % 28.40/4.55 | | | % 28.40/4.55 | | | BETA: splitting (78) gives: % 28.40/4.55 | | | % 28.40/4.55 | | | Case 1: % 28.40/4.55 | | | | % 28.40/4.55 | | | | (132) all_106_1 = 0 % 28.40/4.55 | | | | % 28.40/4.55 | | | | REDUCE: (36), (132) imply: % 28.40/4.55 | | | | (133) $false % 28.40/4.55 | | | | % 28.40/4.55 | | | | CLOSE: (133) is inconsistent. % 28.40/4.55 | | | | % 28.40/4.55 | | | Case 2: % 28.40/4.55 | | | | % 28.40/4.55 | | | | (134) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: % 28.40/4.55 | | | | vTerm] : ? [v4: vOptTerm] : (vreduce(v3) = v4 & vreduce(v0) % 28.40/4.55 | | | | = v1 & visSomeTerm(v1) = v2 & vPred(v0) = v3 & % 28.40/4.55 | | | | vSucc(all_106_4) = v0 & vOptTerm(v4) & vOptTerm(v1) & % 28.40/4.55 | | | | vTerm(v3) & vTerm(v0) & (v4 = vnoTerm | v2 = 0)) % 28.40/4.55 | | | | % 28.40/4.55 | | | | DELTA: instantiating (134) with fresh symbols all_257_0, all_257_1, % 28.40/4.55 | | | | all_257_2, all_257_3, all_257_4 gives: % 28.40/4.55 | | | | (135) vreduce(all_257_1) = all_257_0 & vreduce(all_257_4) = all_257_3 % 28.40/4.55 | | | | & visSomeTerm(all_257_3) = all_257_2 & vPred(all_257_4) = % 28.40/4.55 | | | | all_257_1 & vSucc(all_106_4) = all_257_4 & vOptTerm(all_257_0) % 28.40/4.55 | | | | & vOptTerm(all_257_3) & vTerm(all_257_1) & vTerm(all_257_4) & % 28.40/4.55 | | | | (all_257_0 = vnoTerm | all_257_2 = 0) % 28.40/4.55 | | | | % 28.40/4.55 | | | | ALPHA: (135) implies: % 28.40/4.55 | | | | (136) vSucc(all_106_4) = all_257_4 % 28.40/4.55 | | | | (137) visSomeTerm(all_257_3) = all_257_2 % 28.40/4.55 | | | | (138) vreduce(all_257_4) = all_257_3 % 28.40/4.55 | | | | % 28.40/4.55 | | | | BETA: splitting (77) gives: % 28.40/4.55 | | | | % 28.40/4.55 | | | | Case 1: % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | (139) all_106_1 = 0 % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | REDUCE: (36), (139) imply: % 28.40/4.55 | | | | | (140) $false % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | CLOSE: (140) is inconsistent. % 28.40/4.55 | | | | | % 28.40/4.55 | | | | Case 2: % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | (141) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: % 28.40/4.55 | | | | | vTerm] : ? [v4: vOptTerm] : (vreduce(v3) = v4 & % 28.40/4.55 | | | | | vreduce(v0) = v1 & visSomeTerm(v1) = v2 & vIszero(v0) = v3 % 28.40/4.55 | | | | | & vSucc(all_106_4) = v0 & vOptTerm(v4) & vOptTerm(v1) & % 28.40/4.55 | | | | | vTerm(v3) & vTerm(v0) & (v4 = vnoTerm | v2 = 0)) % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | DELTA: instantiating (141) with fresh symbols all_262_0, all_262_1, % 28.40/4.55 | | | | | all_262_2, all_262_3, all_262_4 gives: % 28.40/4.55 | | | | | (142) vreduce(all_262_1) = all_262_0 & vreduce(all_262_4) = % 28.40/4.55 | | | | | all_262_3 & visSomeTerm(all_262_3) = all_262_2 & % 28.40/4.55 | | | | | vIszero(all_262_4) = all_262_1 & vSucc(all_106_4) = all_262_4 % 28.40/4.55 | | | | | & vOptTerm(all_262_0) & vOptTerm(all_262_3) & % 28.40/4.55 | | | | | vTerm(all_262_1) & vTerm(all_262_4) & (all_262_0 = vnoTerm | % 28.40/4.55 | | | | | all_262_2 = 0) % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | ALPHA: (142) implies: % 28.40/4.55 | | | | | (143) vSucc(all_106_4) = all_262_4 % 28.40/4.55 | | | | | (144) visSomeTerm(all_262_3) = all_262_2 % 28.40/4.55 | | | | | (145) vreduce(all_262_4) = all_262_3 % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | BETA: splitting (83) gives: % 28.40/4.55 | | | | | % 28.40/4.55 | | | | | Case 1: % 28.40/4.55 | | | | | | % 28.40/4.55 | | | | | | (146) vt1 = vZero % 28.40/4.55 | | | | | | % 28.40/4.55 | | | | | | REDUCE: (35), (146) imply: % 28.40/4.55 | | | | | | (147) $false % 28.40/4.55 | | | | | | % 28.40/4.55 | | | | | | CLOSE: (147) is inconsistent. % 28.40/4.55 | | | | | | % 28.40/4.55 | | | | | Case 2: % 28.40/4.55 | | | | | | % 28.40/4.55 | | | | | | (148) all_106_0 = 0 | all_106_1 = 0 | ? [v0: vTerm] : ? [v1: % 28.40/4.55 | | | | | | vOptTerm] : ? [v2: any] : ? [v3: any] : ? [v4: % 28.40/4.55 | | | | | | vOptTerm] : (vptchecksimple(all_115_1, all_106_3) = v3 & % 28.40/4.55 | | | | | | vreduce(v0) = v1 & visSomeTerm(v1) = v2 & % 28.40/4.55 | | | | | | vsomeTerm(all_106_2) = v4 & vSucc(all_106_4) = v0 & % 28.40/4.55 | | | | | | vOptTerm(v4) & vOptTerm(v1) & vTerm(v0) & ( ~ (v4 = % 28.40/4.55 | | | | | | all_115_0) | ~ (v3 = 0) | ~ (v2 = 0) | ~ (v0 = % 28.40/4.55 | | | | | | vt1))) % 28.40/4.55 | | | | | | % 28.40/4.55 | | | | | | BETA: splitting (76) gives: % 28.40/4.55 | | | | | | % 28.40/4.55 | | | | | | Case 1: % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | (149) all_106_1 = 0 % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | REDUCE: (36), (149) imply: % 28.40/4.55 | | | | | | | (150) $false % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | CLOSE: (150) is inconsistent. % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | Case 2: % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | (151) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: any] : ? % 28.40/4.55 | | | | | | | [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : ? % 28.40/4.55 | | | | | | | [v6: vTerm] : ? [v7: vOptTerm] : (vreduce(v3) = v4 & % 28.40/4.55 | | | | | | | vreduce(v0) = v1 & visSomeTerm(v1) = v2 & vgetTerm(v1) % 28.40/4.55 | | | | | | | = v5 & vsomeTerm(v6) = v7 & vPred(v5) = v6 & vPred(v0) % 28.40/4.55 | | | | | | | = v3 & vSucc(all_106_4) = v0 & vOptTerm(v7) & % 28.40/4.55 | | | | | | | vOptTerm(v4) & vOptTerm(v1) & vTerm(v6) & vTerm(v5) & % 28.40/4.55 | | | | | | | vTerm(v3) & vTerm(v0) & ( ~ (v2 = 0) | v7 = v4)) % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | DELTA: instantiating (151) with fresh symbols all_275_0, % 28.40/4.55 | | | | | | | all_275_1, all_275_2, all_275_3, all_275_4, all_275_5, % 28.40/4.55 | | | | | | | all_275_6, all_275_7 gives: % 28.40/4.55 | | | | | | | (152) vreduce(all_275_4) = all_275_3 & vreduce(all_275_7) = % 28.40/4.55 | | | | | | | all_275_6 & visSomeTerm(all_275_6) = all_275_5 & % 28.40/4.55 | | | | | | | vgetTerm(all_275_6) = all_275_2 & vsomeTerm(all_275_1) = % 28.40/4.55 | | | | | | | all_275_0 & vPred(all_275_2) = all_275_1 & % 28.40/4.55 | | | | | | | vPred(all_275_7) = all_275_4 & vSucc(all_106_4) = % 28.40/4.55 | | | | | | | all_275_7 & vOptTerm(all_275_0) & vOptTerm(all_275_3) & % 28.40/4.55 | | | | | | | vOptTerm(all_275_6) & vTerm(all_275_1) & vTerm(all_275_2) % 28.40/4.55 | | | | | | | & vTerm(all_275_4) & vTerm(all_275_7) & ( ~ (all_275_5 = % 28.40/4.55 | | | | | | | 0) | all_275_0 = all_275_3) % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | ALPHA: (152) implies: % 28.40/4.55 | | | | | | | (153) vSucc(all_106_4) = all_275_7 % 28.40/4.55 | | | | | | | (154) visSomeTerm(all_275_6) = all_275_5 % 28.40/4.55 | | | | | | | (155) vreduce(all_275_7) = all_275_6 % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | GROUND_INST: instantiating (24) with vt1, all_257_4, all_106_4, % 28.40/4.55 | | | | | | | simplifying with (41), (136) gives: % 28.40/4.55 | | | | | | | (156) all_257_4 = vt1 % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | GROUND_INST: instantiating (24) with all_257_4, all_262_4, % 28.40/4.55 | | | | | | | all_106_4, simplifying with (136), (143) gives: % 28.40/4.55 | | | | | | | (157) all_262_4 = all_257_4 % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | GROUND_INST: instantiating (24) with all_262_4, all_275_7, % 28.40/4.55 | | | | | | | all_106_4, simplifying with (143), (153) gives: % 28.40/4.55 | | | | | | | (158) all_275_7 = all_262_4 % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | GROUND_INST: instantiating (24) with all_241_1, all_275_7, % 28.40/4.55 | | | | | | | all_106_4, simplifying with (126), (153) gives: % 28.40/4.55 | | | | | | | (159) all_275_7 = all_241_1 % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | GROUND_INST: instantiating (26) with all_106_5, all_247_0, % 28.40/4.55 | | | | | | | all_106_2, simplifying with (43), (131) gives: % 28.40/4.55 | | | | | | | (160) all_247_0 = all_106_5 % 28.40/4.55 | | | | | | | % 28.40/4.55 | | | | | | | GROUND_INST: instantiating (27) with all_148_1, all_188_3, % 28.40/4.55 | | | | | | | all_106_4, simplifying with (88), (100) gives: % 28.40/4.56 | | | | | | | (161) all_188_3 = all_148_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (27) with all_188_3, all_190_4, % 28.40/4.56 | | | | | | | all_106_4, simplifying with (100), (102) gives: % 28.40/4.56 | | | | | | | (162) all_190_4 = all_188_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (27) with all_106_1, all_204_7, % 28.40/4.56 | | | | | | | all_106_4, simplifying with (44), (114) gives: % 28.40/4.56 | | | | | | | (163) all_204_7 = all_106_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (27) with all_190_4, all_204_7, % 28.40/4.56 | | | | | | | all_106_4, simplifying with (102), (114) gives: % 28.40/4.56 | | | | | | | (164) all_204_7 = all_190_4 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (27) with all_192_4, all_206_7, % 28.40/4.56 | | | | | | | all_106_4, simplifying with (106), (118) gives: % 28.40/4.56 | | | | | | | (165) all_206_7 = all_192_4 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (27) with all_190_4, all_206_7, % 28.40/4.56 | | | | | | | all_106_4, simplifying with (102), (118) gives: % 28.40/4.56 | | | | | | | (166) all_206_7 = all_190_4 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (27) with all_156_0, all_206_7, % 28.40/4.56 | | | | | | | all_106_4, simplifying with (94), (118) gives: % 28.40/4.56 | | | | | | | (167) all_206_7 = all_156_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (28) with all_170_2, all_196_5, % 28.40/4.56 | | | | | | | all_103_0, simplifying with (96), (110) gives: % 28.40/4.56 | | | | | | | (168) all_196_5 = all_170_2 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (29) with all_103_0, all_202_3, vt1, % 28.40/4.56 | | | | | | | simplifying with (32), (112) gives: % 28.40/4.56 | | | | | | | (169) all_202_3 = all_103_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (29) with all_192_3, all_202_3, vt1, % 28.40/4.56 | | | | | | | simplifying with (108), (112) gives: % 28.40/4.56 | | | | | | | (170) all_202_3 = all_192_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (29) with all_172_0, all_202_3, vt1, % 28.40/4.56 | | | | | | | simplifying with (98), (112) gives: % 28.40/4.56 | | | | | | | (171) all_202_3 = all_172_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (29) with all_204_6, all_206_6, vt1, % 28.40/4.56 | | | | | | | simplifying with (116), (120) gives: % 28.40/4.56 | | | | | | | (172) all_206_6 = all_204_6 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (29) with all_202_3, all_206_6, vt1, % 28.40/4.56 | | | | | | | simplifying with (112), (120) gives: % 28.40/4.56 | | | | | | | (173) all_206_6 = all_202_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (29) with all_190_3, all_206_6, vt1, % 28.40/4.56 | | | | | | | simplifying with (104), (120) gives: % 28.40/4.56 | | | | | | | (174) all_206_6 = all_190_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (30) with all_152_1, all_154_0, vB, % 28.40/4.56 | | | | | | | all_106_6, simplifying with (90), (92) gives: % 28.40/4.56 | | | | | | | (175) all_154_0 = all_152_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | GROUND_INST: instantiating (30) with 0, all_154_0, vB, all_106_6, % 28.40/4.56 | | | | | | | simplifying with (92), (121) gives: % 28.40/4.56 | | | | | | | (176) all_154_0 = 0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (158), (159) imply: % 28.40/4.56 | | | | | | | (177) all_262_4 = all_241_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (177) implies: % 28.40/4.56 | | | | | | | (178) all_262_4 = all_241_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (157), (178) imply: % 28.40/4.56 | | | | | | | (179) all_257_4 = all_241_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (179) implies: % 28.40/4.56 | | | | | | | (180) all_257_4 = all_241_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (156), (180) imply: % 28.40/4.56 | | | | | | | (181) all_241_1 = vt1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (181) implies: % 28.40/4.56 | | | | | | | (182) all_241_1 = vt1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (172), (173) imply: % 28.40/4.56 | | | | | | | (183) all_204_6 = all_202_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (172), (174) imply: % 28.40/4.56 | | | | | | | (184) all_204_6 = all_190_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (165), (167) imply: % 28.40/4.56 | | | | | | | (185) all_192_4 = all_156_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (165), (166) imply: % 28.40/4.56 | | | | | | | (186) all_192_4 = all_190_4 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (183), (184) imply: % 28.40/4.56 | | | | | | | (187) all_202_3 = all_190_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (187) implies: % 28.40/4.56 | | | | | | | (188) all_202_3 = all_190_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (163), (164) imply: % 28.40/4.56 | | | | | | | (189) all_190_4 = all_106_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (189) implies: % 28.40/4.56 | | | | | | | (190) all_190_4 = all_106_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (170), (171) imply: % 28.40/4.56 | | | | | | | (191) all_192_3 = all_172_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (169), (170) imply: % 28.40/4.56 | | | | | | | (192) all_192_3 = all_103_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (170), (188) imply: % 28.40/4.56 | | | | | | | (193) all_192_3 = all_190_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (191), (193) imply: % 28.40/4.56 | | | | | | | (194) all_190_3 = all_172_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (192), (193) imply: % 28.40/4.56 | | | | | | | (195) all_190_3 = all_103_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (185), (186) imply: % 28.40/4.56 | | | | | | | (196) all_190_4 = all_156_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (196) implies: % 28.40/4.56 | | | | | | | (197) all_190_4 = all_156_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (194), (195) imply: % 28.40/4.56 | | | | | | | (198) all_172_0 = all_103_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (190), (197) imply: % 28.40/4.56 | | | | | | | (199) all_156_0 = all_106_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (162), (197) imply: % 28.40/4.56 | | | | | | | (200) all_188_3 = all_156_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (200) implies: % 28.40/4.56 | | | | | | | (201) all_188_3 = all_156_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (161), (201) imply: % 28.40/4.56 | | | | | | | (202) all_156_0 = all_148_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (202) implies: % 28.40/4.56 | | | | | | | (203) all_156_0 = all_148_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (199), (203) imply: % 28.40/4.56 | | | | | | | (204) all_148_1 = all_106_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (204) implies: % 28.40/4.56 | | | | | | | (205) all_148_1 = all_106_1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (175), (176) imply: % 28.40/4.56 | | | | | | | (206) all_152_1 = 0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | SIMP: (206) implies: % 28.40/4.56 | | | | | | | (207) all_152_1 = 0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (184), (195) imply: % 28.40/4.56 | | | | | | | (208) all_204_6 = all_103_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (172), (208) imply: % 28.40/4.56 | | | | | | | (209) all_206_6 = all_103_0 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (178), (182) imply: % 28.40/4.56 | | | | | | | (210) all_262_4 = vt1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | COMBINE_EQS: (159), (182) imply: % 28.40/4.56 | | | | | | | (211) all_275_7 = vt1 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | REDUCE: (155), (211) imply: % 28.40/4.56 | | | | | | | (212) vreduce(vt1) = all_275_6 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | REDUCE: (145), (210) imply: % 28.40/4.56 | | | | | | | (213) vreduce(vt1) = all_262_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | REDUCE: (138), (156) imply: % 28.40/4.56 | | | | | | | (214) vreduce(vt1) = all_257_3 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | REDUCE: (119), (209) imply: % 28.40/4.56 | | | | | | | (215) visSomeTerm(all_103_0) = all_206_5 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | REDUCE: (115), (208) imply: % 28.40/4.56 | | | | | | | (216) visSomeTerm(all_103_0) = all_204_5 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | REDUCE: (107), (192) imply: % 28.40/4.56 | | | | | | | (217) visSomeTerm(all_103_0) = all_192_2 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | REDUCE: (103), (195) imply: % 28.40/4.56 | | | | | | | (218) visSomeTerm(all_103_0) = all_190_2 % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | BETA: splitting (84) gives: % 28.40/4.56 | | | | | | | % 28.40/4.56 | | | | | | | Case 1: % 28.40/4.56 | | | | | | | | % 28.40/4.56 | | | | | | | | (219) vt1 = vZero % 28.40/4.56 | | | | | | | | % 28.40/4.56 | | | | | | | | REDUCE: (35), (219) imply: % 28.40/4.56 | | | | | | | | (220) $false % 28.40/4.56 | | | | | | | | % 28.40/4.56 | | | | | | | | CLOSE: (220) is inconsistent. % 28.40/4.56 | | | | | | | | % 28.40/4.56 | | | | | | | Case 2: % 28.40/4.56 | | | | | | | | % 28.40/4.57 | | | | | | | | (221) all_106_0 = 0 | ? [v0: vOptTerm] : ? [v1: any] : ? % 28.40/4.57 | | | | | | | | [v2: any] : ? [v3: any] : ? [v4: vOptTerm] : % 28.40/4.57 | | | | | | | | (vptchecksimple(all_118_1, all_106_3) = v3 & % 28.40/4.57 | | | | | | | | vreduce(vt1) = v0 & visSomeTerm(v0) = v1 & % 28.40/4.57 | | | | | | | | visNV(all_106_4) = v2 & vsomeTerm(all_106_2) = v4 & % 28.40/4.57 | | | | | | | | vOptTerm(v4) & vOptTerm(v0) & ( ~ (v4 = all_118_0) | % 28.40/4.57 | | | | | | | | ~ (v3 = 0) | v2 = 0 | v1 = 0)) % 28.40/4.57 | | | | | | | | % 28.40/4.57 | | | | | | | | BETA: splitting (221) gives: % 28.40/4.57 | | | | | | | | % 28.40/4.57 | | | | | | | | Case 1: % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | (222) all_106_0 = 0 % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | REDUCE: (37), (222) imply: % 28.40/4.57 | | | | | | | | | (223) $false % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | CLOSE: (223) is inconsistent. % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | Case 2: % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | (224) ? [v0: vOptTerm] : ? [v1: any] : ? [v2: any] : ? % 28.40/4.57 | | | | | | | | | [v3: any] : ? [v4: vOptTerm] : % 28.40/4.57 | | | | | | | | | (vptchecksimple(all_118_1, all_106_3) = v3 & % 28.40/4.57 | | | | | | | | | vreduce(vt1) = v0 & visSomeTerm(v0) = v1 & % 28.40/4.57 | | | | | | | | | visNV(all_106_4) = v2 & vsomeTerm(all_106_2) = v4 & % 28.40/4.57 | | | | | | | | | vOptTerm(v4) & vOptTerm(v0) & ( ~ (v4 = all_118_0) % 28.40/4.57 | | | | | | | | | | ~ (v3 = 0) | v2 = 0 | v1 = 0)) % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | DELTA: instantiating (224) with fresh symbols all_300_0, % 28.40/4.57 | | | | | | | | | all_300_1, all_300_2, all_300_3, all_300_4 gives: % 28.40/4.57 | | | | | | | | | (225) vptchecksimple(all_118_1, all_106_3) = all_300_1 & % 28.40/4.57 | | | | | | | | | vreduce(vt1) = all_300_4 & visSomeTerm(all_300_4) = % 28.40/4.57 | | | | | | | | | all_300_3 & visNV(all_106_4) = all_300_2 & % 28.40/4.57 | | | | | | | | | vsomeTerm(all_106_2) = all_300_0 & % 28.40/4.57 | | | | | | | | | vOptTerm(all_300_0) & vOptTerm(all_300_4) & ( ~ % 28.40/4.57 | | | | | | | | | (all_300_0 = all_118_0) | ~ (all_300_1 = 0) | % 28.40/4.57 | | | | | | | | | all_300_2 = 0 | all_300_3 = 0) % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | ALPHA: (225) implies: % 28.40/4.57 | | | | | | | | | (226) vsomeTerm(all_106_2) = all_300_0 % 28.40/4.57 | | | | | | | | | (227) visNV(all_106_4) = all_300_2 % 28.40/4.57 | | | | | | | | | (228) visSomeTerm(all_300_4) = all_300_3 % 28.40/4.57 | | | | | | | | | (229) vreduce(vt1) = all_300_4 % 28.40/4.57 | | | | | | | | | (230) vptchecksimple(all_118_1, all_106_3) = all_300_1 % 28.40/4.57 | | | | | | | | | (231) ~ (all_300_0 = all_118_0) | ~ (all_300_1 = 0) | % 28.40/4.57 | | | | | | | | | all_300_2 = 0 | all_300_3 = 0 % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | REDUCE: (58), (82), (230) imply: % 28.40/4.57 | | | | | | | | | (232) vptchecksimple(all_106_6, vB) = all_300_1 % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | BETA: splitting (85) gives: % 28.40/4.57 | | | | | | | | | % 28.40/4.57 | | | | | | | | | Case 1: % 28.40/4.57 | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | (233) vt1 = vZero % 28.40/4.57 | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | REDUCE: (35), (233) imply: % 28.40/4.57 | | | | | | | | | | (234) $false % 28.40/4.57 | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | CLOSE: (234) is inconsistent. % 28.40/4.57 | | | | | | | | | | % 28.40/4.57 | | | | | | | | | Case 2: % 28.40/4.57 | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | (235) all_106_0 = 0 | ? [v0: vOptTerm] : ? [v1: any] : % 28.40/4.57 | | | | | | | | | | ? [v2: any] : ? [v3: any] : ? [v4: vOptTerm] : % 28.40/4.57 | | | | | | | | | | (vptchecksimple(all_115_1, all_106_3) = v3 & % 28.40/4.57 | | | | | | | | | | vreduce(vt1) = v0 & visSomeTerm(v0) = v1 & % 28.40/4.57 | | | | | | | | | | visNV(all_106_4) = v2 & vsomeTerm(all_106_2) = v4 % 28.40/4.57 | | | | | | | | | | & vOptTerm(v4) & vOptTerm(v0) & ( ~ (v4 = % 28.40/4.57 | | | | | | | | | | all_115_0) | ~ (v3 = 0) | ~ (v1 = 0) | v2 = % 28.40/4.57 | | | | | | | | | | 0)) % 28.40/4.57 | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | BETA: splitting (148) gives: % 28.40/4.57 | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | Case 1: % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | (236) all_106_0 = 0 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | REDUCE: (37), (236) imply: % 28.40/4.57 | | | | | | | | | | | (237) $false % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | CLOSE: (237) is inconsistent. % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | Case 2: % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | (238) all_106_1 = 0 | ? [v0: vTerm] : ? [v1: vOptTerm] % 28.40/4.57 | | | | | | | | | | | : ? [v2: any] : ? [v3: any] : ? [v4: vOptTerm] % 28.40/4.57 | | | | | | | | | | | : (vptchecksimple(all_115_1, all_106_3) = v3 & % 28.40/4.57 | | | | | | | | | | | vreduce(v0) = v1 & visSomeTerm(v1) = v2 & % 28.40/4.57 | | | | | | | | | | | vsomeTerm(all_106_2) = v4 & vSucc(all_106_4) = % 28.40/4.57 | | | | | | | | | | | v0 & vOptTerm(v4) & vOptTerm(v1) & vTerm(v0) & ( % 28.40/4.57 | | | | | | | | | | | ~ (v4 = all_115_0) | ~ (v3 = 0) | ~ (v2 = 0) % 28.40/4.57 | | | | | | | | | | | | ~ (v0 = vt1))) % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (26) with all_106_5, all_300_0, % 28.40/4.57 | | | | | | | | | | | all_106_2, simplifying with (43), (226) gives: % 28.40/4.57 | | | | | | | | | | | (239) all_300_0 = all_106_5 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (27) with all_106_1, all_300_2, % 28.40/4.57 | | | | | | | | | | | all_106_4, simplifying with (44), (227) gives: % 28.40/4.57 | | | | | | | | | | | (240) all_300_2 = all_106_1 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (28) with all_190_2, all_192_2, % 28.40/4.57 | | | | | | | | | | | all_103_0, simplifying with (217), (218) gives: % 28.40/4.57 | | | | | | | | | | | (241) all_192_2 = all_190_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (28) with all_170_2, all_206_5, % 28.40/4.57 | | | | | | | | | | | all_103_0, simplifying with (96), (215) gives: % 28.40/4.57 | | | | | | | | | | | (242) all_206_5 = all_170_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (28) with all_204_5, all_206_5, % 28.40/4.57 | | | | | | | | | | | all_103_0, simplifying with (215), (216) gives: % 28.40/4.57 | | | | | | | | | | | (243) all_206_5 = all_204_5 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (28) with all_192_2, all_206_5, % 28.40/4.57 | | | | | | | | | | | all_103_0, simplifying with (215), (217) gives: % 28.40/4.57 | | | | | | | | | | | (244) all_206_5 = all_192_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (29) with all_262_3, all_275_6, vt1, % 28.40/4.57 | | | | | | | | | | | simplifying with (212), (213) gives: % 28.40/4.57 | | | | | | | | | | | (245) all_275_6 = all_262_3 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (29) with all_257_3, all_275_6, vt1, % 28.40/4.57 | | | | | | | | | | | simplifying with (212), (214) gives: % 28.40/4.57 | | | | | | | | | | | (246) all_275_6 = all_257_3 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (29) with all_103_0, all_300_4, vt1, % 28.40/4.57 | | | | | | | | | | | simplifying with (32), (229) gives: % 28.40/4.57 | | | | | | | | | | | (247) all_300_4 = all_103_0 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (29) with all_262_3, all_300_4, vt1, % 28.40/4.57 | | | | | | | | | | | simplifying with (213), (229) gives: % 28.40/4.57 | | | | | | | | | | | (248) all_300_4 = all_262_3 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | GROUND_INST: instantiating (30) with 0, all_300_1, vB, % 28.40/4.57 | | | | | | | | | | | all_106_6, simplifying with (121), (232) gives: % 28.40/4.57 | | | | | | | | | | | (249) all_300_1 = 0 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (247), (248) imply: % 28.40/4.57 | | | | | | | | | | | (250) all_262_3 = all_103_0 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | SIMP: (250) implies: % 28.40/4.57 | | | | | | | | | | | (251) all_262_3 = all_103_0 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (245), (246) imply: % 28.40/4.57 | | | | | | | | | | | (252) all_262_3 = all_257_3 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | SIMP: (252) implies: % 28.40/4.57 | | | | | | | | | | | (253) all_262_3 = all_257_3 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (251), (253) imply: % 28.40/4.57 | | | | | | | | | | | (254) all_257_3 = all_103_0 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (243), (244) imply: % 28.40/4.57 | | | | | | | | | | | (255) all_204_5 = all_192_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (242), (243) imply: % 28.40/4.57 | | | | | | | | | | | (256) all_204_5 = all_170_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (255), (256) imply: % 28.40/4.57 | | | | | | | | | | | (257) all_192_2 = all_170_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | SIMP: (257) implies: % 28.40/4.57 | | | | | | | | | | | (258) all_192_2 = all_170_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (241), (258) imply: % 28.40/4.57 | | | | | | | | | | | (259) all_190_2 = all_170_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | COMBINE_EQS: (246), (254) imply: % 28.40/4.57 | | | | | | | | | | | (260) all_275_6 = all_103_0 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | REDUCE: (228), (247) imply: % 28.40/4.57 | | | | | | | | | | | (261) visSomeTerm(all_103_0) = all_300_3 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | REDUCE: (154), (260) imply: % 28.40/4.57 | | | | | | | | | | | (262) visSomeTerm(all_103_0) = all_275_5 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | REDUCE: (144), (251) imply: % 28.40/4.57 | | | | | | | | | | | (263) visSomeTerm(all_103_0) = all_262_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | REDUCE: (137), (254) imply: % 28.40/4.57 | | | | | | | | | | | (264) visSomeTerm(all_103_0) = all_257_2 % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | BETA: splitting (231) gives: % 28.40/4.57 | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | Case 1: % 28.40/4.57 | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | (265) ~ (all_300_1 = 0) % 28.40/4.57 | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | REDUCE: (249), (265) imply: % 28.40/4.57 | | | | | | | | | | | | (266) $false % 28.40/4.57 | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | CLOSE: (266) is inconsistent. % 28.40/4.57 | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | Case 2: % 28.40/4.57 | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | (267) ~ (all_300_0 = all_118_0) | all_300_2 = 0 | % 28.40/4.57 | | | | | | | | | | | | all_300_3 = 0 % 28.40/4.57 | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | BETA: splitting (267) gives: % 28.40/4.57 | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | Case 1: % 28.40/4.57 | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | | (268) ~ (all_300_0 = all_118_0) % 28.40/4.57 | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | | REDUCE: (62), (239), (268) imply: % 28.40/4.57 | | | | | | | | | | | | | (269) $false % 28.40/4.57 | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | | CLOSE: (269) is inconsistent. % 28.40/4.57 | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | Case 2: % 28.40/4.57 | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | | (270) all_300_2 = 0 | all_300_3 = 0 % 28.40/4.57 | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | | BETA: splitting (270) gives: % 28.40/4.57 | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | | Case 1: % 28.40/4.57 | | | | | | | | | | | | | | % 28.40/4.57 | | | | | | | | | | | | | | (271) all_300_2 = 0 % 28.40/4.57 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | COMBINE_EQS: (240), (271) imply: % 28.40/4.58 | | | | | | | | | | | | | | (272) all_106_1 = 0 % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | REDUCE: (36), (272) imply: % 28.40/4.58 | | | | | | | | | | | | | | (273) $false % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | CLOSE: (273) is inconsistent. % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | Case 2: % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | (274) all_300_3 = 0 % 28.40/4.58 | | | | | | | | | | | | | | (275) ~ (all_300_2 = 0) % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | REDUCE: (261), (274) imply: % 28.40/4.58 | | | | | | | | | | | | | | (276) visSomeTerm(all_103_0) = 0 % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | BETA: splitting (235) gives: % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | Case 1: % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | (277) all_106_0 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | REDUCE: (37), (277) imply: % 28.40/4.58 | | | | | | | | | | | | | | | (278) $false % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | CLOSE: (278) is inconsistent. % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | Case 2: % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | (279) ? [v0: vOptTerm] : ? [v1: any] : ? [v2: any] : % 28.40/4.58 | | | | | | | | | | | | | | | ? [v3: any] : ? [v4: vOptTerm] : % 28.40/4.58 | | | | | | | | | | | | | | | (vptchecksimple(all_115_1, all_106_3) = v3 & % 28.40/4.58 | | | | | | | | | | | | | | | vreduce(vt1) = v0 & visSomeTerm(v0) = v1 & % 28.40/4.58 | | | | | | | | | | | | | | | visNV(all_106_4) = v2 & vsomeTerm(all_106_2) = % 28.40/4.58 | | | | | | | | | | | | | | | v4 & vOptTerm(v4) & vOptTerm(v0) & ( ~ (v4 = % 28.40/4.58 | | | | | | | | | | | | | | | all_115_0) | ~ (v3 = 0) | ~ (v1 = 0) | v2 % 28.40/4.58 | | | | | | | | | | | | | | | = 0)) % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | DELTA: instantiating (279) with fresh symbols all_362_0, % 28.40/4.58 | | | | | | | | | | | | | | | all_362_1, all_362_2, all_362_3, all_362_4 gives: % 28.40/4.58 | | | | | | | | | | | | | | | (280) vptchecksimple(all_115_1, all_106_3) = all_362_1 & % 28.40/4.58 | | | | | | | | | | | | | | | vreduce(vt1) = all_362_4 & visSomeTerm(all_362_4) % 28.40/4.58 | | | | | | | | | | | | | | | = all_362_3 & visNV(all_106_4) = all_362_2 & % 28.40/4.58 | | | | | | | | | | | | | | | vsomeTerm(all_106_2) = all_362_0 & % 28.40/4.58 | | | | | | | | | | | | | | | vOptTerm(all_362_0) & vOptTerm(all_362_4) & ( ~ % 28.40/4.58 | | | | | | | | | | | | | | | (all_362_0 = all_115_0) | ~ (all_362_1 = 0) | % 28.40/4.58 | | | | | | | | | | | | | | | ~ (all_362_3 = 0) | all_362_2 = 0) % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | ALPHA: (280) implies: % 28.40/4.58 | | | | | | | | | | | | | | | (281) vsomeTerm(all_106_2) = all_362_0 % 28.40/4.58 | | | | | | | | | | | | | | | (282) visNV(all_106_4) = all_362_2 % 28.40/4.58 | | | | | | | | | | | | | | | (283) visSomeTerm(all_362_4) = all_362_3 % 28.40/4.58 | | | | | | | | | | | | | | | (284) vreduce(vt1) = all_362_4 % 28.40/4.58 | | | | | | | | | | | | | | | (285) vptchecksimple(all_115_1, all_106_3) = all_362_1 % 28.40/4.58 | | | | | | | | | | | | | | | (286) ~ (all_362_0 = all_115_0) | ~ (all_362_1 = 0) | % 28.40/4.58 | | | | | | | | | | | | | | | ~ (all_362_3 = 0) | all_362_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | REDUCE: (59), (82), (285) imply: % 28.40/4.58 | | | | | | | | | | | | | | | (287) vptchecksimple(all_106_6, vB) = all_362_1 % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | BETA: splitting (238) gives: % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | Case 1: % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | (288) all_106_1 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | REDUCE: (36), (288) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (289) $false % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | CLOSE: (289) is inconsistent. % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | Case 2: % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | (290) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: any] % 28.40/4.58 | | | | | | | | | | | | | | | | : ? [v3: any] : ? [v4: vOptTerm] : % 28.40/4.58 | | | | | | | | | | | | | | | | (vptchecksimple(all_115_1, all_106_3) = v3 & % 28.40/4.58 | | | | | | | | | | | | | | | | vreduce(v0) = v1 & visSomeTerm(v1) = v2 & % 28.40/4.58 | | | | | | | | | | | | | | | | vsomeTerm(all_106_2) = v4 & vSucc(all_106_4) = % 28.40/4.58 | | | | | | | | | | | | | | | | v0 & vOptTerm(v4) & vOptTerm(v1) & vTerm(v0) & ( % 28.40/4.58 | | | | | | | | | | | | | | | | ~ (v4 = all_115_0) | ~ (v3 = 0) | ~ (v2 = 0) % 28.40/4.58 | | | | | | | | | | | | | | | | | ~ (v0 = vt1))) % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | DELTA: instantiating (290) with fresh symbols all_368_0, % 28.40/4.58 | | | | | | | | | | | | | | | | all_368_1, all_368_2, all_368_3, all_368_4 gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (291) vptchecksimple(all_115_1, all_106_3) = all_368_1 & % 28.40/4.58 | | | | | | | | | | | | | | | | vreduce(all_368_4) = all_368_3 & % 28.40/4.58 | | | | | | | | | | | | | | | | visSomeTerm(all_368_3) = all_368_2 & % 28.40/4.58 | | | | | | | | | | | | | | | | vsomeTerm(all_106_2) = all_368_0 & % 28.40/4.58 | | | | | | | | | | | | | | | | vSucc(all_106_4) = all_368_4 & vOptTerm(all_368_0) % 28.40/4.58 | | | | | | | | | | | | | | | | & vOptTerm(all_368_3) & vTerm(all_368_4) & ( ~ % 28.40/4.58 | | | | | | | | | | | | | | | | (all_368_0 = all_115_0) | ~ (all_368_1 = 0) | % 28.40/4.58 | | | | | | | | | | | | | | | | ~ (all_368_2 = 0) | ~ (all_368_4 = vt1)) % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | ALPHA: (291) implies: % 28.40/4.58 | | | | | | | | | | | | | | | | (292) vsomeTerm(all_106_2) = all_368_0 % 28.40/4.58 | | | | | | | | | | | | | | | | (293) vptchecksimple(all_115_1, all_106_3) = all_368_1 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | REDUCE: (59), (82), (293) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (294) vptchecksimple(all_106_6, vB) = all_368_1 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_106_5, all_368_0, % 28.40/4.58 | | | | | | | | | | | | | | | | all_106_2, simplifying with (43), (292) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (295) all_368_0 = all_106_5 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (26) with all_362_0, all_368_0, % 28.40/4.58 | | | | | | | | | | | | | | | | all_106_2, simplifying with (281), (292) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (296) all_368_0 = all_362_0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with all_106_1, all_362_2, % 28.40/4.58 | | | | | | | | | | | | | | | | all_106_4, simplifying with (44), (282) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (297) all_362_2 = all_106_1 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with all_170_2, all_262_2, % 28.40/4.58 | | | | | | | | | | | | | | | | all_103_0, simplifying with (96), (263) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (298) all_262_2 = all_170_2 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with all_257_2, all_262_2, % 28.40/4.58 | | | | | | | | | | | | | | | | all_103_0, simplifying with (263), (264) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (299) all_262_2 = all_257_2 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with all_257_2, all_275_5, % 28.40/4.58 | | | | | | | | | | | | | | | | all_103_0, simplifying with (262), (264) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (300) all_275_5 = all_257_2 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with 0, all_275_5, all_103_0, % 28.40/4.58 | | | | | | | | | | | | | | | | simplifying with (262), (276) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (301) all_275_5 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (29) with all_103_0, all_362_4, vt1, % 28.40/4.58 | | | | | | | | | | | | | | | | simplifying with (32), (284) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (302) all_362_4 = all_103_0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (30) with 0, all_368_1, vB, % 28.40/4.58 | | | | | | | | | | | | | | | | all_106_6, simplifying with (121), (294) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (303) all_368_1 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (30) with all_362_1, all_368_1, vB, % 28.40/4.58 | | | | | | | | | | | | | | | | all_106_6, simplifying with (287), (294) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | (304) all_368_1 = all_362_1 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | COMBINE_EQS: (295), (296) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (305) all_362_0 = all_106_5 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | COMBINE_EQS: (303), (304) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (306) all_362_1 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | COMBINE_EQS: (300), (301) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (307) all_257_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | SIMP: (307) implies: % 28.40/4.58 | | | | | | | | | | | | | | | | (308) all_257_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | COMBINE_EQS: (298), (299) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (309) all_257_2 = all_170_2 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | SIMP: (309) implies: % 28.40/4.58 | | | | | | | | | | | | | | | | (310) all_257_2 = all_170_2 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | COMBINE_EQS: (308), (310) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (311) all_170_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | SIMP: (311) implies: % 28.40/4.58 | | | | | | | | | | | | | | | | (312) all_170_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | REDUCE: (283), (302) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | (313) visSomeTerm(all_103_0) = all_362_3 % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | BETA: splitting (286) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | Case 1: % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | (314) ~ (all_362_1 = 0) % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | REDUCE: (306), (314) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | | (315) $false % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | CLOSE: (315) is inconsistent. % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | Case 2: % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | (316) ~ (all_362_0 = all_115_0) | ~ (all_362_3 = 0) | % 28.40/4.58 | | | | | | | | | | | | | | | | | all_362_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | BETA: splitting (316) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | Case 1: % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | (317) ~ (all_362_3 = 0) % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (28) with 0, all_362_3, all_103_0, % 28.40/4.58 | | | | | | | | | | | | | | | | | | simplifying with (276), (313) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | | | (318) all_362_3 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | REDUCE: (317), (318) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | | | (319) $false % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | CLOSE: (319) is inconsistent. % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | Case 2: % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | (320) ~ (all_362_0 = all_115_0) | all_362_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | BETA: splitting (320) gives: % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | Case 1: % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | (321) ~ (all_362_0 = all_115_0) % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | REDUCE: (64), (305), (321) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | | | | (322) $false % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | CLOSE: (322) is inconsistent. % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | Case 2: % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | (323) all_362_2 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (297), (323) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | | | | (324) all_106_1 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | SIMP: (324) implies: % 28.40/4.58 | | | | | | | | | | | | | | | | | | | (325) all_106_1 = 0 % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | REDUCE: (36), (325) imply: % 28.40/4.58 | | | | | | | | | | | | | | | | | | | (326) $false % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | | CLOSE: (326) is inconsistent. % 28.40/4.58 | | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | | % 28.40/4.58 | | | | | | | | | | | End of split % 28.40/4.58 | | | | | | | | | | | % 28.40/4.59 | | | | | | | | | | End of split % 28.40/4.59 | | | | | | | | | | % 28.40/4.59 | | | | | | | | | End of split % 28.40/4.59 | | | | | | | | | % 28.40/4.59 | | | | | | | | End of split % 28.40/4.59 | | | | | | | | % 28.40/4.59 | | | | | | | End of split % 28.40/4.59 | | | | | | | % 28.40/4.59 | | | | | | End of split % 28.40/4.59 | | | | | | % 28.40/4.59 | | | | | End of split % 28.40/4.59 | | | | | % 28.40/4.59 | | | | End of split % 28.40/4.59 | | | | % 28.40/4.59 | | | End of split % 28.40/4.59 | | | % 28.40/4.59 | | End of split % 28.40/4.59 | | % 28.40/4.59 | End of split % 28.40/4.59 | % 28.40/4.59 End of proof % 28.40/4.59 % SZS output end Proof for theBenchmark % 28.40/4.59 % 28.40/4.59 3958ms %------------------------------------------------------------------------------