%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW638_2 : TPTP v8.1.2. Released v6.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n019.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 : Fri Sep 1 00:50:58 EDT 2023 % Result : Theorem 29.74s 4.91s % Output : Proof 31.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWW638_2 : TPTP v8.1.2. Released v6.1.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.35 % Computer : n019.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Sun Aug 27 19:42:13 EDT 2023 % 0.16/0.35 % CPUTime : % 0.20/0.61 ________ _____ % 0.20/0.61 ___ __ \_________(_)________________________________ % 0.20/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.61 % 0.20/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.61 (2023-06-19) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2023 % 0.20/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.61 Amanda Stjerna. % 0.20/0.61 Free software under BSD-3-Clause. % 0.20/0.61 % 0.20/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.61 % 0.20/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.20/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 3.97/1.33 Prover 5: Preprocessing ... % 3.97/1.33 Prover 6: Preprocessing ... % 3.97/1.33 Prover 2: Preprocessing ... % 3.97/1.33 Prover 0: Preprocessing ... % 3.97/1.33 Prover 1: Preprocessing ... % 3.97/1.33 Prover 3: Preprocessing ... % 3.97/1.33 Prover 4: Preprocessing ... % 10.03/2.20 Prover 1: Warning: ignoring some quantifiers % 10.61/2.26 Prover 4: Warning: ignoring some quantifiers % 10.61/2.28 Prover 3: Warning: ignoring some quantifiers % 10.61/2.28 Prover 5: Proving ... % 10.61/2.28 Prover 1: Constructing countermodel ... % 10.61/2.29 Prover 6: Proving ... % 10.61/2.30 Prover 4: Constructing countermodel ... % 10.61/2.30 Prover 3: Constructing countermodel ... % 10.61/2.31 Prover 0: Proving ... % 11.46/2.38 Prover 2: Proving ... % 29.74/4.89 Prover 4: Found proof (size 255) % 29.74/4.90 Prover 4: proved (4250ms) % 29.74/4.91 Prover 3: stopped % 29.74/4.91 Prover 1: stopped % 29.74/4.91 Prover 2: stopped % 29.74/4.91 Prover 0: stopped % 29.74/4.91 Prover 5: stopped % 29.74/4.91 Prover 6: stopped % 29.74/4.91 % 29.74/4.91 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 29.74/4.91 % 30.41/4.94 % SZS output start Proof for theBenchmark % 30.41/4.95 Assumptions after simplification: % 30.41/4.95 --------------------------------- % 30.41/4.95 % 30.41/4.95 (alt_Concat) % 30.41/4.96 ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : ! [v3: regexp1] : ! % 30.41/4.96 [v4: regexp1] : ( ~ (concat1(v2, v3) = v4) | ~ (alt1(v0, v1) = v4) | ~ % 30.41/4.96 regexp1(v3) | ~ regexp1(v2) | ~ regexp1(v1) | ~ regexp1(v0)) % 30.41/4.96 % 30.41/4.96 (append_length) % 30.41/4.96 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (infix_plpl(v0, % 30.41/4.96 v1, v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: int] : ? % 30.41/4.96 [v5: int] : (length1(v0, v3) = v4 & length1(v0, v2) = $difference(v4, v5) & % 30.41/4.96 length1(v0, v1) = v5)) % 30.41/4.96 % 30.41/4.96 (bridgeL) % 30.41/4.96 ! [v0: list_char] : ! [v1: uni] : ( ~ (t2tb(v0) = v1) | ~ list_char(v0) | % 30.41/4.96 tb2t(v1) = v0) % 30.41/4.96 % 30.41/4.96 (bridgeR) % 30.41/4.97 ! [v0: uni] : ! [v1: list_char] : ( ~ (tb2t(v0) = v1) | ~ uni(v0) | % 30.41/4.97 t2tb(v1) = v0) % 30.41/4.97 % 30.41/4.97 (char_Concat) % 30.41/4.97 ! [v0: char2] : ! [v1: regexp1] : ! [v2: regexp1] : ! [v3: regexp1] : ( ~ % 30.41/4.97 (concat1(v1, v2) = v3) | ~ (char3(v0) = v3) | ~ regexp1(v2) | ~ % 30.41/4.97 regexp1(v1) | ~ char2(v0)) % 30.41/4.97 % 30.41/4.97 (concat_Star) % 30.41/4.97 ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : ! [v3: regexp1] : ( % 30.41/4.97 ~ (star1(v2) = v3) | ~ (concat1(v0, v1) = v3) | ~ regexp1(v2) | ~ % 30.41/4.97 regexp1(v1) | ~ regexp1(v0)) % 30.41/4.97 % 30.41/4.97 (concat_proj_1_def) % 30.41/4.97 ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : ( ~ (concat1(v0, v1) % 30.41/4.97 = v2) | ~ regexp1(v1) | ~ regexp1(v0) | concat_proj_11(v2) = v0) % 30.41/4.97 % 30.41/4.97 (concat_proj_2_def) % 30.41/4.97 ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : ( ~ (concat1(v0, v1) % 30.41/4.97 = v2) | ~ regexp1(v1) | ~ regexp1(v0) | concat_proj_21(v2) = v1) % 30.41/4.97 % 30.41/4.97 (empty_Concat) % 30.41/4.97 regexp1(empty1) & ! [v0: regexp1] : ! [v1: regexp1] : ( ~ (concat1(v0, v1) = % 30.41/4.97 empty1) | ~ regexp1(v1) | ~ regexp1(v0)) % 30.41/4.97 % 30.41/4.97 (epsilon_Concat) % 30.41/4.97 regexp1(epsilon1) & ! [v0: regexp1] : ! [v1: regexp1] : ( ~ (concat1(v0, v1) % 30.41/4.97 = epsilon1) | ~ regexp1(v1) | ~ regexp1(v0)) % 30.41/4.97 % 30.41/4.97 (length_def) % 30.41/4.97 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 30.41/4.97 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: int] : % 30.41/4.97 (length1(v0, v3) = v4 & length1(v0, v2) = $sum(v4, -1))) & ! [v0: ty] : ! % 30.41/4.97 [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | length1(v0, v1) = 0) % 30.41/4.97 % 30.41/4.97 (length_nil) % 30.41/4.98 ! [v0: ty] : ! [v1: uni] : ! [v2: int] : (v2 = 0 | ~ (length1(v0, v1) = % 30.41/4.98 v2) | ~ ty(v0) | ~ uni(v1) | ? [v3: uni] : ( ~ (v3 = v1) & nil(v0) = v3 % 30.41/4.98 & uni(v3))) & ! [v0: ty] : ! [v1: uni] : ( ~ (length1(v0, v1) = 0) | ~ % 30.41/4.98 ty(v0) | ~ uni(v1) | nil(v0) = v1) % 30.41/4.98 % 30.41/4.98 (length_nonnegative) % 30.41/4.98 ! [v0: ty] : ! [v1: uni] : ! [v2: int] : ( ~ ($lesseq(v2, -1)) | ~ % 30.41/4.98 (length1(v0, v1) = v2) | ~ ty(v0) | ~ uni(v1)) % 30.41/4.98 % 30.41/4.98 (mem_char) % 30.41/4.98 ty(char1) & ? [v0: uni] : (nil(char1) = v0 & uni(v0) & ! [v1: char2] : ! % 30.41/4.98 [v2: uni] : ( ~ (t2tb1(v1) = v2) | ~ char2(v1) | ? [v3: uni] : ? [v4: % 30.41/4.98 list_char] : ? [v5: regexp1] : (mem2(v4, v5) = 0 & tb2t(v3) = v4 & % 30.41/4.98 cons(char1, v2, v0) = v3 & char3(v1) = v5 & list_char(v4) & regexp1(v5) % 30.41/4.98 & uni(v3))) & ! [v1: char2] : ! [v2: regexp1] : ( ~ (char3(v1) = v2) | % 30.41/4.98 ~ char2(v1) | ? [v3: uni] : ? [v4: uni] : ? [v5: list_char] : % 30.41/4.98 (t2tb1(v1) = v3 & mem2(v5, v2) = 0 & tb2t(v4) = v5 & cons(char1, v3, v0) = % 30.41/4.98 v4 & list_char(v5) & uni(v4) & uni(v3)))) % 30.41/4.98 % 30.41/4.98 (mem_eps) % 30.41/4.98 regexp1(epsilon1) & ty(char1) & ? [v0: uni] : ? [v1: list_char] : (mem2(v1, % 30.41/4.98 epsilon1) = 0 & tb2t(v0) = v1 & nil(char1) = v0 & list_char(v1) & uni(v0)) % 30.41/4.98 % 30.41/4.98 (mem_inversion) % 30.41/4.99 regexp1(epsilon1) & ty(char1) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) % 30.41/4.99 = v1 & nil(char1) = v0 & list_char(v1) & uni(v0) & ! [v2: list_char] : ! % 30.41/4.99 [v3: regexp1] : (v3 = epsilon1 | ~ (mem2(v2, v3) = 0) | ~ list_char(v2) | % 30.41/4.99 ~ regexp1(v3) | ? [v4: list_char] : ? [v5: list_char] : ? [v6: regexp1] % 30.41/4.99 : ? [v7: int] : ? [v8: regexp1] : ? [v9: int] : ? [v10: uni] : ? % 30.41/4.99 [v11: uni] : ? [v12: uni] : ? [v13: list_char] : ? [v14: regexp1] : ? % 30.41/4.99 [v15: regexp1] : ? [v16: list_char] : ? [v17: list_char] : ? [v18: % 30.41/4.99 regexp1] : ? [v19: regexp1] : ? [v20: int] : ? [v21: int] : ? [v22: % 30.41/4.99 uni] : ? [v23: uni] : ? [v24: uni] : ? [v25: list_char] : ? [v26: % 30.41/4.99 regexp1] : ? [v27: list_char] : ? [v28: regexp1] : ? [v29: regexp1] : % 30.41/4.99 ? [v30: int] : ? [v31: regexp1] : ? [v32: list_char] : ? [v33: % 30.41/4.99 regexp1] : ? [v34: regexp1] : ? [v35: int] : ? [v36: regexp1] : ? % 30.41/4.99 [v37: char2] : ? [v38: uni] : ? [v39: uni] : ? [v40: list_char] : ? % 30.41/4.99 [v41: regexp1] : (list_char(v32) & list_char(v27) & list_char(v17) & % 30.41/4.99 list_char(v16) & list_char(v5) & list_char(v4) & regexp1(v34) & % 30.41/4.99 regexp1(v33) & regexp1(v29) & regexp1(v28) & regexp1(v19) & regexp1(v18) % 30.41/4.99 & regexp1(v14) & regexp1(v6) & char2(v37) & ((v41 = v3 & v40 = v2 & % 30.41/4.99 t2tb1(v37) = v38 & tb2t(v39) = v2 & cons(char1, v38, v0) = v39 & % 30.41/4.99 char3(v37) = v3 & uni(v39) & uni(v38)) | (v36 = v3 & v35 = 0 & v32 = % 30.41/4.99 v2 & mem2(v2, v33) = 0 & alt1(v33, v34) = v3) | (v31 = v3 & v30 = 0 % 30.41/4.99 & v27 = v2 & mem2(v2, v29) = 0 & alt1(v28, v29) = v3) | (v26 = v3 & % 30.41/4.99 v25 = v2 & v21 = 0 & v20 = 0 & mem2(v17, v19) = 0 & mem2(v16, v18) = % 30.41/4.99 0 & tb2t(v24) = v2 & t2tb(v17) = v23 & t2tb(v16) = v22 & % 30.41/4.99 infix_plpl(char1, v22, v23) = v24 & concat1(v18, v19) = v3 & % 30.41/4.99 uni(v24) & uni(v23) & uni(v22)) | (v15 = v3 & v2 = v1 & star1(v14) = % 30.41/4.99 v3) | (v13 = v2 & v9 = 0 & v8 = v3 & v7 = 0 & mem2(v5, v3) = 0 & % 30.41/4.99 mem2(v4, v6) = 0 & tb2t(v12) = v2 & t2tb(v5) = v11 & t2tb(v4) = v10 % 30.41/4.99 & infix_plpl(char1, v10, v11) = v12 & star1(v6) = v3 & uni(v12) & % 30.41/4.99 uni(v11) & uni(v10))))) & ! [v2: list_char] : ! [v3: regexp1] : % 30.41/4.99 (v2 = v1 | ~ (mem2(v2, v3) = 0) | ~ list_char(v2) | ~ regexp1(v3) | ? % 30.41/4.99 [v4: list_char] : ? [v5: list_char] : ? [v6: regexp1] : ? [v7: int] : % 30.41/4.99 ? [v8: regexp1] : ? [v9: int] : ? [v10: uni] : ? [v11: uni] : ? [v12: % 30.41/4.99 uni] : ? [v13: list_char] : ? [v14: regexp1] : ? [v15: list_char] : % 30.41/4.99 ? [v16: list_char] : ? [v17: regexp1] : ? [v18: regexp1] : ? [v19: int] % 30.41/4.99 : ? [v20: int] : ? [v21: uni] : ? [v22: uni] : ? [v23: uni] : ? [v24: % 30.41/4.99 list_char] : ? [v25: regexp1] : ? [v26: list_char] : ? [v27: regexp1] % 30.41/4.99 : ? [v28: regexp1] : ? [v29: int] : ? [v30: regexp1] : ? [v31: % 30.41/4.99 list_char] : ? [v32: regexp1] : ? [v33: regexp1] : ? [v34: int] : ? % 30.41/4.99 [v35: regexp1] : ? [v36: char2] : ? [v37: uni] : ? [v38: uni] : ? % 30.41/4.99 [v39: list_char] : ? [v40: regexp1] : (list_char(v31) & list_char(v26) & % 30.41/4.99 list_char(v16) & list_char(v15) & list_char(v5) & list_char(v4) & % 30.41/4.99 regexp1(v33) & regexp1(v32) & regexp1(v28) & regexp1(v27) & regexp1(v18) % 30.41/4.99 & regexp1(v17) & regexp1(v14) & regexp1(v6) & char2(v36) & ((v40 = v3 & % 30.41/4.99 v39 = v2 & t2tb1(v36) = v37 & tb2t(v38) = v2 & cons(char1, v37, v0) % 30.41/4.99 = v38 & char3(v36) = v3 & uni(v38) & uni(v37)) | (v35 = v3 & v34 = 0 % 30.41/4.99 & v31 = v2 & mem2(v2, v32) = 0 & alt1(v32, v33) = v3) | (v30 = v3 & % 30.41/4.99 v29 = 0 & v26 = v2 & mem2(v2, v28) = 0 & alt1(v27, v28) = v3) | (v25 % 30.41/4.99 = v3 & v24 = v2 & v20 = 0 & v19 = 0 & mem2(v16, v18) = 0 & mem2(v15, % 30.41/4.99 v17) = 0 & tb2t(v23) = v2 & t2tb(v16) = v22 & t2tb(v15) = v21 & % 30.41/4.99 infix_plpl(char1, v21, v22) = v23 & concat1(v17, v18) = v3 & % 30.41/4.99 uni(v23) & uni(v22) & uni(v21)) | (v13 = v2 & v9 = 0 & v8 = v3 & v7 % 30.41/4.99 = 0 & mem2(v5, v3) = 0 & mem2(v4, v6) = 0 & tb2t(v12) = v2 & % 30.41/4.99 t2tb(v5) = v11 & t2tb(v4) = v10 & infix_plpl(char1, v10, v11) = v12 % 30.41/4.99 & star1(v6) = v3 & uni(v12) & uni(v11) & uni(v10)))))) % 30.41/4.99 % 30.41/4.99 (mems1) % 30.41/4.99 ty(char1) & ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char1) = % 30.41/4.99 v0 & list_char(v1) & uni(v0) & ! [v2: regexp1] : ! [v3: regexp1] : ( ~ % 30.41/4.99 (star1(v2) = v3) | ~ regexp1(v2) | mem2(v1, v3) = 0)) % 30.41/4.99 % 30.41/4.99 (nil_Cons) % 30.41/4.99 ! [v0: ty] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ( ~ (cons(v0, v1, % 30.41/4.99 v2) = v3) | ~ ty(v0) | ~ uni(v2) | ~ uni(v1) | ? [v4: uni] : ( ~ (v4 % 30.41/4.99 = v3) & nil(v0) = v4 & uni(v4))) % 30.41/4.99 % 30.41/4.99 (nil_sort1) % 30.41/4.99 ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | ? [v2: ty] : % 30.41/4.99 (list(v0) = v2 & sort1(v2, v1) = 0 & ty(v2))) & ! [v0: ty] : ! [v1: ty] : % 30.41/4.99 ( ~ (list(v0) = v1) | ~ ty(v0) | ? [v2: uni] : (nil(v0) = v2 & sort1(v1, v2) % 30.41/4.99 = 0 & uni(v2))) % 30.41/4.99 % 30.41/4.99 (regexp_inversion) % 30.41/5.00 regexp1(epsilon1) & regexp1(empty1) & ! [v0: regexp1] : ! [v1: regexp1] : % 30.41/5.00 (v0 = epsilon1 | v0 = empty1 | ~ (star_proj_11(v0) = v1) | ~ regexp1(v0) | % 30.41/5.00 ? [v2: char2] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 30.41/5.00 [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? % 30.41/5.00 [v10: regexp1] : (concat_proj_21(v0) = v8 & concat_proj_11(v0) = v7 & % 30.41/5.00 alt_proj_21(v0) = v5 & alt_proj_11(v0) = v4 & char_proj_11(v0) = v2 & % 30.41/5.00 star1(v1) = v10 & concat1(v7, v8) = v9 & alt1(v4, v5) = v6 & char3(v2) = % 30.41/5.00 v3 & regexp1(v10) & regexp1(v9) & regexp1(v8) & regexp1(v7) & regexp1(v6) % 30.41/5.00 & regexp1(v5) & regexp1(v4) & regexp1(v3) & char2(v2) & (v10 = v0 | v9 = % 30.41/5.00 v0 | v6 = v0 | v3 = v0))) & ! [v0: regexp1] : ! [v1: regexp1] : (v0 = % 30.41/5.00 epsilon1 | v0 = empty1 | ~ (concat_proj_21(v0) = v1) | ~ regexp1(v0) | ? % 30.41/5.00 [v2: char2] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 30.41/5.00 [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? % 30.41/5.00 [v10: regexp1] : (star_proj_11(v0) = v9 & concat_proj_11(v0) = v7 & % 30.41/5.00 alt_proj_21(v0) = v5 & alt_proj_11(v0) = v4 & char_proj_11(v0) = v2 & % 30.41/5.00 star1(v9) = v10 & concat1(v7, v1) = v8 & alt1(v4, v5) = v6 & char3(v2) = % 30.41/5.00 v3 & regexp1(v10) & regexp1(v9) & regexp1(v8) & regexp1(v7) & regexp1(v6) % 30.41/5.00 & regexp1(v5) & regexp1(v4) & regexp1(v3) & char2(v2) & (v10 = v0 | v8 = % 30.41/5.00 v0 | v6 = v0 | v3 = v0))) & ! [v0: regexp1] : ! [v1: regexp1] : (v0 = % 30.41/5.00 epsilon1 | v0 = empty1 | ~ (concat_proj_11(v0) = v1) | ~ regexp1(v0) | ? % 30.41/5.00 [v2: char2] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 30.41/5.00 [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? % 30.41/5.00 [v10: regexp1] : (star_proj_11(v0) = v9 & concat_proj_21(v0) = v7 & % 30.41/5.00 alt_proj_21(v0) = v5 & alt_proj_11(v0) = v4 & char_proj_11(v0) = v2 & % 30.41/5.00 star1(v9) = v10 & concat1(v1, v7) = v8 & alt1(v4, v5) = v6 & char3(v2) = % 30.41/5.00 v3 & regexp1(v10) & regexp1(v9) & regexp1(v8) & regexp1(v7) & regexp1(v6) % 30.41/5.00 & regexp1(v5) & regexp1(v4) & regexp1(v3) & char2(v2) & (v10 = v0 | v8 = % 30.41/5.00 v0 | v6 = v0 | v3 = v0))) & ! [v0: regexp1] : ! [v1: regexp1] : (v0 = % 30.41/5.00 epsilon1 | v0 = empty1 | ~ (alt_proj_21(v0) = v1) | ~ regexp1(v0) | ? % 30.41/5.00 [v2: char2] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 30.41/5.00 [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? % 30.41/5.00 [v10: regexp1] : (star_proj_11(v0) = v9 & concat_proj_21(v0) = v7 & % 30.41/5.00 concat_proj_11(v0) = v6 & alt_proj_11(v0) = v4 & char_proj_11(v0) = v2 & % 30.41/5.00 star1(v9) = v10 & concat1(v6, v7) = v8 & alt1(v4, v1) = v5 & char3(v2) = % 30.41/5.00 v3 & regexp1(v10) & regexp1(v9) & regexp1(v8) & regexp1(v7) & regexp1(v6) % 30.41/5.00 & regexp1(v5) & regexp1(v4) & regexp1(v3) & char2(v2) & (v10 = v0 | v8 = % 30.41/5.00 v0 | v5 = v0 | v3 = v0))) & ! [v0: regexp1] : ! [v1: regexp1] : (v0 = % 30.41/5.00 epsilon1 | v0 = empty1 | ~ (alt_proj_11(v0) = v1) | ~ regexp1(v0) | ? % 30.41/5.00 [v2: char2] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 30.41/5.00 [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? % 30.41/5.00 [v10: regexp1] : (star_proj_11(v0) = v9 & concat_proj_21(v0) = v7 & % 30.41/5.00 concat_proj_11(v0) = v6 & alt_proj_21(v0) = v4 & char_proj_11(v0) = v2 & % 30.41/5.00 star1(v9) = v10 & concat1(v6, v7) = v8 & alt1(v1, v4) = v5 & char3(v2) = % 30.41/5.00 v3 & regexp1(v10) & regexp1(v9) & regexp1(v8) & regexp1(v7) & regexp1(v6) % 30.41/5.00 & regexp1(v5) & regexp1(v4) & regexp1(v3) & char2(v2) & (v10 = v0 | v8 = % 30.41/5.00 v0 | v5 = v0 | v3 = v0))) & ! [v0: regexp1] : ! [v1: char2] : (v0 = % 30.41/5.00 epsilon1 | v0 = empty1 | ~ (char_proj_11(v0) = v1) | ~ regexp1(v0) | ? % 30.41/5.00 [v2: regexp1] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 30.41/5.00 [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? % 30.41/5.00 [v10: regexp1] : (star_proj_11(v0) = v9 & concat_proj_21(v0) = v7 & % 30.41/5.00 concat_proj_11(v0) = v6 & alt_proj_21(v0) = v4 & alt_proj_11(v0) = v3 & % 30.41/5.00 star1(v9) = v10 & concat1(v6, v7) = v8 & alt1(v3, v4) = v5 & char3(v1) = % 30.41/5.00 v2 & regexp1(v10) & regexp1(v9) & regexp1(v8) & regexp1(v7) & regexp1(v6) % 30.41/5.00 & regexp1(v5) & regexp1(v4) & regexp1(v3) & regexp1(v2) & (v10 = v0 | v8 = % 30.41/5.00 v0 | v5 = v0 | v2 = v0))) % 30.41/5.00 % 30.41/5.00 (t2tb_sort) % 30.41/5.00 ty(char1) & ? [v0: ty] : (list(char1) = v0 & ty(v0) & ! [v1: list_char] : ! % 30.41/5.00 [v2: uni] : ( ~ (t2tb(v1) = v2) | ~ list_char(v1) | sort1(v0, v2) = 0)) % 30.41/5.00 % 30.41/5.00 (wP_parameter_accepts_epsilon) % 30.41/5.01 bool1(true1) & ty(char1) & ? [v0: uni] : ? [v1: list_char] : ? [v2: % 30.41/5.01 regexp1] : ? [v3: regexp1] : ? [v4: int] : ? [v5: regexp1] : ? [v6: % 30.41/5.01 bool1] : ( ~ (v6 = true1) & ~ (v4 = 0) & mem2(v1, v5) = 0 & mem2(v1, v3) = % 30.41/5.01 v4 & mem2(v1, v2) = 0 & tb2t(v0) = v1 & nil(char1) = v0 & concat1(v2, v3) = % 30.41/5.01 v5 & list_char(v1) & regexp1(v5) & regexp1(v3) & regexp1(v2) & bool1(v6) & % 30.41/5.01 uni(v0)) % 30.41/5.01 % 30.41/5.01 (function-axioms) % 30.41/5.01 ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! % 30.41/5.01 [v5: uni] : ! [v6: uni] : ! [v7: uni] : ! [v8: regexp1] : ! [v9: ty] : (v1 % 30.41/5.01 = v0 | ~ (match_regexp1(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 30.41/5.01 (match_regexp1(v9, v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! % 30.41/5.01 [v1: uni] : ! [v2: uni] : ! [v3: uni] : ! [v4: uni] : ! [v5: ty] : ! [v6: % 30.41/5.01 ty] : (v1 = v0 | ~ (match_list(v6, v5, v4, v3, v2) = v1) | ~ % 30.41/5.01 (match_list(v6, v5, v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 30.41/5.01 [v2: uni] : ! [v3: uni] : ! [v4: bool1] : ! [v5: ty] : (v1 = v0 | ~ % 30.41/5.01 (match_bool1(v5, v4, v3, v2) = v1) | ~ (match_bool1(v5, v4, v3, v2) = v0)) % 30.41/5.01 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! % 30.41/5.01 [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (mem(v4, v3, v2) = v1) | ~ (mem(v4, % 30.41/5.01 v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: % 30.41/5.01 uni] : ! [v4: ty] : (v1 = v0 | ~ (infix_plpl(v4, v3, v2) = v1) | ~ % 30.41/5.01 (infix_plpl(v4, v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] % 30.41/5.01 : ! [v3: uni] : ! [v4: ty] : (v1 = v0 | ~ (cons(v4, v3, v2) = v1) | ~ % 30.41/5.01 (cons(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 30.41/5.01 MultipleValueBool] : ! [v2: regexp1] : ! [v3: list_char] : (v1 = v0 | ~ % 30.41/5.01 (mem2(v3, v2) = v1) | ~ (mem2(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] % 30.41/5.01 : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | ~ (length1(v3, v2) = v1) | ~ % 30.41/5.01 (length1(v3, v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! % 30.41/5.01 [v3: ty] : (v1 = v0 | ~ (cons_proj_2(v3, v2) = v1) | ~ (cons_proj_2(v3, v2) % 30.41/5.01 = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: uni] : ! [v3: ty] : (v1 = % 30.41/5.01 v0 | ~ (cons_proj_1(v3, v2) = v1) | ~ (cons_proj_1(v3, v2) = v0)) & ! % 30.41/5.01 [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : ! [v3: regexp1] : (v1 = % 30.41/5.01 v0 | ~ (concat1(v3, v2) = v1) | ~ (concat1(v3, v2) = v0)) & ! [v0: % 30.41/5.01 regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : ! [v3: regexp1] : (v1 = v0 % 30.41/5.01 | ~ (alt1(v3, v2) = v1) | ~ (alt1(v3, v2) = v0)) & ! [v0: % 30.41/5.01 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: uni] : ! [v3: ty] % 30.41/5.01 : (v1 = v0 | ~ (sort1(v3, v2) = v1) | ~ (sort1(v3, v2) = v0)) & ! [v0: % 30.41/5.01 char2] : ! [v1: char2] : ! [v2: uni] : (v1 = v0 | ~ (tb2t1(v2) = v1) | ~ % 30.41/5.01 (tb2t1(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: char2] : (v1 = v0 % 30.41/5.01 | ~ (t2tb1(v2) = v1) | ~ (t2tb1(v2) = v0)) & ! [v0: list_char] : ! [v1: % 30.41/5.01 list_char] : ! [v2: uni] : (v1 = v0 | ~ (tb2t(v2) = v1) | ~ (tb2t(v2) = % 30.41/5.01 v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: list_char] : (v1 = v0 | ~ % 30.41/5.01 (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! % 30.41/5.01 [v2: ty] : (v1 = v0 | ~ (nil(v2) = v1) | ~ (nil(v2) = v0)) & ! [v0: ty] : % 30.41/5.01 ! [v1: ty] : ! [v2: ty] : (v1 = v0 | ~ (list(v2) = v1) | ~ (list(v2) = v0)) % 30.41/5.01 & ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : (v1 = v0 | ~ % 30.41/5.01 (star_proj_11(v2) = v1) | ~ (star_proj_11(v2) = v0)) & ! [v0: regexp1] : % 30.41/5.01 ! [v1: regexp1] : ! [v2: regexp1] : (v1 = v0 | ~ (concat_proj_21(v2) = v1) | % 30.41/5.01 ~ (concat_proj_21(v2) = v0)) & ! [v0: regexp1] : ! [v1: regexp1] : ! % 30.41/5.01 [v2: regexp1] : (v1 = v0 | ~ (concat_proj_11(v2) = v1) | ~ % 30.41/5.01 (concat_proj_11(v2) = v0)) & ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: % 30.41/5.01 regexp1] : (v1 = v0 | ~ (alt_proj_21(v2) = v1) | ~ (alt_proj_21(v2) = v0)) % 30.41/5.01 & ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : (v1 = v0 | ~ % 30.41/5.01 (alt_proj_11(v2) = v1) | ~ (alt_proj_11(v2) = v0)) & ! [v0: char2] : ! % 30.41/5.01 [v1: char2] : ! [v2: regexp1] : (v1 = v0 | ~ (char_proj_11(v2) = v1) | ~ % 30.41/5.01 (char_proj_11(v2) = v0)) & ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: % 30.41/5.01 regexp1] : (v1 = v0 | ~ (star1(v2) = v1) | ~ (star1(v2) = v0)) & ! [v0: % 30.41/5.01 regexp1] : ! [v1: regexp1] : ! [v2: char2] : (v1 = v0 | ~ (char3(v2) = % 30.41/5.01 v1) | ~ (char3(v2) = v0)) & ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : % 30.41/5.02 (v1 = v0 | ~ (witness1(v2) = v1) | ~ (witness1(v2) = v0)) % 30.41/5.02 % 30.41/5.02 Further assumptions not needed in the proof: % 30.41/5.02 -------------------------------------------- % 30.41/5.02 alt_Star, alt_proj_1_def, alt_proj_2_def, append_assoc, append_l_nil, % 30.41/5.02 bool_inversion, bridgeL1, bridgeR1, char_Alt, char_Star, char_proj_1_def, % 30.41/5.02 compatOrderMult, cons_proj_1_def, cons_proj_1_sort1, cons_proj_2_def, % 30.41/5.02 cons_proj_2_sort1, cons_sort1, empty_Alt, empty_Char, empty_Epsilon, empty_Star, % 30.41/5.02 epsilon_Alt, epsilon_Char, epsilon_Star, infix_plpl_def, infix_plpl_sort1, % 30.41/5.02 list_inversion, match_bool_False, match_bool_True, match_bool_sort1, % 30.41/5.02 match_list_Cons, match_list_Nil, match_list_sort1, match_regexp_Alt, % 30.41/5.02 match_regexp_Char, match_regexp_Concat, match_regexp_Empty, % 30.41/5.02 match_regexp_Epsilon, match_regexp_Star, match_regexp_sort1, mem_altl, mem_altr, % 30.41/5.02 mem_append, mem_concat, mem_decomp, mem_def, mems2, star_proj_1_def, t2tb_sort1, % 30.41/5.02 true_False, tuple0_inversion, witness_sort1 % 30.41/5.02 % 30.41/5.02 Those formulas are unsatisfiable: % 30.41/5.02 --------------------------------- % 30.41/5.02 % 30.41/5.02 Begin of proof % 30.41/5.02 | % 30.41/5.02 | ALPHA: (empty_Concat) implies: % 30.84/5.02 | (1) ! [v0: regexp1] : ! [v1: regexp1] : ( ~ (concat1(v0, v1) = empty1) | % 30.84/5.02 | ~ regexp1(v1) | ~ regexp1(v0)) % 30.84/5.02 | % 30.84/5.02 | ALPHA: (epsilon_Concat) implies: % 30.84/5.02 | (2) ! [v0: regexp1] : ! [v1: regexp1] : ( ~ (concat1(v0, v1) = epsilon1) % 30.84/5.02 | | ~ regexp1(v1) | ~ regexp1(v0)) % 30.84/5.02 | % 30.84/5.02 | ALPHA: (regexp_inversion) implies: % 30.84/5.02 | (3) ! [v0: regexp1] : ! [v1: regexp1] : (v0 = epsilon1 | v0 = empty1 | ~ % 30.84/5.02 | (concat_proj_11(v0) = v1) | ~ regexp1(v0) | ? [v2: char2] : ? [v3: % 30.84/5.02 | regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? [v6: regexp1] : % 30.84/5.02 | ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? [v10: % 30.84/5.02 | regexp1] : (star_proj_11(v0) = v9 & concat_proj_21(v0) = v7 & % 30.84/5.02 | alt_proj_21(v0) = v5 & alt_proj_11(v0) = v4 & char_proj_11(v0) = v2 % 30.84/5.02 | & star1(v9) = v10 & concat1(v1, v7) = v8 & alt1(v4, v5) = v6 & % 30.84/5.02 | char3(v2) = v3 & regexp1(v10) & regexp1(v9) & regexp1(v8) & % 30.84/5.02 | regexp1(v7) & regexp1(v6) & regexp1(v5) & regexp1(v4) & regexp1(v3) % 30.84/5.02 | & char2(v2) & (v10 = v0 | v8 = v0 | v6 = v0 | v3 = v0))) % 30.84/5.03 | (4) ! [v0: regexp1] : ! [v1: regexp1] : (v0 = epsilon1 | v0 = empty1 | ~ % 30.84/5.03 | (concat_proj_21(v0) = v1) | ~ regexp1(v0) | ? [v2: char2] : ? [v3: % 30.84/5.03 | regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? [v6: regexp1] : % 30.84/5.03 | ? [v7: regexp1] : ? [v8: regexp1] : ? [v9: regexp1] : ? [v10: % 30.84/5.03 | regexp1] : (star_proj_11(v0) = v9 & concat_proj_11(v0) = v7 & % 30.84/5.03 | alt_proj_21(v0) = v5 & alt_proj_11(v0) = v4 & char_proj_11(v0) = v2 % 30.84/5.03 | & star1(v9) = v10 & concat1(v7, v1) = v8 & alt1(v4, v5) = v6 & % 30.84/5.03 | char3(v2) = v3 & regexp1(v10) & regexp1(v9) & regexp1(v8) & % 30.84/5.03 | regexp1(v7) & regexp1(v6) & regexp1(v5) & regexp1(v4) & regexp1(v3) % 30.84/5.03 | & char2(v2) & (v10 = v0 | v8 = v0 | v6 = v0 | v3 = v0))) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (nil_sort1) implies: % 30.84/5.03 | (5) ! [v0: ty] : ! [v1: ty] : ( ~ (list(v0) = v1) | ~ ty(v0) | ? [v2: % 30.84/5.03 | uni] : (nil(v0) = v2 & sort1(v1, v2) = 0 & uni(v2))) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (length_def) implies: % 30.84/5.03 | (6) ! [v0: ty] : ! [v1: uni] : ( ~ (nil(v0) = v1) | ~ ty(v0) | % 30.84/5.03 | length1(v0, v1) = 0) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (length_nil) implies: % 30.84/5.03 | (7) ! [v0: ty] : ! [v1: uni] : ( ~ (length1(v0, v1) = 0) | ~ ty(v0) | ~ % 30.84/5.03 | uni(v1) | nil(v0) = v1) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (t2tb_sort) implies: % 30.84/5.03 | (8) ? [v0: ty] : (list(char1) = v0 & ty(v0) & ! [v1: list_char] : ! [v2: % 30.84/5.03 | uni] : ( ~ (t2tb(v1) = v2) | ~ list_char(v1) | sort1(v0, v2) = 0)) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (mem_eps) implies: % 30.84/5.03 | (9) ? [v0: uni] : ? [v1: list_char] : (mem2(v1, epsilon1) = 0 & tb2t(v0) % 30.84/5.03 | = v1 & nil(char1) = v0 & list_char(v1) & uni(v0)) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (mem_char) implies: % 30.84/5.03 | (10) ? [v0: uni] : (nil(char1) = v0 & uni(v0) & ! [v1: char2] : ! [v2: % 30.84/5.03 | uni] : ( ~ (t2tb1(v1) = v2) | ~ char2(v1) | ? [v3: uni] : ? % 30.84/5.03 | [v4: list_char] : ? [v5: regexp1] : (mem2(v4, v5) = 0 & tb2t(v3) % 30.84/5.03 | = v4 & cons(char1, v2, v0) = v3 & char3(v1) = v5 & list_char(v4) % 30.84/5.03 | & regexp1(v5) & uni(v3))) & ! [v1: char2] : ! [v2: regexp1] : % 30.84/5.03 | ( ~ (char3(v1) = v2) | ~ char2(v1) | ? [v3: uni] : ? [v4: uni] : % 30.84/5.03 | ? [v5: list_char] : (t2tb1(v1) = v3 & mem2(v5, v2) = 0 & tb2t(v4) % 30.84/5.03 | = v5 & cons(char1, v3, v0) = v4 & list_char(v5) & uni(v4) & % 30.84/5.03 | uni(v3)))) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (mems1) implies: % 30.84/5.03 | (11) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char1) = v0 & % 30.84/5.03 | list_char(v1) & uni(v0) & ! [v2: regexp1] : ! [v3: regexp1] : ( ~ % 30.84/5.03 | (star1(v2) = v3) | ~ regexp1(v2) | mem2(v1, v3) = 0)) % 30.84/5.03 | % 30.84/5.03 | ALPHA: (mem_inversion) implies: % 30.84/5.04 | (12) ? [v0: uni] : ? [v1: list_char] : (tb2t(v0) = v1 & nil(char1) = v0 & % 30.84/5.04 | list_char(v1) & uni(v0) & ! [v2: list_char] : ! [v3: regexp1] : % 30.84/5.04 | (v3 = epsilon1 | ~ (mem2(v2, v3) = 0) | ~ list_char(v2) | ~ % 30.84/5.04 | regexp1(v3) | ? [v4: list_char] : ? [v5: list_char] : ? [v6: % 30.84/5.04 | regexp1] : ? [v7: int] : ? [v8: regexp1] : ? [v9: int] : ? % 30.84/5.04 | [v10: uni] : ? [v11: uni] : ? [v12: uni] : ? [v13: list_char] : % 30.84/5.04 | ? [v14: regexp1] : ? [v15: regexp1] : ? [v16: list_char] : ? % 30.84/5.04 | [v17: list_char] : ? [v18: regexp1] : ? [v19: regexp1] : ? % 30.84/5.04 | [v20: int] : ? [v21: int] : ? [v22: uni] : ? [v23: uni] : ? % 30.84/5.04 | [v24: uni] : ? [v25: list_char] : ? [v26: regexp1] : ? [v27: % 30.84/5.04 | list_char] : ? [v28: regexp1] : ? [v29: regexp1] : ? [v30: % 30.84/5.04 | int] : ? [v31: regexp1] : ? [v32: list_char] : ? [v33: % 30.84/5.04 | regexp1] : ? [v34: regexp1] : ? [v35: int] : ? [v36: regexp1] % 30.84/5.04 | : ? [v37: char2] : ? [v38: uni] : ? [v39: uni] : ? [v40: % 30.84/5.04 | list_char] : ? [v41: regexp1] : (list_char(v32) & % 30.84/5.04 | list_char(v27) & list_char(v17) & list_char(v16) & list_char(v5) % 30.84/5.04 | & list_char(v4) & regexp1(v34) & regexp1(v33) & regexp1(v29) & % 30.84/5.04 | regexp1(v28) & regexp1(v19) & regexp1(v18) & regexp1(v14) & % 30.84/5.04 | regexp1(v6) & char2(v37) & ((v41 = v3 & v40 = v2 & t2tb1(v37) = % 30.84/5.04 | v38 & tb2t(v39) = v2 & cons(char1, v38, v0) = v39 & % 30.84/5.04 | char3(v37) = v3 & uni(v39) & uni(v38)) | (v36 = v3 & v35 = 0 % 30.84/5.04 | & v32 = v2 & mem2(v2, v33) = 0 & alt1(v33, v34) = v3) | (v31 % 30.84/5.04 | = v3 & v30 = 0 & v27 = v2 & mem2(v2, v29) = 0 & alt1(v28, % 30.84/5.04 | v29) = v3) | (v26 = v3 & v25 = v2 & v21 = 0 & v20 = 0 & % 30.84/5.04 | mem2(v17, v19) = 0 & mem2(v16, v18) = 0 & tb2t(v24) = v2 & % 30.84/5.04 | t2tb(v17) = v23 & t2tb(v16) = v22 & infix_plpl(char1, v22, % 30.84/5.04 | v23) = v24 & concat1(v18, v19) = v3 & uni(v24) & uni(v23) % 30.84/5.04 | & uni(v22)) | (v15 = v3 & v2 = v1 & star1(v14) = v3) | (v13 % 30.84/5.04 | = v2 & v9 = 0 & v8 = v3 & v7 = 0 & mem2(v5, v3) = 0 & % 30.84/5.04 | mem2(v4, v6) = 0 & tb2t(v12) = v2 & t2tb(v5) = v11 & % 30.84/5.04 | t2tb(v4) = v10 & infix_plpl(char1, v10, v11) = v12 & % 30.84/5.04 | star1(v6) = v3 & uni(v12) & uni(v11) & uni(v10))))) & ! % 30.84/5.04 | [v2: list_char] : ! [v3: regexp1] : (v2 = v1 | ~ (mem2(v2, v3) = % 30.84/5.04 | 0) | ~ list_char(v2) | ~ regexp1(v3) | ? [v4: list_char] : ? % 30.84/5.04 | [v5: list_char] : ? [v6: regexp1] : ? [v7: int] : ? [v8: % 30.84/5.04 | regexp1] : ? [v9: int] : ? [v10: uni] : ? [v11: uni] : ? % 30.84/5.04 | [v12: uni] : ? [v13: list_char] : ? [v14: regexp1] : ? [v15: % 30.84/5.04 | list_char] : ? [v16: list_char] : ? [v17: regexp1] : ? [v18: % 30.84/5.04 | regexp1] : ? [v19: int] : ? [v20: int] : ? [v21: uni] : ? % 30.84/5.04 | [v22: uni] : ? [v23: uni] : ? [v24: list_char] : ? [v25: % 30.84/5.04 | regexp1] : ? [v26: list_char] : ? [v27: regexp1] : ? [v28: % 30.84/5.04 | regexp1] : ? [v29: int] : ? [v30: regexp1] : ? [v31: % 30.84/5.04 | list_char] : ? [v32: regexp1] : ? [v33: regexp1] : ? [v34: % 30.84/5.04 | int] : ? [v35: regexp1] : ? [v36: char2] : ? [v37: uni] : ? % 30.84/5.04 | [v38: uni] : ? [v39: list_char] : ? [v40: regexp1] : % 30.84/5.04 | (list_char(v31) & list_char(v26) & list_char(v16) & list_char(v15) % 30.84/5.04 | & list_char(v5) & list_char(v4) & regexp1(v33) & regexp1(v32) & % 30.84/5.04 | regexp1(v28) & regexp1(v27) & regexp1(v18) & regexp1(v17) & % 30.84/5.04 | regexp1(v14) & regexp1(v6) & char2(v36) & ((v40 = v3 & v39 = v2 % 30.84/5.04 | & t2tb1(v36) = v37 & tb2t(v38) = v2 & cons(char1, v37, v0) = % 30.84/5.04 | v38 & char3(v36) = v3 & uni(v38) & uni(v37)) | (v35 = v3 & % 30.84/5.04 | v34 = 0 & v31 = v2 & mem2(v2, v32) = 0 & alt1(v32, v33) = % 30.84/5.04 | v3) | (v30 = v3 & v29 = 0 & v26 = v2 & mem2(v2, v28) = 0 & % 30.84/5.04 | alt1(v27, v28) = v3) | (v25 = v3 & v24 = v2 & v20 = 0 & v19 % 30.84/5.04 | = 0 & mem2(v16, v18) = 0 & mem2(v15, v17) = 0 & tb2t(v23) = % 30.84/5.04 | v2 & t2tb(v16) = v22 & t2tb(v15) = v21 & infix_plpl(char1, % 30.84/5.04 | v21, v22) = v23 & concat1(v17, v18) = v3 & uni(v23) & % 30.84/5.04 | uni(v22) & uni(v21)) | (v13 = v2 & v9 = 0 & v8 = v3 & v7 = 0 % 30.84/5.04 | & mem2(v5, v3) = 0 & mem2(v4, v6) = 0 & tb2t(v12) = v2 & % 30.84/5.04 | t2tb(v5) = v11 & t2tb(v4) = v10 & infix_plpl(char1, v10, % 30.84/5.04 | v11) = v12 & star1(v6) = v3 & uni(v12) & uni(v11) & % 30.84/5.04 | uni(v10)))))) % 30.84/5.04 | % 30.84/5.04 | ALPHA: (wP_parameter_accepts_epsilon) implies: % 30.84/5.04 | (13) ty(char1) % 30.84/5.04 | (14) ? [v0: uni] : ? [v1: list_char] : ? [v2: regexp1] : ? [v3: % 30.84/5.04 | regexp1] : ? [v4: int] : ? [v5: regexp1] : ? [v6: bool1] : ( ~ % 30.84/5.04 | (v6 = true1) & ~ (v4 = 0) & mem2(v1, v5) = 0 & mem2(v1, v3) = v4 & % 30.84/5.04 | mem2(v1, v2) = 0 & tb2t(v0) = v1 & nil(char1) = v0 & concat1(v2, v3) % 30.84/5.04 | = v5 & list_char(v1) & regexp1(v5) & regexp1(v3) & regexp1(v2) & % 30.84/5.04 | bool1(v6) & uni(v0)) % 30.84/5.04 | % 30.84/5.04 | ALPHA: (function-axioms) implies: % 30.84/5.04 | (15) ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : (v1 = v0 | ~ % 30.84/5.04 | (concat_proj_11(v2) = v1) | ~ (concat_proj_11(v2) = v0)) % 30.84/5.04 | (16) ! [v0: regexp1] : ! [v1: regexp1] : ! [v2: regexp1] : (v1 = v0 | ~ % 30.84/5.04 | (concat_proj_21(v2) = v1) | ~ (concat_proj_21(v2) = v0)) % 30.84/5.04 | (17) ! [v0: uni] : ! [v1: uni] : ! [v2: ty] : (v1 = v0 | ~ (nil(v2) = % 30.84/5.04 | v1) | ~ (nil(v2) = v0)) % 30.84/5.04 | (18) ! [v0: uni] : ! [v1: uni] : ! [v2: list_char] : (v1 = v0 | ~ % 30.84/5.04 | (t2tb(v2) = v1) | ~ (t2tb(v2) = v0)) % 30.84/5.04 | (19) ! [v0: list_char] : ! [v1: list_char] : ! [v2: uni] : (v1 = v0 | ~ % 30.84/5.04 | (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 30.84/5.04 | (20) ! [v0: int] : ! [v1: int] : ! [v2: uni] : ! [v3: ty] : (v1 = v0 | % 30.84/5.04 | ~ (length1(v3, v2) = v1) | ~ (length1(v3, v2) = v0)) % 30.84/5.04 | (21) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 30.84/5.04 | regexp1] : ! [v3: list_char] : (v1 = v0 | ~ (mem2(v3, v2) = v1) | % 30.84/5.04 | ~ (mem2(v3, v2) = v0)) % 30.84/5.04 | % 30.84/5.05 | DELTA: instantiating (9) with fresh symbols all_83_0, all_83_1 gives: % 30.84/5.05 | (22) mem2(all_83_0, epsilon1) = 0 & tb2t(all_83_1) = all_83_0 & nil(char1) % 30.84/5.05 | = all_83_1 & list_char(all_83_0) & uni(all_83_1) % 30.84/5.05 | % 30.84/5.05 | ALPHA: (22) implies: % 30.84/5.05 | (23) nil(char1) = all_83_1 % 30.84/5.05 | (24) tb2t(all_83_1) = all_83_0 % 30.84/5.05 | % 30.84/5.05 | DELTA: instantiating (8) with fresh symbol all_86_0 gives: % 30.84/5.05 | (25) list(char1) = all_86_0 & ty(all_86_0) & ! [v0: list_char] : ! [v1: % 30.84/5.05 | uni] : ( ~ (t2tb(v0) = v1) | ~ list_char(v0) | sort1(all_86_0, v1) % 30.84/5.05 | = 0) % 30.84/5.05 | % 30.84/5.05 | ALPHA: (25) implies: % 30.84/5.05 | (26) list(char1) = all_86_0 % 30.84/5.05 | % 30.84/5.05 | DELTA: instantiating (11) with fresh symbols all_89_0, all_89_1 gives: % 30.84/5.05 | (27) tb2t(all_89_1) = all_89_0 & nil(char1) = all_89_1 & % 30.84/5.05 | list_char(all_89_0) & uni(all_89_1) & ! [v0: regexp1] : ! [v1: % 30.84/5.05 | regexp1] : ( ~ (star1(v0) = v1) | ~ regexp1(v0) | mem2(all_89_0, % 30.84/5.05 | v1) = 0) % 30.84/5.05 | % 30.84/5.05 | ALPHA: (27) implies: % 30.84/5.05 | (28) uni(all_89_1) % 30.84/5.05 | (29) list_char(all_89_0) % 30.84/5.05 | (30) nil(char1) = all_89_1 % 30.84/5.05 | (31) tb2t(all_89_1) = all_89_0 % 30.84/5.05 | % 30.84/5.05 | DELTA: instantiating (14) with fresh symbols all_92_0, all_92_1, all_92_2, % 30.84/5.05 | all_92_3, all_92_4, all_92_5, all_92_6 gives: % 30.84/5.05 | (32) ~ (all_92_0 = true1) & ~ (all_92_2 = 0) & mem2(all_92_5, all_92_1) = % 30.84/5.05 | 0 & mem2(all_92_5, all_92_3) = all_92_2 & mem2(all_92_5, all_92_4) = 0 % 30.84/5.05 | & tb2t(all_92_6) = all_92_5 & nil(char1) = all_92_6 & % 30.84/5.05 | concat1(all_92_4, all_92_3) = all_92_1 & list_char(all_92_5) & % 30.84/5.05 | regexp1(all_92_1) & regexp1(all_92_3) & regexp1(all_92_4) & % 30.84/5.05 | bool1(all_92_0) & uni(all_92_6) % 30.84/5.05 | % 30.84/5.05 | ALPHA: (32) implies: % 30.84/5.05 | (33) ~ (all_92_2 = 0) % 30.84/5.05 | (34) regexp1(all_92_4) % 30.84/5.05 | (35) regexp1(all_92_3) % 30.84/5.05 | (36) regexp1(all_92_1) % 30.84/5.05 | (37) concat1(all_92_4, all_92_3) = all_92_1 % 30.84/5.05 | (38) nil(char1) = all_92_6 % 30.84/5.05 | (39) tb2t(all_92_6) = all_92_5 % 30.84/5.05 | (40) mem2(all_92_5, all_92_4) = 0 % 30.84/5.05 | (41) mem2(all_92_5, all_92_3) = all_92_2 % 30.84/5.05 | (42) mem2(all_92_5, all_92_1) = 0 % 30.84/5.05 | % 30.84/5.05 | DELTA: instantiating (10) with fresh symbol all_94_0 gives: % 30.84/5.05 | (43) nil(char1) = all_94_0 & uni(all_94_0) & ! [v0: char2] : ! [v1: uni] % 30.84/5.05 | : ( ~ (t2tb1(v0) = v1) | ~ char2(v0) | ? [v2: uni] : ? [v3: % 30.84/5.05 | list_char] : ? [v4: regexp1] : (mem2(v3, v4) = 0 & tb2t(v2) = v3 % 30.84/5.05 | & cons(char1, v1, all_94_0) = v2 & char3(v0) = v4 & list_char(v3) % 30.84/5.05 | & regexp1(v4) & uni(v2))) & ! [v0: char2] : ! [v1: regexp1] : ( % 30.84/5.05 | ~ (char3(v0) = v1) | ~ char2(v0) | ? [v2: uni] : ? [v3: uni] : ? % 30.84/5.05 | [v4: list_char] : (t2tb1(v0) = v2 & mem2(v4, v1) = 0 & tb2t(v3) = v4 % 30.84/5.05 | & cons(char1, v2, all_94_0) = v3 & list_char(v4) & uni(v3) & % 30.84/5.05 | uni(v2))) % 30.84/5.05 | % 30.84/5.05 | ALPHA: (43) implies: % 30.84/5.05 | (44) nil(char1) = all_94_0 % 30.84/5.05 | (45) ! [v0: char2] : ! [v1: regexp1] : ( ~ (char3(v0) = v1) | ~ % 30.84/5.05 | char2(v0) | ? [v2: uni] : ? [v3: uni] : ? [v4: list_char] : % 30.84/5.05 | (t2tb1(v0) = v2 & mem2(v4, v1) = 0 & tb2t(v3) = v4 & cons(char1, v2, % 30.84/5.05 | all_94_0) = v3 & list_char(v4) & uni(v3) & uni(v2))) % 30.84/5.05 | % 30.84/5.05 | DELTA: instantiating (12) with fresh symbols all_97_0, all_97_1 gives: % 30.84/5.06 | (46) tb2t(all_97_1) = all_97_0 & nil(char1) = all_97_1 & % 30.84/5.06 | list_char(all_97_0) & uni(all_97_1) & ! [v0: list_char] : ! [v1: % 30.84/5.06 | regexp1] : (v1 = epsilon1 | ~ (mem2(v0, v1) = 0) | ~ list_char(v0) % 30.84/5.06 | | ~ regexp1(v1) | ? [v2: list_char] : ? [v3: list_char] : ? [v4: % 30.84/5.06 | regexp1] : ? [v5: int] : ? [v6: regexp1] : ? [v7: int] : ? % 30.84/5.06 | [v8: uni] : ? [v9: uni] : ? [v10: uni] : ? [v11: list_char] : ? % 30.84/5.06 | [v12: regexp1] : ? [v13: regexp1] : ? [v14: list_char] : ? [v15: % 30.84/5.06 | list_char] : ? [v16: regexp1] : ? [v17: regexp1] : ? [v18: int] % 30.84/5.06 | : ? [v19: int] : ? [v20: uni] : ? [v21: uni] : ? [v22: uni] : ? % 30.84/5.06 | [v23: list_char] : ? [v24: regexp1] : ? [v25: list_char] : ? % 30.84/5.06 | [v26: regexp1] : ? [v27: regexp1] : ? [v28: int] : ? [v29: % 30.84/5.06 | regexp1] : ? [v30: list_char] : ? [v31: regexp1] : ? [v32: % 30.84/5.06 | regexp1] : ? [v33: int] : ? [v34: regexp1] : ? [v35: char2] : % 30.84/5.06 | ? [v36: uni] : ? [v37: uni] : ? [v38: list_char] : ? [v39: % 30.84/5.06 | regexp1] : (list_char(v30) & list_char(v25) & list_char(v15) & % 30.84/5.06 | list_char(v14) & list_char(v3) & list_char(v2) & regexp1(v32) & % 30.84/5.06 | regexp1(v31) & regexp1(v27) & regexp1(v26) & regexp1(v17) & % 30.84/5.06 | regexp1(v16) & regexp1(v12) & regexp1(v4) & char2(v35) & ((v39 = % 30.84/5.06 | v1 & v38 = v0 & t2tb1(v35) = v36 & tb2t(v37) = v0 & % 30.84/5.06 | cons(char1, v36, all_97_1) = v37 & char3(v35) = v1 & uni(v37) % 30.84/5.06 | & uni(v36)) | (v34 = v1 & v33 = 0 & v30 = v0 & mem2(v0, v31) = % 30.84/5.06 | 0 & alt1(v31, v32) = v1) | (v29 = v1 & v28 = 0 & v25 = v0 & % 30.84/5.06 | mem2(v0, v27) = 0 & alt1(v26, v27) = v1) | (v24 = v1 & v23 = % 30.84/5.06 | v0 & v19 = 0 & v18 = 0 & mem2(v15, v17) = 0 & mem2(v14, v16) = % 30.84/5.06 | 0 & tb2t(v22) = v0 & t2tb(v15) = v21 & t2tb(v14) = v20 & % 30.84/5.06 | infix_plpl(char1, v20, v21) = v22 & concat1(v16, v17) = v1 & % 30.84/5.06 | uni(v22) & uni(v21) & uni(v20)) | (v13 = v1 & v0 = all_97_0 & % 30.84/5.06 | star1(v12) = v1) | (v11 = v0 & v7 = 0 & v6 = v1 & v5 = 0 & % 30.84/5.06 | mem2(v3, v1) = 0 & mem2(v2, v4) = 0 & tb2t(v10) = v0 & % 30.84/5.06 | t2tb(v3) = v9 & t2tb(v2) = v8 & infix_plpl(char1, v8, v9) = % 30.84/5.06 | v10 & star1(v4) = v1 & uni(v10) & uni(v9) & uni(v8))))) & ! % 30.84/5.06 | [v0: any] : ! [v1: regexp1] : (v0 = all_97_0 | ~ (mem2(v0, v1) = 0) % 30.84/5.06 | | ~ list_char(v0) | ~ regexp1(v1) | ? [v2: list_char] : ? [v3: % 30.84/5.06 | list_char] : ? [v4: regexp1] : ? [v5: int] : ? [v6: regexp1] : % 30.84/5.06 | ? [v7: int] : ? [v8: uni] : ? [v9: uni] : ? [v10: uni] : ? [v11: % 30.84/5.06 | any] : ? [v12: regexp1] : ? [v13: list_char] : ? [v14: % 30.84/5.06 | list_char] : ? [v15: regexp1] : ? [v16: regexp1] : ? [v17: int] % 30.84/5.06 | : ? [v18: int] : ? [v19: uni] : ? [v20: uni] : ? [v21: uni] : ? % 30.84/5.06 | [v22: any] : ? [v23: regexp1] : ? [v24: list_char] : ? [v25: % 30.84/5.06 | regexp1] : ? [v26: regexp1] : ? [v27: int] : ? [v28: regexp1] : % 30.84/5.06 | ? [v29: list_char] : ? [v30: regexp1] : ? [v31: regexp1] : ? % 30.84/5.06 | [v32: int] : ? [v33: regexp1] : ? [v34: char2] : ? [v35: uni] : % 30.84/5.06 | ? [v36: uni] : ? [v37: any] : ? [v38: regexp1] : (list_char(v29) & % 30.84/5.06 | list_char(v24) & list_char(v14) & list_char(v13) & list_char(v3) & % 30.84/5.06 | list_char(v2) & regexp1(v31) & regexp1(v30) & regexp1(v26) & % 30.84/5.06 | regexp1(v25) & regexp1(v16) & regexp1(v15) & regexp1(v12) & % 30.84/5.06 | regexp1(v4) & char2(v34) & ((v38 = v1 & v37 = v0 & t2tb1(v34) = % 30.84/5.06 | v35 & tb2t(v36) = v0 & cons(char1, v35, all_97_1) = v36 & % 30.84/5.06 | char3(v34) = v1 & uni(v36) & uni(v35)) | (v33 = v1 & v32 = 0 & % 30.84/5.06 | v29 = v0 & mem2(v0, v30) = 0 & alt1(v30, v31) = v1) | (v28 = % 30.84/5.06 | v1 & v27 = 0 & v24 = v0 & mem2(v0, v26) = 0 & alt1(v25, v26) = % 30.84/5.06 | v1) | (v23 = v1 & v22 = v0 & v18 = 0 & v17 = 0 & mem2(v14, % 30.84/5.06 | v16) = 0 & mem2(v13, v15) = 0 & tb2t(v21) = v0 & t2tb(v14) = % 30.84/5.06 | v20 & t2tb(v13) = v19 & infix_plpl(char1, v19, v20) = v21 & % 30.84/5.06 | concat1(v15, v16) = v1 & uni(v21) & uni(v20) & uni(v19)) | % 30.84/5.06 | (v11 = v0 & v7 = 0 & v6 = v1 & v5 = 0 & mem2(v3, v1) = 0 & % 30.84/5.06 | mem2(v2, v4) = 0 & tb2t(v10) = v0 & t2tb(v3) = v9 & t2tb(v2) = % 30.84/5.06 | v8 & infix_plpl(char1, v8, v9) = v10 & star1(v4) = v1 & % 30.84/5.06 | uni(v10) & uni(v9) & uni(v8))))) % 30.84/5.06 | % 30.84/5.06 | ALPHA: (46) implies: % 30.84/5.06 | (47) nil(char1) = all_97_1 % 30.84/5.06 | (48) tb2t(all_97_1) = all_97_0 % 30.84/5.06 | (49) ! [v0: list_char] : ! [v1: regexp1] : (v1 = epsilon1 | ~ (mem2(v0, % 30.84/5.06 | v1) = 0) | ~ list_char(v0) | ~ regexp1(v1) | ? [v2: % 30.84/5.06 | list_char] : ? [v3: list_char] : ? [v4: regexp1] : ? [v5: int] % 30.84/5.06 | : ? [v6: regexp1] : ? [v7: int] : ? [v8: uni] : ? [v9: uni] : ? % 30.84/5.06 | [v10: uni] : ? [v11: list_char] : ? [v12: regexp1] : ? [v13: % 30.84/5.06 | regexp1] : ? [v14: list_char] : ? [v15: list_char] : ? [v16: % 30.84/5.06 | regexp1] : ? [v17: regexp1] : ? [v18: int] : ? [v19: int] : ? % 30.84/5.06 | [v20: uni] : ? [v21: uni] : ? [v22: uni] : ? [v23: list_char] : % 30.84/5.06 | ? [v24: regexp1] : ? [v25: list_char] : ? [v26: regexp1] : ? % 30.84/5.06 | [v27: regexp1] : ? [v28: int] : ? [v29: regexp1] : ? [v30: % 30.84/5.06 | list_char] : ? [v31: regexp1] : ? [v32: regexp1] : ? [v33: int] % 30.84/5.06 | : ? [v34: regexp1] : ? [v35: char2] : ? [v36: uni] : ? [v37: % 30.84/5.06 | uni] : ? [v38: list_char] : ? [v39: regexp1] : (list_char(v30) & % 30.84/5.06 | list_char(v25) & list_char(v15) & list_char(v14) & list_char(v3) & % 30.84/5.06 | list_char(v2) & regexp1(v32) & regexp1(v31) & regexp1(v27) & % 30.84/5.06 | regexp1(v26) & regexp1(v17) & regexp1(v16) & regexp1(v12) & % 30.84/5.06 | regexp1(v4) & char2(v35) & ((v39 = v1 & v38 = v0 & t2tb1(v35) = % 30.84/5.06 | v36 & tb2t(v37) = v0 & cons(char1, v36, all_97_1) = v37 & % 30.84/5.06 | char3(v35) = v1 & uni(v37) & uni(v36)) | (v34 = v1 & v33 = 0 & % 30.84/5.06 | v30 = v0 & mem2(v0, v31) = 0 & alt1(v31, v32) = v1) | (v29 = % 30.84/5.06 | v1 & v28 = 0 & v25 = v0 & mem2(v0, v27) = 0 & alt1(v26, v27) = % 30.84/5.06 | v1) | (v24 = v1 & v23 = v0 & v19 = 0 & v18 = 0 & mem2(v15, % 30.84/5.06 | v17) = 0 & mem2(v14, v16) = 0 & tb2t(v22) = v0 & t2tb(v15) = % 30.84/5.06 | v21 & t2tb(v14) = v20 & infix_plpl(char1, v20, v21) = v22 & % 30.84/5.06 | concat1(v16, v17) = v1 & uni(v22) & uni(v21) & uni(v20)) | % 30.84/5.06 | (v13 = v1 & v0 = all_97_0 & star1(v12) = v1) | (v11 = v0 & v7 = % 30.84/5.06 | 0 & v6 = v1 & v5 = 0 & mem2(v3, v1) = 0 & mem2(v2, v4) = 0 & % 30.84/5.06 | tb2t(v10) = v0 & t2tb(v3) = v9 & t2tb(v2) = v8 & % 30.84/5.06 | infix_plpl(char1, v8, v9) = v10 & star1(v4) = v1 & uni(v10) & % 30.84/5.06 | uni(v9) & uni(v8))))) % 30.84/5.06 | % 30.84/5.06 | GROUND_INST: instantiating (17) with all_92_6, all_94_0, char1, simplifying % 30.84/5.06 | with (38), (44) gives: % 30.84/5.06 | (50) all_94_0 = all_92_6 % 30.84/5.06 | % 30.84/5.06 | GROUND_INST: instantiating (17) with all_89_1, all_94_0, char1, simplifying % 30.84/5.06 | with (30), (44) gives: % 30.84/5.06 | (51) all_94_0 = all_89_1 % 30.84/5.06 | % 30.84/5.06 | GROUND_INST: instantiating (17) with all_94_0, all_97_1, char1, simplifying % 30.84/5.06 | with (44), (47) gives: % 30.84/5.06 | (52) all_97_1 = all_94_0 % 30.84/5.06 | % 30.84/5.06 | GROUND_INST: instantiating (17) with all_83_1, all_97_1, char1, simplifying % 30.84/5.06 | with (23), (47) gives: % 30.84/5.06 | (53) all_97_1 = all_83_1 % 30.84/5.06 | % 30.84/5.06 | COMBINE_EQS: (52), (53) imply: % 30.84/5.06 | (54) all_94_0 = all_83_1 % 30.84/5.06 | % 30.84/5.06 | SIMP: (54) implies: % 30.84/5.07 | (55) all_94_0 = all_83_1 % 30.84/5.07 | % 30.84/5.07 | COMBINE_EQS: (50), (55) imply: % 30.84/5.07 | (56) all_92_6 = all_83_1 % 30.84/5.07 | % 30.84/5.07 | COMBINE_EQS: (50), (51) imply: % 30.84/5.07 | (57) all_92_6 = all_89_1 % 30.84/5.07 | % 30.84/5.07 | COMBINE_EQS: (56), (57) imply: % 30.84/5.07 | (58) all_89_1 = all_83_1 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (48), (53) imply: % 30.84/5.07 | (59) tb2t(all_83_1) = all_97_0 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (39), (56) imply: % 30.84/5.07 | (60) tb2t(all_83_1) = all_92_5 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (31), (58) imply: % 30.84/5.07 | (61) tb2t(all_83_1) = all_89_0 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (28), (58) imply: % 30.84/5.07 | (62) uni(all_83_1) % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (19) with all_83_0, all_92_5, all_83_1, simplifying % 30.84/5.07 | with (24), (60) gives: % 30.84/5.07 | (63) all_92_5 = all_83_0 % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (19) with all_92_5, all_97_0, all_83_1, simplifying % 30.84/5.07 | with (59), (60) gives: % 30.84/5.07 | (64) all_97_0 = all_92_5 % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (19) with all_89_0, all_97_0, all_83_1, simplifying % 30.84/5.07 | with (59), (61) gives: % 30.84/5.07 | (65) all_97_0 = all_89_0 % 30.84/5.07 | % 30.84/5.07 | COMBINE_EQS: (64), (65) imply: % 30.84/5.07 | (66) all_92_5 = all_89_0 % 30.84/5.07 | % 30.84/5.07 | SIMP: (66) implies: % 30.84/5.07 | (67) all_92_5 = all_89_0 % 30.84/5.07 | % 30.84/5.07 | COMBINE_EQS: (63), (67) imply: % 30.84/5.07 | (68) all_89_0 = all_83_0 % 30.84/5.07 | % 30.84/5.07 | SIMP: (68) implies: % 30.84/5.07 | (69) all_89_0 = all_83_0 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (42), (63) imply: % 30.84/5.07 | (70) mem2(all_83_0, all_92_1) = 0 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (41), (63) imply: % 30.84/5.07 | (71) mem2(all_83_0, all_92_3) = all_92_2 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (40), (63) imply: % 30.84/5.07 | (72) mem2(all_83_0, all_92_4) = 0 % 30.84/5.07 | % 30.84/5.07 | REDUCE: (29), (69) imply: % 30.84/5.07 | (73) list_char(all_83_0) % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (concat_proj_2_def) with all_92_4, all_92_3, % 30.84/5.07 | all_92_1, simplifying with (34), (35), (37) gives: % 30.84/5.07 | (74) concat_proj_21(all_92_1) = all_92_3 % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (concat_proj_1_def) with all_92_4, all_92_3, % 30.84/5.07 | all_92_1, simplifying with (34), (35), (37) gives: % 30.84/5.07 | (75) concat_proj_11(all_92_1) = all_92_4 % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (5) with char1, all_86_0, simplifying with (13), % 30.84/5.07 | (26) gives: % 30.84/5.07 | (76) ? [v0: uni] : (nil(char1) = v0 & sort1(all_86_0, v0) = 0 & uni(v0)) % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (6) with char1, all_83_1, simplifying with (13), % 30.84/5.07 | (23) gives: % 30.84/5.07 | (77) length1(char1, all_83_1) = 0 % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (bridgeR) with all_83_1, all_83_0, simplifying with % 30.84/5.07 | (24), (62) gives: % 30.84/5.07 | (78) t2tb(all_83_0) = all_83_1 % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (49) with all_83_0, all_92_4, simplifying with % 30.84/5.07 | (34), (72), (73) gives: % 30.84/5.07 | (79) all_92_4 = epsilon1 | ? [v0: list_char] : ? [v1: list_char] : ? % 30.84/5.07 | [v2: regexp1] : ? [v3: int] : ? [v4: int] : ? [v5: int] : ? [v6: % 30.84/5.07 | uni] : ? [v7: uni] : ? [v8: uni] : ? [v9: int] : ? [v10: % 30.84/5.07 | regexp1] : ? [v11: int] : ? [v12: list_char] : ? [v13: list_char] % 30.84/5.07 | : ? [v14: regexp1] : ? [v15: regexp1] : ? [v16: int] : ? [v17: % 30.84/5.07 | int] : ? [v18: uni] : ? [v19: uni] : ? [v20: uni] : ? [v21: int] % 30.84/5.07 | : ? [v22: int] : ? [v23: list_char] : ? [v24: regexp1] : ? [v25: % 30.84/5.07 | regexp1] : ? [v26: int] : ? [v27: int] : ? [v28: list_char] : ? % 30.84/5.07 | [v29: regexp1] : ? [v30: regexp1] : ? [v31: int] : ? [v32: int] : % 30.84/5.07 | ? [v33: char2] : ? [v34: uni] : ? [v35: uni] : ? [v36: int] : ? % 30.84/5.07 | [v37: int] : (list_char(v28) & list_char(v23) & list_char(v13) & % 30.84/5.07 | list_char(v12) & list_char(v1) & list_char(v0) & regexp1(v30) & % 30.84/5.07 | regexp1(v29) & regexp1(v25) & regexp1(v24) & regexp1(v15) & % 30.84/5.07 | regexp1(v14) & regexp1(v10) & regexp1(v2) & char2(v33) & ((v37 = % 30.84/5.07 | all_92_4 & v36 = all_83_0 & t2tb1(v33) = v34 & tb2t(v35) = % 30.84/5.07 | all_83_0 & cons(char1, v34, all_97_1) = v35 & char3(v33) = % 30.84/5.07 | all_92_4 & uni(v35) & uni(v34)) | (v32 = all_92_4 & v31 = 0 & % 30.84/5.07 | v28 = all_83_0 & mem2(all_83_0, v29) = 0 & alt1(v29, v30) = % 30.84/5.07 | all_92_4) | (v27 = all_92_4 & v26 = 0 & v23 = all_83_0 & % 30.84/5.07 | mem2(all_83_0, v25) = 0 & alt1(v24, v25) = all_92_4) | (v22 = % 30.84/5.07 | all_92_4 & v21 = all_83_0 & v17 = 0 & v16 = 0 & mem2(v13, v15) = % 30.84/5.07 | 0 & mem2(v12, v14) = 0 & tb2t(v20) = all_83_0 & t2tb(v13) = v19 % 30.84/5.07 | & t2tb(v12) = v18 & infix_plpl(char1, v18, v19) = v20 & % 30.84/5.07 | concat1(v14, v15) = all_92_4 & uni(v20) & uni(v19) & uni(v18)) | % 30.84/5.07 | (v11 = all_92_4 & all_97_0 = all_83_0 & star1(v10) = all_92_4) | % 30.84/5.07 | (v9 = all_83_0 & v5 = 0 & v4 = all_92_4 & v3 = 0 & mem2(v1, % 30.84/5.07 | all_92_4) = 0 & mem2(v0, v2) = 0 & tb2t(v8) = all_83_0 & % 30.84/5.07 | t2tb(v1) = v7 & t2tb(v0) = v6 & infix_plpl(char1, v6, v7) = v8 & % 30.84/5.07 | star1(v2) = all_92_4 & uni(v8) & uni(v7) & uni(v6)))) % 30.84/5.07 | % 30.84/5.07 | GROUND_INST: instantiating (49) with all_83_0, all_92_1, simplifying with % 30.84/5.07 | (36), (70), (73) gives: % 30.84/5.08 | (80) all_92_1 = epsilon1 | ? [v0: list_char] : ? [v1: list_char] : ? % 30.84/5.08 | [v2: regexp1] : ? [v3: int] : ? [v4: int] : ? [v5: int] : ? [v6: % 30.84/5.08 | uni] : ? [v7: uni] : ? [v8: uni] : ? [v9: int] : ? [v10: % 30.84/5.08 | regexp1] : ? [v11: int] : ? [v12: list_char] : ? [v13: list_char] % 30.84/5.08 | : ? [v14: regexp1] : ? [v15: regexp1] : ? [v16: int] : ? [v17: % 30.84/5.08 | int] : ? [v18: uni] : ? [v19: uni] : ? [v20: uni] : ? [v21: int] % 30.84/5.08 | : ? [v22: int] : ? [v23: list_char] : ? [v24: regexp1] : ? [v25: % 30.84/5.08 | regexp1] : ? [v26: int] : ? [v27: int] : ? [v28: list_char] : ? % 30.84/5.08 | [v29: regexp1] : ? [v30: regexp1] : ? [v31: int] : ? [v32: int] : % 30.84/5.08 | ? [v33: char2] : ? [v34: uni] : ? [v35: uni] : ? [v36: int] : ? % 30.84/5.08 | [v37: int] : (list_char(v28) & list_char(v23) & list_char(v13) & % 30.84/5.08 | list_char(v12) & list_char(v1) & list_char(v0) & regexp1(v30) & % 30.84/5.08 | regexp1(v29) & regexp1(v25) & regexp1(v24) & regexp1(v15) & % 30.84/5.08 | regexp1(v14) & regexp1(v10) & regexp1(v2) & char2(v33) & ((v37 = % 30.84/5.08 | all_92_1 & v36 = all_83_0 & t2tb1(v33) = v34 & tb2t(v35) = % 30.84/5.08 | all_83_0 & cons(char1, v34, all_97_1) = v35 & char3(v33) = % 30.84/5.08 | all_92_1 & uni(v35) & uni(v34)) | (v32 = all_92_1 & v31 = 0 & % 30.84/5.08 | v28 = all_83_0 & mem2(all_83_0, v29) = 0 & alt1(v29, v30) = % 30.84/5.08 | all_92_1) | (v27 = all_92_1 & v26 = 0 & v23 = all_83_0 & % 30.84/5.08 | mem2(all_83_0, v25) = 0 & alt1(v24, v25) = all_92_1) | (v22 = % 30.84/5.08 | all_92_1 & v21 = all_83_0 & v17 = 0 & v16 = 0 & mem2(v13, v15) = % 30.84/5.08 | 0 & mem2(v12, v14) = 0 & tb2t(v20) = all_83_0 & t2tb(v13) = v19 % 30.84/5.08 | & t2tb(v12) = v18 & infix_plpl(char1, v18, v19) = v20 & % 30.84/5.08 | concat1(v14, v15) = all_92_1 & uni(v20) & uni(v19) & uni(v18)) | % 30.84/5.08 | (v11 = all_92_1 & all_97_0 = all_83_0 & star1(v10) = all_92_1) | % 30.84/5.08 | (v9 = all_83_0 & v5 = 0 & v4 = all_92_1 & v3 = 0 & mem2(v1, % 30.84/5.08 | all_92_1) = 0 & mem2(v0, v2) = 0 & tb2t(v8) = all_83_0 & % 30.84/5.08 | t2tb(v1) = v7 & t2tb(v0) = v6 & infix_plpl(char1, v6, v7) = v8 & % 30.84/5.08 | star1(v2) = all_92_1 & uni(v8) & uni(v7) & uni(v6)))) % 30.84/5.08 | % 30.84/5.08 | DELTA: instantiating (76) with fresh symbol all_118_0 gives: % 30.84/5.08 | (81) nil(char1) = all_118_0 & sort1(all_86_0, all_118_0) = 0 & % 30.84/5.08 | uni(all_118_0) % 30.84/5.08 | % 30.84/5.08 | ALPHA: (81) implies: % 30.84/5.08 | (82) nil(char1) = all_118_0 % 30.84/5.08 | % 30.84/5.08 | GROUND_INST: instantiating (17) with all_83_1, all_118_0, char1, simplifying % 30.84/5.08 | with (23), (82) gives: % 30.84/5.08 | (83) all_118_0 = all_83_1 % 30.84/5.08 | % 30.84/5.08 | GROUND_INST: instantiating (3) with all_92_1, all_92_4, simplifying with (36), % 30.84/5.08 | (75) gives: % 30.84/5.08 | (84) all_92_1 = epsilon1 | all_92_1 = empty1 | ? [v0: char2] : ? [v1: % 30.84/5.08 | regexp1] : ? [v2: regexp1] : ? [v3: regexp1] : ? [v4: regexp1] : % 30.84/5.08 | ? [v5: regexp1] : ? [v6: regexp1] : ? [v7: regexp1] : ? [v8: % 30.84/5.08 | regexp1] : (star_proj_11(all_92_1) = v7 & concat_proj_21(all_92_1) = % 30.84/5.08 | v5 & alt_proj_21(all_92_1) = v3 & alt_proj_11(all_92_1) = v2 & % 30.84/5.08 | char_proj_11(all_92_1) = v0 & star1(v7) = v8 & concat1(all_92_4, v5) % 30.84/5.08 | = v6 & alt1(v2, v3) = v4 & char3(v0) = v1 & regexp1(v8) & % 30.84/5.08 | regexp1(v7) & regexp1(v6) & regexp1(v5) & regexp1(v4) & regexp1(v3) % 30.84/5.08 | & regexp1(v2) & regexp1(v1) & char2(v0) & (v8 = all_92_1 | v6 = % 30.84/5.08 | all_92_1 | v4 = all_92_1 | v1 = all_92_1)) % 30.84/5.08 | % 30.84/5.08 | GROUND_INST: instantiating (4) with all_92_1, all_92_3, simplifying with (36), % 30.84/5.08 | (74) gives: % 30.84/5.08 | (85) all_92_1 = epsilon1 | all_92_1 = empty1 | ? [v0: char2] : ? [v1: % 30.84/5.08 | regexp1] : ? [v2: regexp1] : ? [v3: regexp1] : ? [v4: regexp1] : % 30.84/5.08 | ? [v5: regexp1] : ? [v6: regexp1] : ? [v7: regexp1] : ? [v8: % 30.84/5.08 | regexp1] : (star_proj_11(all_92_1) = v7 & concat_proj_11(all_92_1) = % 30.84/5.08 | v5 & alt_proj_21(all_92_1) = v3 & alt_proj_11(all_92_1) = v2 & % 30.84/5.08 | char_proj_11(all_92_1) = v0 & star1(v7) = v8 & concat1(v5, all_92_3) % 30.84/5.08 | = v6 & alt1(v2, v3) = v4 & char3(v0) = v1 & regexp1(v8) & % 30.84/5.08 | regexp1(v7) & regexp1(v6) & regexp1(v5) & regexp1(v4) & regexp1(v3) % 30.84/5.08 | & regexp1(v2) & regexp1(v1) & char2(v0) & (v8 = all_92_1 | v6 = % 30.84/5.08 | all_92_1 | v4 = all_92_1 | v1 = all_92_1)) % 30.84/5.08 | % 30.84/5.08 | BETA: splitting (80) gives: % 30.84/5.08 | % 30.84/5.08 | Case 1: % 30.84/5.08 | | % 30.84/5.08 | | (86) all_92_1 = epsilon1 % 30.84/5.08 | | % 30.84/5.08 | | REDUCE: (37), (86) imply: % 30.84/5.08 | | (87) concat1(all_92_4, all_92_3) = epsilon1 % 30.84/5.08 | | % 30.84/5.08 | | GROUND_INST: instantiating (2) with all_92_4, all_92_3, simplifying with % 30.84/5.08 | | (34), (35), (87) gives: % 30.84/5.08 | | (88) $false % 30.84/5.08 | | % 30.84/5.08 | | CLOSE: (88) is inconsistent. % 30.84/5.08 | | % 30.84/5.08 | Case 2: % 30.84/5.08 | | % 30.84/5.08 | | (89) ~ (all_92_1 = epsilon1) % 30.84/5.09 | | (90) ? [v0: list_char] : ? [v1: list_char] : ? [v2: regexp1] : ? [v3: % 30.84/5.09 | | int] : ? [v4: int] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : % 30.84/5.09 | | ? [v8: uni] : ? [v9: int] : ? [v10: regexp1] : ? [v11: int] : ? % 30.84/5.09 | | [v12: list_char] : ? [v13: list_char] : ? [v14: regexp1] : ? % 30.84/5.09 | | [v15: regexp1] : ? [v16: int] : ? [v17: int] : ? [v18: uni] : ? % 30.84/5.09 | | [v19: uni] : ? [v20: uni] : ? [v21: int] : ? [v22: int] : ? % 30.84/5.09 | | [v23: list_char] : ? [v24: regexp1] : ? [v25: regexp1] : ? [v26: % 30.84/5.09 | | int] : ? [v27: int] : ? [v28: list_char] : ? [v29: regexp1] : % 30.84/5.09 | | ? [v30: regexp1] : ? [v31: int] : ? [v32: int] : ? [v33: char2] : % 30.84/5.09 | | ? [v34: uni] : ? [v35: uni] : ? [v36: int] : ? [v37: int] : % 30.84/5.09 | | (list_char(v28) & list_char(v23) & list_char(v13) & list_char(v12) & % 30.84/5.09 | | list_char(v1) & list_char(v0) & regexp1(v30) & regexp1(v29) & % 30.84/5.09 | | regexp1(v25) & regexp1(v24) & regexp1(v15) & regexp1(v14) & % 30.84/5.09 | | regexp1(v10) & regexp1(v2) & char2(v33) & ((v37 = all_92_1 & v36 = % 30.84/5.09 | | all_83_0 & t2tb1(v33) = v34 & tb2t(v35) = all_83_0 & % 30.84/5.09 | | cons(char1, v34, all_97_1) = v35 & char3(v33) = all_92_1 & % 30.84/5.09 | | uni(v35) & uni(v34)) | (v32 = all_92_1 & v31 = 0 & v28 = % 30.84/5.09 | | all_83_0 & mem2(all_83_0, v29) = 0 & alt1(v29, v30) = % 30.84/5.09 | | all_92_1) | (v27 = all_92_1 & v26 = 0 & v23 = all_83_0 & % 30.84/5.09 | | mem2(all_83_0, v25) = 0 & alt1(v24, v25) = all_92_1) | (v22 = % 30.84/5.09 | | all_92_1 & v21 = all_83_0 & v17 = 0 & v16 = 0 & mem2(v13, v15) % 30.84/5.09 | | = 0 & mem2(v12, v14) = 0 & tb2t(v20) = all_83_0 & t2tb(v13) = % 30.84/5.09 | | v19 & t2tb(v12) = v18 & infix_plpl(char1, v18, v19) = v20 & % 30.84/5.09 | | concat1(v14, v15) = all_92_1 & uni(v20) & uni(v19) & uni(v18)) % 30.84/5.09 | | | (v11 = all_92_1 & all_97_0 = all_83_0 & star1(v10) = all_92_1) % 30.84/5.09 | | | (v9 = all_83_0 & v5 = 0 & v4 = all_92_1 & v3 = 0 & mem2(v1, % 30.84/5.09 | | all_92_1) = 0 & mem2(v0, v2) = 0 & tb2t(v8) = all_83_0 & % 30.84/5.09 | | t2tb(v1) = v7 & t2tb(v0) = v6 & infix_plpl(char1, v6, v7) = v8 % 30.84/5.09 | | & star1(v2) = all_92_1 & uni(v8) & uni(v7) & uni(v6)))) % 30.84/5.09 | | % 30.84/5.09 | | DELTA: instantiating (90) with fresh symbols all_241_0, all_241_1, % 30.84/5.09 | | all_241_2, all_241_3, all_241_4, all_241_5, all_241_6, all_241_7, % 30.84/5.09 | | all_241_8, all_241_9, all_241_10, all_241_11, all_241_12, all_241_13, % 30.84/5.09 | | all_241_14, all_241_15, all_241_16, all_241_17, all_241_18, % 30.84/5.09 | | all_241_19, all_241_20, all_241_21, all_241_22, all_241_23, % 30.84/5.09 | | all_241_24, all_241_25, all_241_26, all_241_27, all_241_28, % 30.84/5.09 | | all_241_29, all_241_30, all_241_31, all_241_32, all_241_33, % 30.84/5.09 | | all_241_34, all_241_35, all_241_36, all_241_37 gives: % 31.15/5.09 | | (91) list_char(all_241_9) & list_char(all_241_14) & list_char(all_241_24) % 31.15/5.09 | | & list_char(all_241_25) & list_char(all_241_36) & % 31.15/5.09 | | list_char(all_241_37) & regexp1(all_241_7) & regexp1(all_241_8) & % 31.15/5.09 | | regexp1(all_241_12) & regexp1(all_241_13) & regexp1(all_241_22) & % 31.15/5.09 | | regexp1(all_241_23) & regexp1(all_241_27) & regexp1(all_241_35) & % 31.15/5.09 | | char2(all_241_4) & ((all_241_0 = all_92_1 & all_241_1 = all_83_0 & % 31.15/5.09 | | t2tb1(all_241_4) = all_241_3 & tb2t(all_241_2) = all_83_0 & % 31.15/5.09 | | cons(char1, all_241_3, all_97_1) = all_241_2 & char3(all_241_4) % 31.15/5.09 | | = all_92_1 & uni(all_241_2) & uni(all_241_3)) | (all_241_5 = % 31.15/5.09 | | all_92_1 & all_241_6 = 0 & all_241_9 = all_83_0 & mem2(all_83_0, % 31.15/5.09 | | all_241_8) = 0 & alt1(all_241_8, all_241_7) = all_92_1) | % 31.15/5.09 | | (all_241_10 = all_92_1 & all_241_11 = 0 & all_241_14 = all_83_0 & % 31.15/5.09 | | mem2(all_83_0, all_241_12) = 0 & alt1(all_241_13, all_241_12) = % 31.15/5.09 | | all_92_1) | (all_241_15 = all_92_1 & all_241_16 = all_83_0 & % 31.15/5.09 | | all_241_20 = 0 & all_241_21 = 0 & mem2(all_241_24, all_241_22) = % 31.15/5.09 | | 0 & mem2(all_241_25, all_241_23) = 0 & tb2t(all_241_17) = % 31.15/5.09 | | all_83_0 & t2tb(all_241_24) = all_241_18 & t2tb(all_241_25) = % 31.15/5.09 | | all_241_19 & infix_plpl(char1, all_241_19, all_241_18) = % 31.15/5.09 | | all_241_17 & concat1(all_241_23, all_241_22) = all_92_1 & % 31.15/5.09 | | uni(all_241_17) & uni(all_241_18) & uni(all_241_19)) | % 31.15/5.09 | | (all_241_26 = all_92_1 & all_97_0 = all_83_0 & star1(all_241_27) = % 31.15/5.09 | | all_92_1) | (all_241_28 = all_83_0 & all_241_32 = 0 & all_241_33 % 31.15/5.09 | | = all_92_1 & all_241_34 = 0 & mem2(all_241_36, all_92_1) = 0 & % 31.15/5.09 | | mem2(all_241_37, all_241_35) = 0 & tb2t(all_241_29) = all_83_0 & % 31.15/5.09 | | t2tb(all_241_36) = all_241_30 & t2tb(all_241_37) = all_241_31 & % 31.15/5.09 | | infix_plpl(char1, all_241_31, all_241_30) = all_241_29 & % 31.15/5.09 | | star1(all_241_35) = all_92_1 & uni(all_241_29) & uni(all_241_30) % 31.15/5.09 | | & uni(all_241_31))) % 31.15/5.09 | | % 31.15/5.09 | | ALPHA: (91) implies: % 31.15/5.09 | | (92) char2(all_241_4) % 31.15/5.09 | | (93) regexp1(all_241_35) % 31.15/5.09 | | (94) regexp1(all_241_27) % 31.15/5.09 | | (95) regexp1(all_241_23) % 31.15/5.09 | | (96) regexp1(all_241_22) % 31.15/5.09 | | (97) regexp1(all_241_13) % 31.15/5.09 | | (98) regexp1(all_241_12) % 31.15/5.09 | | (99) regexp1(all_241_8) % 31.15/5.09 | | (100) regexp1(all_241_7) % 31.15/5.09 | | (101) list_char(all_241_25) % 31.15/5.09 | | (102) list_char(all_241_24) % 31.15/5.09 | | (103) (all_241_0 = all_92_1 & all_241_1 = all_83_0 & t2tb1(all_241_4) = % 31.15/5.09 | | all_241_3 & tb2t(all_241_2) = all_83_0 & cons(char1, all_241_3, % 31.15/5.09 | | all_97_1) = all_241_2 & char3(all_241_4) = all_92_1 & % 31.15/5.09 | | uni(all_241_2) & uni(all_241_3)) | (all_241_5 = all_92_1 & % 31.15/5.09 | | all_241_6 = 0 & all_241_9 = all_83_0 & mem2(all_83_0, all_241_8) % 31.15/5.09 | | = 0 & alt1(all_241_8, all_241_7) = all_92_1) | (all_241_10 = % 31.15/5.09 | | all_92_1 & all_241_11 = 0 & all_241_14 = all_83_0 & % 31.15/5.09 | | mem2(all_83_0, all_241_12) = 0 & alt1(all_241_13, all_241_12) = % 31.15/5.09 | | all_92_1) | (all_241_15 = all_92_1 & all_241_16 = all_83_0 & % 31.15/5.09 | | all_241_20 = 0 & all_241_21 = 0 & mem2(all_241_24, all_241_22) = % 31.15/5.09 | | 0 & mem2(all_241_25, all_241_23) = 0 & tb2t(all_241_17) = % 31.15/5.09 | | all_83_0 & t2tb(all_241_24) = all_241_18 & t2tb(all_241_25) = % 31.15/5.09 | | all_241_19 & infix_plpl(char1, all_241_19, all_241_18) = % 31.15/5.09 | | all_241_17 & concat1(all_241_23, all_241_22) = all_92_1 & % 31.15/5.09 | | uni(all_241_17) & uni(all_241_18) & uni(all_241_19)) | % 31.15/5.09 | | (all_241_26 = all_92_1 & all_97_0 = all_83_0 & star1(all_241_27) = % 31.15/5.09 | | all_92_1) | (all_241_28 = all_83_0 & all_241_32 = 0 & all_241_33 % 31.15/5.09 | | = all_92_1 & all_241_34 = 0 & mem2(all_241_36, all_92_1) = 0 & % 31.15/5.09 | | mem2(all_241_37, all_241_35) = 0 & tb2t(all_241_29) = all_83_0 & % 31.15/5.09 | | t2tb(all_241_36) = all_241_30 & t2tb(all_241_37) = all_241_31 & % 31.15/5.09 | | infix_plpl(char1, all_241_31, all_241_30) = all_241_29 & % 31.15/5.09 | | star1(all_241_35) = all_92_1 & uni(all_241_29) & uni(all_241_30) % 31.15/5.09 | | & uni(all_241_31)) % 31.15/5.09 | | % 31.15/5.09 | | BETA: splitting (79) gives: % 31.15/5.09 | | % 31.15/5.09 | | Case 1: % 31.15/5.09 | | | % 31.15/5.09 | | | (104) all_92_4 = epsilon1 % 31.15/5.09 | | | % 31.15/5.09 | | | REDUCE: (75), (104) imply: % 31.15/5.09 | | | (105) concat_proj_11(all_92_1) = epsilon1 % 31.15/5.09 | | | % 31.15/5.09 | | | BETA: splitting (85) gives: % 31.15/5.09 | | | % 31.15/5.09 | | | Case 1: % 31.15/5.09 | | | | % 31.15/5.09 | | | | (106) all_92_1 = epsilon1 % 31.15/5.09 | | | | % 31.15/5.09 | | | | REDUCE: (89), (106) imply: % 31.15/5.09 | | | | (107) $false % 31.15/5.09 | | | | % 31.15/5.09 | | | | CLOSE: (107) is inconsistent. % 31.15/5.09 | | | | % 31.15/5.09 | | | Case 2: % 31.15/5.09 | | | | % 31.15/5.09 | | | | (108) all_92_1 = empty1 | ? [v0: char2] : ? [v1: regexp1] : ? [v2: % 31.15/5.09 | | | | regexp1] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: % 31.15/5.09 | | | | regexp1] : ? [v6: regexp1] : ? [v7: regexp1] : ? [v8: % 31.15/5.09 | | | | regexp1] : (star_proj_11(all_92_1) = v7 & % 31.15/5.09 | | | | concat_proj_11(all_92_1) = v5 & alt_proj_21(all_92_1) = v3 & % 31.15/5.09 | | | | alt_proj_11(all_92_1) = v2 & char_proj_11(all_92_1) = v0 & % 31.15/5.09 | | | | star1(v7) = v8 & concat1(v5, all_92_3) = v6 & alt1(v2, v3) = % 31.15/5.09 | | | | v4 & char3(v0) = v1 & regexp1(v8) & regexp1(v7) & regexp1(v6) % 31.15/5.09 | | | | & regexp1(v5) & regexp1(v4) & regexp1(v3) & regexp1(v2) & % 31.15/5.09 | | | | regexp1(v1) & char2(v0) & (v8 = all_92_1 | v6 = all_92_1 | v4 % 31.15/5.09 | | | | = all_92_1 | v1 = all_92_1)) % 31.15/5.09 | | | | % 31.15/5.09 | | | | BETA: splitting (103) gives: % 31.15/5.09 | | | | % 31.15/5.09 | | | | Case 1: % 31.15/5.09 | | | | | % 31.15/5.09 | | | | | (109) (all_241_0 = all_92_1 & all_241_1 = all_83_0 & % 31.15/5.09 | | | | | t2tb1(all_241_4) = all_241_3 & tb2t(all_241_2) = all_83_0 & % 31.15/5.09 | | | | | cons(char1, all_241_3, all_97_1) = all_241_2 & % 31.15/5.09 | | | | | char3(all_241_4) = all_92_1 & uni(all_241_2) & % 31.15/5.09 | | | | | uni(all_241_3)) | (all_241_5 = all_92_1 & all_241_6 = 0 & % 31.15/5.09 | | | | | all_241_9 = all_83_0 & mem2(all_83_0, all_241_8) = 0 & % 31.15/5.09 | | | | | alt1(all_241_8, all_241_7) = all_92_1) | (all_241_10 = % 31.15/5.09 | | | | | all_92_1 & all_241_11 = 0 & all_241_14 = all_83_0 & % 31.15/5.09 | | | | | mem2(all_83_0, all_241_12) = 0 & alt1(all_241_13, % 31.15/5.09 | | | | | all_241_12) = all_92_1) % 31.15/5.09 | | | | | % 31.15/5.09 | | | | | BETA: splitting (109) gives: % 31.15/5.09 | | | | | % 31.15/5.09 | | | | | Case 1: % 31.15/5.09 | | | | | | % 31.15/5.09 | | | | | | (110) all_241_0 = all_92_1 & all_241_1 = all_83_0 & % 31.15/5.09 | | | | | | t2tb1(all_241_4) = all_241_3 & tb2t(all_241_2) = all_83_0 & % 31.15/5.09 | | | | | | cons(char1, all_241_3, all_97_1) = all_241_2 & % 31.15/5.09 | | | | | | char3(all_241_4) = all_92_1 & uni(all_241_2) & % 31.15/5.09 | | | | | | uni(all_241_3) % 31.15/5.09 | | | | | | % 31.15/5.09 | | | | | | ALPHA: (110) implies: % 31.15/5.09 | | | | | | (111) char3(all_241_4) = all_92_1 % 31.15/5.09 | | | | | | % 31.15/5.09 | | | | | | GROUND_INST: instantiating (char_Concat) with all_241_4, all_92_4, % 31.15/5.09 | | | | | | all_92_3, all_92_1, simplifying with (34), (35), (37), % 31.15/5.09 | | | | | | (92), (111) gives: % 31.15/5.09 | | | | | | (112) $false % 31.15/5.09 | | | | | | % 31.15/5.09 | | | | | | CLOSE: (112) is inconsistent. % 31.15/5.09 | | | | | | % 31.15/5.09 | | | | | Case 2: % 31.15/5.09 | | | | | | % 31.15/5.10 | | | | | | (113) (all_241_5 = all_92_1 & all_241_6 = 0 & all_241_9 = % 31.15/5.10 | | | | | | all_83_0 & mem2(all_83_0, all_241_8) = 0 & % 31.15/5.10 | | | | | | alt1(all_241_8, all_241_7) = all_92_1) | (all_241_10 = % 31.15/5.10 | | | | | | all_92_1 & all_241_11 = 0 & all_241_14 = all_83_0 & % 31.15/5.10 | | | | | | mem2(all_83_0, all_241_12) = 0 & alt1(all_241_13, % 31.15/5.10 | | | | | | all_241_12) = all_92_1) % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | BETA: splitting (113) gives: % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | Case 1: % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | (114) all_241_5 = all_92_1 & all_241_6 = 0 & all_241_9 = % 31.15/5.10 | | | | | | | all_83_0 & mem2(all_83_0, all_241_8) = 0 & % 31.15/5.10 | | | | | | | alt1(all_241_8, all_241_7) = all_92_1 % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | ALPHA: (114) implies: % 31.15/5.10 | | | | | | | (115) alt1(all_241_8, all_241_7) = all_92_1 % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | GROUND_INST: instantiating (alt_Concat) with all_241_8, all_241_7, % 31.15/5.10 | | | | | | | all_92_4, all_92_3, all_92_1, simplifying with (34), % 31.15/5.10 | | | | | | | (35), (37), (99), (100), (115) gives: % 31.15/5.10 | | | | | | | (116) $false % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | CLOSE: (116) is inconsistent. % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | Case 2: % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | (117) all_241_10 = all_92_1 & all_241_11 = 0 & all_241_14 = % 31.15/5.10 | | | | | | | all_83_0 & mem2(all_83_0, all_241_12) = 0 & % 31.15/5.10 | | | | | | | alt1(all_241_13, all_241_12) = all_92_1 % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | ALPHA: (117) implies: % 31.15/5.10 | | | | | | | (118) alt1(all_241_13, all_241_12) = all_92_1 % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | GROUND_INST: instantiating (alt_Concat) with all_241_13, % 31.15/5.10 | | | | | | | all_241_12, all_92_4, all_92_3, all_92_1, simplifying % 31.15/5.10 | | | | | | | with (34), (35), (37), (97), (98), (118) gives: % 31.15/5.10 | | | | | | | (119) $false % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | | CLOSE: (119) is inconsistent. % 31.15/5.10 | | | | | | | % 31.15/5.10 | | | | | | End of split % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | End of split % 31.15/5.10 | | | | | % 31.15/5.10 | | | | Case 2: % 31.15/5.10 | | | | | % 31.15/5.10 | | | | | (120) (all_241_15 = all_92_1 & all_241_16 = all_83_0 & all_241_20 = % 31.15/5.10 | | | | | 0 & all_241_21 = 0 & mem2(all_241_24, all_241_22) = 0 & % 31.15/5.10 | | | | | mem2(all_241_25, all_241_23) = 0 & tb2t(all_241_17) = % 31.15/5.10 | | | | | all_83_0 & t2tb(all_241_24) = all_241_18 & t2tb(all_241_25) % 31.15/5.10 | | | | | = all_241_19 & infix_plpl(char1, all_241_19, all_241_18) = % 31.15/5.10 | | | | | all_241_17 & concat1(all_241_23, all_241_22) = all_92_1 & % 31.15/5.10 | | | | | uni(all_241_17) & uni(all_241_18) & uni(all_241_19)) | % 31.15/5.10 | | | | | (all_241_26 = all_92_1 & all_97_0 = all_83_0 & % 31.15/5.10 | | | | | star1(all_241_27) = all_92_1) | (all_241_28 = all_83_0 & % 31.15/5.10 | | | | | all_241_32 = 0 & all_241_33 = all_92_1 & all_241_34 = 0 & % 31.15/5.10 | | | | | mem2(all_241_36, all_92_1) = 0 & mem2(all_241_37, % 31.15/5.10 | | | | | all_241_35) = 0 & tb2t(all_241_29) = all_83_0 & % 31.15/5.10 | | | | | t2tb(all_241_36) = all_241_30 & t2tb(all_241_37) = % 31.15/5.10 | | | | | all_241_31 & infix_plpl(char1, all_241_31, all_241_30) = % 31.15/5.10 | | | | | all_241_29 & star1(all_241_35) = all_92_1 & uni(all_241_29) % 31.15/5.10 | | | | | & uni(all_241_30) & uni(all_241_31)) % 31.15/5.10 | | | | | % 31.15/5.10 | | | | | BETA: splitting (120) gives: % 31.15/5.10 | | | | | % 31.15/5.10 | | | | | Case 1: % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | (121) all_241_15 = all_92_1 & all_241_16 = all_83_0 & all_241_20 % 31.15/5.10 | | | | | | = 0 & all_241_21 = 0 & mem2(all_241_24, all_241_22) = 0 & % 31.15/5.10 | | | | | | mem2(all_241_25, all_241_23) = 0 & tb2t(all_241_17) = % 31.15/5.10 | | | | | | all_83_0 & t2tb(all_241_24) = all_241_18 & t2tb(all_241_25) % 31.15/5.10 | | | | | | = all_241_19 & infix_plpl(char1, all_241_19, all_241_18) = % 31.15/5.10 | | | | | | all_241_17 & concat1(all_241_23, all_241_22) = all_92_1 & % 31.15/5.10 | | | | | | uni(all_241_17) & uni(all_241_18) & uni(all_241_19) % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | ALPHA: (121) implies: % 31.15/5.10 | | | | | | (122) uni(all_241_19) % 31.15/5.10 | | | | | | (123) uni(all_241_18) % 31.15/5.10 | | | | | | (124) uni(all_241_17) % 31.15/5.10 | | | | | | (125) concat1(all_241_23, all_241_22) = all_92_1 % 31.15/5.10 | | | | | | (126) infix_plpl(char1, all_241_19, all_241_18) = all_241_17 % 31.15/5.10 | | | | | | (127) t2tb(all_241_25) = all_241_19 % 31.15/5.10 | | | | | | (128) t2tb(all_241_24) = all_241_18 % 31.15/5.10 | | | | | | (129) tb2t(all_241_17) = all_83_0 % 31.15/5.10 | | | | | | (130) mem2(all_241_24, all_241_22) = 0 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (concat_proj_2_def) with all_241_23, % 31.15/5.10 | | | | | | all_241_22, all_92_1, simplifying with (95), (96), % 31.15/5.10 | | | | | | (125) gives: % 31.15/5.10 | | | | | | (131) concat_proj_21(all_92_1) = all_241_22 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (concat_proj_1_def) with all_241_23, % 31.15/5.10 | | | | | | all_241_22, all_92_1, simplifying with (95), (96), % 31.15/5.10 | | | | | | (125) gives: % 31.15/5.10 | | | | | | (132) concat_proj_11(all_92_1) = all_241_23 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (append_length) with char1, all_241_19, % 31.15/5.10 | | | | | | all_241_18, all_241_17, simplifying with (13), (122), % 31.15/5.10 | | | | | | (123), (126) gives: % 31.15/5.10 | | | | | | (133) ? [v0: int] : ? [v1: int] : (length1(char1, all_241_17) = % 31.15/5.10 | | | | | | v0 & length1(char1, all_241_18) = $difference(v0, v1) & % 31.15/5.10 | | | | | | length1(char1, all_241_19) = v1) % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (bridgeL) with all_241_25, all_241_19, % 31.15/5.10 | | | | | | simplifying with (101), (127) gives: % 31.15/5.10 | | | | | | (134) tb2t(all_241_19) = all_241_25 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (bridgeL) with all_241_24, all_241_18, % 31.15/5.10 | | | | | | simplifying with (102), (128) gives: % 31.15/5.10 | | | | | | (135) tb2t(all_241_18) = all_241_24 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (bridgeR) with all_241_17, all_83_0, % 31.15/5.10 | | | | | | simplifying with (124), (129) gives: % 31.15/5.10 | | | | | | (136) t2tb(all_83_0) = all_241_17 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | DELTA: instantiating (133) with fresh symbols all_380_0, all_380_1 % 31.15/5.10 | | | | | | gives: % 31.15/5.10 | | | | | | (137) length1(char1, all_241_17) = all_380_1 & length1(char1, % 31.15/5.10 | | | | | | all_241_18) = $difference(all_380_1, all_380_0) & % 31.15/5.10 | | | | | | length1(char1, all_241_19) = all_380_0 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | ALPHA: (137) implies: % 31.15/5.10 | | | | | | (138) length1(char1, all_241_19) = all_380_0 % 31.15/5.10 | | | | | | (139) length1(char1, all_241_18) = $difference(all_380_1, % 31.15/5.10 | | | | | | all_380_0) % 31.15/5.10 | | | | | | (140) length1(char1, all_241_17) = all_380_1 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (15) with epsilon1, all_241_23, all_92_1, % 31.15/5.10 | | | | | | simplifying with (105), (132) gives: % 31.15/5.10 | | | | | | (141) all_241_23 = epsilon1 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (16) with all_92_3, all_241_22, all_92_1, % 31.15/5.10 | | | | | | simplifying with (74), (131) gives: % 31.15/5.10 | | | | | | (142) all_241_22 = all_92_3 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | GROUND_INST: instantiating (18) with all_83_1, all_241_17, all_83_0, % 31.15/5.10 | | | | | | simplifying with (78), (136) gives: % 31.15/5.10 | | | | | | (143) all_241_17 = all_83_1 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | REDUCE: (130), (142) imply: % 31.15/5.10 | | | | | | (144) mem2(all_241_24, all_92_3) = 0 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | REDUCE: (140), (143) imply: % 31.15/5.10 | | | | | | (145) length1(char1, all_83_1) = all_380_1 % 31.15/5.10 | | | | | | % 31.15/5.10 | | | | | | REDUCE: (125), (141), (142) imply: % 31.15/5.10 | | | | | | (146) concat1(epsilon1, all_92_3) = all_92_1 % 31.15/5.10 | | | | | | % 31.15/5.11 | | | | | | REDUCE: (95), (141) imply: % 31.15/5.11 | | | | | | (147) regexp1(epsilon1) % 31.15/5.11 | | | | | | % 31.15/5.11 | | | | | | GROUND_INST: instantiating (20) with 0, all_380_1, all_83_1, char1, % 31.15/5.11 | | | | | | simplifying with (77), (145) gives: % 31.15/5.11 | | | | | | (148) all_380_1 = 0 % 31.15/5.11 | | | | | | % 31.15/5.11 | | | | | | REDUCE: (139), (148) imply: % 31.15/5.11 | | | | | | (149) length1(char1, all_241_18) = $product(-1, all_380_0) % 31.15/5.11 | | | | | | % 31.15/5.11 | | | | | | BETA: splitting (108) gives: % 31.15/5.11 | | | | | | % 31.15/5.11 | | | | | | Case 1: % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | (150) all_92_1 = empty1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | REDUCE: (146), (150) imply: % 31.15/5.11 | | | | | | | (151) concat1(epsilon1, all_92_3) = empty1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (1) with epsilon1, all_92_3, % 31.15/5.11 | | | | | | | simplifying with (35), (147), (151) gives: % 31.15/5.11 | | | | | | | (152) $false % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | CLOSE: (152) is inconsistent. % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | Case 2: % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | (153) ? [v0: char2] : ? [v1: regexp1] : ? [v2: regexp1] : ? % 31.15/5.11 | | | | | | | [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 31.15/5.11 | | | | | | | [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : % 31.15/5.11 | | | | | | | (star_proj_11(all_92_1) = v7 & concat_proj_11(all_92_1) = % 31.15/5.11 | | | | | | | v5 & alt_proj_21(all_92_1) = v3 & alt_proj_11(all_92_1) % 31.15/5.11 | | | | | | | = v2 & char_proj_11(all_92_1) = v0 & star1(v7) = v8 & % 31.15/5.11 | | | | | | | concat1(v5, all_92_3) = v6 & alt1(v2, v3) = v4 & % 31.15/5.11 | | | | | | | char3(v0) = v1 & regexp1(v8) & regexp1(v7) & % 31.15/5.11 | | | | | | | regexp1(v6) & regexp1(v5) & regexp1(v4) & regexp1(v3) & % 31.15/5.11 | | | | | | | regexp1(v2) & regexp1(v1) & char2(v0) & (v8 = all_92_1 % 31.15/5.11 | | | | | | | | v6 = all_92_1 | v4 = all_92_1 | v1 = all_92_1)) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | DELTA: instantiating (153) with fresh symbols all_403_0, % 31.15/5.11 | | | | | | | all_403_1, all_403_2, all_403_3, all_403_4, all_403_5, % 31.15/5.11 | | | | | | | all_403_6, all_403_7, all_403_8 gives: % 31.15/5.11 | | | | | | | (154) star_proj_11(all_92_1) = all_403_1 & % 31.15/5.11 | | | | | | | concat_proj_11(all_92_1) = all_403_3 & % 31.15/5.11 | | | | | | | alt_proj_21(all_92_1) = all_403_5 & alt_proj_11(all_92_1) % 31.15/5.11 | | | | | | | = all_403_6 & char_proj_11(all_92_1) = all_403_8 & % 31.15/5.11 | | | | | | | star1(all_403_1) = all_403_0 & concat1(all_403_3, % 31.15/5.11 | | | | | | | all_92_3) = all_403_2 & alt1(all_403_6, all_403_5) = % 31.15/5.11 | | | | | | | all_403_4 & char3(all_403_8) = all_403_7 & % 31.15/5.11 | | | | | | | regexp1(all_403_0) & regexp1(all_403_1) & % 31.15/5.11 | | | | | | | regexp1(all_403_2) & regexp1(all_403_3) & % 31.15/5.11 | | | | | | | regexp1(all_403_4) & regexp1(all_403_5) & % 31.15/5.11 | | | | | | | regexp1(all_403_6) & regexp1(all_403_7) & % 31.15/5.11 | | | | | | | char2(all_403_8) & (all_403_0 = all_92_1 | all_403_2 = % 31.15/5.11 | | | | | | | all_92_1 | all_403_4 = all_92_1 | all_403_7 = all_92_1) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | ALPHA: (154) implies: % 31.15/5.11 | | | | | | | (155) char2(all_403_8) % 31.15/5.11 | | | | | | | (156) char3(all_403_8) = all_403_7 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (45) with all_403_8, all_403_7, % 31.15/5.11 | | | | | | | simplifying with (155), (156) gives: % 31.15/5.11 | | | | | | | (157) ? [v0: uni] : ? [v1: uni] : ? [v2: list_char] : % 31.15/5.11 | | | | | | | (t2tb1(all_403_8) = v0 & mem2(v2, all_403_7) = 0 & % 31.15/5.11 | | | | | | | tb2t(v1) = v2 & cons(char1, v0, all_94_0) = v1 & % 31.15/5.11 | | | | | | | list_char(v2) & uni(v1) & uni(v0)) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (length_nonnegative) with char1, % 31.15/5.11 | | | | | | | all_241_19, all_380_0, simplifying with (13), (122), % 31.15/5.11 | | | | | | | (138) gives: % 31.15/5.11 | | | | | | | (158) $lesseq(0, all_380_0) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (length_nonnegative) with char1, % 31.15/5.11 | | | | | | | all_241_18, $product(-1, all_380_0), simplifying with % 31.15/5.11 | | | | | | | (13), (123), (149) gives: % 31.15/5.11 | | | | | | | (159) $lesseq(all_380_0, 0) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | ANTI_SYMM: (158), (159) imply: % 31.15/5.11 | | | | | | | (160) all_380_0 = 0 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | DELTA: instantiating (157) with fresh symbols all_430_0, % 31.15/5.11 | | | | | | | all_430_1, all_430_2 gives: % 31.15/5.11 | | | | | | | (161) t2tb1(all_403_8) = all_430_2 & mem2(all_430_0, all_403_7) % 31.15/5.11 | | | | | | | = 0 & tb2t(all_430_1) = all_430_0 & cons(char1, % 31.15/5.11 | | | | | | | all_430_2, all_94_0) = all_430_1 & list_char(all_430_0) % 31.15/5.11 | | | | | | | & uni(all_430_1) & uni(all_430_2) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | ALPHA: (161) implies: % 31.15/5.11 | | | | | | | (162) uni(all_430_2) % 31.15/5.11 | | | | | | | (163) cons(char1, all_430_2, all_94_0) = all_430_1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | REDUCE: (149), (160) imply: % 31.15/5.11 | | | | | | | (164) length1(char1, all_241_18) = 0 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | REDUCE: (138), (160) imply: % 31.15/5.11 | | | | | | | (165) length1(char1, all_241_19) = 0 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | REDUCE: (55), (163) imply: % 31.15/5.11 | | | | | | | (166) cons(char1, all_430_2, all_83_1) = all_430_1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (nil_Cons) with char1, all_430_2, % 31.15/5.11 | | | | | | | all_83_1, all_430_1, simplifying with (13), (62), % 31.15/5.11 | | | | | | | (162), (166) gives: % 31.15/5.11 | | | | | | | (167) ? [v0: any] : ( ~ (v0 = all_430_1) & nil(char1) = v0 & % 31.15/5.11 | | | | | | | uni(v0)) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (7) with char1, all_241_19, simplifying % 31.15/5.11 | | | | | | | with (13), (122), (165) gives: % 31.15/5.11 | | | | | | | (168) nil(char1) = all_241_19 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (7) with char1, all_241_18, simplifying % 31.15/5.11 | | | | | | | with (13), (123), (164) gives: % 31.15/5.11 | | | | | | | (169) nil(char1) = all_241_18 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | DELTA: instantiating (167) with fresh symbol all_447_0 gives: % 31.15/5.11 | | | | | | | (170) ~ (all_447_0 = all_430_1) & nil(char1) = all_447_0 & % 31.15/5.11 | | | | | | | uni(all_447_0) % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | ALPHA: (170) implies: % 31.15/5.11 | | | | | | | (171) nil(char1) = all_447_0 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (17) with all_241_19, all_241_18, % 31.15/5.11 | | | | | | | char1, simplifying with (168), (169) gives: % 31.15/5.11 | | | | | | | (172) all_241_18 = all_241_19 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (17) with all_83_1, all_447_0, char1, % 31.15/5.11 | | | | | | | simplifying with (23), (171) gives: % 31.15/5.11 | | | | | | | (173) all_447_0 = all_83_1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | GROUND_INST: instantiating (17) with all_241_18, all_447_0, char1, % 31.15/5.11 | | | | | | | simplifying with (169), (171) gives: % 31.15/5.11 | | | | | | | (174) all_447_0 = all_241_18 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | COMBINE_EQS: (173), (174) imply: % 31.15/5.11 | | | | | | | (175) all_241_18 = all_83_1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | SIMP: (175) implies: % 31.15/5.11 | | | | | | | (176) all_241_18 = all_83_1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | COMBINE_EQS: (172), (176) imply: % 31.15/5.11 | | | | | | | (177) all_241_19 = all_83_1 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | REDUCE: (135), (176) imply: % 31.15/5.11 | | | | | | | (178) tb2t(all_83_1) = all_241_24 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | REDUCE: (134), (177) imply: % 31.15/5.11 | | | | | | | (179) tb2t(all_83_1) = all_241_25 % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | | REF_CLOSE: (19), (21), (24), (33), (71), (144), (178), (179) are % 31.15/5.11 | | | | | | | inconsistent by sub-proof #1. % 31.15/5.11 | | | | | | | % 31.15/5.11 | | | | | | End of split % 31.15/5.11 | | | | | | % 31.15/5.11 | | | | | Case 2: % 31.15/5.11 | | | | | | % 31.15/5.12 | | | | | | (180) (all_241_26 = all_92_1 & all_97_0 = all_83_0 & % 31.15/5.12 | | | | | | star1(all_241_27) = all_92_1) | (all_241_28 = all_83_0 & % 31.15/5.12 | | | | | | all_241_32 = 0 & all_241_33 = all_92_1 & all_241_34 = 0 & % 31.15/5.12 | | | | | | mem2(all_241_36, all_92_1) = 0 & mem2(all_241_37, % 31.15/5.12 | | | | | | all_241_35) = 0 & tb2t(all_241_29) = all_83_0 & % 31.15/5.12 | | | | | | t2tb(all_241_36) = all_241_30 & t2tb(all_241_37) = % 31.15/5.12 | | | | | | all_241_31 & infix_plpl(char1, all_241_31, all_241_30) = % 31.15/5.12 | | | | | | all_241_29 & star1(all_241_35) = all_92_1 & % 31.15/5.12 | | | | | | uni(all_241_29) & uni(all_241_30) & uni(all_241_31)) % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | BETA: splitting (180) gives: % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | Case 1: % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | (181) all_241_26 = all_92_1 & all_97_0 = all_83_0 & % 31.15/5.12 | | | | | | | star1(all_241_27) = all_92_1 % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | ALPHA: (181) implies: % 31.15/5.12 | | | | | | | (182) star1(all_241_27) = all_92_1 % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | GROUND_INST: instantiating (concat_Star) with all_92_4, all_92_3, % 31.15/5.12 | | | | | | | all_241_27, all_92_1, simplifying with (34), (35), % 31.15/5.12 | | | | | | | (37), (94), (182) gives: % 31.15/5.12 | | | | | | | (183) $false % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | CLOSE: (183) is inconsistent. % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | Case 2: % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | (184) all_241_28 = all_83_0 & all_241_32 = 0 & all_241_33 = % 31.15/5.12 | | | | | | | all_92_1 & all_241_34 = 0 & mem2(all_241_36, all_92_1) = % 31.15/5.12 | | | | | | | 0 & mem2(all_241_37, all_241_35) = 0 & tb2t(all_241_29) = % 31.15/5.12 | | | | | | | all_83_0 & t2tb(all_241_36) = all_241_30 & % 31.15/5.12 | | | | | | | t2tb(all_241_37) = all_241_31 & infix_plpl(char1, % 31.15/5.12 | | | | | | | all_241_31, all_241_30) = all_241_29 & % 31.15/5.12 | | | | | | | star1(all_241_35) = all_92_1 & uni(all_241_29) & % 31.15/5.12 | | | | | | | uni(all_241_30) & uni(all_241_31) % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | ALPHA: (184) implies: % 31.15/5.12 | | | | | | | (185) star1(all_241_35) = all_92_1 % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | GROUND_INST: instantiating (concat_Star) with all_92_4, all_92_3, % 31.15/5.12 | | | | | | | all_241_35, all_92_1, simplifying with (34), (35), % 31.15/5.12 | | | | | | | (37), (93), (185) gives: % 31.15/5.12 | | | | | | | (186) $false % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | CLOSE: (186) is inconsistent. % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | End of split % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | End of split % 31.15/5.12 | | | | | % 31.15/5.12 | | | | End of split % 31.15/5.12 | | | | % 31.15/5.12 | | | End of split % 31.15/5.12 | | | % 31.15/5.12 | | Case 2: % 31.15/5.12 | | | % 31.15/5.12 | | | (187) ~ (all_92_4 = epsilon1) % 31.15/5.12 | | | % 31.15/5.12 | | | BETA: splitting (84) gives: % 31.15/5.12 | | | % 31.15/5.12 | | | Case 1: % 31.15/5.12 | | | | % 31.15/5.12 | | | | (188) all_92_1 = epsilon1 % 31.15/5.12 | | | | % 31.15/5.12 | | | | REDUCE: (89), (188) imply: % 31.15/5.12 | | | | (189) $false % 31.15/5.12 | | | | % 31.15/5.12 | | | | CLOSE: (189) is inconsistent. % 31.15/5.12 | | | | % 31.15/5.12 | | | Case 2: % 31.15/5.12 | | | | % 31.15/5.12 | | | | (190) all_92_1 = empty1 | ? [v0: char2] : ? [v1: regexp1] : ? [v2: % 31.15/5.12 | | | | regexp1] : ? [v3: regexp1] : ? [v4: regexp1] : ? [v5: % 31.15/5.12 | | | | regexp1] : ? [v6: regexp1] : ? [v7: regexp1] : ? [v8: % 31.15/5.12 | | | | regexp1] : (star_proj_11(all_92_1) = v7 & % 31.15/5.12 | | | | concat_proj_21(all_92_1) = v5 & alt_proj_21(all_92_1) = v3 & % 31.15/5.12 | | | | alt_proj_11(all_92_1) = v2 & char_proj_11(all_92_1) = v0 & % 31.15/5.12 | | | | star1(v7) = v8 & concat1(all_92_4, v5) = v6 & alt1(v2, v3) = % 31.15/5.12 | | | | v4 & char3(v0) = v1 & regexp1(v8) & regexp1(v7) & regexp1(v6) % 31.15/5.12 | | | | & regexp1(v5) & regexp1(v4) & regexp1(v3) & regexp1(v2) & % 31.15/5.12 | | | | regexp1(v1) & char2(v0) & (v8 = all_92_1 | v6 = all_92_1 | v4 % 31.15/5.12 | | | | = all_92_1 | v1 = all_92_1)) % 31.15/5.12 | | | | % 31.15/5.12 | | | | BETA: splitting (103) gives: % 31.15/5.12 | | | | % 31.15/5.12 | | | | Case 1: % 31.15/5.12 | | | | | % 31.15/5.12 | | | | | (191) (all_241_0 = all_92_1 & all_241_1 = all_83_0 & % 31.15/5.12 | | | | | t2tb1(all_241_4) = all_241_3 & tb2t(all_241_2) = all_83_0 & % 31.15/5.12 | | | | | cons(char1, all_241_3, all_97_1) = all_241_2 & % 31.15/5.12 | | | | | char3(all_241_4) = all_92_1 & uni(all_241_2) & % 31.15/5.12 | | | | | uni(all_241_3)) | (all_241_5 = all_92_1 & all_241_6 = 0 & % 31.15/5.12 | | | | | all_241_9 = all_83_0 & mem2(all_83_0, all_241_8) = 0 & % 31.15/5.12 | | | | | alt1(all_241_8, all_241_7) = all_92_1) | (all_241_10 = % 31.15/5.12 | | | | | all_92_1 & all_241_11 = 0 & all_241_14 = all_83_0 & % 31.15/5.12 | | | | | mem2(all_83_0, all_241_12) = 0 & alt1(all_241_13, % 31.15/5.12 | | | | | all_241_12) = all_92_1) % 31.15/5.12 | | | | | % 31.15/5.12 | | | | | BETA: splitting (191) gives: % 31.15/5.12 | | | | | % 31.15/5.12 | | | | | Case 1: % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | (192) all_241_0 = all_92_1 & all_241_1 = all_83_0 & % 31.15/5.12 | | | | | | t2tb1(all_241_4) = all_241_3 & tb2t(all_241_2) = all_83_0 & % 31.15/5.12 | | | | | | cons(char1, all_241_3, all_97_1) = all_241_2 & % 31.15/5.12 | | | | | | char3(all_241_4) = all_92_1 & uni(all_241_2) & % 31.15/5.12 | | | | | | uni(all_241_3) % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | ALPHA: (192) implies: % 31.15/5.12 | | | | | | (193) char3(all_241_4) = all_92_1 % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | GROUND_INST: instantiating (char_Concat) with all_241_4, all_92_4, % 31.15/5.12 | | | | | | all_92_3, all_92_1, simplifying with (34), (35), (37), % 31.15/5.12 | | | | | | (92), (193) gives: % 31.15/5.12 | | | | | | (194) $false % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | CLOSE: (194) is inconsistent. % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | Case 2: % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | (195) (all_241_5 = all_92_1 & all_241_6 = 0 & all_241_9 = % 31.15/5.12 | | | | | | all_83_0 & mem2(all_83_0, all_241_8) = 0 & % 31.15/5.12 | | | | | | alt1(all_241_8, all_241_7) = all_92_1) | (all_241_10 = % 31.15/5.12 | | | | | | all_92_1 & all_241_11 = 0 & all_241_14 = all_83_0 & % 31.15/5.12 | | | | | | mem2(all_83_0, all_241_12) = 0 & alt1(all_241_13, % 31.15/5.12 | | | | | | all_241_12) = all_92_1) % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | BETA: splitting (195) gives: % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | | Case 1: % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | (196) all_241_5 = all_92_1 & all_241_6 = 0 & all_241_9 = % 31.15/5.12 | | | | | | | all_83_0 & mem2(all_83_0, all_241_8) = 0 & % 31.15/5.12 | | | | | | | alt1(all_241_8, all_241_7) = all_92_1 % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | ALPHA: (196) implies: % 31.15/5.12 | | | | | | | (197) alt1(all_241_8, all_241_7) = all_92_1 % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | GROUND_INST: instantiating (alt_Concat) with all_241_8, all_241_7, % 31.15/5.12 | | | | | | | all_92_4, all_92_3, all_92_1, simplifying with (34), % 31.15/5.12 | | | | | | | (35), (37), (99), (100), (197) gives: % 31.15/5.12 | | | | | | | (198) $false % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | CLOSE: (198) is inconsistent. % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | Case 2: % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | (199) all_241_10 = all_92_1 & all_241_11 = 0 & all_241_14 = % 31.15/5.12 | | | | | | | all_83_0 & mem2(all_83_0, all_241_12) = 0 & % 31.15/5.12 | | | | | | | alt1(all_241_13, all_241_12) = all_92_1 % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | ALPHA: (199) implies: % 31.15/5.12 | | | | | | | (200) alt1(all_241_13, all_241_12) = all_92_1 % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | GROUND_INST: instantiating (alt_Concat) with all_241_13, % 31.15/5.12 | | | | | | | all_241_12, all_92_4, all_92_3, all_92_1, simplifying % 31.15/5.12 | | | | | | | with (34), (35), (37), (97), (98), (200) gives: % 31.15/5.12 | | | | | | | (201) $false % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | | CLOSE: (201) is inconsistent. % 31.15/5.12 | | | | | | | % 31.15/5.12 | | | | | | End of split % 31.15/5.12 | | | | | | % 31.15/5.12 | | | | | End of split % 31.15/5.12 | | | | | % 31.15/5.12 | | | | Case 2: % 31.15/5.12 | | | | | % 31.15/5.12 | | | | | (202) (all_241_15 = all_92_1 & all_241_16 = all_83_0 & all_241_20 = % 31.15/5.12 | | | | | 0 & all_241_21 = 0 & mem2(all_241_24, all_241_22) = 0 & % 31.15/5.12 | | | | | mem2(all_241_25, all_241_23) = 0 & tb2t(all_241_17) = % 31.15/5.12 | | | | | all_83_0 & t2tb(all_241_24) = all_241_18 & t2tb(all_241_25) % 31.15/5.12 | | | | | = all_241_19 & infix_plpl(char1, all_241_19, all_241_18) = % 31.15/5.12 | | | | | all_241_17 & concat1(all_241_23, all_241_22) = all_92_1 & % 31.15/5.12 | | | | | uni(all_241_17) & uni(all_241_18) & uni(all_241_19)) | % 31.15/5.12 | | | | | (all_241_26 = all_92_1 & all_97_0 = all_83_0 & % 31.15/5.12 | | | | | star1(all_241_27) = all_92_1) | (all_241_28 = all_83_0 & % 31.15/5.12 | | | | | all_241_32 = 0 & all_241_33 = all_92_1 & all_241_34 = 0 & % 31.15/5.12 | | | | | mem2(all_241_36, all_92_1) = 0 & mem2(all_241_37, % 31.15/5.12 | | | | | all_241_35) = 0 & tb2t(all_241_29) = all_83_0 & % 31.15/5.12 | | | | | t2tb(all_241_36) = all_241_30 & t2tb(all_241_37) = % 31.15/5.12 | | | | | all_241_31 & infix_plpl(char1, all_241_31, all_241_30) = % 31.15/5.12 | | | | | all_241_29 & star1(all_241_35) = all_92_1 & uni(all_241_29) % 31.15/5.12 | | | | | & uni(all_241_30) & uni(all_241_31)) % 31.15/5.12 | | | | | % 31.15/5.12 | | | | | BETA: splitting (202) gives: % 31.15/5.12 | | | | | % 31.15/5.12 | | | | | Case 1: % 31.15/5.12 | | | | | | % 31.15/5.13 | | | | | | (203) all_241_15 = all_92_1 & all_241_16 = all_83_0 & all_241_20 % 31.15/5.13 | | | | | | = 0 & all_241_21 = 0 & mem2(all_241_24, all_241_22) = 0 & % 31.15/5.13 | | | | | | mem2(all_241_25, all_241_23) = 0 & tb2t(all_241_17) = % 31.15/5.13 | | | | | | all_83_0 & t2tb(all_241_24) = all_241_18 & t2tb(all_241_25) % 31.15/5.13 | | | | | | = all_241_19 & infix_plpl(char1, all_241_19, all_241_18) = % 31.15/5.13 | | | | | | all_241_17 & concat1(all_241_23, all_241_22) = all_92_1 & % 31.15/5.13 | | | | | | uni(all_241_17) & uni(all_241_18) & uni(all_241_19) % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | ALPHA: (203) implies: % 31.15/5.13 | | | | | | (204) uni(all_241_19) % 31.15/5.13 | | | | | | (205) uni(all_241_18) % 31.15/5.13 | | | | | | (206) uni(all_241_17) % 31.15/5.13 | | | | | | (207) concat1(all_241_23, all_241_22) = all_92_1 % 31.15/5.13 | | | | | | (208) infix_plpl(char1, all_241_19, all_241_18) = all_241_17 % 31.15/5.13 | | | | | | (209) t2tb(all_241_25) = all_241_19 % 31.15/5.13 | | | | | | (210) t2tb(all_241_24) = all_241_18 % 31.15/5.13 | | | | | | (211) tb2t(all_241_17) = all_83_0 % 31.15/5.13 | | | | | | (212) mem2(all_241_25, all_241_23) = 0 % 31.15/5.13 | | | | | | (213) mem2(all_241_24, all_241_22) = 0 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (concat_proj_2_def) with all_241_23, % 31.15/5.13 | | | | | | all_241_22, all_92_1, simplifying with (95), (96), % 31.15/5.13 | | | | | | (207) gives: % 31.15/5.13 | | | | | | (214) concat_proj_21(all_92_1) = all_241_22 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (concat_proj_1_def) with all_241_23, % 31.15/5.13 | | | | | | all_241_22, all_92_1, simplifying with (95), (96), % 31.15/5.13 | | | | | | (207) gives: % 31.15/5.13 | | | | | | (215) concat_proj_11(all_92_1) = all_241_23 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (append_length) with char1, all_241_19, % 31.15/5.13 | | | | | | all_241_18, all_241_17, simplifying with (13), (204), % 31.15/5.13 | | | | | | (205), (208) gives: % 31.15/5.13 | | | | | | (216) ? [v0: int] : ? [v1: int] : (length1(char1, all_241_17) = % 31.15/5.13 | | | | | | v0 & length1(char1, all_241_18) = $difference(v0, v1) & % 31.15/5.13 | | | | | | length1(char1, all_241_19) = v1) % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (bridgeL) with all_241_25, all_241_19, % 31.15/5.13 | | | | | | simplifying with (101), (209) gives: % 31.15/5.13 | | | | | | (217) tb2t(all_241_19) = all_241_25 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (bridgeL) with all_241_24, all_241_18, % 31.15/5.13 | | | | | | simplifying with (102), (210) gives: % 31.15/5.13 | | | | | | (218) tb2t(all_241_18) = all_241_24 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (bridgeR) with all_241_17, all_83_0, % 31.15/5.13 | | | | | | simplifying with (206), (211) gives: % 31.15/5.13 | | | | | | (219) t2tb(all_83_0) = all_241_17 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | DELTA: instantiating (216) with fresh symbols all_385_0, all_385_1 % 31.15/5.13 | | | | | | gives: % 31.15/5.13 | | | | | | (220) length1(char1, all_241_17) = all_385_1 & length1(char1, % 31.15/5.13 | | | | | | all_241_18) = $difference(all_385_1, all_385_0) & % 31.15/5.13 | | | | | | length1(char1, all_241_19) = all_385_0 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | ALPHA: (220) implies: % 31.15/5.13 | | | | | | (221) length1(char1, all_241_19) = all_385_0 % 31.15/5.13 | | | | | | (222) length1(char1, all_241_18) = $difference(all_385_1, % 31.15/5.13 | | | | | | all_385_0) % 31.15/5.13 | | | | | | (223) length1(char1, all_241_17) = all_385_1 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (15) with all_92_4, all_241_23, all_92_1, % 31.15/5.13 | | | | | | simplifying with (75), (215) gives: % 31.15/5.13 | | | | | | (224) all_241_23 = all_92_4 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (16) with all_92_3, all_241_22, all_92_1, % 31.15/5.13 | | | | | | simplifying with (74), (214) gives: % 31.15/5.13 | | | | | | (225) all_241_22 = all_92_3 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (18) with all_83_1, all_241_17, all_83_0, % 31.15/5.13 | | | | | | simplifying with (78), (219) gives: % 31.15/5.13 | | | | | | (226) all_241_17 = all_83_1 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | REDUCE: (213), (225) imply: % 31.15/5.13 | | | | | | (227) mem2(all_241_24, all_92_3) = 0 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | REDUCE: (212), (224) imply: % 31.15/5.13 | | | | | | (228) mem2(all_241_25, all_92_4) = 0 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | REDUCE: (223), (226) imply: % 31.15/5.13 | | | | | | (229) length1(char1, all_83_1) = all_385_1 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | GROUND_INST: instantiating (20) with 0, all_385_1, all_83_1, char1, % 31.15/5.13 | | | | | | simplifying with (77), (229) gives: % 31.15/5.13 | | | | | | (230) all_385_1 = 0 % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | REDUCE: (222), (230) imply: % 31.15/5.13 | | | | | | (231) length1(char1, all_241_18) = $product(-1, all_385_0) % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | BETA: splitting (190) gives: % 31.15/5.13 | | | | | | % 31.15/5.13 | | | | | | Case 1: % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | (232) all_92_1 = empty1 % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | REDUCE: (37), (232) imply: % 31.15/5.13 | | | | | | | (233) concat1(all_92_4, all_92_3) = empty1 % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | GROUND_INST: instantiating (1) with all_92_4, all_92_3, % 31.15/5.13 | | | | | | | simplifying with (34), (35), (233) gives: % 31.15/5.13 | | | | | | | (234) $false % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | CLOSE: (234) is inconsistent. % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | Case 2: % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | (235) ? [v0: char2] : ? [v1: regexp1] : ? [v2: regexp1] : ? % 31.15/5.13 | | | | | | | [v3: regexp1] : ? [v4: regexp1] : ? [v5: regexp1] : ? % 31.15/5.13 | | | | | | | [v6: regexp1] : ? [v7: regexp1] : ? [v8: regexp1] : % 31.15/5.13 | | | | | | | (star_proj_11(all_92_1) = v7 & concat_proj_21(all_92_1) = % 31.15/5.13 | | | | | | | v5 & alt_proj_21(all_92_1) = v3 & alt_proj_11(all_92_1) % 31.15/5.13 | | | | | | | = v2 & char_proj_11(all_92_1) = v0 & star1(v7) = v8 & % 31.15/5.13 | | | | | | | concat1(all_92_4, v5) = v6 & alt1(v2, v3) = v4 & % 31.15/5.13 | | | | | | | char3(v0) = v1 & regexp1(v8) & regexp1(v7) & % 31.15/5.13 | | | | | | | regexp1(v6) & regexp1(v5) & regexp1(v4) & regexp1(v3) & % 31.15/5.13 | | | | | | | regexp1(v2) & regexp1(v1) & char2(v0) & (v8 = all_92_1 % 31.15/5.13 | | | | | | | | v6 = all_92_1 | v4 = all_92_1 | v1 = all_92_1)) % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | DELTA: instantiating (235) with fresh symbols all_415_0, % 31.15/5.13 | | | | | | | all_415_1, all_415_2, all_415_3, all_415_4, all_415_5, % 31.15/5.13 | | | | | | | all_415_6, all_415_7, all_415_8 gives: % 31.15/5.13 | | | | | | | (236) star_proj_11(all_92_1) = all_415_1 & % 31.15/5.13 | | | | | | | concat_proj_21(all_92_1) = all_415_3 & % 31.15/5.13 | | | | | | | alt_proj_21(all_92_1) = all_415_5 & alt_proj_11(all_92_1) % 31.15/5.13 | | | | | | | = all_415_6 & char_proj_11(all_92_1) = all_415_8 & % 31.15/5.13 | | | | | | | star1(all_415_1) = all_415_0 & concat1(all_92_4, % 31.15/5.13 | | | | | | | all_415_3) = all_415_2 & alt1(all_415_6, all_415_5) = % 31.15/5.13 | | | | | | | all_415_4 & char3(all_415_8) = all_415_7 & % 31.15/5.13 | | | | | | | regexp1(all_415_0) & regexp1(all_415_1) & % 31.15/5.13 | | | | | | | regexp1(all_415_2) & regexp1(all_415_3) & % 31.15/5.13 | | | | | | | regexp1(all_415_4) & regexp1(all_415_5) & % 31.15/5.13 | | | | | | | regexp1(all_415_6) & regexp1(all_415_7) & % 31.15/5.13 | | | | | | | char2(all_415_8) & (all_415_0 = all_92_1 | all_415_2 = % 31.15/5.13 | | | | | | | all_92_1 | all_415_4 = all_92_1 | all_415_7 = all_92_1) % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | ALPHA: (236) implies: % 31.15/5.13 | | | | | | | (237) char2(all_415_8) % 31.15/5.13 | | | | | | | (238) char3(all_415_8) = all_415_7 % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | GROUND_INST: instantiating (45) with all_415_8, all_415_7, % 31.15/5.13 | | | | | | | simplifying with (237), (238) gives: % 31.15/5.13 | | | | | | | (239) ? [v0: uni] : ? [v1: uni] : ? [v2: list_char] : % 31.15/5.13 | | | | | | | (t2tb1(all_415_8) = v0 & mem2(v2, all_415_7) = 0 & % 31.15/5.13 | | | | | | | tb2t(v1) = v2 & cons(char1, v0, all_94_0) = v1 & % 31.15/5.13 | | | | | | | list_char(v2) & uni(v1) & uni(v0)) % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | GROUND_INST: instantiating (length_nonnegative) with char1, % 31.15/5.13 | | | | | | | all_241_19, all_385_0, simplifying with (13), (204), % 31.15/5.13 | | | | | | | (221) gives: % 31.15/5.13 | | | | | | | (240) $lesseq(0, all_385_0) % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | GROUND_INST: instantiating (length_nonnegative) with char1, % 31.15/5.13 | | | | | | | all_241_18, $product(-1, all_385_0), simplifying with % 31.15/5.13 | | | | | | | (13), (205), (231) gives: % 31.15/5.13 | | | | | | | (241) $lesseq(all_385_0, 0) % 31.15/5.13 | | | | | | | % 31.15/5.13 | | | | | | | GROUND_INST: instantiating (49) with all_241_25, all_92_4, % 31.15/5.13 | | | | | | | simplifying with (34), (101), (228) gives: % 31.15/5.14 | | | | | | | (242) all_92_4 = epsilon1 | ? [v0: list_char] : ? [v1: % 31.15/5.14 | | | | | | | list_char] : ? [v2: regexp1] : ? [v3: int] : ? [v4: % 31.15/5.14 | | | | | | | int] : ? [v5: int] : ? [v6: uni] : ? [v7: uni] : ? % 31.15/5.14 | | | | | | | [v8: uni] : ? [v9: int] : ? [v10: regexp1] : ? [v11: % 31.15/5.14 | | | | | | | int] : ? [v12: list_char] : ? [v13: list_char] : ? % 31.15/5.14 | | | | | | | [v14: regexp1] : ? [v15: regexp1] : ? [v16: int] : ? % 31.15/5.14 | | | | | | | [v17: int] : ? [v18: uni] : ? [v19: uni] : ? [v20: % 31.15/5.14 | | | | | | | uni] : ? [v21: int] : ? [v22: int] : ? [v23: % 31.15/5.14 | | | | | | | list_char] : ? [v24: regexp1] : ? [v25: regexp1] : ? % 31.15/5.14 | | | | | | | [v26: int] : ? [v27: int] : ? [v28: list_char] : ? % 31.15/5.14 | | | | | | | [v29: regexp1] : ? [v30: regexp1] : ? [v31: int] : ? % 31.15/5.14 | | | | | | | [v32: int] : ? [v33: char2] : ? [v34: uni] : ? [v35: % 31.15/5.14 | | | | | | | uni] : ? [v36: int] : ? [v37: int] : (list_char(v28) % 31.15/5.14 | | | | | | | & list_char(v23) & list_char(v13) & list_char(v12) & % 31.15/5.14 | | | | | | | list_char(v1) & list_char(v0) & regexp1(v30) & % 31.15/5.14 | | | | | | | regexp1(v29) & regexp1(v25) & regexp1(v24) & % 31.15/5.14 | | | | | | | regexp1(v15) & regexp1(v14) & regexp1(v10) & % 31.15/5.14 | | | | | | | regexp1(v2) & char2(v33) & ((v37 = all_92_4 & v36 = % 31.15/5.14 | | | | | | | all_241_25 & t2tb1(v33) = v34 & tb2t(v35) = % 31.15/5.14 | | | | | | | all_241_25 & cons(char1, v34, all_97_1) = v35 & % 31.15/5.14 | | | | | | | char3(v33) = all_92_4 & uni(v35) & uni(v34)) | (v32 % 31.15/5.14 | | | | | | | = all_92_4 & v31 = 0 & v28 = all_241_25 & % 31.15/5.14 | | | | | | | mem2(all_241_25, v29) = 0 & alt1(v29, v30) = % 31.15/5.14 | | | | | | | all_92_4) | (v27 = all_92_4 & v26 = 0 & v23 = % 31.15/5.14 | | | | | | | all_241_25 & mem2(all_241_25, v25) = 0 & alt1(v24, % 31.15/5.14 | | | | | | | v25) = all_92_4) | (v22 = all_92_4 & v21 = % 31.15/5.14 | | | | | | | all_241_25 & v17 = 0 & v16 = 0 & mem2(v13, v15) = 0 % 31.15/5.14 | | | | | | | & mem2(v12, v14) = 0 & tb2t(v20) = all_241_25 & % 31.15/5.14 | | | | | | | t2tb(v13) = v19 & t2tb(v12) = v18 & % 31.15/5.14 | | | | | | | infix_plpl(char1, v18, v19) = v20 & concat1(v14, % 31.15/5.14 | | | | | | | v15) = all_92_4 & uni(v20) & uni(v19) & uni(v18)) % 31.15/5.14 | | | | | | | | (v11 = all_92_4 & all_241_25 = all_97_0 & % 31.15/5.14 | | | | | | | star1(v10) = all_92_4) | (v9 = all_241_25 & v5 = 0 % 31.15/5.14 | | | | | | | & v4 = all_92_4 & v3 = 0 & mem2(v1, all_92_4) = 0 & % 31.15/5.14 | | | | | | | mem2(v0, v2) = 0 & tb2t(v8) = all_241_25 & t2tb(v1) % 31.15/5.14 | | | | | | | = v7 & t2tb(v0) = v6 & infix_plpl(char1, v6, v7) = % 31.15/5.14 | | | | | | | v8 & star1(v2) = all_92_4 & uni(v8) & uni(v7) & % 31.15/5.14 | | | | | | | uni(v6)))) % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | ANTI_SYMM: (240), (241) imply: % 31.15/5.14 | | | | | | | (243) all_385_0 = 0 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | DELTA: instantiating (239) with fresh symbols all_449_0, % 31.15/5.14 | | | | | | | all_449_1, all_449_2 gives: % 31.15/5.14 | | | | | | | (244) t2tb1(all_415_8) = all_449_2 & mem2(all_449_0, all_415_7) % 31.15/5.14 | | | | | | | = 0 & tb2t(all_449_1) = all_449_0 & cons(char1, % 31.15/5.14 | | | | | | | all_449_2, all_94_0) = all_449_1 & list_char(all_449_0) % 31.15/5.14 | | | | | | | & uni(all_449_1) & uni(all_449_2) % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | ALPHA: (244) implies: % 31.15/5.14 | | | | | | | (245) uni(all_449_2) % 31.15/5.14 | | | | | | | (246) cons(char1, all_449_2, all_94_0) = all_449_1 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | REDUCE: (231), (243) imply: % 31.15/5.14 | | | | | | | (247) length1(char1, all_241_18) = 0 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | REDUCE: (221), (243) imply: % 31.15/5.14 | | | | | | | (248) length1(char1, all_241_19) = 0 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | REDUCE: (55), (246) imply: % 31.15/5.14 | | | | | | | (249) cons(char1, all_449_2, all_83_1) = all_449_1 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | BETA: splitting (242) gives: % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | Case 1: % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | (250) all_92_4 = epsilon1 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | REDUCE: (187), (250) imply: % 31.15/5.14 | | | | | | | | (251) $false % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | CLOSE: (251) is inconsistent. % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | Case 2: % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | GROUND_INST: instantiating (nil_Cons) with char1, all_449_2, % 31.15/5.14 | | | | | | | | all_83_1, all_449_1, simplifying with (13), (62), % 31.15/5.14 | | | | | | | | (245), (249) gives: % 31.15/5.14 | | | | | | | | (252) ? [v0: any] : ( ~ (v0 = all_449_1) & nil(char1) = v0 & % 31.15/5.14 | | | | | | | | uni(v0)) % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | GROUND_INST: instantiating (7) with char1, all_241_19, % 31.15/5.14 | | | | | | | | simplifying with (13), (204), (248) gives: % 31.15/5.14 | | | | | | | | (253) nil(char1) = all_241_19 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | GROUND_INST: instantiating (7) with char1, all_241_18, % 31.15/5.14 | | | | | | | | simplifying with (13), (205), (247) gives: % 31.15/5.14 | | | | | | | | (254) nil(char1) = all_241_18 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | DELTA: instantiating (252) with fresh symbol all_472_0 gives: % 31.15/5.14 | | | | | | | | (255) ~ (all_472_0 = all_449_1) & nil(char1) = all_472_0 & % 31.15/5.14 | | | | | | | | uni(all_472_0) % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | ALPHA: (255) implies: % 31.15/5.14 | | | | | | | | (256) nil(char1) = all_472_0 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | GROUND_INST: instantiating (17) with all_241_19, all_241_18, % 31.15/5.14 | | | | | | | | char1, simplifying with (253), (254) gives: % 31.15/5.14 | | | | | | | | (257) all_241_18 = all_241_19 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | GROUND_INST: instantiating (17) with all_83_1, all_472_0, char1, % 31.15/5.14 | | | | | | | | simplifying with (23), (256) gives: % 31.15/5.14 | | | | | | | | (258) all_472_0 = all_83_1 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | GROUND_INST: instantiating (17) with all_241_18, all_472_0, % 31.15/5.14 | | | | | | | | char1, simplifying with (254), (256) gives: % 31.15/5.14 | | | | | | | | (259) all_472_0 = all_241_18 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | COMBINE_EQS: (258), (259) imply: % 31.15/5.14 | | | | | | | | (260) all_241_18 = all_83_1 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | SIMP: (260) implies: % 31.15/5.14 | | | | | | | | (261) all_241_18 = all_83_1 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | COMBINE_EQS: (257), (261) imply: % 31.15/5.14 | | | | | | | | (262) all_241_19 = all_83_1 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | REDUCE: (218), (261) imply: % 31.15/5.14 | | | | | | | | (263) tb2t(all_83_1) = all_241_24 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | REDUCE: (217), (262) imply: % 31.15/5.14 | | | | | | | | (264) tb2t(all_83_1) = all_241_25 % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | | REF_CLOSE: (19), (21), (24), (33), (71), (227), (263), (264) are % 31.15/5.14 | | | | | | | | inconsistent by sub-proof #1. % 31.15/5.14 | | | | | | | | % 31.15/5.14 | | | | | | | End of split % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | End of split % 31.15/5.14 | | | | | | % 31.15/5.14 | | | | | Case 2: % 31.15/5.14 | | | | | | % 31.15/5.14 | | | | | | (265) (all_241_26 = all_92_1 & all_97_0 = all_83_0 & % 31.15/5.14 | | | | | | star1(all_241_27) = all_92_1) | (all_241_28 = all_83_0 & % 31.15/5.14 | | | | | | all_241_32 = 0 & all_241_33 = all_92_1 & all_241_34 = 0 & % 31.15/5.14 | | | | | | mem2(all_241_36, all_92_1) = 0 & mem2(all_241_37, % 31.15/5.14 | | | | | | all_241_35) = 0 & tb2t(all_241_29) = all_83_0 & % 31.15/5.14 | | | | | | t2tb(all_241_36) = all_241_30 & t2tb(all_241_37) = % 31.15/5.14 | | | | | | all_241_31 & infix_plpl(char1, all_241_31, all_241_30) = % 31.15/5.14 | | | | | | all_241_29 & star1(all_241_35) = all_92_1 & % 31.15/5.14 | | | | | | uni(all_241_29) & uni(all_241_30) & uni(all_241_31)) % 31.15/5.14 | | | | | | % 31.15/5.14 | | | | | | BETA: splitting (265) gives: % 31.15/5.14 | | | | | | % 31.15/5.14 | | | | | | Case 1: % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | (266) all_241_26 = all_92_1 & all_97_0 = all_83_0 & % 31.15/5.14 | | | | | | | star1(all_241_27) = all_92_1 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | ALPHA: (266) implies: % 31.15/5.14 | | | | | | | (267) star1(all_241_27) = all_92_1 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | GROUND_INST: instantiating (concat_Star) with all_92_4, all_92_3, % 31.15/5.14 | | | | | | | all_241_27, all_92_1, simplifying with (34), (35), % 31.15/5.14 | | | | | | | (37), (94), (267) gives: % 31.15/5.14 | | | | | | | (268) $false % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | CLOSE: (268) is inconsistent. % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | Case 2: % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | (269) all_241_28 = all_83_0 & all_241_32 = 0 & all_241_33 = % 31.15/5.14 | | | | | | | all_92_1 & all_241_34 = 0 & mem2(all_241_36, all_92_1) = % 31.15/5.14 | | | | | | | 0 & mem2(all_241_37, all_241_35) = 0 & tb2t(all_241_29) = % 31.15/5.14 | | | | | | | all_83_0 & t2tb(all_241_36) = all_241_30 & % 31.15/5.14 | | | | | | | t2tb(all_241_37) = all_241_31 & infix_plpl(char1, % 31.15/5.14 | | | | | | | all_241_31, all_241_30) = all_241_29 & % 31.15/5.14 | | | | | | | star1(all_241_35) = all_92_1 & uni(all_241_29) & % 31.15/5.14 | | | | | | | uni(all_241_30) & uni(all_241_31) % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | ALPHA: (269) implies: % 31.15/5.14 | | | | | | | (270) star1(all_241_35) = all_92_1 % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | GROUND_INST: instantiating (concat_Star) with all_92_4, all_92_3, % 31.15/5.14 | | | | | | | all_241_35, all_92_1, simplifying with (34), (35), % 31.15/5.14 | | | | | | | (37), (93), (270) gives: % 31.15/5.14 | | | | | | | (271) $false % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | | CLOSE: (271) is inconsistent. % 31.15/5.14 | | | | | | | % 31.15/5.14 | | | | | | End of split % 31.15/5.14 | | | | | | % 31.15/5.14 | | | | | End of split % 31.15/5.14 | | | | | % 31.15/5.14 | | | | End of split % 31.15/5.14 | | | | % 31.15/5.14 | | | End of split % 31.15/5.14 | | | % 31.15/5.14 | | End of split % 31.15/5.14 | | % 31.15/5.14 | End of split % 31.15/5.14 | % 31.15/5.14 End of proof % 31.15/5.15 % 31.15/5.15 Sub-proof #1 shows that the following formulas are inconsistent: % 31.15/5.15 ---------------------------------------------------------------- % 31.15/5.15 (1) ! [v0: list_char] : ! [v1: list_char] : ! [v2: uni] : (v1 = v0 | ~ % 31.15/5.15 (tb2t(v2) = v1) | ~ (tb2t(v2) = v0)) % 31.15/5.15 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 31.15/5.15 regexp1] : ! [v3: list_char] : (v1 = v0 | ~ (mem2(v3, v2) = v1) | ~ % 31.15/5.15 (mem2(v3, v2) = v0)) % 31.15/5.15 (3) ~ (all_92_2 = 0) % 31.15/5.15 (4) mem2(all_83_0, all_92_3) = all_92_2 % 31.15/5.15 (5) tb2t(all_83_1) = all_241_25 % 31.15/5.15 (6) tb2t(all_83_1) = all_241_24 % 31.15/5.15 (7) mem2(all_241_24, all_92_3) = 0 % 31.15/5.15 (8) tb2t(all_83_1) = all_83_0 % 31.15/5.15 % 31.15/5.15 Begin of proof % 31.15/5.15 | % 31.15/5.15 | GROUND_INST: instantiating (1) with all_83_0, all_241_24, all_83_1, % 31.15/5.15 | simplifying with (6), (8) gives: % 31.15/5.15 | (9) all_241_24 = all_83_0 % 31.15/5.15 | % 31.15/5.15 | GROUND_INST: instantiating (1) with all_241_25, all_241_24, all_83_1, % 31.15/5.15 | simplifying with (5), (6) gives: % 31.15/5.15 | (10) all_241_24 = all_241_25 % 31.15/5.15 | % 31.15/5.15 | COMBINE_EQS: (9), (10) imply: % 31.15/5.15 | (11) all_241_25 = all_83_0 % 31.15/5.15 | % 31.15/5.15 | REDUCE: (7), (9) imply: % 31.15/5.15 | (12) mem2(all_83_0, all_92_3) = 0 % 31.15/5.15 | % 31.15/5.15 | GROUND_INST: instantiating (2) with all_92_2, 0, all_92_3, all_83_0, % 31.15/5.15 | simplifying with (4), (12) gives: % 31.15/5.15 | (13) all_92_2 = 0 % 31.15/5.15 | % 31.15/5.15 | REDUCE: (3), (13) imply: % 31.15/5.15 | (14) $false % 31.15/5.15 | % 31.15/5.15 | CLOSE: (14) is inconsistent. % 31.15/5.15 | % 31.15/5.15 End of proof % 31.15/5.15 % SZS output end Proof for theBenchmark % 31.15/5.15 % 31.15/5.15 4532ms %------------------------------------------------------------------------------