%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM225_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 : n012.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:36 PM UTC 2026 % Result : Theorem 32.45s 4.95s % Output : Proof 89.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : COM225_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.09/0.24 % Computer : n012.cluster.edu % 0.09/0.24 % Model : x86_64 x86_64 % 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.24 % Memory : 8042.1875MB % 0.09/0.24 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.25 % CPULimit : 300 % 0.09/0.25 % WCLimit : 300 % 0.09/0.25 % DateTime : Mon May 4 19:08:00 EDT 2026 % 0.09/0.25 % CPUTime : % 0.17/0.43 ________ _____ % 0.17/0.43 ___ __ \_________(_)________________________________ % 0.17/0.43 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.17/0.43 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.17/0.43 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.17/0.43 % 0.17/0.43 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.17/0.43 (2023-06-19) % 0.17/0.43 % 0.17/0.43 (c) Philipp Rümmer, 2009-2023 % 0.17/0.43 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.17/0.43 Amanda Stjerna. % 0.17/0.43 Free software under BSD-3-Clause. % 0.17/0.43 % 0.17/0.43 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.17/0.43 % 0.17/0.43 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.37/0.44 Running up to 7 provers in parallel. % 0.37/0.45 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.37/0.45 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.37/0.45 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.37/0.45 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.37/0.45 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.37/0.45 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.37/0.45 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.03/1.19 Prover 1: Preprocessing ... % 4.57/1.23 Prover 4: Preprocessing ... % 4.57/1.27 Prover 5: Preprocessing ... % 4.57/1.27 Prover 2: Preprocessing ... % 4.57/1.29 Prover 3: Preprocessing ... % 4.57/1.29 Prover 6: Preprocessing ... % 4.57/1.29 Prover 0: Preprocessing ... % 11.82/2.28 Prover 1: Warning: ignoring some quantifiers % 12.59/2.32 Prover 3: Warning: ignoring some quantifiers % 12.59/2.36 Prover 1: Constructing countermodel ... % 12.59/2.37 Prover 3: Constructing countermodel ... % 12.59/2.37 Prover 6: Proving ... % 14.12/2.51 Prover 5: Proving ... % 14.12/2.53 Prover 4: Warning: ignoring some quantifiers % 14.12/2.58 Prover 0: Proving ... % 14.82/2.62 Prover 4: Constructing countermodel ... % 15.59/2.79 Prover 2: Proving ... % 32.45/4.95 Prover 0: proved (4493ms) % 32.45/4.95 % 32.45/4.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.45/4.95 % 32.45/4.96 Prover 2: stopped % 32.45/4.96 Prover 5: stopped % 32.45/4.96 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 32.45/4.96 Prover 6: stopped % 32.45/4.96 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 32.45/4.97 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 32.45/4.97 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 33.27/5.02 Prover 3: stopped % 33.27/5.02 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 34.07/5.17 Prover 13: Preprocessing ... % 34.71/5.20 Prover 7: Preprocessing ... % 34.71/5.20 Prover 8: Preprocessing ... % 34.71/5.20 Prover 11: Preprocessing ... % 34.71/5.21 Prover 10: Preprocessing ... % 36.29/5.45 Prover 8: Warning: ignoring some quantifiers % 36.29/5.48 Prover 8: Constructing countermodel ... % 37.05/5.51 Prover 10: Warning: ignoring some quantifiers % 37.05/5.52 Prover 7: Warning: ignoring some quantifiers % 37.05/5.52 Prover 10: Constructing countermodel ... % 37.05/5.53 Prover 7: Constructing countermodel ... % 37.05/5.59 Prover 11: Warning: ignoring some quantifiers % 37.85/5.60 Prover 11: Constructing countermodel ... % 37.85/5.63 Prover 13: Warning: ignoring some quantifiers % 37.85/5.67 Prover 13: Constructing countermodel ... % 72.25/10.05 Prover 13: stopped % 72.25/10.06 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 73.67/10.24 Prover 16: Preprocessing ... % 75.27/10.42 Prover 16: Warning: ignoring some quantifiers % 75.27/10.45 Prover 16: Constructing countermodel ... % 88.62/12.19 Prover 16: Found proof (size 123) % 88.62/12.19 Prover 16: proved (2129ms) % 88.62/12.20 Prover 4: stopped % 88.62/12.20 Prover 10: stopped % 88.62/12.20 Prover 8: stopped % 89.29/12.20 Prover 7: stopped % 89.29/12.20 Prover 1: stopped % 89.29/12.22 Prover 11: stopped % 89.29/12.22 % 89.29/12.22 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 89.29/12.22 % 89.29/12.23 % SZS output start Proof for theBenchmark % 89.29/12.23 Assumptions after simplification: % 89.29/12.23 --------------------------------- % 89.29/12.23 % 89.29/12.23 (EQ-someTerm) % 89.29/12.25 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : (v1 = v0 | ~ % 89.29/12.25 (vsomeTerm(v1) = v2) | ~ (vsomeTerm(v0) = v2) | ~ vTerm(v1) | ~ % 89.29/12.25 vTerm(v0)) % 89.29/12.25 % 89.29/12.26 (Preservation-Pred-IH0) % 89.29/12.26 vTerm(vt1) & ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: % 89.29/12.26 vTy] : ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ % 89.29/12.26 vTerm(v2) | ~ vptchecksimple(vt1, v1) | vptchecksimple(v2, v1))) % 89.29/12.26 % 89.29/12.26 (Preservation-Pred-t1) % 89.29/12.26 vTerm(vt1) & vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTy] % 89.29/12.26 : ? [v3: vTerm] : ( ~ (vt1 = vZero) & vreduce(v0) = v1 & vsomeTerm(v3) = v1 & % 89.29/12.26 vPred(vt1) = v0 & vTy(v2) & vOptTerm(v1) & vTerm(v3) & vTerm(v0) & % 89.29/12.26 vptchecksimple(v0, v2) & ~ vptchecksimple(v3, v2) & ! [v4: vTerm] : ( ~ % 89.29/12.26 (vSucc(v4) = vt1) | ~ vTerm(v4))) % 89.29/12.26 % 89.29/12.26 (Preservation-Pred-t1-isSomeTerm-False) % 89.29/12.26 vTerm(vt1) & vTerm(vZero) & ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: % 89.29/12.26 vOptTerm] : (vreduce(v1) = v2 & vreduce(vt1) = v0 & vPred(vt1) = v1 & % 89.29/12.26 vOptTerm(v2) & vOptTerm(v0) & vTerm(v1) & ! [v3: vTy] : ! [v4: vTerm] : % 89.29/12.26 (vt1 = vZero | ~ (vsomeTerm(v4) = v2) | ~ vTy(v3) | ~ vTerm(v4) | ~ % 89.29/12.26 vptchecksimple(v1, v3) | vptchecksimple(v4, v3) | visSomeTerm(v0) | ? % 89.29/12.26 [v5: vTerm] : (vSucc(v5) = vt1 & vTerm(v5)))) % 89.29/12.26 % 89.29/12.26 (Preservation-Pred-t1-isSomeTerm-True) % 89.29/12.26 vTerm(vt1) & vTerm(vZero) & ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: % 89.29/12.26 vOptTerm] : (vreduce(v1) = v2 & vreduce(vt1) = v0 & vPred(vt1) = v1 & % 89.29/12.26 vOptTerm(v2) & vOptTerm(v0) & vTerm(v1) & ! [v3: vTy] : ! [v4: vTerm] : % 89.29/12.26 (vt1 = vZero | ~ (vsomeTerm(v4) = v2) | ~ vTy(v3) | ~ vTerm(v4) | ~ % 89.29/12.26 vptchecksimple(v1, v3) | ~ visSomeTerm(v0) | vptchecksimple(v4, v3) | ? % 89.29/12.26 [v5: vTerm] : (vSucc(v5) = vt1 & vTerm(v5)))) % 89.29/12.26 % 89.29/12.26 (TPred_inv2) % 89.29/12.26 vTy(vNat) & ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vNat | ~ % 89.29/12.26 (vPred(v0) = v2) | ~ vTy(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, v1)) % 89.29/12.27 % 89.29/12.27 (TZero) % 89.29/12.27 vTy(vNat) & vTerm(vZero) & vptchecksimple(vZero, vNat) % 89.29/12.27 % 89.29/12.27 (isSomeTerm-0) % 89.29/12.27 vOptTerm(vnoTerm) & ~ visSomeTerm(vnoTerm) % 89.29/12.27 % 89.29/12.27 (isSomeTerm-1) % 89.29/12.27 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vsomeTerm(v0) = v1) | ~ vTerm(v0) | % 89.29/12.27 visSomeTerm(v1)) % 89.29/12.27 % 89.29/12.27 (reduce-10) % 89.29/12.27 vTerm(vZero) & ! [v0: vTerm] : ! [v1: vTerm] : (v0 = vZero | ~ (vPred(v0) = % 89.29/12.27 v1) | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: vOptTerm] : ? [v4: % 89.29/12.27 vTerm] : ? [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 89.29/12.27 vTerm] : (vTerm(v7) & ((v8 = v0 & vSucc(v7) = v0) | (vreduce(v0) = v2 & % 89.29/12.27 vOptTerm(v2) & ( ~ visSomeTerm(v2) | (v6 = v3 & vreduce(v1) = v3 & % 89.29/12.27 vgetTerm(v2) = v4 & vsomeTerm(v5) = v3 & vPred(v4) = v5 & % 89.29/12.27 vOptTerm(v3) & vTerm(v5) & vTerm(v4))))))) % 89.29/12.27 % 89.29/12.27 (reduce-11) % 89.29/12.27 vOptTerm(vnoTerm) & vTerm(vZero) & ! [v0: vTerm] : ! [v1: vTerm] : (v0 = % 89.29/12.27 vZero | ~ (vPred(v0) = v1) | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: % 89.29/12.27 vOptTerm] : ? [v4: vTerm] : ? [v5: vTerm] : (vTerm(v4) & ((v5 = v0 & % 89.29/12.27 vSucc(v4) = v0) | (v3 = vnoTerm & vreduce(v1) = vnoTerm) | % 89.29/12.27 (vreduce(v0) = v2 & vOptTerm(v2) & visSomeTerm(v2))))) % 89.29/12.27 % 89.29/12.27 (reduce-6) % 89.29/12.27 vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 89.29/12.27 vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 89.29/12.27 % 89.29/12.27 (reduce-INV) % 89.29/12.29 vOptTerm(vnoTerm) & vTerm(vFalse) & vTerm(vTrue) & vTerm(vZero) & ? [v0: % 89.29/12.29 vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 89.29/12.29 vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 89.29/12.29 vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 89.29/12.29 vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & ? [v5: % 89.29/12.29 vTerm] : ( ~ vTerm(v5) | ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 89.29/12.29 vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: vOptTerm] : ? % 89.29/12.29 [v12: vTerm] : ? [v13: vTerm] : ? [v14: vTerm] : ? [v15: vOptTerm] : ? % 89.29/12.29 [v16: vOptTerm] : ? [v17: vTerm] : ? [v18: vTerm] : ? [v19: vTerm] : ? % 89.29/12.29 [v20: vOptTerm] : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : % 89.29/12.29 ? [v24: vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 89.29/12.29 ? [v28: vOptTerm] : ? [v29: vOptTerm] : ? [v30: vTerm] : ? [v31: % 89.29/12.29 vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: vTerm] : ? % 89.29/12.29 [v35: vTerm] : ? [v36: vTerm] : ? [v37: vTerm] : ? [v38: vOptTerm] : ? % 89.29/12.29 [v39: vTerm] : ? [v40: vOptTerm] : ? [v41: vOptTerm] : ? [v42: vTerm] : % 89.29/12.29 ? [v43: vTerm] : ? [v44: vOptTerm] : ? [v45: vOptTerm] : ? [v46: % 89.29/12.29 vTerm] : ? [v47: vTerm] : ? [v48: vTerm] : ? [v49: vOptTerm] : ? % 89.29/12.29 [v50: vTerm] : ? [v51: vOptTerm] : ? [v52: vTerm] : ? [v53: vOptTerm] : % 89.29/12.29 ? [v54: vTerm] : ? [v55: vTerm] : ? [v56: vOptTerm] : ? [v57: vTerm] : % 89.29/12.29 ? [v58: vOptTerm] : ? [v59: vTerm] : ? [v60: vTerm] : ? [v61: vTerm] : % 89.29/12.29 ? [v62: vOptTerm] : ? [v63: vTerm] : ? [v64: vTerm] : ? [v65: vTerm] : % 89.29/12.29 ? [v66: vTerm] : ? [v67: vOptTerm] : ? [v68: vOptTerm] : ? [v69: % 89.29/12.29 vTerm] : ? [v70: vTerm] : ? [v71: vOptTerm] : ? [v72: vOptTerm] : ? % 89.29/12.29 [v73: vTerm] : ? [v74: vTerm] : ? [v75: vTerm] : ? [v76: vOptTerm] : ? % 89.29/12.29 [v77: vTerm] : ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: vOptTerm] : % 89.29/12.29 ? [v81: vTerm] : ? [v82: vTerm] : ? [v83: vOptTerm] : ? [v84: vTerm] : % 89.29/12.29 ? [v85: vOptTerm] : ? [v86: vTerm] : ? [v87: vTerm] : ? [v88: vTerm] : % 89.29/12.29 ? [v89: vOptTerm] : ? [v90: vTerm] : ? [v91: vTerm] : ? [v92: vTerm] : % 89.29/12.29 ? [v93: vOptTerm] : ? [v94: vTerm] : ? [v95: vOptTerm] : ? [v96: % 89.29/12.29 vOptTerm] : ? [v97: vTerm] : ? [v98: vTerm] : ? [v99: vOptTerm] : ? % 89.29/12.29 [v100: vOptTerm] : ? [v101: vTerm] : ? [v102: vTerm] : ? [v103: vTerm] % 89.29/12.29 : ? [v104: vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: % 89.29/12.29 vTerm] : ? [v108: vOptTerm] : ? [v109: vOptTerm] : ? [v110: vTerm] : % 89.29/12.29 ? [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : ? [v114: % 89.29/12.29 vOptTerm] : ? [v115: vOptTerm] : ? [v116: vTerm] : ? [v117: vTerm] : % 89.29/12.29 ? [v118: vTerm] : ? [v119: vOptTerm] : ? [v120: vTerm] : ? [v121: % 89.29/12.29 vTerm] : ? [v122: vTerm] : ? [v123: vOptTerm] : ? [v124: vTerm] : ? % 89.29/12.29 [v125: vTerm] : ? [v126: vTerm] : ? [v127: vOptTerm] : (vreduce(v5) = v6 % 89.29/12.29 & vOptTerm(v114) & vOptTerm(v108) & vOptTerm(v99) & vOptTerm(v95) & % 89.29/12.29 vOptTerm(v83) & vOptTerm(v78) & vOptTerm(v71) & vOptTerm(v67) & % 89.29/12.29 vOptTerm(v56) & vOptTerm(v51) & vOptTerm(v44) & vOptTerm(v40) & % 89.29/12.29 vOptTerm(v28) & vOptTerm(v23) & vOptTerm(v15) & vOptTerm(v10) & % 89.29/12.29 vOptTerm(v6) & vTerm(v125) & vTerm(v124) & vTerm(v121) & vTerm(v120) & % 89.29/12.29 vTerm(v113) & vTerm(v112) & vTerm(v111) & vTerm(v107) & vTerm(v106) & % 89.29/12.29 vTerm(v105) & vTerm(v98) & vTerm(v94) & vTerm(v90) & vTerm(v82) & % 89.29/12.29 vTerm(v77) & vTerm(v70) & vTerm(v66) & vTerm(v63) & vTerm(v55) & % 89.29/12.29 vTerm(v50) & vTerm(v43) & vTerm(v39) & vTerm(v35) & vTerm(v34) & % 89.29/12.29 vTerm(v27) & vTerm(v26) & vTerm(v22) & vTerm(v21) & vTerm(v14) & % 89.29/12.29 vTerm(v13) & vTerm(v9) & vTerm(v8) & vTerm(v7) & ((v127 = v6 & v126 = v5 % 89.29/12.29 & vsomeTerm(v124) = v6 & vIfelse(vTrue, v124, v125) = v5) | (v123 = % 89.29/12.29 v6 & v122 = v5 & vsomeTerm(v121) = v6 & vIfelse(vFalse, v120, v121) % 89.29/12.29 = v5) | (v119 = v6 & v116 = v5 & v115 = v114 & ~ (v111 = vFalse) & % 89.29/12.29 ~ (v111 = vTrue) & vreduce(v111) = v114 & vgetTerm(v114) = v117 & % 89.29/12.29 vsomeTerm(v118) = v6 & vIfelse(v117, v112, v113) = v118 & % 89.29/12.29 vIfelse(v111, v112, v113) = v5 & vTerm(v118) & vTerm(v117) & % 89.29/12.29 visSomeTerm(v114)) | (v110 = v5 & v109 = v108 & v6 = vnoTerm & ~ % 89.29/12.29 (v105 = vFalse) & ~ (v105 = vTrue) & vreduce(v105) = v108 & % 89.29/12.29 vIfelse(v105, v106, v107) = v5 & ~ visSomeTerm(v108)) | (v104 = v6 % 89.29/12.29 & v101 = v5 & v100 = v99 & vreduce(v98) = v99 & vgetTerm(v99) = v102 % 89.29/12.29 & vsomeTerm(v103) = v6 & vSucc(v102) = v103 & vSucc(v98) = v5 & % 89.29/12.29 vTerm(v103) & vTerm(v102) & visSomeTerm(v99)) | (v97 = v5 & v96 = % 89.29/12.29 v95 & v6 = vnoTerm & vreduce(v94) = v95 & vSucc(v94) = v5 & ~ % 89.29/12.29 visSomeTerm(v95)) | (v93 = v6 & v92 = v5 & vsomeTerm(v90) = v6 & % 89.29/12.29 vPred(v91) = v5 & vSucc(v90) = v91 & vTerm(v91) & visNV(v90)) | (v89 % 89.29/12.29 = v6 & v86 = v5 & v85 = v83 & vreduce(v84) = v83 & vgetTerm(v83) = % 89.29/12.29 v87 & vsomeTerm(v88) = v6 & vPred(v87) = v88 & vPred(v84) = v5 & % 89.29/12.29 vSucc(v82) = v84 & vTerm(v88) & vTerm(v87) & vTerm(v84) & % 89.29/12.29 visSomeTerm(v83) & ~ visNV(v82)) | (v81 = v5 & v80 = v78 & v6 = % 89.29/12.29 vnoTerm & vreduce(v79) = v78 & vPred(v79) = v5 & vSucc(v77) = v79 & % 89.29/12.29 vTerm(v79) & ~ visSomeTerm(v78) & ~ visNV(v77)) | (v76 = v6 & v73 % 89.29/12.29 = v5 & v72 = v71 & ~ (v70 = vZero) & vreduce(v70) = v71 & % 89.29/12.29 vgetTerm(v71) = v74 & vsomeTerm(v75) = v6 & vPred(v74) = v75 & % 89.29/12.29 vPred(v70) = v5 & vTerm(v75) & vTerm(v74) & visSomeTerm(v71) & ! % 89.29/12.29 [v128: vTerm] : ( ~ (vSucc(v128) = v70) | ~ vTerm(v128))) | (v69 = % 89.29/12.29 v5 & v68 = v67 & v6 = vnoTerm & ~ (v66 = vZero) & vreduce(v66) = % 89.29/12.29 v67 & vPred(v66) = v5 & ~ visSomeTerm(v67) & ! [v128: vTerm] : ( ~ % 89.29/12.29 (vSucc(v128) = v66) | ~ vTerm(v128))) | (v65 = v5 & v6 = v4 & % 89.29/12.29 vIszero(v64) = v5 & vSucc(v63) = v64 & vTerm(v64) & visNV(v63)) | % 89.29/12.29 (v62 = v6 & v59 = v5 & v58 = v56 & vreduce(v57) = v56 & vgetTerm(v56) % 89.29/12.29 = v60 & vsomeTerm(v61) = v6 & vIszero(v60) = v61 & vIszero(v57) = v5 % 89.29/12.29 & vSucc(v55) = v57 & vTerm(v61) & vTerm(v60) & vTerm(v57) & % 89.29/12.29 visSomeTerm(v56) & ~ visNV(v55)) | (v54 = v5 & v53 = v51 & v6 = % 89.29/12.29 vnoTerm & vreduce(v52) = v51 & vIszero(v52) = v5 & vSucc(v50) = v52 % 89.29/12.29 & vTerm(v52) & ~ visSomeTerm(v51) & ~ visNV(v50)) | (v49 = v6 & % 89.29/12.29 v46 = v5 & v45 = v44 & ~ (v43 = vZero) & vreduce(v43) = v44 & % 89.29/12.29 vgetTerm(v44) = v47 & vsomeTerm(v48) = v6 & vIszero(v47) = v48 & % 89.29/12.29 vIszero(v43) = v5 & vTerm(v48) & vTerm(v47) & visSomeTerm(v44) & ! % 89.29/12.29 [v128: vTerm] : ( ~ (vSucc(v128) = v43) | ~ vTerm(v128))) | (v42 = % 89.29/12.29 v5 & v41 = v40 & v6 = vnoTerm & ~ (v39 = vZero) & vreduce(v39) = % 89.29/12.29 v40 & vIszero(v39) = v5 & ~ visSomeTerm(v40) & ! [v128: vTerm] : ( % 89.29/12.29 ~ (vSucc(v128) = v39) | ~ vTerm(v128))) | (v38 = v6 & v36 = v5 & % 89.29/12.29 vplusop(v34, v35) = v37 & vsomeTerm(v37) = v6 & vPlus(v34, v35) = v5 % 89.29/12.29 & vTerm(v37) & visNV(v35) & visNV(v34)) | (v33 = v6 & v30 = v5 & v29 % 89.29/12.29 = v28 & vreduce(v27) = v28 & vgetTerm(v28) = v31 & vsomeTerm(v32) = % 89.29/12.29 v6 & vPlus(v26, v31) = v32 & vPlus(v26, v27) = v5 & vTerm(v32) & % 89.29/12.29 vTerm(v31) & visSomeTerm(v28) & visNV(v26) & ~ visNV(v27)) | (v25 = % 89.29/12.29 v5 & v24 = v23 & v6 = vnoTerm & vreduce(v22) = v23 & vPlus(v21, v22) % 89.29/12.29 = v5 & visNV(v21) & ~ visSomeTerm(v23) & ~ visNV(v22)) | (v20 = v6 % 89.29/12.29 & v17 = v5 & v16 = v15 & vreduce(v13) = v15 & vgetTerm(v15) = v18 & % 89.29/12.29 vsomeTerm(v19) = v6 & vPlus(v18, v14) = v19 & vPlus(v13, v14) = v5 & % 89.29/12.29 vTerm(v19) & vTerm(v18) & visSomeTerm(v15) & ~ visNV(v13)) | (v12 = % 89.29/12.29 v5 & v11 = v10 & v6 = vnoTerm & vreduce(v8) = v10 & vPlus(v8, v9) = % 89.29/12.29 v5 & ~ visSomeTerm(v10) & ~ visNV(v8)) | (v7 = v5 & v6 = vnoTerm & % 89.29/12.29 ~ (v5 = v2) & ~ (v5 = v0) & ! [v128: vTerm] : ! [v129: vTerm] : % 89.29/12.29 ! [v130: vTerm] : ( ~ (vIfelse(v128, v129, v130) = v5) | ~ % 89.29/12.29 vTerm(v130) | ~ vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] % 89.29/12.29 : ! [v129: vTerm] : ( ~ (vPlus(v128, v129) = v5) | ~ vTerm(v129) | % 89.29/12.29 ~ vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 89.29/12.29 (vSucc(v128) = v129) | ~ vTerm(v128) | ? [v130: vTerm] : ( ~ % 89.29/12.29 (v130 = v5) & vIszero(v129) = v130 & vTerm(v130))) & ! [v128: % 89.29/12.29 vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = v129) | ~ % 89.29/12.29 vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = v5) & vPred(v129) = % 89.29/12.29 v130 & vTerm(v130))) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 89.29/12.29 (vIfelse(vFalse, v128, v129) = v5) | ~ vTerm(v129) | ~ % 89.29/12.29 vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 89.29/12.29 (vIfelse(vTrue, v128, v129) = v5) | ~ vTerm(v129) | ~ % 89.29/12.29 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vIszero(v128) = v5) | ~ % 89.29/12.29 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vPred(v128) = v5) | ~ % 89.29/12.29 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vSucc(v128) = v5) | ~ % 89.29/12.29 vTerm(v128))) | (v6 = v3 & v5 = v2) | (v6 = v1 & v5 = v0))))) % 89.29/12.29 % 89.29/12.29 (function-axioms) % 89.29/12.29 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 89.29/12.29 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 89.29/12.29 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] % 89.29/12.30 : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ (vplusop(v3, v2) = v0)) & ! [v0: % 89.29/12.30 vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ % 89.29/12.30 (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) & ! [v0: vOptTerm] : ! % 89.29/12.30 [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vreduce(v2) = v1) | ~ % 89.29/12.30 (vreduce(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 89.29/12.30 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 89.29/12.30 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 89.29/12.30 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 89.29/12.30 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 89.29/12.30 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 89.29/12.30 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 89.29/12.30 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 89.29/12.30 % 89.29/12.30 Further assumptions not needed in the proof: % 89.29/12.30 -------------------------------------------- % 89.29/12.30 DIFF-B-Nat, DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, % 89.29/12.30 DIFF-False-Pred, DIFF-False-Succ, DIFF-False-Zero, DIFF-Ifelse-Iszero, % 89.29/12.30 DIFF-Ifelse-Plus, DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, % 89.29/12.30 DIFF-Iszero-Plus, DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, % 89.29/12.30 DIFF-Succ-Plus, DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, % 89.29/12.30 DIFF-True-Iszero, DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, % 89.29/12.30 DIFF-True-Zero, DIFF-Zero-Iszero, DIFF-Zero-Plus, DIFF-Zero-Pred, % 89.29/12.30 DIFF-Zero-Succ, DIFF-noTerm-someTerm, EQ-Ifelse, EQ-Iszero, EQ-Plus, EQ-Pred, % 89.29/12.30 EQ-Succ, TPlus, TPlus_inv0, TPlus_inv1, TPlus_inv2, TPred, TPred_inv1, TSucc, % 89.29/12.30 TSucc_inv1, TSucc_inv2, TZero_inv, Tfalse, Tif, Tif_inv1, Tif_inv2, Tif_inv3, % 89.29/12.30 Tiszero, Tiszero_inv1, Tiszero_inv2, Ttrue, dom-OptTerm, dom-Term, dom-Ty, % 89.29/12.30 getTerm-0, isNV-0, isNV-1, isNV-2, isNV-false-INV, isNV-true-INV, % 89.29/12.30 isSomeTerm-false-INV, isSomeTerm-true-INV, isValue-0, isValue-1, isValue-2, % 89.29/12.30 isValue-false-INV, isValue-true-INV, plusop-0, plusop-1, plusop-2, plusop-INV, % 89.29/12.30 reduce-0, reduce-1, reduce-12, reduce-13, reduce-14, reduce-15, reduce-16, % 89.29/12.30 reduce-17, reduce-18, reduce-19, reduce-2, reduce-20, reduce-21, reduce-22, % 89.29/12.30 reduce-23, reduce-3, reduce-4, reduce-5, reduce-7, reduce-8, reduce-9 % 89.29/12.30 % 89.29/12.30 Those formulas are unsatisfiable: % 89.29/12.30 --------------------------------- % 89.29/12.30 % 89.29/12.30 Begin of proof % 89.74/12.30 | % 89.74/12.30 | ALPHA: (isSomeTerm-0) implies: % 89.74/12.30 | (1) ~ visSomeTerm(vnoTerm) % 89.74/12.30 | % 89.74/12.30 | ALPHA: (reduce-6) implies: % 89.74/12.30 | (2) ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 89.74/12.30 | vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 89.74/12.30 | % 89.74/12.30 | ALPHA: (reduce-10) implies: % 89.74/12.30 | (3) ! [v0: vTerm] : ! [v1: vTerm] : (v0 = vZero | ~ (vPred(v0) = v1) | % 89.74/12.30 | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: vOptTerm] : ? [v4: vTerm] % 89.74/12.30 | : ? [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 89.74/12.30 | vTerm] : (vTerm(v7) & ((v8 = v0 & vSucc(v7) = v0) | (vreduce(v0) = % 89.74/12.30 | v2 & vOptTerm(v2) & ( ~ visSomeTerm(v2) | (v6 = v3 & % 89.74/12.30 | vreduce(v1) = v3 & vgetTerm(v2) = v4 & vsomeTerm(v5) = v3 & % 89.74/12.30 | vPred(v4) = v5 & vOptTerm(v3) & vTerm(v5) & vTerm(v4))))))) % 89.74/12.30 | % 89.74/12.30 | ALPHA: (reduce-11) implies: % 89.74/12.30 | (4) ! [v0: vTerm] : ! [v1: vTerm] : (v0 = vZero | ~ (vPred(v0) = v1) | % 89.74/12.30 | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: vOptTerm] : ? [v4: vTerm] % 89.74/12.30 | : ? [v5: vTerm] : (vTerm(v4) & ((v5 = v0 & vSucc(v4) = v0) | (v3 = % 89.74/12.30 | vnoTerm & vreduce(v1) = vnoTerm) | (vreduce(v0) = v2 & % 89.74/12.30 | vOptTerm(v2) & visSomeTerm(v2))))) % 89.74/12.30 | % 89.74/12.30 | ALPHA: (reduce-INV) implies: % 89.74/12.32 | (5) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] % 89.74/12.32 | : ? [v4: vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 89.74/12.32 | vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 89.74/12.32 | vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & % 89.74/12.32 | ? [v5: vTerm] : ( ~ vTerm(v5) | ? [v6: vOptTerm] : ? [v7: vTerm] : % 89.74/12.32 | ? [v8: vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: % 89.74/12.32 | vOptTerm] : ? [v12: vTerm] : ? [v13: vTerm] : ? [v14: vTerm] : % 89.74/12.32 | ? [v15: vOptTerm] : ? [v16: vOptTerm] : ? [v17: vTerm] : ? % 89.74/12.32 | [v18: vTerm] : ? [v19: vTerm] : ? [v20: vOptTerm] : ? [v21: % 89.74/12.32 | vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : ? [v24: % 89.74/12.32 | vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 89.74/12.32 | ? [v28: vOptTerm] : ? [v29: vOptTerm] : ? [v30: vTerm] : ? % 89.74/12.32 | [v31: vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: % 89.74/12.32 | vTerm] : ? [v35: vTerm] : ? [v36: vTerm] : ? [v37: vTerm] : ? % 89.74/12.32 | [v38: vOptTerm] : ? [v39: vTerm] : ? [v40: vOptTerm] : ? [v41: % 89.74/12.32 | vOptTerm] : ? [v42: vTerm] : ? [v43: vTerm] : ? [v44: % 89.74/12.32 | vOptTerm] : ? [v45: vOptTerm] : ? [v46: vTerm] : ? [v47: % 89.74/12.32 | vTerm] : ? [v48: vTerm] : ? [v49: vOptTerm] : ? [v50: vTerm] : % 89.74/12.32 | ? [v51: vOptTerm] : ? [v52: vTerm] : ? [v53: vOptTerm] : ? % 89.74/12.32 | [v54: vTerm] : ? [v55: vTerm] : ? [v56: vOptTerm] : ? [v57: % 89.74/12.32 | vTerm] : ? [v58: vOptTerm] : ? [v59: vTerm] : ? [v60: vTerm] : % 89.74/12.32 | ? [v61: vTerm] : ? [v62: vOptTerm] : ? [v63: vTerm] : ? [v64: % 89.74/12.32 | vTerm] : ? [v65: vTerm] : ? [v66: vTerm] : ? [v67: vOptTerm] : % 89.74/12.32 | ? [v68: vOptTerm] : ? [v69: vTerm] : ? [v70: vTerm] : ? [v71: % 89.74/12.32 | vOptTerm] : ? [v72: vOptTerm] : ? [v73: vTerm] : ? [v74: % 89.74/12.32 | vTerm] : ? [v75: vTerm] : ? [v76: vOptTerm] : ? [v77: vTerm] : % 89.74/12.32 | ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: vOptTerm] : ? % 89.74/12.32 | [v81: vTerm] : ? [v82: vTerm] : ? [v83: vOptTerm] : ? [v84: % 89.74/12.32 | vTerm] : ? [v85: vOptTerm] : ? [v86: vTerm] : ? [v87: vTerm] : % 89.74/12.32 | ? [v88: vTerm] : ? [v89: vOptTerm] : ? [v90: vTerm] : ? [v91: % 89.74/12.32 | vTerm] : ? [v92: vTerm] : ? [v93: vOptTerm] : ? [v94: vTerm] : % 89.74/12.32 | ? [v95: vOptTerm] : ? [v96: vOptTerm] : ? [v97: vTerm] : ? % 89.74/12.32 | [v98: vTerm] : ? [v99: vOptTerm] : ? [v100: vOptTerm] : ? [v101: % 89.74/12.32 | vTerm] : ? [v102: vTerm] : ? [v103: vTerm] : ? [v104: % 89.74/12.32 | vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: % 89.74/12.32 | vTerm] : ? [v108: vOptTerm] : ? [v109: vOptTerm] : ? [v110: % 89.74/12.32 | vTerm] : ? [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : % 89.74/12.32 | ? [v114: vOptTerm] : ? [v115: vOptTerm] : ? [v116: vTerm] : ? % 89.74/12.32 | [v117: vTerm] : ? [v118: vTerm] : ? [v119: vOptTerm] : ? [v120: % 89.74/12.32 | vTerm] : ? [v121: vTerm] : ? [v122: vTerm] : ? [v123: % 89.74/12.32 | vOptTerm] : ? [v124: vTerm] : ? [v125: vTerm] : ? [v126: % 89.74/12.32 | vTerm] : ? [v127: vOptTerm] : (vreduce(v5) = v6 & vOptTerm(v114) % 89.74/12.32 | & vOptTerm(v108) & vOptTerm(v99) & vOptTerm(v95) & vOptTerm(v83) % 89.74/12.32 | & vOptTerm(v78) & vOptTerm(v71) & vOptTerm(v67) & vOptTerm(v56) & % 89.74/12.32 | vOptTerm(v51) & vOptTerm(v44) & vOptTerm(v40) & vOptTerm(v28) & % 89.74/12.32 | vOptTerm(v23) & vOptTerm(v15) & vOptTerm(v10) & vOptTerm(v6) & % 89.74/12.32 | vTerm(v125) & vTerm(v124) & vTerm(v121) & vTerm(v120) & % 89.74/12.32 | vTerm(v113) & vTerm(v112) & vTerm(v111) & vTerm(v107) & % 89.74/12.32 | vTerm(v106) & vTerm(v105) & vTerm(v98) & vTerm(v94) & vTerm(v90) % 89.74/12.32 | & vTerm(v82) & vTerm(v77) & vTerm(v70) & vTerm(v66) & vTerm(v63) % 89.74/12.32 | & vTerm(v55) & vTerm(v50) & vTerm(v43) & vTerm(v39) & vTerm(v35) % 89.74/12.32 | & vTerm(v34) & vTerm(v27) & vTerm(v26) & vTerm(v22) & vTerm(v21) % 89.74/12.32 | & vTerm(v14) & vTerm(v13) & vTerm(v9) & vTerm(v8) & vTerm(v7) & % 89.74/12.32 | ((v127 = v6 & v126 = v5 & vsomeTerm(v124) = v6 & vIfelse(vTrue, % 89.74/12.32 | v124, v125) = v5) | (v123 = v6 & v122 = v5 & % 89.74/12.32 | vsomeTerm(v121) = v6 & vIfelse(vFalse, v120, v121) = v5) | % 89.74/12.32 | (v119 = v6 & v116 = v5 & v115 = v114 & ~ (v111 = vFalse) & ~ % 89.74/12.32 | (v111 = vTrue) & vreduce(v111) = v114 & vgetTerm(v114) = v117 % 89.74/12.32 | & vsomeTerm(v118) = v6 & vIfelse(v117, v112, v113) = v118 & % 89.74/12.32 | vIfelse(v111, v112, v113) = v5 & vTerm(v118) & vTerm(v117) & % 89.74/12.32 | visSomeTerm(v114)) | (v110 = v5 & v109 = v108 & v6 = vnoTerm % 89.74/12.32 | & ~ (v105 = vFalse) & ~ (v105 = vTrue) & vreduce(v105) = % 89.74/12.32 | v108 & vIfelse(v105, v106, v107) = v5 & ~ visSomeTerm(v108)) % 89.74/12.32 | | (v104 = v6 & v101 = v5 & v100 = v99 & vreduce(v98) = v99 & % 89.74/12.32 | vgetTerm(v99) = v102 & vsomeTerm(v103) = v6 & vSucc(v102) = % 89.74/12.32 | v103 & vSucc(v98) = v5 & vTerm(v103) & vTerm(v102) & % 89.74/12.32 | visSomeTerm(v99)) | (v97 = v5 & v96 = v95 & v6 = vnoTerm & % 89.74/12.32 | vreduce(v94) = v95 & vSucc(v94) = v5 & ~ visSomeTerm(v95)) | % 89.74/12.32 | (v93 = v6 & v92 = v5 & vsomeTerm(v90) = v6 & vPred(v91) = v5 & % 89.74/12.32 | vSucc(v90) = v91 & vTerm(v91) & visNV(v90)) | (v89 = v6 & v86 % 89.74/12.32 | = v5 & v85 = v83 & vreduce(v84) = v83 & vgetTerm(v83) = v87 & % 89.74/12.32 | vsomeTerm(v88) = v6 & vPred(v87) = v88 & vPred(v84) = v5 & % 89.74/12.32 | vSucc(v82) = v84 & vTerm(v88) & vTerm(v87) & vTerm(v84) & % 89.74/12.32 | visSomeTerm(v83) & ~ visNV(v82)) | (v81 = v5 & v80 = v78 & % 89.74/12.32 | v6 = vnoTerm & vreduce(v79) = v78 & vPred(v79) = v5 & % 89.74/12.32 | vSucc(v77) = v79 & vTerm(v79) & ~ visSomeTerm(v78) & ~ % 89.74/12.32 | visNV(v77)) | (v76 = v6 & v73 = v5 & v72 = v71 & ~ (v70 = % 89.74/12.32 | vZero) & vreduce(v70) = v71 & vgetTerm(v71) = v74 & % 89.74/12.32 | vsomeTerm(v75) = v6 & vPred(v74) = v75 & vPred(v70) = v5 & % 89.74/12.32 | vTerm(v75) & vTerm(v74) & visSomeTerm(v71) & ! [v128: vTerm] % 89.74/12.32 | : ( ~ (vSucc(v128) = v70) | ~ vTerm(v128))) | (v69 = v5 & % 89.74/12.32 | v68 = v67 & v6 = vnoTerm & ~ (v66 = vZero) & vreduce(v66) = % 89.74/12.32 | v67 & vPred(v66) = v5 & ~ visSomeTerm(v67) & ! [v128: % 89.74/12.32 | vTerm] : ( ~ (vSucc(v128) = v66) | ~ vTerm(v128))) | (v65 % 89.74/12.32 | = v5 & v6 = v4 & vIszero(v64) = v5 & vSucc(v63) = v64 & % 89.74/12.32 | vTerm(v64) & visNV(v63)) | (v62 = v6 & v59 = v5 & v58 = v56 & % 89.74/12.32 | vreduce(v57) = v56 & vgetTerm(v56) = v60 & vsomeTerm(v61) = % 89.74/12.32 | v6 & vIszero(v60) = v61 & vIszero(v57) = v5 & vSucc(v55) = % 89.74/12.32 | v57 & vTerm(v61) & vTerm(v60) & vTerm(v57) & visSomeTerm(v56) % 89.74/12.32 | & ~ visNV(v55)) | (v54 = v5 & v53 = v51 & v6 = vnoTerm & % 89.74/12.32 | vreduce(v52) = v51 & vIszero(v52) = v5 & vSucc(v50) = v52 & % 89.74/12.32 | vTerm(v52) & ~ visSomeTerm(v51) & ~ visNV(v50)) | (v49 = v6 % 89.74/12.32 | & v46 = v5 & v45 = v44 & ~ (v43 = vZero) & vreduce(v43) = % 89.74/12.32 | v44 & vgetTerm(v44) = v47 & vsomeTerm(v48) = v6 & % 89.74/12.32 | vIszero(v47) = v48 & vIszero(v43) = v5 & vTerm(v48) & % 89.74/12.32 | vTerm(v47) & visSomeTerm(v44) & ! [v128: vTerm] : ( ~ % 89.74/12.32 | (vSucc(v128) = v43) | ~ vTerm(v128))) | (v42 = v5 & v41 = % 89.74/12.32 | v40 & v6 = vnoTerm & ~ (v39 = vZero) & vreduce(v39) = v40 & % 89.74/12.32 | vIszero(v39) = v5 & ~ visSomeTerm(v40) & ! [v128: vTerm] : % 89.74/12.32 | ( ~ (vSucc(v128) = v39) | ~ vTerm(v128))) | (v38 = v6 & v36 % 89.74/12.32 | = v5 & vplusop(v34, v35) = v37 & vsomeTerm(v37) = v6 & % 89.74/12.32 | vPlus(v34, v35) = v5 & vTerm(v37) & visNV(v35) & visNV(v34)) % 89.74/12.32 | | (v33 = v6 & v30 = v5 & v29 = v28 & vreduce(v27) = v28 & % 89.74/12.32 | vgetTerm(v28) = v31 & vsomeTerm(v32) = v6 & vPlus(v26, v31) = % 89.74/12.32 | v32 & vPlus(v26, v27) = v5 & vTerm(v32) & vTerm(v31) & % 89.74/12.32 | visSomeTerm(v28) & visNV(v26) & ~ visNV(v27)) | (v25 = v5 & % 89.74/12.32 | v24 = v23 & v6 = vnoTerm & vreduce(v22) = v23 & vPlus(v21, % 89.74/12.32 | v22) = v5 & visNV(v21) & ~ visSomeTerm(v23) & ~ % 89.74/12.32 | visNV(v22)) | (v20 = v6 & v17 = v5 & v16 = v15 & vreduce(v13) % 89.74/12.32 | = v15 & vgetTerm(v15) = v18 & vsomeTerm(v19) = v6 & % 89.74/12.32 | vPlus(v18, v14) = v19 & vPlus(v13, v14) = v5 & vTerm(v19) & % 89.74/12.32 | vTerm(v18) & visSomeTerm(v15) & ~ visNV(v13)) | (v12 = v5 & % 89.74/12.32 | v11 = v10 & v6 = vnoTerm & vreduce(v8) = v10 & vPlus(v8, v9) % 89.74/12.32 | = v5 & ~ visSomeTerm(v10) & ~ visNV(v8)) | (v7 = v5 & v6 = % 89.74/12.32 | vnoTerm & ~ (v5 = v2) & ~ (v5 = v0) & ! [v128: vTerm] : ! % 89.74/12.32 | [v129: vTerm] : ! [v130: vTerm] : ( ~ (vIfelse(v128, v129, % 89.74/12.32 | v130) = v5) | ~ vTerm(v130) | ~ vTerm(v129) | ~ % 89.74/12.32 | vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 89.74/12.32 | (vPlus(v128, v129) = v5) | ~ vTerm(v129) | ~ vTerm(v128)) % 89.74/12.32 | & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = % 89.74/12.32 | v129) | ~ vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = % 89.74/12.32 | v5) & vIszero(v129) = v130 & vTerm(v130))) & ! [v128: % 89.74/12.32 | vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = v129) | ~ % 89.74/12.32 | vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = v5) & % 89.74/12.32 | vPred(v129) = v130 & vTerm(v130))) & ! [v128: vTerm] : % 89.74/12.32 | ! [v129: vTerm] : ( ~ (vIfelse(vFalse, v128, v129) = v5) | ~ % 89.74/12.32 | vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] : ! % 89.74/12.32 | [v129: vTerm] : ( ~ (vIfelse(vTrue, v128, v129) = v5) | ~ % 89.74/12.32 | vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] : ( ~ % 89.74/12.32 | (vIszero(v128) = v5) | ~ vTerm(v128)) & ! [v128: vTerm] : % 89.74/12.32 | ( ~ (vPred(v128) = v5) | ~ vTerm(v128)) & ! [v128: vTerm] : % 89.74/12.32 | ( ~ (vSucc(v128) = v5) | ~ vTerm(v128))) | (v6 = v3 & v5 = % 89.74/12.32 | v2) | (v6 = v1 & v5 = v0))))) % 89.74/12.32 | % 89.74/12.32 | ALPHA: (TZero) implies: % 89.74/12.32 | (6) vptchecksimple(vZero, vNat) % 89.74/12.32 | % 89.74/12.32 | ALPHA: (TPred_inv2) implies: % 89.74/12.32 | (7) ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vNat | ~ % 89.74/12.32 | (vPred(v0) = v2) | ~ vTy(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, % 89.74/12.32 | v1)) % 89.74/12.32 | % 89.74/12.32 | ALPHA: (Preservation-Pred-IH0) implies: % 89.74/12.32 | (8) ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: vTy] : % 89.74/12.32 | ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ vTerm(v2) % 89.74/12.32 | | ~ vptchecksimple(vt1, v1) | vptchecksimple(v2, v1))) % 89.74/12.32 | % 89.74/12.32 | ALPHA: (Preservation-Pred-t1-isSomeTerm-True) implies: % 89.74/12.32 | (9) ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: vOptTerm] : (vreduce(v1) = % 89.74/12.32 | v2 & vreduce(vt1) = v0 & vPred(vt1) = v1 & vOptTerm(v2) & % 89.74/12.32 | vOptTerm(v0) & vTerm(v1) & ! [v3: vTy] : ! [v4: vTerm] : (vt1 = % 89.74/12.32 | vZero | ~ (vsomeTerm(v4) = v2) | ~ vTy(v3) | ~ vTerm(v4) | ~ % 89.74/12.32 | vptchecksimple(v1, v3) | ~ visSomeTerm(v0) | vptchecksimple(v4, % 89.74/12.32 | v3) | ? [v5: vTerm] : (vSucc(v5) = vt1 & vTerm(v5)))) % 89.74/12.32 | % 89.74/12.32 | ALPHA: (Preservation-Pred-t1-isSomeTerm-False) implies: % 89.74/12.32 | (10) ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: vOptTerm] : (vreduce(v1) % 89.74/12.32 | = v2 & vreduce(vt1) = v0 & vPred(vt1) = v1 & vOptTerm(v2) & % 89.74/12.32 | vOptTerm(v0) & vTerm(v1) & ! [v3: vTy] : ! [v4: vTerm] : (vt1 = % 89.74/12.32 | vZero | ~ (vsomeTerm(v4) = v2) | ~ vTy(v3) | ~ vTerm(v4) | ~ % 89.74/12.32 | vptchecksimple(v1, v3) | vptchecksimple(v4, v3) | visSomeTerm(v0) % 89.74/12.32 | | ? [v5: vTerm] : (vSucc(v5) = vt1 & vTerm(v5)))) % 89.74/12.32 | % 89.74/12.32 | ALPHA: (Preservation-Pred-t1) implies: % 89.74/12.33 | (11) vTerm(vZero) % 89.74/12.33 | (12) vTerm(vt1) % 89.74/12.33 | (13) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTy] : ? [v3: vTerm] : ( % 89.74/12.33 | ~ (vt1 = vZero) & vreduce(v0) = v1 & vsomeTerm(v3) = v1 & vPred(vt1) % 89.74/12.33 | = v0 & vTy(v2) & vOptTerm(v1) & vTerm(v3) & vTerm(v0) & % 89.74/12.33 | vptchecksimple(v0, v2) & ~ vptchecksimple(v3, v2) & ! [v4: vTerm] % 89.74/12.33 | : ( ~ (vSucc(v4) = vt1) | ~ vTerm(v4))) % 89.74/12.33 | % 89.74/12.33 | ALPHA: (function-axioms) implies: % 89.74/12.33 | (14) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 89.74/12.33 | (vPred(v2) = v1) | ~ (vPred(v2) = v0)) % 89.74/12.33 | (15) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 89.74/12.33 | (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) % 89.74/12.33 | (16) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 89.74/12.33 | (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) % 89.74/12.33 | % 89.74/12.33 | DELTA: instantiating (2) with fresh symbols all_90_0, all_90_1 gives: % 89.74/12.33 | (17) vreduce(all_90_1) = all_90_0 & vsomeTerm(vZero) = all_90_0 & % 89.74/12.33 | vPred(vZero) = all_90_1 & vOptTerm(all_90_0) & vTerm(all_90_1) % 89.74/12.33 | % 89.74/12.33 | ALPHA: (17) implies: % 89.74/12.33 | (18) vsomeTerm(vZero) = all_90_0 % 89.74/12.33 | % 89.74/12.33 | DELTA: instantiating (8) with fresh symbol all_95_0 gives: % 89.74/12.33 | (19) vreduce(vt1) = all_95_0 & vOptTerm(all_95_0) & ! [v0: vTy] : ! [v1: % 89.74/12.33 | vTerm] : ( ~ (vsomeTerm(v1) = all_95_0) | ~ vTy(v0) | ~ vTerm(v1) % 89.74/12.33 | | ~ vptchecksimple(vt1, v0) | vptchecksimple(v1, v0)) % 89.74/12.33 | % 89.74/12.33 | ALPHA: (19) implies: % 89.74/12.33 | (20) vreduce(vt1) = all_95_0 % 89.74/12.33 | % 89.74/12.33 | DELTA: instantiating (13) with fresh symbols all_107_0, all_107_1, all_107_2, % 89.74/12.33 | all_107_3 gives: % 89.74/12.33 | (21) ~ (vt1 = vZero) & vreduce(all_107_3) = all_107_2 & % 89.74/12.33 | vsomeTerm(all_107_0) = all_107_2 & vPred(vt1) = all_107_3 & % 89.74/12.33 | vTy(all_107_1) & vOptTerm(all_107_2) & vTerm(all_107_0) & % 89.74/12.33 | vTerm(all_107_3) & vptchecksimple(all_107_3, all_107_1) & ~ % 89.74/12.33 | vptchecksimple(all_107_0, all_107_1) & ! [v0: vTerm] : ( ~ (vSucc(v0) % 89.74/12.33 | = vt1) | ~ vTerm(v0)) % 89.74/12.33 | % 89.74/12.33 | ALPHA: (21) implies: % 89.74/12.33 | (22) ~ (vt1 = vZero) % 89.74/12.33 | (23) ~ vptchecksimple(all_107_0, all_107_1) % 89.74/12.33 | (24) vptchecksimple(all_107_3, all_107_1) % 89.74/12.33 | (25) vTerm(all_107_0) % 89.74/12.33 | (26) vTy(all_107_1) % 89.74/12.33 | (27) vPred(vt1) = all_107_3 % 89.74/12.33 | (28) vsomeTerm(all_107_0) = all_107_2 % 89.74/12.33 | (29) vreduce(all_107_3) = all_107_2 % 89.74/12.33 | (30) ! [v0: vTerm] : ( ~ (vSucc(v0) = vt1) | ~ vTerm(v0)) % 89.74/12.33 | % 89.74/12.33 | DELTA: instantiating (9) with fresh symbols all_110_0, all_110_1, all_110_2 % 89.74/12.33 | gives: % 89.74/12.33 | (31) vreduce(all_110_1) = all_110_0 & vreduce(vt1) = all_110_2 & vPred(vt1) % 89.74/12.33 | = all_110_1 & vOptTerm(all_110_0) & vOptTerm(all_110_2) & % 89.74/12.33 | vTerm(all_110_1) & ! [v0: vTy] : ! [v1: vTerm] : (vt1 = vZero | ~ % 89.74/12.33 | (vsomeTerm(v1) = all_110_0) | ~ vTy(v0) | ~ vTerm(v1) | ~ % 89.74/12.33 | vptchecksimple(all_110_1, v0) | ~ visSomeTerm(all_110_2) | % 89.74/12.33 | vptchecksimple(v1, v0) | ? [v2: vTerm] : (vSucc(v2) = vt1 & % 89.74/12.33 | vTerm(v2))) % 89.74/12.33 | % 89.74/12.33 | ALPHA: (31) implies: % 89.74/12.33 | (32) vPred(vt1) = all_110_1 % 89.74/12.33 | (33) vreduce(vt1) = all_110_2 % 89.74/12.33 | (34) vreduce(all_110_1) = all_110_0 % 89.74/12.33 | (35) ! [v0: vTy] : ! [v1: vTerm] : (vt1 = vZero | ~ (vsomeTerm(v1) = % 89.74/12.33 | all_110_0) | ~ vTy(v0) | ~ vTerm(v1) | ~ % 89.74/12.33 | vptchecksimple(all_110_1, v0) | ~ visSomeTerm(all_110_2) | % 89.74/12.33 | vptchecksimple(v1, v0) | ? [v2: vTerm] : (vSucc(v2) = vt1 & % 89.74/12.33 | vTerm(v2))) % 89.74/12.33 | % 89.74/12.33 | DELTA: instantiating (10) with fresh symbols all_113_0, all_113_1, all_113_2 % 89.74/12.33 | gives: % 89.74/12.33 | (36) vreduce(all_113_1) = all_113_0 & vreduce(vt1) = all_113_2 & vPred(vt1) % 89.74/12.33 | = all_113_1 & vOptTerm(all_113_0) & vOptTerm(all_113_2) & % 89.74/12.33 | vTerm(all_113_1) & ! [v0: vTy] : ! [v1: vTerm] : (vt1 = vZero | ~ % 89.74/12.33 | (vsomeTerm(v1) = all_113_0) | ~ vTy(v0) | ~ vTerm(v1) | ~ % 89.74/12.33 | vptchecksimple(all_113_1, v0) | vptchecksimple(v1, v0) | % 89.74/12.33 | visSomeTerm(all_113_2) | ? [v2: vTerm] : (vSucc(v2) = vt1 & % 89.74/12.33 | vTerm(v2))) % 89.74/12.33 | % 89.74/12.33 | ALPHA: (36) implies: % 89.74/12.33 | (37) vPred(vt1) = all_113_1 % 89.74/12.33 | (38) vreduce(vt1) = all_113_2 % 89.74/12.33 | (39) vreduce(all_113_1) = all_113_0 % 89.74/12.33 | % 89.74/12.33 | DELTA: instantiating (5) with fresh symbols all_120_0, all_120_1, all_120_2, % 89.74/12.33 | all_120_3, all_120_4 gives: % 89.74/12.35 | (40) vsomeTerm(vFalse) = all_120_0 & vsomeTerm(vTrue) = all_120_1 & % 89.74/12.35 | vsomeTerm(vZero) = all_120_3 & vIszero(vZero) = all_120_2 & % 89.74/12.35 | vPred(vZero) = all_120_4 & vOptTerm(all_120_0) & vOptTerm(all_120_1) & % 89.74/12.35 | vOptTerm(all_120_3) & vTerm(all_120_2) & vTerm(all_120_4) & ? [v0: % 89.74/12.35 | vTerm] : ( ~ vTerm(v0) | ? [v1: vOptTerm] : ? [v2: vTerm] : ? % 89.74/12.35 | [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : ? [v6: vOptTerm] % 89.74/12.35 | : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : ? [v10: % 89.74/12.35 | vOptTerm] : ? [v11: vOptTerm] : ? [v12: vTerm] : ? [v13: vTerm] % 89.74/12.35 | : ? [v14: vTerm] : ? [v15: vOptTerm] : ? [v16: vTerm] : ? [v17: % 89.74/12.35 | vTerm] : ? [v18: vOptTerm] : ? [v19: vOptTerm] : ? [v20: vTerm] % 89.74/12.35 | : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : ? [v24: % 89.74/12.35 | vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 89.74/12.35 | ? [v28: vOptTerm] : ? [v29: vTerm] : ? [v30: vTerm] : ? [v31: % 89.74/12.35 | vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: vTerm] : % 89.74/12.35 | ? [v35: vOptTerm] : ? [v36: vOptTerm] : ? [v37: vTerm] : ? [v38: % 89.74/12.35 | vTerm] : ? [v39: vOptTerm] : ? [v40: vOptTerm] : ? [v41: vTerm] % 89.74/12.35 | : ? [v42: vTerm] : ? [v43: vTerm] : ? [v44: vOptTerm] : ? [v45: % 89.74/12.35 | vTerm] : ? [v46: vOptTerm] : ? [v47: vTerm] : ? [v48: vOptTerm] % 89.74/12.35 | : ? [v49: vTerm] : ? [v50: vTerm] : ? [v51: vOptTerm] : ? [v52: % 89.74/12.35 | vTerm] : ? [v53: vOptTerm] : ? [v54: vTerm] : ? [v55: vTerm] : % 89.74/12.35 | ? [v56: vTerm] : ? [v57: vOptTerm] : ? [v58: vTerm] : ? [v59: % 89.74/12.35 | vTerm] : ? [v60: vTerm] : ? [v61: vTerm] : ? [v62: vOptTerm] : % 89.74/12.35 | ? [v63: vOptTerm] : ? [v64: vTerm] : ? [v65: vTerm] : ? [v66: % 89.74/12.35 | vOptTerm] : ? [v67: vOptTerm] : ? [v68: vTerm] : ? [v69: vTerm] % 89.74/12.35 | : ? [v70: vTerm] : ? [v71: vOptTerm] : ? [v72: vTerm] : ? [v73: % 89.74/12.35 | vOptTerm] : ? [v74: vTerm] : ? [v75: vOptTerm] : ? [v76: vTerm] % 89.74/12.35 | : ? [v77: vTerm] : ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: % 89.74/12.35 | vOptTerm] : ? [v81: vTerm] : ? [v82: vTerm] : ? [v83: vTerm] : % 89.74/12.35 | ? [v84: vOptTerm] : ? [v85: vTerm] : ? [v86: vTerm] : ? [v87: % 89.74/12.35 | vTerm] : ? [v88: vOptTerm] : ? [v89: vTerm] : ? [v90: vOptTerm] % 89.74/12.35 | : ? [v91: vOptTerm] : ? [v92: vTerm] : ? [v93: vTerm] : ? [v94: % 89.74/12.35 | vOptTerm] : ? [v95: vOptTerm] : ? [v96: vTerm] : ? [v97: vTerm] % 89.74/12.35 | : ? [v98: vTerm] : ? [v99: vOptTerm] : ? [v100: vTerm] : ? % 89.74/12.35 | [v101: vTerm] : ? [v102: vTerm] : ? [v103: vOptTerm] : ? [v104: % 89.74/12.35 | vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: vTerm] % 89.74/12.35 | : ? [v108: vTerm] : ? [v109: vOptTerm] : ? [v110: vOptTerm] : ? % 89.74/12.35 | [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : ? [v114: % 89.74/12.35 | vOptTerm] : ? [v115: vTerm] : ? [v116: vTerm] : ? [v117: vTerm] % 89.74/12.35 | : ? [v118: vOptTerm] : ? [v119: vTerm] : ? [v120: vTerm] : ? % 89.74/12.35 | [v121: vTerm] : ? [v122: vOptTerm] : (vreduce(v0) = v1 & % 89.74/12.35 | vOptTerm(v109) & vOptTerm(v103) & vOptTerm(v94) & vOptTerm(v90) & % 89.74/12.35 | vOptTerm(v78) & vOptTerm(v73) & vOptTerm(v66) & vOptTerm(v62) & % 89.74/12.35 | vOptTerm(v51) & vOptTerm(v46) & vOptTerm(v39) & vOptTerm(v35) & % 89.74/12.35 | vOptTerm(v23) & vOptTerm(v18) & vOptTerm(v10) & vOptTerm(v5) & % 89.74/12.35 | vOptTerm(v1) & vTerm(v120) & vTerm(v119) & vTerm(v116) & % 89.74/12.35 | vTerm(v115) & vTerm(v108) & vTerm(v107) & vTerm(v106) & % 89.74/12.35 | vTerm(v102) & vTerm(v101) & vTerm(v100) & vTerm(v93) & vTerm(v89) % 89.74/12.35 | & vTerm(v85) & vTerm(v77) & vTerm(v72) & vTerm(v65) & vTerm(v61) & % 89.74/12.35 | vTerm(v58) & vTerm(v50) & vTerm(v45) & vTerm(v38) & vTerm(v34) & % 89.74/12.35 | vTerm(v30) & vTerm(v29) & vTerm(v22) & vTerm(v21) & vTerm(v17) & % 89.74/12.35 | vTerm(v16) & vTerm(v9) & vTerm(v8) & vTerm(v4) & vTerm(v3) & % 89.74/12.35 | vTerm(v2) & ((v122 = v1 & v121 = v0 & vsomeTerm(v119) = v1 & % 89.74/12.35 | vIfelse(vTrue, v119, v120) = v0) | (v118 = v1 & v117 = v0 & % 89.74/12.35 | vsomeTerm(v116) = v1 & vIfelse(vFalse, v115, v116) = v0) | % 89.74/12.35 | (v114 = v1 & v111 = v0 & v110 = v109 & ~ (v106 = vFalse) & ~ % 89.74/12.35 | (v106 = vTrue) & vreduce(v106) = v109 & vgetTerm(v109) = v112 % 89.74/12.35 | & vsomeTerm(v113) = v1 & vIfelse(v112, v107, v108) = v113 & % 89.74/12.35 | vIfelse(v106, v107, v108) = v0 & vTerm(v113) & vTerm(v112) & % 89.74/12.35 | visSomeTerm(v109)) | (v105 = v0 & v104 = v103 & v1 = vnoTerm & % 89.74/12.35 | ~ (v100 = vFalse) & ~ (v100 = vTrue) & vreduce(v100) = v103 % 89.74/12.35 | & vIfelse(v100, v101, v102) = v0 & ~ visSomeTerm(v103)) | % 89.74/12.35 | (v99 = v1 & v96 = v0 & v95 = v94 & vreduce(v93) = v94 & % 89.74/12.35 | vgetTerm(v94) = v97 & vsomeTerm(v98) = v1 & vSucc(v97) = v98 & % 89.74/12.35 | vSucc(v93) = v0 & vTerm(v98) & vTerm(v97) & visSomeTerm(v94)) % 89.74/12.35 | | (v92 = v0 & v91 = v90 & v1 = vnoTerm & vreduce(v89) = v90 & % 89.74/12.35 | vSucc(v89) = v0 & ~ visSomeTerm(v90)) | (v88 = v1 & v87 = v0 % 89.74/12.35 | & vsomeTerm(v85) = v1 & vPred(v86) = v0 & vSucc(v85) = v86 & % 89.74/12.35 | vTerm(v86) & visNV(v85)) | (v84 = v1 & v81 = v0 & v80 = v78 & % 89.74/12.35 | vreduce(v79) = v78 & vgetTerm(v78) = v82 & vsomeTerm(v83) = v1 % 89.74/12.35 | & vPred(v82) = v83 & vPred(v79) = v0 & vSucc(v77) = v79 & % 89.74/12.35 | vTerm(v83) & vTerm(v82) & vTerm(v79) & visSomeTerm(v78) & ~ % 89.74/12.35 | visNV(v77)) | (v76 = v0 & v75 = v73 & v1 = vnoTerm & % 89.74/12.35 | vreduce(v74) = v73 & vPred(v74) = v0 & vSucc(v72) = v74 & % 89.74/12.35 | vTerm(v74) & ~ visSomeTerm(v73) & ~ visNV(v72)) | (v71 = v1 % 89.74/12.35 | & v68 = v0 & v67 = v66 & ~ (v65 = vZero) & vreduce(v65) = v66 % 89.74/12.35 | & vgetTerm(v66) = v69 & vsomeTerm(v70) = v1 & vPred(v69) = v70 % 89.74/12.35 | & vPred(v65) = v0 & vTerm(v70) & vTerm(v69) & visSomeTerm(v66) % 89.74/12.35 | & ! [v123: vTerm] : ( ~ (vSucc(v123) = v65) | ~ % 89.74/12.35 | vTerm(v123))) | (v64 = v0 & v63 = v62 & v1 = vnoTerm & ~ % 89.74/12.35 | (v61 = vZero) & vreduce(v61) = v62 & vPred(v61) = v0 & ~ % 89.74/12.35 | visSomeTerm(v62) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v61) % 89.74/12.35 | | ~ vTerm(v123))) | (v60 = v0 & v1 = all_120_0 & % 89.74/12.35 | vIszero(v59) = v0 & vSucc(v58) = v59 & vTerm(v59) & % 89.74/12.35 | visNV(v58)) | (v57 = v1 & v54 = v0 & v53 = v51 & vreduce(v52) % 89.74/12.35 | = v51 & vgetTerm(v51) = v55 & vsomeTerm(v56) = v1 & % 89.74/12.35 | vIszero(v55) = v56 & vIszero(v52) = v0 & vSucc(v50) = v52 & % 89.74/12.35 | vTerm(v56) & vTerm(v55) & vTerm(v52) & visSomeTerm(v51) & ~ % 89.74/12.35 | visNV(v50)) | (v49 = v0 & v48 = v46 & v1 = vnoTerm & % 89.74/12.35 | vreduce(v47) = v46 & vIszero(v47) = v0 & vSucc(v45) = v47 & % 89.74/12.35 | vTerm(v47) & ~ visSomeTerm(v46) & ~ visNV(v45)) | (v44 = v1 % 89.74/12.35 | & v41 = v0 & v40 = v39 & ~ (v38 = vZero) & vreduce(v38) = v39 % 89.74/12.35 | & vgetTerm(v39) = v42 & vsomeTerm(v43) = v1 & vIszero(v42) = % 89.74/12.35 | v43 & vIszero(v38) = v0 & vTerm(v43) & vTerm(v42) & % 89.74/12.35 | visSomeTerm(v39) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v38) % 89.74/12.35 | | ~ vTerm(v123))) | (v37 = v0 & v36 = v35 & v1 = vnoTerm & % 89.74/12.35 | ~ (v34 = vZero) & vreduce(v34) = v35 & vIszero(v34) = v0 & ~ % 89.74/12.35 | visSomeTerm(v35) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v34) % 89.74/12.35 | | ~ vTerm(v123))) | (v33 = v1 & v31 = v0 & vplusop(v29, % 89.74/12.35 | v30) = v32 & vsomeTerm(v32) = v1 & vPlus(v29, v30) = v0 & % 89.74/12.35 | vTerm(v32) & visNV(v30) & visNV(v29)) | (v28 = v1 & v25 = v0 & % 89.74/12.35 | v24 = v23 & vreduce(v22) = v23 & vgetTerm(v23) = v26 & % 89.74/12.35 | vsomeTerm(v27) = v1 & vPlus(v21, v26) = v27 & vPlus(v21, v22) % 89.74/12.35 | = v0 & vTerm(v27) & vTerm(v26) & visSomeTerm(v23) & visNV(v21) % 89.74/12.35 | & ~ visNV(v22)) | (v20 = v0 & v19 = v18 & v1 = vnoTerm & % 89.74/12.35 | vreduce(v17) = v18 & vPlus(v16, v17) = v0 & visNV(v16) & ~ % 89.74/12.35 | visSomeTerm(v18) & ~ visNV(v17)) | (v15 = v1 & v12 = v0 & v11 % 89.74/12.35 | = v10 & vreduce(v8) = v10 & vgetTerm(v10) = v13 & % 89.74/12.35 | vsomeTerm(v14) = v1 & vPlus(v13, v9) = v14 & vPlus(v8, v9) = % 89.74/12.35 | v0 & vTerm(v14) & vTerm(v13) & visSomeTerm(v10) & ~ % 89.74/12.35 | visNV(v8)) | (v7 = v0 & v6 = v5 & v1 = vnoTerm & vreduce(v3) = % 89.74/12.35 | v5 & vPlus(v3, v4) = v0 & ~ visSomeTerm(v5) & ~ visNV(v3)) | % 89.74/12.35 | (v2 = v0 & v1 = vnoTerm & ~ (v0 = all_120_2) & ~ (v0 = % 89.74/12.35 | all_120_4) & ! [v123: vTerm] : ! [v124: vTerm] : ! [v125: % 89.74/12.35 | vTerm] : ( ~ (vIfelse(v123, v124, v125) = v0) | ~ % 89.74/12.35 | vTerm(v125) | ~ vTerm(v124) | ~ vTerm(v123)) & ! [v123: % 89.74/12.35 | vTerm] : ! [v124: vTerm] : ( ~ (vPlus(v123, v124) = v0) | % 89.74/12.35 | ~ vTerm(v124) | ~ vTerm(v123)) & ! [v123: vTerm] : ! % 89.74/12.35 | [v124: vTerm] : ( ~ (vSucc(v123) = v124) | ~ vTerm(v123) | ? % 89.74/12.35 | [v125: vTerm] : ( ~ (v125 = v0) & vIszero(v124) = v125 & % 89.74/12.35 | vTerm(v125))) & ! [v123: vTerm] : ! [v124: vTerm] : ( ~ % 89.74/12.35 | (vSucc(v123) = v124) | ~ vTerm(v123) | ? [v125: vTerm] : ( % 89.74/12.35 | ~ (v125 = v0) & vPred(v124) = v125 & vTerm(v125))) & ! % 89.74/12.35 | [v123: vTerm] : ! [v124: vTerm] : ( ~ (vIfelse(vFalse, v123, % 89.74/12.35 | v124) = v0) | ~ vTerm(v124) | ~ vTerm(v123)) & ! % 89.74/12.35 | [v123: vTerm] : ! [v124: vTerm] : ( ~ (vIfelse(vTrue, v123, % 89.74/12.35 | v124) = v0) | ~ vTerm(v124) | ~ vTerm(v123)) & ! % 89.74/12.35 | [v123: vTerm] : ( ~ (vIszero(v123) = v0) | ~ vTerm(v123)) & % 89.74/12.35 | ! [v123: vTerm] : ( ~ (vPred(v123) = v0) | ~ vTerm(v123)) & % 89.74/12.35 | ! [v123: vTerm] : ( ~ (vSucc(v123) = v0) | ~ vTerm(v123))) | % 89.74/12.35 | (v1 = all_120_1 & v0 = all_120_2) | (v1 = all_120_3 & v0 = % 89.74/12.35 | all_120_4)))) % 89.74/12.35 | % 89.74/12.35 | ALPHA: (40) implies: % 89.74/12.35 | (41) vsomeTerm(vZero) = all_120_3 % 89.74/12.35 | % 89.74/12.35 | GROUND_INST: instantiating (14) with all_110_1, all_113_1, vt1, simplifying % 89.74/12.35 | with (32), (37) gives: % 89.74/12.35 | (42) all_113_1 = all_110_1 % 89.74/12.35 | % 89.74/12.35 | GROUND_INST: instantiating (14) with all_107_3, all_113_1, vt1, simplifying % 89.74/12.35 | with (27), (37) gives: % 89.74/12.35 | (43) all_113_1 = all_107_3 % 89.74/12.35 | % 89.74/12.35 | GROUND_INST: instantiating (15) with all_90_0, all_120_3, vZero, simplifying % 89.74/12.35 | with (18), (41) gives: % 89.74/12.35 | (44) all_120_3 = all_90_0 % 89.74/12.35 | % 89.74/12.35 | GROUND_INST: instantiating (16) with all_110_2, all_113_2, vt1, simplifying % 89.74/12.35 | with (33), (38) gives: % 89.74/12.35 | (45) all_113_2 = all_110_2 % 89.74/12.35 | % 89.74/12.35 | GROUND_INST: instantiating (16) with all_95_0, all_113_2, vt1, simplifying % 89.74/12.35 | with (20), (38) gives: % 89.74/12.35 | (46) all_113_2 = all_95_0 % 89.74/12.35 | % 89.74/12.35 | GROUND_INST: instantiating (16) with all_110_0, all_113_0, all_110_1, % 89.74/12.35 | simplifying with (34) gives: % 89.74/12.35 | (47) all_113_0 = all_110_0 | ~ (vreduce(all_110_1) = all_113_0) % 89.74/12.35 | % 89.74/12.35 | GROUND_INST: instantiating (16) with all_107_2, all_113_0, all_107_3, % 89.74/12.35 | simplifying with (29) gives: % 89.74/12.35 | (48) all_113_0 = all_107_2 | ~ (vreduce(all_107_3) = all_113_0) % 89.74/12.35 | % 89.74/12.35 | COMBINE_EQS: (42), (43) imply: % 89.74/12.35 | (49) all_110_1 = all_107_3 % 89.74/12.35 | % 89.74/12.35 | SIMP: (49) implies: % 89.74/12.35 | (50) all_110_1 = all_107_3 % 89.74/12.35 | % 89.74/12.35 | COMBINE_EQS: (45), (46) imply: % 89.74/12.35 | (51) all_110_2 = all_95_0 % 89.74/12.35 | % 89.74/12.35 | REDUCE: (39), (43) imply: % 89.74/12.35 | (52) vreduce(all_107_3) = all_113_0 % 89.74/12.35 | % 89.74/12.35 | BETA: splitting (47) gives: % 89.74/12.35 | % 89.74/12.35 | Case 1: % 89.74/12.35 | | % 89.74/12.35 | | (53) ~ (vreduce(all_110_1) = all_113_0) % 89.74/12.35 | | % 89.74/12.35 | | REDUCE: (50), (53) imply: % 89.74/12.35 | | (54) ~ (vreduce(all_107_3) = all_113_0) % 89.74/12.35 | | % 89.74/12.35 | | PRED_UNIFY: (52), (54) imply: % 89.74/12.35 | | (55) $false % 89.74/12.35 | | % 89.74/12.35 | | CLOSE: (55) is inconsistent. % 89.74/12.35 | | % 89.74/12.35 | Case 2: % 89.74/12.35 | | % 89.74/12.35 | | (56) all_113_0 = all_110_0 % 89.74/12.35 | | % 89.74/12.35 | | REDUCE: (52), (56) imply: % 89.74/12.35 | | (57) vreduce(all_107_3) = all_110_0 % 89.74/12.35 | | % 89.74/12.35 | | BETA: splitting (48) gives: % 89.74/12.35 | | % 89.74/12.35 | | Case 1: % 89.74/12.35 | | | % 89.74/12.35 | | | (58) ~ (vreduce(all_107_3) = all_113_0) % 89.74/12.35 | | | % 89.74/12.35 | | | PRED_UNIFY: (52), (58) imply: % 89.74/12.35 | | | (59) $false % 89.74/12.35 | | | % 89.74/12.35 | | | CLOSE: (59) is inconsistent. % 89.74/12.35 | | | % 89.74/12.35 | | Case 2: % 89.74/12.35 | | | % 89.74/12.35 | | | (60) all_113_0 = all_107_2 % 89.74/12.35 | | | % 89.74/12.35 | | | COMBINE_EQS: (56), (60) imply: % 89.74/12.35 | | | (61) all_110_0 = all_107_2 % 89.74/12.35 | | | % 89.74/12.35 | | | SIMP: (61) implies: % 89.74/12.35 | | | (62) all_110_0 = all_107_2 % 89.74/12.35 | | | % 89.74/12.35 | | | GROUND_INST: instantiating (7) with vt1, all_107_1, all_107_3, simplifying % 89.74/12.35 | | | with (12), (24), (26), (27) gives: % 89.74/12.35 | | | (63) all_107_1 = vNat % 89.74/12.35 | | | % 89.74/12.35 | | | GROUND_INST: instantiating (3) with vt1, all_107_3, simplifying with (12), % 89.74/12.35 | | | (27) gives: % 89.74/12.35 | | | (64) vt1 = vZero | ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: % 89.74/12.35 | | | vTerm] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : % 89.74/12.35 | | | ? [v6: vTerm] : (vTerm(v5) & ((v6 = vt1 & vSucc(v5) = vt1) | % 89.74/12.35 | | | (vreduce(vt1) = v0 & vOptTerm(v0) & ( ~ visSomeTerm(v0) | (v4 % 89.74/12.35 | | | = v1 & vreduce(all_107_3) = v1 & vgetTerm(v0) = v2 & % 89.74/12.35 | | | vsomeTerm(v3) = v1 & vPred(v2) = v3 & vOptTerm(v1) & % 89.74/12.35 | | | vTerm(v3) & vTerm(v2)))))) % 89.74/12.35 | | | % 89.74/12.35 | | | GROUND_INST: instantiating (4) with vt1, all_107_3, simplifying with (12), % 89.74/12.35 | | | (27) gives: % 89.74/12.36 | | | (65) vt1 = vZero | ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: % 89.74/12.36 | | | vTerm] : ? [v3: vTerm] : (vTerm(v2) & ((v3 = vt1 & vSucc(v2) = % 89.74/12.36 | | | vt1) | (v1 = vnoTerm & vreduce(all_107_3) = vnoTerm) | % 89.74/12.36 | | | (vreduce(vt1) = v0 & vOptTerm(v0) & visSomeTerm(v0)))) % 89.74/12.36 | | | % 89.74/12.36 | | | GROUND_INST: instantiating (EQ-someTerm) with vZero, all_107_0, all_90_0, % 89.74/12.36 | | | simplifying with (11), (18), (25) gives: % 89.74/12.36 | | | (66) all_107_0 = vZero | ~ (vsomeTerm(all_107_0) = all_90_0) % 89.74/12.36 | | | % 89.74/12.36 | | | GROUND_INST: instantiating (isSomeTerm-1) with all_107_0, all_107_2, % 89.74/12.36 | | | simplifying with (25), (28) gives: % 89.74/12.36 | | | (67) visSomeTerm(all_107_2) % 89.74/12.36 | | | % 89.74/12.36 | | | REDUCE: (26), (63) imply: % 89.74/12.36 | | | (68) vTy(vNat) % 89.74/12.36 | | | % 89.74/12.36 | | | REDUCE: (24), (63) imply: % 89.74/12.36 | | | (69) vptchecksimple(all_107_3, vNat) % 89.74/12.36 | | | % 89.74/12.36 | | | REDUCE: (23), (63) imply: % 89.74/12.36 | | | (70) ~ vptchecksimple(all_107_0, vNat) % 89.74/12.36 | | | % 89.74/12.36 | | | BETA: splitting (65) gives: % 89.74/12.36 | | | % 89.74/12.36 | | | Case 1: % 89.74/12.36 | | | | % 89.74/12.36 | | | | (71) vt1 = vZero % 89.74/12.36 | | | | % 89.74/12.36 | | | | REDUCE: (22), (71) imply: % 89.74/12.36 | | | | (72) $false % 89.74/12.36 | | | | % 89.74/12.36 | | | | CLOSE: (72) is inconsistent. % 89.74/12.36 | | | | % 89.74/12.36 | | | Case 2: % 89.74/12.36 | | | | % 89.74/12.36 | | | | (73) ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: % 89.74/12.36 | | | | vTerm] : (vTerm(v2) & ((v3 = vt1 & vSucc(v2) = vt1) | (v1 = % 89.74/12.36 | | | | vnoTerm & vreduce(all_107_3) = vnoTerm) | (vreduce(vt1) = % 89.74/12.36 | | | | v0 & vOptTerm(v0) & visSomeTerm(v0)))) % 89.74/12.36 | | | | % 89.74/12.36 | | | | DELTA: instantiating (73) with fresh symbols all_162_0, all_162_1, % 89.74/12.36 | | | | all_162_2, all_162_3 gives: % 89.74/12.36 | | | | (74) vTerm(all_162_1) & ((all_162_0 = vt1 & vSucc(all_162_1) = vt1) | % 89.74/12.36 | | | | (all_162_2 = vnoTerm & vreduce(all_107_3) = vnoTerm) | % 89.74/12.36 | | | | (vreduce(vt1) = all_162_3 & vOptTerm(all_162_3) & % 89.74/12.36 | | | | visSomeTerm(all_162_3))) % 89.74/12.36 | | | | % 89.74/12.36 | | | | ALPHA: (74) implies: % 89.74/12.36 | | | | (75) vTerm(all_162_1) % 89.74/12.36 | | | | (76) (all_162_0 = vt1 & vSucc(all_162_1) = vt1) | (all_162_2 = % 89.74/12.36 | | | | vnoTerm & vreduce(all_107_3) = vnoTerm) | (vreduce(vt1) = % 89.74/12.36 | | | | all_162_3 & vOptTerm(all_162_3) & visSomeTerm(all_162_3)) % 89.74/12.36 | | | | % 89.74/12.36 | | | | BETA: splitting (64) gives: % 89.74/12.36 | | | | % 89.74/12.36 | | | | Case 1: % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | (77) vt1 = vZero % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | REDUCE: (22), (77) imply: % 89.74/12.36 | | | | | (78) $false % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | CLOSE: (78) is inconsistent. % 89.74/12.36 | | | | | % 89.74/12.36 | | | | Case 2: % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | (79) ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? % 89.74/12.36 | | | | | [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: % 89.74/12.36 | | | | | vTerm] : (vTerm(v5) & ((v6 = vt1 & vSucc(v5) = vt1) | % 89.74/12.36 | | | | | (vreduce(vt1) = v0 & vOptTerm(v0) & ( ~ visSomeTerm(v0) | % 89.74/12.36 | | | | | (v4 = v1 & vreduce(all_107_3) = v1 & vgetTerm(v0) = v2 % 89.74/12.36 | | | | | & vsomeTerm(v3) = v1 & vPred(v2) = v3 & vOptTerm(v1) % 89.74/12.36 | | | | | & vTerm(v3) & vTerm(v2)))))) % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | DELTA: instantiating (79) with fresh symbols all_167_0, all_167_1, % 89.74/12.36 | | | | | all_167_2, all_167_3, all_167_4, all_167_5, all_167_6 gives: % 89.74/12.36 | | | | | (80) vTerm(all_167_1) & ((all_167_0 = vt1 & vSucc(all_167_1) = vt1) % 89.74/12.36 | | | | | | (vreduce(vt1) = all_167_6 & vOptTerm(all_167_6) & ( ~ % 89.74/12.36 | | | | | visSomeTerm(all_167_6) | (all_167_2 = all_167_5 & % 89.74/12.36 | | | | | vreduce(all_107_3) = all_167_5 & vgetTerm(all_167_6) = % 89.74/12.36 | | | | | all_167_4 & vsomeTerm(all_167_3) = all_167_5 & % 89.74/12.36 | | | | | vPred(all_167_4) = all_167_3 & vOptTerm(all_167_5) & % 89.74/12.36 | | | | | vTerm(all_167_3) & vTerm(all_167_4))))) % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | ALPHA: (80) implies: % 89.74/12.36 | | | | | (81) vTerm(all_167_1) % 89.74/12.36 | | | | | (82) (all_167_0 = vt1 & vSucc(all_167_1) = vt1) | (vreduce(vt1) = % 89.74/12.36 | | | | | all_167_6 & vOptTerm(all_167_6) & ( ~ visSomeTerm(all_167_6) % 89.74/12.36 | | | | | | (all_167_2 = all_167_5 & vreduce(all_107_3) = all_167_5 % 89.74/12.36 | | | | | & vgetTerm(all_167_6) = all_167_4 & vsomeTerm(all_167_3) % 89.74/12.36 | | | | | = all_167_5 & vPred(all_167_4) = all_167_3 & % 89.74/12.36 | | | | | vOptTerm(all_167_5) & vTerm(all_167_3) & % 89.74/12.36 | | | | | vTerm(all_167_4)))) % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | PRED_UNIFY: (1), (67) imply: % 89.74/12.36 | | | | | (83) ~ (all_107_2 = vnoTerm) % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | PRED_UNIFY: (6), (70) imply: % 89.74/12.36 | | | | | (84) ~ (all_107_0 = vZero) % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | BETA: splitting (66) gives: % 89.74/12.36 | | | | | % 89.74/12.36 | | | | | Case 1: % 89.74/12.36 | | | | | | % 89.74/12.36 | | | | | | % 89.74/12.36 | | | | | | GROUND_INST: instantiating (35) with vNat, all_107_0, simplifying % 89.74/12.36 | | | | | | with (25), (68), (70) gives: % 89.74/12.36 | | | | | | (85) vt1 = vZero | ~ (vsomeTerm(all_107_0) = all_110_0) | ~ % 89.74/12.36 | | | | | | vptchecksimple(all_110_1, vNat) | ~ visSomeTerm(all_110_2) % 89.74/12.36 | | | | | | | ? [v0: vTerm] : (vSucc(v0) = vt1 & vTerm(v0)) % 89.74/12.36 | | | | | | % 89.74/12.36 | | | | | | BETA: splitting (82) gives: % 89.74/12.36 | | | | | | % 89.74/12.36 | | | | | | Case 1: % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | (86) all_167_0 = vt1 & vSucc(all_167_1) = vt1 % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | ALPHA: (86) implies: % 89.74/12.36 | | | | | | | (87) vSucc(all_167_1) = vt1 % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | GROUND_INST: instantiating (30) with all_167_1, simplifying with % 89.74/12.36 | | | | | | | (81), (87) gives: % 89.74/12.36 | | | | | | | (88) $false % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | CLOSE: (88) is inconsistent. % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | Case 2: % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | (89) vreduce(vt1) = all_167_6 & vOptTerm(all_167_6) & ( ~ % 89.74/12.36 | | | | | | | visSomeTerm(all_167_6) | (all_167_2 = all_167_5 & % 89.74/12.36 | | | | | | | vreduce(all_107_3) = all_167_5 & vgetTerm(all_167_6) = % 89.74/12.36 | | | | | | | all_167_4 & vsomeTerm(all_167_3) = all_167_5 & % 89.74/12.36 | | | | | | | vPred(all_167_4) = all_167_3 & vOptTerm(all_167_5) & % 89.74/12.36 | | | | | | | vTerm(all_167_3) & vTerm(all_167_4))) % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | ALPHA: (89) implies: % 89.74/12.36 | | | | | | | (90) vreduce(vt1) = all_167_6 % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | GROUND_INST: instantiating (16) with all_95_0, all_167_6, vt1, % 89.74/12.36 | | | | | | | simplifying with (20), (90) gives: % 89.74/12.36 | | | | | | | (91) all_167_6 = all_95_0 % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | BETA: splitting (76) gives: % 89.74/12.36 | | | | | | | % 89.74/12.36 | | | | | | | Case 1: % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | | (92) all_162_0 = vt1 & vSucc(all_162_1) = vt1 % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | | ALPHA: (92) implies: % 89.74/12.36 | | | | | | | | (93) vSucc(all_162_1) = vt1 % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | | GROUND_INST: instantiating (30) with all_162_1, simplifying with % 89.74/12.36 | | | | | | | | (75), (93) gives: % 89.74/12.36 | | | | | | | | (94) $false % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | | CLOSE: (94) is inconsistent. % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | Case 2: % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | | (95) (all_162_2 = vnoTerm & vreduce(all_107_3) = vnoTerm) | % 89.74/12.36 | | | | | | | | (vreduce(vt1) = all_162_3 & vOptTerm(all_162_3) & % 89.74/12.36 | | | | | | | | visSomeTerm(all_162_3)) % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | | BETA: splitting (95) gives: % 89.74/12.36 | | | | | | | | % 89.74/12.36 | | | | | | | | Case 1: % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | (96) all_162_2 = vnoTerm & vreduce(all_107_3) = vnoTerm % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | ALPHA: (96) implies: % 89.74/12.36 | | | | | | | | | (97) vreduce(all_107_3) = vnoTerm % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | GROUND_INST: instantiating (16) with all_107_2, vnoTerm, % 89.74/12.36 | | | | | | | | | all_107_3, simplifying with (29), (97) gives: % 89.74/12.36 | | | | | | | | | (98) all_107_2 = vnoTerm % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | REDUCE: (83), (98) imply: % 89.74/12.36 | | | | | | | | | (99) $false % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | CLOSE: (99) is inconsistent. % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | Case 2: % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | (100) vreduce(vt1) = all_162_3 & vOptTerm(all_162_3) & % 89.74/12.36 | | | | | | | | | visSomeTerm(all_162_3) % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | ALPHA: (100) implies: % 89.74/12.36 | | | | | | | | | (101) visSomeTerm(all_162_3) % 89.74/12.36 | | | | | | | | | (102) vreduce(vt1) = all_162_3 % 89.74/12.36 | | | | | | | | | % 89.74/12.36 | | | | | | | | | GROUND_INST: instantiating (16) with all_95_0, all_162_3, vt1, % 89.74/12.36 | | | | | | | | | simplifying with (20), (102) gives: % 89.74/12.37 | | | | | | | | | (103) all_162_3 = all_95_0 % 89.74/12.37 | | | | | | | | | % 89.74/12.37 | | | | | | | | | REDUCE: (101), (103) imply: % 89.74/12.37 | | | | | | | | | (104) visSomeTerm(all_95_0) % 89.74/12.37 | | | | | | | | | % 89.74/12.37 | | | | | | | | | BETA: splitting (85) gives: % 89.74/12.37 | | | | | | | | | % 89.74/12.37 | | | | | | | | | Case 1: % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | (105) ~ vptchecksimple(all_110_1, vNat) % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | REDUCE: (50), (105) imply: % 89.74/12.37 | | | | | | | | | | (106) ~ vptchecksimple(all_107_3, vNat) % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | PRED_UNIFY: (69), (106) imply: % 89.74/12.37 | | | | | | | | | | (107) $false % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | CLOSE: (107) is inconsistent. % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | Case 2: % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | (108) vt1 = vZero | ~ (vsomeTerm(all_107_0) = all_110_0) % 89.74/12.37 | | | | | | | | | | | ~ visSomeTerm(all_110_2) | ? [v0: vTerm] : % 89.74/12.37 | | | | | | | | | | (vSucc(v0) = vt1 & vTerm(v0)) % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | BETA: splitting (108) gives: % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | Case 1: % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | (109) ~ (vsomeTerm(all_107_0) = all_110_0) % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | REDUCE: (62), (109) imply: % 89.74/12.37 | | | | | | | | | | | (110) ~ (vsomeTerm(all_107_0) = all_107_2) % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | PRED_UNIFY: (28), (110) imply: % 89.74/12.37 | | | | | | | | | | | (111) $false % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | CLOSE: (111) is inconsistent. % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | Case 2: % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | (112) vt1 = vZero | ~ visSomeTerm(all_110_2) | ? [v0: % 89.74/12.37 | | | | | | | | | | | vTerm] : (vSucc(v0) = vt1 & vTerm(v0)) % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | BETA: splitting (112) gives: % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | Case 1: % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | (113) ~ visSomeTerm(all_110_2) % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | REDUCE: (51), (113) imply: % 89.74/12.37 | | | | | | | | | | | | (114) ~ visSomeTerm(all_95_0) % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | PRED_UNIFY: (104), (114) imply: % 89.74/12.37 | | | | | | | | | | | | (115) $false % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | CLOSE: (115) is inconsistent. % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | Case 2: % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | (116) vt1 = vZero | ? [v0: vTerm] : (vSucc(v0) = vt1 & % 89.74/12.37 | | | | | | | | | | | | vTerm(v0)) % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | BETA: splitting (116) gives: % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | Case 1: % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | (117) vt1 = vZero % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | REDUCE: (22), (117) imply: % 89.74/12.37 | | | | | | | | | | | | | (118) $false % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | CLOSE: (118) is inconsistent. % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | Case 2: % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | (119) ? [v0: vTerm] : (vSucc(v0) = vt1 & vTerm(v0)) % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | DELTA: instantiating (119) with fresh symbol all_692_0 % 89.74/12.37 | | | | | | | | | | | | | gives: % 89.74/12.37 | | | | | | | | | | | | | (120) vSucc(all_692_0) = vt1 & vTerm(all_692_0) % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | ALPHA: (120) implies: % 89.74/12.37 | | | | | | | | | | | | | (121) vTerm(all_692_0) % 89.74/12.37 | | | | | | | | | | | | | (122) vSucc(all_692_0) = vt1 % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | GROUND_INST: instantiating (30) with all_692_0, simplifying % 89.74/12.37 | | | | | | | | | | | | | with (121), (122) gives: % 89.74/12.37 | | | | | | | | | | | | | (123) $false % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | | CLOSE: (123) is inconsistent. % 89.74/12.37 | | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | | End of split % 89.74/12.37 | | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | | End of split % 89.74/12.37 | | | | | | | | | | | % 89.74/12.37 | | | | | | | | | | End of split % 89.74/12.37 | | | | | | | | | | % 89.74/12.37 | | | | | | | | | End of split % 89.74/12.37 | | | | | | | | | % 89.74/12.37 | | | | | | | | End of split % 89.74/12.37 | | | | | | | | % 89.74/12.37 | | | | | | | End of split % 89.74/12.37 | | | | | | | % 89.74/12.37 | | | | | | End of split % 89.74/12.37 | | | | | | % 89.74/12.37 | | | | | Case 2: % 89.74/12.37 | | | | | | % 89.74/12.37 | | | | | | (124) all_107_0 = vZero % 89.74/12.37 | | | | | | % 89.74/12.37 | | | | | | REDUCE: (84), (124) imply: % 89.74/12.37 | | | | | | (125) $false % 89.74/12.37 | | | | | | % 89.74/12.37 | | | | | | CLOSE: (125) is inconsistent. % 89.74/12.37 | | | | | | % 89.74/12.37 | | | | | End of split % 89.74/12.37 | | | | | % 89.74/12.37 | | | | End of split % 89.74/12.37 | | | | % 89.74/12.37 | | | End of split % 89.74/12.37 | | | % 89.74/12.37 | | End of split % 89.74/12.37 | | % 89.74/12.37 | End of split % 89.74/12.37 | % 89.74/12.37 End of proof % 89.74/12.37 % SZS output end Proof for theBenchmark % 89.74/12.37 % 89.74/12.37 11942ms %------------------------------------------------------------------------------