%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW473+2 : TPTP v8.1.2. Released v5.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n014.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:18 EDT 2023 % Result : Theorem 59.03s 8.83s % Output : Proof 128.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW473+2 : TPTP v8.1.2. Released v5.3.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n014.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Aug 27 22:10:16 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.59 ________ _____ % 0.19/0.59 ___ __ \_________(_)________________________________ % 0.19/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.59 % 0.19/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.59 (2023-06-19) % 0.19/0.59 % 0.19/0.59 (c) Philipp Rümmer, 2009-2023 % 0.19/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.59 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 15.82/2.91 Prover 4: Preprocessing ... % 15.82/2.92 Prover 1: Preprocessing ... % 16.15/2.98 Prover 0: Preprocessing ... % 16.15/2.98 Prover 5: Preprocessing ... % 16.15/3.04 Prover 3: Preprocessing ... % 16.15/3.06 Prover 2: Preprocessing ... % 16.15/3.10 Prover 6: Preprocessing ... % 46.52/7.04 Prover 3: Warning: ignoring some quantifiers % 47.09/7.14 Prover 1: Warning: ignoring some quantifiers % 47.48/7.24 Prover 3: Constructing countermodel ... % 48.62/7.43 Prover 1: Constructing countermodel ... % 50.07/7.53 Prover 6: Proving ... % 50.27/7.62 Prover 4: Warning: ignoring some quantifiers % 54.81/8.18 Prover 4: Constructing countermodel ... % 57.14/8.50 Prover 5: Proving ... % 58.11/8.59 Prover 0: Proving ... % 58.68/8.82 Prover 3: proved (8201ms) % 58.68/8.82 % 59.03/8.83 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.03/8.83 % 59.03/8.83 Prover 5: stopped % 59.03/8.84 Prover 6: stopped % 59.03/8.84 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 59.03/8.84 Prover 0: stopped % 59.03/8.84 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 59.03/8.84 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 59.03/8.84 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 69.11/10.02 Prover 7: Preprocessing ... % 69.61/10.09 Prover 10: Preprocessing ... % 69.61/10.23 Prover 8: Preprocessing ... % 69.61/10.26 Prover 11: Preprocessing ... % 74.96/11.00 Prover 2: Proving ... % 74.96/11.00 Prover 2: stopped % 76.71/11.04 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 80.12/11.59 Prover 10: Warning: ignoring some quantifiers % 80.73/11.69 Prover 13: Preprocessing ... % 81.89/11.77 Prover 10: Constructing countermodel ... % 83.54/11.96 Prover 8: Warning: ignoring some quantifiers % 84.83/12.11 Prover 8: Constructing countermodel ... % 85.57/12.24 Prover 7: Warning: ignoring some quantifiers % 87.84/12.50 Prover 7: Constructing countermodel ... % 89.31/12.70 Prover 11: Warning: ignoring some quantifiers % 90.40/12.97 Prover 11: Constructing countermodel ... % 93.59/13.25 Prover 13: Warning: ignoring some quantifiers % 95.08/13.46 Prover 13: Constructing countermodel ... % 109.32/15.35 Prover 13: stopped % 109.32/15.36 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 114.16/15.98 Prover 1: stopped % 114.39/15.99 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 115.88/16.24 Prover 16: Preprocessing ... % 120.65/16.82 Prover 19: Preprocessing ... % 121.59/17.13 Prover 10: Found proof (size 117) % 121.59/17.13 Prover 10: proved (8295ms) % 122.33/17.14 Prover 7: stopped % 122.33/17.14 Prover 4: stopped % 122.33/17.14 Prover 11: stopped % 122.33/17.14 Prover 8: stopped % 125.76/17.64 Prover 16: Warning: ignoring some quantifiers % 126.07/17.73 Prover 16: Constructing countermodel ... % 126.07/17.74 Prover 16: stopped % 126.36/17.93 Prover 19: Warning: ignoring some quantifiers % 126.74/18.03 Prover 19: Constructing countermodel ... % 126.74/18.04 Prover 19: stopped % 126.74/18.04 % 126.74/18.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 126.74/18.04 % 127.23/18.06 % SZS output start Proof for theBenchmark % 127.39/18.08 Assumptions after simplification: % 127.39/18.08 --------------------------------- % 127.39/18.08 % 127.39/18.08 (conj_0) % 127.39/18.10 $i(u) & $i(finite_finite_pname) & ? [v0: $i] : % 127.39/18.10 (hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & $i(v0) & hBOOL(v0)) % 127.39/18.10 % 127.39/18.10 (conj_1) % 127.39/18.11 $i(mgt_call) & $i(ord_le1311769555a_bool) & $i(u) & $i(g) & ? [v0: $i] : ? % 127.39/18.11 [v1: $i] : ? [v2: $i] : (hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = % 127.39/18.11 v0 & hAPP_fun_a_bool_bool(v0, v1) = v2 & image_pname_a(mgt_call, u) = v1 & % 127.39/18.11 $i(v2) & $i(v1) & $i(v0) & hBOOL(v2)) % 127.39/18.11 % 127.39/18.11 (conj_2) % 127.39/18.11 $i(na) & $i(mgt_call) & $i(suc) & $i(finite_card_a) & $i(ord_less_eq_nat) & % 127.39/18.11 $i(u) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 127.39/18.11 (hAPP_nat_nat(suc, na) = v0 & hAPP_fun_a_bool_nat(finite_card_a, v2) = v3 & % 127.39/18.11 hAPP_n1699378549t_bool(ord_less_eq_nat, v0) = v1 & hAPP_nat_bool(v1, v3) = % 127.39/18.11 v4 & image_pname_a(mgt_call, u) = v2 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 127.39/18.11 $i(v0) & hBOOL(v4)) % 127.39/18.11 % 127.39/18.11 (conj_3) % 127.39/18.11 $i(na) & $i(mgt_call) & $i(suc) & $i(finite_card_a) & $i(u) & $i(g) & ? [v0: % 127.39/18.11 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 127.39/18.11 (minus_minus_nat(v2) = v3 & hAPP_nat_nat(v3, v4) = v0 & hAPP_nat_nat(suc, na) % 127.39/18.11 = v4 & hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 127.39/18.11 hAPP_fun_a_bool_nat(finite_card_a, g) = v0 & image_pname_a(mgt_call, u) = v1 % 127.39/18.11 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 127.39/18.11 % 127.39/18.11 (conj_4) % 127.39/18.11 $i(member_pname) & $i(pn) & $i(u) & ? [v0: $i] : ? [v1: $i] : % 127.39/18.11 (hAPP_f1664156314l_bool(v0, u) = v1 & hAPP_p338031245l_bool(member_pname, pn) % 127.39/18.11 = v0 & $i(v1) & $i(v0) & hBOOL(v1)) % 127.39/18.11 % 127.39/18.11 (conj_5) % 127.39/18.11 $i(mgt_call) & $i(member_a) & $i(pn) & $i(g) & ? [v0: $i] : ? [v1: $i] : ? % 127.39/18.11 [v2: $i] : (hAPP_fun_a_bool_bool(v1, g) = v2 & hAPP_pname_a(mgt_call, pn) = v0 % 127.39/18.11 & hAPP_a85458249l_bool(member_a, v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ~ % 127.39/18.11 hBOOL(v2)) % 127.39/18.11 % 127.39/18.12 (conj_6) % 127.39/18.12 $i(mgt_call) & $i(ord_le1311769555a_bool) & $i(pn) & $i(u) & $i(g) & ? [v0: % 127.39/18.12 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 127.39/18.12 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2 & % 127.39/18.12 hAPP_fun_a_bool_bool(v2, v3) = v4 & hAPP_pname_a(mgt_call, pn) = v0 & % 127.39/18.12 insert_a(v0, g) = v1 & image_pname_a(mgt_call, u) = v3 & $i(v4) & $i(v3) & % 127.39/18.12 $i(v2) & $i(v1) & $i(v0) & ~ hBOOL(v4)) % 127.39/18.12 % 127.39/18.12 (fact_154_finite__surj) % 127.39/18.12 $i(ord_le1311769555a_bool) & $i(finite_finite_pname) & $i(finite_finite_a) & % 127.39/18.12 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 127.39/18.12 $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v0) = v3) | ~ % 127.39/18.12 (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ (image_pname_a(v1, v2) = v4) | ~ % 127.39/18.12 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : % 127.39/18.12 ((hAPP_f1664156314l_bool(finite_finite_pname, v2) = v6 & $i(v6) & ~ % 127.39/18.12 hBOOL(v6)) | (hAPP_fun_a_bool_bool(finite_finite_a, v0) = v7 & $i(v7) & % 127.39/18.12 hBOOL(v7)))) % 127.39/18.12 % 127.39/18.12 (fact_264_insert__absorb) % 127.39/18.12 $i(member_pname) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 127.39/18.12 (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 127.39/18.12 (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 127.39/18.12 hBOOL(v3) | ~ is_fun_pname_bool(v1) | insert_pname(v0, v1) = v1) % 127.39/18.12 % 127.39/18.12 (fact_312_rev__image__eqI) % 127.39/18.12 $i(member_a) & $i(member_pname) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.39/18.12 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 127.39/18.12 : ( ~ (hAPP_f1664156314l_bool(v4, v3) = v5) | ~ (hAPP_fun_a_bool_bool(v6, v7) % 127.39/18.12 = v8) | ~ (hAPP_p338031245l_bool(member_pname, v2) = v4) | ~ % 127.39/18.12 (hAPP_a85458249l_bool(member_a, v0) = v6) | ~ (image_pname_a(v1, v3) = v7) % 127.39/18.12 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ hBOOL(v5) | hBOOL(v8) | % 127.39/18.12 ? [v9: $i] : ( ~ (v9 = v0) & hAPP_pname_a(v1, v2) = v9 & $i(v9))) % 127.39/18.12 % 127.39/18.12 (fact_324_insert__subset) % 127.39/18.13 $i(member_a) & $i(ord_le1311769555a_bool) & ! [v0: $i] : ! [v1: $i] : ! % 127.39/18.13 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 127.39/18.13 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = v4) | ~ % 127.39/18.13 (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ (insert_a(v0, v1) = v3) | ~ $i(v2) % 127.39/18.13 | ~ $i(v1) | ~ $i(v0) | ~ hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : ? [v8: % 127.39/18.13 $i] : ? [v9: $i] : (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = % 127.39/18.13 v8 & hAPP_fun_a_bool_bool(v8, v2) = v9 & hAPP_fun_a_bool_bool(v6, v2) = v7 % 127.39/18.13 & hAPP_a85458249l_bool(member_a, v0) = v6 & $i(v9) & $i(v8) & $i(v7) & % 127.39/18.13 $i(v6) & hBOOL(v9) & hBOOL(v7))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.39/18.13 : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 127.39/18.13 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = v4) | ~ % 127.39/18.13 (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ (insert_a(v0, v1) = v3) | ~ $i(v2) % 127.39/18.13 | ~ $i(v1) | ~ $i(v0) | hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : ? [v8: % 127.39/18.13 $i] : ? [v9: $i] : ((hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = % 127.39/18.13 v8 & hAPP_fun_a_bool_bool(v8, v2) = v9 & $i(v9) & $i(v8) & ~ hBOOL(v9)) % 127.39/18.13 | (hAPP_fun_a_bool_bool(v6, v2) = v7 & hAPP_a85458249l_bool(member_a, v0) % 127.39/18.13 = v6 & $i(v7) & $i(v6) & ~ hBOOL(v7)))) % 127.39/18.13 % 127.39/18.13 (fact_359_subsetI) % 127.39/18.13 $i(member_a) & $i(ord_le1311769555a_bool) & ! [v0: $i] : ! [v1: $i] : ! % 127.39/18.13 [v2: $i] : ! [v3: $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, % 127.39/18.13 v1) = v2) | ~ (hAPP_fun_a_bool_bool(v2, v0) = v3) | ~ $i(v1) | ~ % 127.39/18.13 $i(v0) | hBOOL(v3) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 127.39/18.13 (hAPP_fun_a_bool_bool(v5, v1) = v6 & hAPP_fun_a_bool_bool(v5, v0) = v7 & % 127.39/18.13 hAPP_a85458249l_bool(member_a, v4) = v5 & $i(v7) & $i(v6) & $i(v5) & % 127.39/18.13 $i(v4) & hBOOL(v6) & is_a(v4) & ~ hBOOL(v7))) % 127.39/18.13 % 127.39/18.13 (fact_64_card__insert__if) % 127.39/18.13 $i(member_pname) & $i(suc) & $i(finite_card_pname) & $i(finite_finite_pname) & % 127.39/18.13 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 127.39/18.13 (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 127.39/18.13 (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 127.39/18.13 [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 127.39/18.13 ((hAPP_f1664156314l_bool(finite_finite_pname, v1) = v4 & $i(v4) & ~ % 127.39/18.13 hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 127.39/18.13 hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 127.39/18.13 hAPP_f921600141ol_nat(finite_card_pname, v1) = v6 & insert_pname(v0, % 127.39/18.13 v1) = v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | (v8 = v6 & % 127.39/18.13 hAPP_nat_nat(suc, v7) = v6 & % 127.39/18.13 hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 127.39/18.13 hAPP_f921600141ol_nat(finite_card_pname, v1) = v7 & insert_pname(v0, % 127.39/18.13 v1) = v5 & $i(v7) & $i(v6) & $i(v5)))))) % 127.39/18.13 % 127.39/18.13 (fact_65_card__insert__if) % 127.39/18.13 $i(member_a) & $i(suc) & $i(finite_card_a) & $i(finite_finite_a) & ! [v0: $i] % 127.39/18.13 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (hAPP_fun_a_bool_bool(v2, v1) % 127.39/18.13 = v3) | ~ (hAPP_a85458249l_bool(member_a, v0) = v2) | ~ $i(v1) | ~ % 127.39/18.13 $i(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] % 127.39/18.13 : ((hAPP_fun_a_bool_bool(finite_finite_a, v1) = v4 & $i(v4) & ~ hBOOL(v4)) % 127.39/18.13 | (( ~ hBOOL(v3) | (v7 = v6 & hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 % 127.39/18.13 & hAPP_fun_a_bool_nat(finite_card_a, v1) = v6 & insert_a(v0, v1) = % 127.39/18.13 v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | (v8 = v6 & hAPP_nat_nat(suc, % 127.39/18.13 v7) = v6 & hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 & % 127.39/18.13 hAPP_fun_a_bool_nat(finite_card_a, v1) = v7 & insert_a(v0, v1) = v5 % 127.39/18.13 & $i(v7) & $i(v6) & $i(v5)))))) % 127.39/18.13 % 127.39/18.13 (gsy_v_U) % 127.39/18.13 $i(u) & is_fun_pname_bool(u) % 127.39/18.13 % 127.67/18.14 (function-axioms) % 127.77/18.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 127.77/18.20 (hAPP_f1476298914l_bool(v3, v2) = v1) | ~ (hAPP_f1476298914l_bool(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (hAPP_f1748468828l_bool(v3, v2) = v1) | ~ (hAPP_f1748468828l_bool(v3, v2) % 127.77/18.20 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 127.77/18.20 | ~ (hAPP_f198738859l_bool(v3, v2) = v1) | ~ (hAPP_f198738859l_bool(v3, % 127.77/18.20 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 127.77/18.20 = v0 | ~ (hAPP_a1392362872l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_a1392362872l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_p393069232l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_p393069232l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n1006566506l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_n1006566506l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_a_fun_bool_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_a_fun_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (nat_case_bool(v3, v2) = v1) | ~ % 127.77/18.20 (nat_case_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (cOMBB_bool_bool_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_bool_bool_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_238756964t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_238756964t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1897541054_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1897541054_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_472261505bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_472261505bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1137537805bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1137537805bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_743407885bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_743407885bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_a_fun_a_bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_a_fun_a_bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_392435466_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_392435466_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_408569982_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_408569982_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_928955006_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_928955006_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1823939024ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1823939024ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f282463732t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f282463732t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_2117322052ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_2117322052ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1066163005t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1066163005t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_2026977092ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_2026977092ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1885489796ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1885489796ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_a_fun_nat_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_a_fun_nat_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_164527437a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_164527437a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1896684278e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1896684278e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1250273980t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1250273980t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_523834888_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_523834888_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_pname_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_pname_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 127.77/18.20 ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1321347587bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1321347587bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_a_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_a_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (cOMBB_800536526ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_800536526ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1693087065a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1693087065a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_598082538e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_598082538e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1246832597l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1246832597l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_141086128t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_141086128t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_p130839763l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_p130839763l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_542850580_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_542850580_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_610033911bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_610033911bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f800510211t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f800510211t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1212655066ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1212655066ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_p1499970991t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_p1499970991t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_b589554111l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_b589554111l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_a_fun_nat_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_a_fun_nat_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_nat_nat(v3, v2) = v1) | ~ % 127.77/18.20 (image_nat_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (cOMBB_1015721476ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1015721476ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_nat_bool_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBS_nat_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_675860798_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_675860798_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_338059395a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_338059395a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_2095475776e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_2095475776e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_444170502t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_444170502t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_1187019125l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBS_1187019125l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1972296269bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_1972296269bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n215258509l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_n215258509l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f285962445l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f285962445l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f556039215l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f556039215l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1951378235l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1951378235l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_nat_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_nat_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (image_pname_nat(v3, v2) = v1) | ~ % 127.77/18.20 (image_pname_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 127.77/18.20 ! [v3: $i] : (v1 = v0 | ~ (hAPP_f22106695ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f22106695ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f2009550088ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f2009550088ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f55526627ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f55526627ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f696928925ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f696928925ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_fun_a_bool_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_fun_a_bool_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n1699378549t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_n1699378549t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f921600141ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f921600141ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (insert_nat(v3, v2) = v1) | ~ % 127.77/18.20 (insert_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (insert_fun_nat_bool(v3, v2) = v1) | ~ % 127.77/18.20 (insert_fun_nat_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_fun_a_bool_nat(v3, v2) = v1) | ~ % 127.77/18.20 (image_fun_a_bool_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1551609309ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (image_1551609309ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_496248727ol_nat(v3, v2) = v1) | ~ % 127.77/18.20 (image_496248727ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_a_nat(v3, v2) = v1) | ~ % 127.77/18.20 (image_a_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (image_26036933t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_26036933t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_2129980159t_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_2129980159t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f103356543l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f103356543l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1434722111l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1434722111l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f510955609l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f510955609l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1772781669l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1772781669l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f937997336l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f937997336l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f389811538l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f389811538l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f292226953l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f292226953l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1637334154l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1637334154l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f559147733l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f559147733l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1935102916l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1935102916l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f2117159681l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f2117159681l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f621171935l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f621171935l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f654413245e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f654413245e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1549043526a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1549043526a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f54304608l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f54304608l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1291551745_pname(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1291551745_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f434788991l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f434788991l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f759274231e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f759274231e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1051908748a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1051908748a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1664156314l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1664156314l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1297739591_pname(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1297739591_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1631501043l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1631501043l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1794073134e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1794073134e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f2050579477a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f2050579477a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_fun_a_bool_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_fun_a_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1128469712_pname(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_f1128469712_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n850744903l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_n850744903l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n1414589940l_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_n1414589940l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n1025906991e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_n1025906991e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_nat_fun_a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_nat_fun_a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_nat_bool(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_nat_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (hAPP_nat_pname(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_nat_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 127.77/18.20 ! [v3: $i] : (v1 = v0 | ~ (hAPP_nat_a(v3, v2) = v1) | ~ (hAPP_nat_a(v3, v2) % 127.77/18.20 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 127.77/18.20 | ~ (hAPP_bool_bool(v3, v2) = v1) | ~ (hAPP_bool_bool(v3, v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 127.77/18.20 (hAPP_p338031245l_bool(v3, v2) = v1) | ~ (hAPP_p338031245l_bool(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (hAPP_p1824510254l_bool(v3, v2) = v1) | ~ (hAPP_p1824510254l_bool(v3, v2) % 127.77/18.20 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 127.77/18.20 | ~ (hAPP_p61793385e_bool(v3, v2) = v1) | ~ (hAPP_p61793385e_bool(v3, v2) % 127.77/18.20 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 127.77/18.20 | ~ (hAPP_p1534023578a_bool(v3, v2) = v1) | ~ (hAPP_p1534023578a_bool(v3, % 127.77/18.20 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 127.77/18.20 = v0 | ~ (hAPP_pname_bool(v3, v2) = v1) | ~ (hAPP_pname_bool(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (hAPP_pname_pname(v3, v2) = v1) | ~ (hAPP_pname_pname(v3, v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 127.77/18.20 (hAPP_pname_a(v3, v2) = v1) | ~ (hAPP_pname_a(v3, v2) = v0)) & ! [v0: $i] % 127.77/18.20 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 127.77/18.20 (hAPP_a217006258l_bool(v3, v2) = v1) | ~ (hAPP_a217006258l_bool(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (hAPP_a85458249l_bool(v3, v2) = v1) | ~ (hAPP_a85458249l_bool(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (hAPP_a93125764e_bool(v3, v2) = v1) | ~ (hAPP_a93125764e_bool(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (hAPP_a_fun_a_bool(v3, v2) = v1) | ~ (hAPP_a_fun_a_bool(v3, v2) = v0)) & % 127.77/18.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 127.77/18.20 (hAPP_a_bool(v3, v2) = v1) | ~ (hAPP_a_bool(v3, v2) = v0)) & ! [v0: $i] : % 127.77/18.20 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_a_pname(v3, v2) = % 127.77/18.20 v1) | ~ (hAPP_a_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.20 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_a_a(v3, v2) = v1) | ~ % 127.77/18.20 (hAPP_a_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 127.77/18.20 $i] : (v1 = v0 | ~ (insert1325755072e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (insert1325755072e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (insert_fun_a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (insert_fun_a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : ! [v3: $i] : (v1 = v0 | ~ (insert_pname(v3, v2) = v1) | ~ % 127.77/18.20 (insert_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (insert_a(v3, v2) = v1) | ~ (insert_a(v3, v2) = v0)) % 127.77/18.20 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 127.77/18.20 (image_1921560913_pname(v3, v2) = v1) | ~ (image_1921560913_pname(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (image_fun_nat_bool_a(v3, v2) = v1) | ~ (image_fun_nat_bool_a(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (image_1283814551_pname(v3, v2) = v1) | ~ (image_1283814551_pname(v3, v2) % 127.77/18.20 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 127.77/18.20 | ~ (image_876012084bool_a(v3, v2) = v1) | ~ (image_876012084bool_a(v3, % 127.77/18.20 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 127.77/18.20 = v0 | ~ (image_1854862208_pname(v3, v2) = v1) | ~ % 127.77/18.20 (image_1854862208_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_fun_a_bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (image_fun_a_bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : ! [v3: $i] : (v1 = v0 | ~ (image_1655916159e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_1655916159e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_nat_fun_a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_nat_fun_a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_nat_pname(v3, v2) = v1) | ~ % 127.77/18.20 (image_nat_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 127.77/18.20 ! [v3: $i] : (v1 = v0 | ~ (image_nat_a(v3, v2) = v1) | ~ (image_nat_a(v3, % 127.77/18.20 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 127.77/18.20 = v0 | ~ (image_47868345e_bool(v3, v2) = v1) | ~ (image_47868345e_bool(v3, % 127.77/18.20 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 127.77/18.20 = v0 | ~ (image_112932426a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_112932426a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_pname_pname(v3, v2) = v1) | ~ % 127.77/18.20 (image_pname_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : ! [v3: $i] : (v1 = v0 | ~ (image_pname_a(v3, v2) = v1) | ~ % 127.77/18.20 (image_pname_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (image_819518260e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_819518260e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_a_fun_a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (image_a_fun_a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : ! [v3: $i] : (v1 = v0 | ~ (image_a_pname(v3, v2) = v1) | ~ % 127.77/18.20 (image_a_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 127.77/18.20 [v3: $i] : (v1 = v0 | ~ (image_a_a(v3, v2) = v1) | ~ (image_a_a(v3, v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 127.77/18.20 ~ (fun(v3, v2) = v1) | ~ (fun(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 127.77/18.20 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_350070575l_bool(v3, v2) = v1) % 127.77/18.20 | ~ (cOMBS_350070575l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.20 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_1035972772l_bool(v3, v2) = v1) | % 127.77/18.20 ~ (cOMBS_1035972772l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.20 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_568398431l_bool(v3, v2) = v1) | % 127.77/18.20 ~ (cOMBS_568398431l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.20 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_a_bool_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBS_a_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_307249310e_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_307249310e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_2140588453a_bool(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_2140588453a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_647938656_pname(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_647938656_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.20 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_bool_bool_a(v3, v2) = v1) | ~ % 127.77/18.20 (cOMBB_bool_bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (plus_plus_nat(v2) = v1) | ~ (plus_plus_nat(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (body(v2) = v1) | ~ % 127.77/18.20 (body(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (the_com(v2) = v1) | ~ (the_com(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.20 [v2: $i] : (v1 = v0 | ~ (cOMBK_a_pname(v2) = v1) | ~ (cOMBK_a_pname(v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBK_bool_nat(v2) = v1) | ~ (cOMBK_bool_nat(v2) = v0)) & ! [v0: $i] : ! % 127.77/18.20 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBK_1994329625t_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBK_1994329625t_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_pname_a_bool(v2) = v1) | ~ (cOMBC_pname_a_bool(v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_1834145417l_bool(v2) = v1) | ~ (cOMBC_1834145417l_bool(v2) = v0)) & % 127.77/18.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_777206479l_bool(v2) = v1) | ~ (cOMBC_777206479l_bool(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBC_a_a_bool(v2) = v1) % 127.77/18.20 | ~ (cOMBC_a_a_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 127.77/18.20 (v1 = v0 | ~ (cOMBC_445755039l_bool(v2) = v1) | ~ (cOMBC_445755039l_bool(v2) % 127.77/18.20 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_267053842l_bool(v2) = v1) | ~ (cOMBC_267053842l_bool(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_1928494297l_bool(v2) = v1) | ~ (cOMBC_1928494297l_bool(v2) = v0)) & % 127.77/18.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_386238098l_bool(v2) = v1) | ~ (cOMBC_386238098l_bool(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBC_nat_a_bool(v2) = % 127.77/18.20 v1) | ~ (cOMBC_nat_a_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.20 [v2: $i] : (v1 = v0 | ~ (cOMBC_619334683t_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_619334683t_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_1666426608t_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1666426608t_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_385542954t_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_385542954t_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_pname_nat_bool(v2) = v1) | ~ (cOMBC_pname_nat_bool(v2) % 127.77/18.20 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_a_nat_bool(v2) = v1) | ~ (cOMBC_a_nat_bool(v2) = v0)) & ! [v0: $i] % 127.77/18.20 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBC_1880041174l_bool(v2) = v1) % 127.77/18.20 | ~ (cOMBC_1880041174l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.20 [v2: $i] : (v1 = v0 | ~ (cOMBC_1738168533e_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1738168533e_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_1988546018l_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1988546018l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_1004116266e_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1004116266e_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_1245412066l_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1245412066l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_615407716e_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_615407716e_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_1058051404l_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1058051404l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_1149511130e_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1149511130e_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_1355376034l_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_1355376034l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_a_pname_bool(v2) = v1) | ~ (cOMBC_a_pname_bool(v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_226598744l_bool(v2) = v1) | ~ (cOMBC_226598744l_bool(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBC_nat_pname_bool(v2) % 127.77/18.20 = v1) | ~ (cOMBC_nat_pname_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 127.77/18.20 ! [v2: $i] : (v1 = v0 | ~ (cOMBC_nat_nat_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_nat_nat_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 127.77/18.20 (v1 = v0 | ~ (minus_minus_nat(v2) = v1) | ~ (minus_minus_nat(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (collect_nat(v2) = v1) | % 127.77/18.20 ~ (collect_nat(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 127.77/18.20 v0 | ~ (cOMBC_1693257480l_bool(v2) = v1) | ~ (cOMBC_1693257480l_bool(v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (collect_fun_nat_bool(v2) = v1) | ~ (collect_fun_nat_bool(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_1284144636l_bool(v2) = v1) | ~ (cOMBC_1284144636l_bool(v2) = v0)) & % 127.77/18.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_1732670874l_bool(v2) = v1) | ~ (cOMBC_1732670874l_bool(v2) = v0)) & % 127.77/18.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (cOMBC_331553030l_bool(v2) = v1) | ~ (cOMBC_331553030l_bool(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (collec707592106l_bool(v2) = v1) | ~ (collec707592106l_bool(v2) = v0)) & ! % 127.77/18.20 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBC_7971162l_bool(v2) % 127.77/18.20 = v1) | ~ (cOMBC_7971162l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 127.77/18.20 ! [v2: $i] : (v1 = v0 | ~ (collec1613912337l_bool(v2) = v1) | ~ % 127.77/18.20 (collec1613912337l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (cOMBC_595898202l_bool(v2) = v1) | ~ % 127.77/18.20 (cOMBC_595898202l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (collec1015864663l_bool(v2) = v1) | ~ % 127.77/18.20 (collec1015864663l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.20 : (v1 = v0 | ~ (wt(v2) = v1) | ~ (wt(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 127.77/18.20 : ! [v2: $i] : (v1 = v0 | ~ (mgt(v2) = v1) | ~ (mgt(v2) = v0)) & ! [v0: % 127.77/18.20 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = % 127.77/18.20 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.20 (collec1974731493e_bool(v2) = v1) | ~ (collec1974731493e_bool(v2) = v0)) & % 127.77/18.20 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (collect_fun_a_bool(v2) % 127.77/18.20 = v1) | ~ (collect_fun_a_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.21 [v2: $i] : (v1 = v0 | ~ (collect_pname(v2) = v1) | ~ (collect_pname(v2) = % 127.77/18.21 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.21 (collect_a(v2) = v1) | ~ (collect_a(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 127.77/18.21 : ! [v2: $i] : (v1 = v0 | ~ (undefi64961550l_bool(v2) = v1) | ~ % 127.77/18.21 (undefi64961550l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 127.77/18.21 (v1 = v0 | ~ (undefi1699038445l_bool(v2) = v1) | ~ % 127.77/18.21 (undefi1699038445l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 127.77/18.21 : (v1 = v0 | ~ (undefi17486888e_bool(v2) = v1) | ~ (undefi17486888e_bool(v2) % 127.77/18.21 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.21 (undefined_fun_a_bool(v2) = v1) | ~ (undefined_fun_a_bool(v2) = v0)) & ! % 127.77/18.21 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (undefined_pname(v2) = % 127.77/18.21 v1) | ~ (undefined_pname(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 127.77/18.21 $i] : (v1 = v0 | ~ (undefined_a(v2) = v1) | ~ (undefined_a(v2) = v0)) & ! % 127.77/18.21 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.21 (cOMBK_1857069011e_bool(v2) = v1) | ~ (cOMBK_1857069011e_bool(v2) = v0)) & % 127.77/18.21 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 127.77/18.21 (cOMBK_324466864a_bool(v2) = v1) | ~ (cOMBK_324466864a_bool(v2) = v0)) & ! % 127.77/18.21 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBK_bool_pname(v2) = % 127.77/18.21 v1) | ~ (cOMBK_bool_pname(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 127.77/18.21 [v2: $i] : (v1 = v0 | ~ (cOMBK_bool_a(v2) = v1) | ~ (cOMBK_bool_a(v2) = v0)) % 127.77/18.21 % 127.77/18.21 Further assumptions not needed in the proof: % 127.77/18.21 -------------------------------------------- % 127.77/18.21 fact_0_assms_I1_J, fact_100_finite__insert, fact_101_finite__insert, % 127.77/18.21 fact_102_finite__insert, fact_103_finite__subset, fact_104_finite__subset, % 127.77/18.21 fact_105_finite__subset, fact_106_finite__subset, fact_107_finite__subset, % 127.77/18.21 fact_108_finite__subset, fact_109_rev__finite__subset, fact_10_finite__imageI, % 127.77/18.21 fact_110_rev__finite__subset, fact_111_rev__finite__subset, % 127.77/18.21 fact_112_rev__finite__subset, fact_113_rev__finite__subset, % 127.77/18.21 fact_114_rev__finite__subset, fact_115_Suc__leD, fact_116_le__SucE, % 127.77/18.21 fact_117_le__SucI, fact_118_Suc__le__mono, fact_119_le__Suc__eq, % 127.77/18.21 fact_11_finite__imageI, fact_120_not__less__eq__eq, fact_121_Suc__n__not__le__n, % 127.77/18.21 fact_122_Suc__diff__diff, fact_123_diff__Suc__Suc, fact_124_le__diff__iff, % 127.77/18.21 fact_125_Nat_Odiff__diff__eq, fact_126_eq__diff__iff, % 127.77/18.21 fact_127_diff__diff__cancel, fact_128_diff__le__mono, fact_129_diff__le__mono2, % 127.77/18.21 fact_12_finite__imageI, fact_130_diff__le__self, fact_131_finite__surj, % 127.77/18.21 fact_132_finite__surj, fact_133_finite__surj, fact_134_finite__surj, % 127.77/18.21 fact_135_finite__surj, fact_136_finite__surj, fact_137_finite__surj, % 127.77/18.21 fact_138_finite__surj, fact_139_finite__surj, fact_13_finite__imageI, % 127.77/18.21 fact_140_finite__surj, fact_141_finite__surj, fact_142_finite__surj, % 127.77/18.21 fact_143_finite__surj, fact_144_finite__surj, fact_145_finite__surj, % 127.77/18.21 fact_146_finite__surj, fact_147_finite__surj, fact_148_finite__surj, % 127.77/18.21 fact_149_finite__surj, fact_14_finite__imageI, fact_150_finite__surj, % 127.77/18.21 fact_151_finite__surj, fact_152_finite__surj, fact_153_finite__surj, % 127.77/18.21 fact_155_finite__subset__image, fact_156_finite__subset__image, % 127.77/18.21 fact_157_finite__subset__image, fact_158_finite__subset__image, % 127.77/18.21 fact_159_finite__subset__image, fact_15_finite__imageI, % 127.77/18.21 fact_160_finite__subset__image, fact_161_finite__subset__image, % 127.77/18.21 fact_162_finite__subset__image, fact_163_finite__subset__image, % 127.77/18.21 fact_164_finite__subset__image, fact_165_finite__subset__image, % 127.77/18.21 fact_166_finite__subset__image, fact_167_finite__subset__image, % 127.77/18.21 fact_168_finite__subset__image, fact_169_finite__subset__image, % 127.77/18.21 fact_16_finite__imageI, fact_170_finite__subset__image, % 127.77/18.21 fact_171_finite__subset__image, fact_172_finite__subset__image, % 127.77/18.21 fact_173_finite__subset__image, fact_174_finite__subset__image, % 127.77/18.21 fact_175_finite__subset__image, fact_176_finite__subset__image, % 127.77/18.21 fact_177_finite__subset__image, fact_178_finite__subset__image, % 127.77/18.21 fact_179_finite__subset__image, fact_17_finite__imageI, % 127.77/18.21 fact_180_finite__subset__image, fact_181_finite__subset__image, % 127.77/18.21 fact_182_lift__Suc__mono__le, fact_183_lift__Suc__mono__le, % 127.77/18.21 fact_184_lift__Suc__mono__le, fact_185_lift__Suc__mono__le, % 127.77/18.21 fact_186_lift__Suc__mono__le, fact_187_pigeonhole__infinite, % 127.77/18.21 fact_188_pigeonhole__infinite, fact_189_pigeonhole__infinite, % 127.77/18.21 fact_18_finite__imageI, fact_190_pigeonhole__infinite, % 127.77/18.21 fact_191_pigeonhole__infinite, fact_192_pigeonhole__infinite, % 127.77/18.21 fact_193_pigeonhole__infinite, fact_194_pigeonhole__infinite, % 127.77/18.21 fact_195_pigeonhole__infinite, fact_196_pigeonhole__infinite, % 127.77/18.21 fact_197_pigeonhole__infinite, fact_198_pigeonhole__infinite, % 127.77/18.21 fact_199_pigeonhole__infinite, fact_19_finite__imageI, % 127.77/18.21 fact_1_finite__Collect__subsets, fact_200_pigeonhole__infinite, % 127.77/18.21 fact_201_pigeonhole__infinite, fact_202_pigeonhole__infinite, % 127.77/18.21 fact_203_pigeonhole__infinite, fact_204_pigeonhole__infinite, % 127.77/18.21 fact_205_pigeonhole__infinite, fact_206_pigeonhole__infinite, % 127.77/18.21 fact_207_pigeonhole__infinite, fact_208_pigeonhole__infinite, % 127.77/18.21 fact_209_pigeonhole__infinite, fact_20_finite__imageI, % 127.77/18.21 fact_210_pigeonhole__infinite, fact_211_image__eqI, fact_212_image__eqI, % 127.77/18.21 fact_213_image__eqI, fact_214_image__eqI, fact_215_image__eqI, % 127.77/18.21 fact_216_equalityI, fact_217_equalityI, fact_218_equalityI, fact_219_subsetD, % 127.77/18.21 fact_21_finite__imageI, fact_220_subsetD, fact_221_subsetD, fact_222_insertCI, % 127.77/18.21 fact_223_insertCI, fact_224_insertCI, fact_225_insertE, fact_226_insertE, % 127.77/18.21 fact_227_insertE, fact_228_zero__induct__lemma, fact_229_Suc__le__D, % 127.77/18.21 fact_22_finite__imageI, fact_230_insertI1, fact_231_insertI1, fact_232_insertI1, % 127.77/18.21 fact_233_insert__compr, fact_234_insert__compr, fact_235_insert__compr, % 127.77/18.21 fact_236_insert__compr, fact_237_insert__compr, fact_238_insert__compr, % 127.77/18.21 fact_239_insert__Collect, fact_23_finite_OinsertI, fact_240_insert__Collect, % 127.77/18.21 fact_241_insert__Collect, fact_242_insert__Collect, fact_243_insert__Collect, % 127.77/18.21 fact_244_insert__Collect, fact_245_insert__absorb2, fact_246_insert__absorb2, % 127.77/18.21 fact_247_insert__absorb2, fact_248_insert__commute, fact_249_insert__commute, % 127.77/18.21 fact_24_finite_OinsertI, fact_250_insert__commute, fact_251_insert__iff, % 127.77/18.21 fact_252_insert__iff, fact_253_insert__iff, fact_254_insert__code, % 127.77/18.21 fact_255_insert__code, fact_256_insert__code, fact_257_insert__ident, % 127.77/18.21 fact_258_insert__ident, fact_259_insert__ident, fact_25_finite_OinsertI, % 127.77/18.21 fact_260_insertI2, fact_261_insertI2, fact_262_insertI2, % 127.77/18.21 fact_263_insert__absorb, fact_265_insert__absorb, fact_266_subset__refl, % 127.77/18.21 fact_267_subset__refl, fact_268_subset__refl, fact_269_set__eq__subset, % 127.77/18.21 fact_26_finite_OinsertI, fact_270_set__eq__subset, fact_271_set__eq__subset, % 127.77/18.21 fact_272_equalityD1, fact_273_equalityD1, fact_274_equalityD1, % 127.77/18.21 fact_275_equalityD2, fact_276_equalityD2, fact_277_equalityD2, % 127.77/18.21 fact_278_in__mono, fact_279_in__mono, fact_27_finite_OinsertI, % 127.77/18.21 fact_280_in__mono, fact_281_set__rev__mp, fact_282_set__rev__mp, % 127.77/18.21 fact_283_set__rev__mp, fact_284_set__mp, fact_285_set__mp, fact_286_set__mp, % 127.77/18.21 fact_287_mem__def, fact_288_mem__def, fact_289_mem__def, % 127.77/18.21 fact_28_finite_OinsertI, fact_290_Collect__def, fact_291_Collect__def, % 127.77/18.21 fact_292_Collect__def, fact_293_Collect__def, fact_294_Collect__def, % 127.77/18.21 fact_295_Collect__def, fact_296_subset__trans, fact_297_subset__trans, % 127.77/18.21 fact_298_subset__trans, fact_299_equalityE, fact_29_card__image__le, % 127.77/18.21 fact_2_finite__Collect__subsets, fact_300_equalityE, fact_301_equalityE, % 127.77/18.21 fact_302_image__iff, fact_303_imageI, fact_304_imageI, fact_305_imageI, % 127.77/18.21 fact_306_imageI, fact_307_imageI, fact_308_rev__image__eqI, % 127.77/18.21 fact_309_rev__image__eqI, fact_30_card__image__le, fact_310_rev__image__eqI, % 127.77/18.21 fact_311_rev__image__eqI, fact_313_insert__compr__raw, % 127.77/18.21 fact_314_insert__compr__raw, fact_315_insert__compr__raw, % 127.77/18.21 fact_316_insert__compr__raw, fact_317_insert__compr__raw, % 127.77/18.21 fact_318_insert__compr__raw, fact_319_subset__insertI, fact_31_card__image__le, % 127.77/18.21 fact_320_subset__insertI, fact_321_subset__insertI, fact_322_insert__subset, % 127.77/18.21 fact_323_insert__subset, fact_325_subset__insert, fact_326_subset__insert, % 127.77/18.21 fact_327_subset__insert, fact_328_subset__insertI2, fact_329_subset__insertI2, % 127.77/18.21 fact_32_card__image__le, fact_330_subset__insertI2, fact_331_insert__mono, % 127.77/18.21 fact_332_insert__mono, fact_333_insert__mono, fact_334_image__insert, % 127.77/18.21 fact_335_image__insert, fact_336_image__insert, fact_337_image__insert, % 127.77/18.21 fact_338_insert__image, fact_339_insert__image, fact_33_card__image__le, % 127.77/18.21 fact_340_insert__image, fact_341_insert__image, fact_342_insert__image, % 127.77/18.21 fact_343_insert__image, fact_344_subset__image__iff, % 127.77/18.21 fact_345_subset__image__iff, fact_346_subset__image__iff, % 127.77/18.21 fact_347_subset__image__iff, fact_348_image__mono, fact_349_image__mono, % 127.77/18.21 fact_34_card__image__le, fact_350_image__mono, fact_351_image__mono, % 127.77/18.21 fact_352_imageE, fact_353_imageE, fact_354_imageE, fact_355_imageE, % 127.77/18.21 fact_356_imageE, fact_357_subsetI, fact_358_subsetI, fact_35_card__image__le, % 127.77/18.21 fact_360_image__subsetI, fact_361_image__subsetI, fact_362_image__subsetI, % 127.77/18.21 fact_363_image__subsetI, fact_364_image__subsetI, fact_365_image__subsetI, % 127.77/18.21 fact_366_image__subsetI, fact_367_order__refl, fact_368_order__refl, % 127.77/18.21 fact_369_order__refl, fact_36_card__image__le, fact_370_order__refl, % 127.77/18.21 fact_371_order__refl, fact_372_finite__nat__set__iff__bounded__le, % 127.77/18.21 fact_373_assms_I3_J, fact_374_le__fun__def, fact_375_le__fun__def, % 127.77/18.21 fact_376_le__fun__def, fact_377_le__funD, fact_378_le__funD, fact_379_le__funD, % 127.77/18.21 fact_37_card__image__le, fact_380_le__funE, fact_381_le__funE, % 127.77/18.21 fact_382_le__funE, fact_383_emptyE, fact_384_emptyE, fact_385_emptyE, % 127.77/18.21 fact_386_finite_OemptyI, fact_387_finite_OemptyI, fact_388_finite_OemptyI, % 127.77/18.21 fact_389_finite_OemptyI, fact_38_card__image__le, fact_390_finite_OemptyI, % 127.77/18.21 fact_391_finite_OemptyI, fact_392_empty__subsetI, fact_393_empty__subsetI, % 127.77/18.21 fact_394_empty__subsetI, fact_395_equals0D, fact_396_equals0D, % 127.77/18.21 fact_397_equals0D, fact_398_Collect__empty__eq, fact_399_Collect__empty__eq, % 127.77/18.21 fact_39_card__image__le, fact_3_finite__Collect__subsets, % 127.77/18.21 fact_400_Collect__empty__eq, fact_401_Collect__empty__eq, % 127.77/18.21 fact_402_Collect__empty__eq, fact_403_Collect__empty__eq, fact_404_empty__iff, % 127.77/18.21 fact_405_empty__iff, fact_406_empty__iff, fact_407_empty__Collect__eq, % 127.77/18.21 fact_408_empty__Collect__eq, fact_409_empty__Collect__eq, % 127.77/18.21 fact_40_card__image__le, fact_410_empty__Collect__eq, % 127.77/18.21 fact_411_empty__Collect__eq, fact_412_empty__Collect__eq, fact_413_ex__in__conv, % 127.77/18.21 fact_414_ex__in__conv, fact_415_ex__in__conv, fact_416_all__not__in__conv, % 127.77/18.21 fact_417_all__not__in__conv, fact_418_all__not__in__conv, fact_419_empty__def, % 127.77/18.21 fact_41_card__image__le, fact_420_empty__def, fact_421_empty__def, % 127.77/18.21 fact_422_empty__def, fact_423_empty__def, fact_424_empty__def, % 127.77/18.21 fact_425_bot__fun__def, fact_426_bot__fun__def, fact_427_bot__fun__def, % 127.77/18.21 fact_428_bot__apply, fact_429_bot__apply, fact_42_card__mono, % 127.77/18.21 fact_430_bot__apply, fact_431_le__bot, fact_432_le__bot, fact_433_le__bot, % 127.77/18.21 fact_434_le__bot, fact_435_le__bot, fact_436_bot__unique, fact_437_bot__unique, % 127.77/18.21 fact_438_bot__unique, fact_439_bot__unique, fact_43_card__mono, % 127.77/18.21 fact_440_bot__unique, fact_441_bot__least, fact_442_bot__least, % 127.77/18.21 fact_443_bot__least, fact_444_bot__least, fact_445_bot__least, % 127.77/18.21 fact_446_singleton__inject, fact_447_singleton__inject, % 127.77/18.21 fact_448_singleton__inject, fact_449_singletonE, fact_44_card__mono, % 127.77/18.21 fact_450_singletonE, fact_451_singletonE, fact_452_doubleton__eq__iff, % 127.77/18.21 fact_453_doubleton__eq__iff, fact_454_doubleton__eq__iff, % 127.77/18.21 fact_455_singleton__iff, fact_456_singleton__iff, fact_457_singleton__iff, % 127.77/18.21 fact_458_insert__not__empty, fact_459_insert__not__empty, fact_45_card__mono, % 127.77/18.21 fact_460_insert__not__empty, fact_461_empty__not__insert, % 127.77/18.21 fact_462_empty__not__insert, fact_463_empty__not__insert, % 127.77/18.21 fact_464_subset__empty, fact_465_subset__empty, fact_466_subset__empty, % 127.77/18.21 fact_467_image__is__empty, fact_468_image__empty, fact_469_empty__is__image, % 127.77/18.21 fact_46_card__mono, fact_470_Collect__conv__if, fact_471_Collect__conv__if, % 127.77/18.21 fact_472_Collect__conv__if, fact_473_Collect__conv__if, % 127.77/18.21 fact_474_Collect__conv__if, fact_475_Collect__conv__if, % 127.77/18.21 fact_476_Collect__conv__if2, fact_477_Collect__conv__if2, % 127.77/18.21 fact_478_Collect__conv__if2, fact_479_Collect__conv__if2, fact_47_card__mono, % 127.77/18.21 fact_480_Collect__conv__if2, fact_481_Collect__conv__if2, % 127.77/18.21 fact_482_singleton__conv, fact_483_singleton__conv, fact_484_singleton__conv, % 127.77/18.21 fact_485_singleton__conv, fact_486_singleton__conv, fact_487_singleton__conv, % 127.77/18.21 fact_488_singleton__conv2, fact_489_singleton__conv2, fact_48_card__seteq, % 127.77/18.21 fact_490_singleton__conv2, fact_491_singleton__conv2, fact_492_singleton__conv2, % 127.77/18.21 fact_493_singleton__conv2, fact_494_subset__singletonD, % 127.77/18.21 fact_495_subset__singletonD, fact_496_subset__singletonD, % 127.77/18.21 fact_497_image__constant, fact_498_image__constant__conv, % 127.77/18.21 fact_499_linorder__le__cases, fact_49_card__seteq, % 127.77/18.21 fact_4_finite__Collect__subsets, fact_500_xt1_I6_J, fact_501_xt1_I6_J, % 127.77/18.21 fact_502_xt1_I6_J, fact_503_xt1_I6_J, fact_504_xt1_I6_J, fact_505_xt1_I5_J, % 127.77/18.21 fact_506_xt1_I5_J, fact_507_xt1_I5_J, fact_508_xt1_I5_J, fact_509_xt1_I5_J, % 127.77/18.21 fact_50_card__seteq, fact_510_order__trans, fact_511_order__trans, % 127.77/18.21 fact_512_order__trans, fact_513_order__trans, fact_514_order__trans, % 127.77/18.21 fact_515_order__antisym, fact_516_order__antisym, fact_517_order__antisym, % 127.77/18.21 fact_518_order__antisym, fact_519_order__antisym, fact_51_card__seteq, % 127.77/18.21 fact_520_xt1_I4_J, fact_521_xt1_I4_J, fact_522_xt1_I4_J, fact_523_xt1_I4_J, % 127.77/18.21 fact_524_xt1_I4_J, fact_525_ord__le__eq__trans, fact_526_ord__le__eq__trans, % 127.77/18.21 fact_527_ord__le__eq__trans, fact_528_ord__le__eq__trans, % 127.77/18.21 fact_529_ord__le__eq__trans, fact_52_card__seteq, fact_530_xt1_I3_J, % 127.77/18.21 fact_531_xt1_I3_J, fact_532_xt1_I3_J, fact_533_xt1_I3_J, fact_534_xt1_I3_J, % 127.77/18.21 fact_535_ord__eq__le__trans, fact_536_ord__eq__le__trans, % 127.77/18.21 fact_537_ord__eq__le__trans, fact_538_ord__eq__le__trans, % 127.77/18.21 fact_539_ord__eq__le__trans, fact_53_card__seteq, fact_540_order__antisym__conv, % 127.77/18.21 fact_541_order__antisym__conv, fact_542_order__antisym__conv, % 127.77/18.21 fact_543_order__antisym__conv, fact_544_order__antisym__conv, % 127.77/18.21 fact_545_order__eq__refl, fact_546_order__eq__refl, fact_547_order__eq__refl, % 127.77/18.21 fact_548_order__eq__refl, fact_549_order__eq__refl, fact_54_card__insert__le, % 127.77/18.21 fact_550_order__eq__iff, fact_551_order__eq__iff, fact_552_order__eq__iff, % 127.77/18.21 fact_553_order__eq__iff, fact_554_order__eq__iff, fact_555_linorder__linear, % 127.77/18.21 fact_556_finite__subset__induct, fact_557_finite__subset__induct, % 127.77/18.21 fact_558_finite__subset__induct, fact_559_finite__subset__induct, % 127.77/18.21 fact_55_card__insert__le, fact_560_finite__subset__induct, % 127.77/18.21 fact_561_finite__subset__induct, fact_562_assms_I2_J, fact_563_finite__induct, % 127.77/18.21 fact_564_finite__induct, fact_565_finite__induct, fact_566_finite__less__ub, % 127.77/18.21 fact_567_assms_I4_J, fact_568_diff__Suc__eq__diff__pred, fact_569_diff__Suc__1, % 127.77/18.21 fact_56_card__insert__le, fact_570_less__eq__nat_Osimps_I2_J, % 127.77/18.21 fact_571_add__Suc__right, fact_572_add__Suc, fact_573_add__Suc__shift, % 127.77/18.21 fact_574_nat__add__right__cancel, fact_575_nat__add__left__cancel, % 127.77/18.21 fact_576_nat__add__assoc, fact_577_nat__add__left__commute, % 127.77/18.21 fact_578_nat__add__commute, fact_579_diff__add__inverse2, % 127.77/18.21 fact_57_card__insert__le, fact_580_diff__add__inverse, % 127.77/18.21 fact_581_diff__diff__left, fact_582_diff__cancel, fact_583_diff__cancel2, % 127.77/18.21 fact_584_le__add2, fact_585_le__add1, fact_586_le__iff__add, % 127.77/18.21 fact_587_nat__add__left__cancel__le, fact_588_trans__le__add1, % 127.77/18.21 fact_589_trans__le__add2, fact_58_card__insert__le, fact_590_add__le__mono1, % 127.77/18.21 fact_591_add__le__mono, fact_592_add__leD2, fact_593_add__leD1, % 127.77/18.21 fact_594_add__leE, fact_595_diff__add__assoc2, fact_596_add__diff__assoc2, % 127.77/18.21 fact_597_diff__add__assoc, fact_598_le__imp__diff__is__add, % 127.77/18.21 fact_599_le__add__diff__inverse2, fact_59_card__insert__le, % 127.77/18.21 fact_5_finite__Collect__subsets, fact_600_le__diff__conv2, % 127.77/18.21 fact_601_add__diff__assoc, fact_602_le__add__diff__inverse, % 127.77/18.21 fact_603_le__add__diff, fact_604_le__diff__conv, fact_605_diff__diff__right, % 127.77/18.21 fact_606_Suc__eq__plus1, fact_607_Suc__eq__plus1__left, % 127.77/18.21 fact_608_diff__Suc__diff__eq2, fact_609_diff__Suc__diff__eq1, % 127.77/18.21 fact_60_card__insert__if, fact_610_termination__basic__simps_I3_J, % 127.77/18.21 fact_611_termination__basic__simps_I4_J, fact_612_lessI, fact_613_Suc__mono, % 127.77/18.21 fact_614_finite__Collect__less__nat, fact_615_termination__basic__simps_I1_J, % 127.77/18.21 fact_616_termination__basic__simps_I2_J, fact_617_add__lessD1, % 127.77/18.21 fact_618_less__add__eq__less, fact_619_add__less__mono, % 127.77/18.21 fact_61_card__insert__if, fact_620_add__less__mono1, fact_621_trans__less__add2, % 127.77/18.21 fact_622_trans__less__add1, fact_623_nat__add__left__cancel__less, % 127.77/18.21 fact_624_not__add__less2, fact_625_not__add__less1, fact_626_Suc__less__SucD, % 127.77/18.21 fact_627_Suc__lessD, fact_628_less__SucE, fact_629_less__trans__Suc, % 127.77/18.21 fact_62_card__insert__if, fact_630_Suc__lessI, fact_631_less__SucI, % 127.77/18.21 fact_632_less__antisym, fact_633_not__less__less__Suc__eq, % 127.77/18.21 fact_634_Suc__less__eq, fact_635_less__Suc__eq, fact_636_not__less__eq, % 127.77/18.21 fact_637_less__or__eq__imp__le, fact_638_le__neq__implies__less, % 127.77/18.21 fact_639_less__imp__le__nat, fact_63_card__insert__if, % 127.77/18.21 fact_640_le__eq__less__or__eq, fact_641_nat__less__le, % 127.77/18.21 fact_642_diff__less__mono2, fact_643_less__imp__diff__less, % 127.77/18.21 fact_644_termination__basic__simps_I5_J, fact_645_less__not__refl, % 127.77/18.21 fact_646_nat__neq__iff, fact_647_linorder__neqE__nat, % 127.77/18.21 fact_648_less__irrefl__nat, fact_649_less__not__refl2, % 127.77/18.21 fact_650_less__not__refl3, fact_651_nat__less__cases, % 127.77/18.21 fact_652_finite__nat__set__iff__bounded, fact_653_card__Collect__less__nat, % 127.77/18.21 fact_654_finite__M__bounded__by__nat, fact_655_less__add__Suc1, % 127.77/18.21 fact_656_less__add__Suc2, fact_657_less__iff__Suc__add, % 127.77/18.21 fact_658_less__eq__Suc__le, fact_659_less__Suc__eq__le, fact_660_Suc__le__eq, % 127.77/18.21 fact_661_le__imp__less__Suc, fact_662_Suc__leI, fact_663_le__less__Suc__eq, % 127.77/18.21 fact_664_Suc__le__lessD, fact_665_diff__less__Suc, fact_666_add__diff__inverse, % 127.77/18.21 fact_667_less__diff__conv, fact_668_diff__less__mono, fact_669_less__diff__iff, % 127.77/18.21 fact_66_card__insert__disjoint, fact_670_less__eq__Suc__le__raw, % 127.77/18.21 fact_671_mono__nat__linear__lb, fact_672_inc__induct, % 127.77/18.21 fact_673_less__imp__Suc__add, fact_674_bounded__nat__set__is__finite, % 127.77/18.21 fact_675_less__mono__imp__le__mono, fact_676_Suc__lessE, fact_677_lessE, % 127.77/18.21 fact_678_less__zeroE, fact_679_le0, fact_67_card__insert__disjoint, % 127.77/18.21 fact_680_zero__less__Suc, fact_681_add__is__1, fact_682_one__is__add, % 127.77/18.21 fact_683_diff__add__0, fact_684_diff__is__0__eq_H, fact_685_diff__is__0__eq, % 127.77/18.21 fact_686_One__nat__def, fact_687_diffs0__imp__equal, fact_688_diff__self__eq__0, % 127.77/18.21 fact_689_minus__nat_Odiff__0, fact_68_card__insert__disjoint, % 127.77/18.21 fact_690_diff__0__eq__0, fact_691_Suc__neq__Zero, fact_692_Zero__neq__Suc, % 127.77/18.21 fact_693_nat_Osimps_I3_J, fact_694_Suc__not__Zero, fact_695_nat_Osimps_I2_J, % 127.77/18.21 fact_696_Zero__not__Suc, fact_697_bot__nat__def, fact_698_le__0__eq, % 127.77/18.21 fact_699_less__eq__nat_Osimps_I1_J, fact_69_card__insert__disjoint, % 127.77/18.21 fact_6_finite__Collect__subsets, fact_70_card__insert__disjoint, % 127.77/18.21 fact_71_card__insert__disjoint, fact_72_finite__Collect__conjI, % 127.77/18.21 fact_73_finite__Collect__conjI, fact_74_finite__Collect__conjI, % 127.77/18.21 fact_75_finite__Collect__conjI, fact_76_finite__Collect__conjI, % 127.77/18.21 fact_77_finite__Collect__conjI, fact_78_Suc__diff__le, % 127.77/18.21 fact_79_finite__Collect__le__nat, fact_7_finite__imageI, % 127.77/18.21 fact_80_card__Collect__le__nat, fact_81_Suc__inject, fact_82_nat_Oinject, % 127.77/18.21 fact_83_Suc__n__not__n, fact_84_n__not__Suc__n, fact_85_le__antisym, % 127.77/18.21 fact_86_le__trans, fact_87_eq__imp__le, fact_88_nat__le__linear, % 127.77/18.21 fact_89_le__refl, fact_8_finite__imageI, fact_90_diff__commute, % 127.77/18.21 fact_91_finite__Collect__disjI, fact_92_finite__Collect__disjI, % 127.77/18.21 fact_93_finite__Collect__disjI, fact_94_finite__Collect__disjI, % 127.77/18.21 fact_95_finite__Collect__disjI, fact_96_finite__Collect__disjI, % 127.77/18.21 fact_97_finite__insert, fact_98_finite__insert, fact_99_finite__insert, % 127.77/18.21 fact_9_finite__imageI, gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000t__a, % 127.77/18.21 gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Opname, % 127.77/18.21 gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_It__a_Mtc__HOL__Obool, % 127.77/18.21 gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Com__Opname_Mtc_, % 127.77/18.21 gsy_c_COMBK_000tc__HOL__Obool_000t__a, % 127.77/18.21 gsy_c_COMBK_000tc__HOL__Obool_000tc__Com__Opname, % 127.77/18.21 gsy_c_COMBK_000tc__HOL__Obool_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_COMBK_000tc__HOL__Obool_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_COMBS_000t__a_000tc__HOL__Obool_000tc__HOL__Obool, % 127.77/18.21 gsy_c_COMBS_000tc__Com__Opname_000tc__HOL__Obool_000tc__HOL__Obool, % 127.77/18.21 gsy_c_COMBS_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool_000tc__HOL__Obo, % 127.77/18.21 gsy_c_COMBS_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__Obool_000t, % 127.77/18.21 gsy_c_Finite__Set_Ofinite_000t__a, gsy_c_Finite__Set_Ofinite_000tc__Com__Opname, % 127.77/18.21 gsy_c_HOL_Oundefined_000t__a, gsy_c_HOL_Oundefined_000tc__Com__Opname, % 127.77/18.21 gsy_c_HOL_Oundefined_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_HOL_Oundefined_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_HOL_Oundefined_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool, % 127.77/18.21 gsy_c_HOL_Oundefined_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc_, % 127.77/18.21 gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool, % 127.77/18.21 gsy_c_Orderings_Obot__class_Obot_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Orderings_Obot__class_Obot_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Orderings_Obot__class_Obot_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc, % 127.77/18.21 gsy_c_Orderings_Obot__class_Obot_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__, % 127.77/18.21 gsy_c_Set_OCollect_000t__a, gsy_c_Set_OCollect_000tc__Com__Opname, % 127.77/18.21 gsy_c_Set_OCollect_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_OCollect_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_Oimage_000t__a_000t__a, gsy_c_Set_Oimage_000t__a_000tc__Com__Opname, % 127.77/18.21 gsy_c_Set_Oimage_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_Oimage_000t__a_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Com__Opname_000t__a, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Com__Opname_000tc__Com__Opname, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Nat__Onat_000t__a, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__Com__Opname, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_Oimage_000tc__fun_It__a_Mtc__HOL__Obool_J_000t__a, % 127.77/18.21 gsy_c_Set_Oimage_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opname, % 127.77/18.21 gsy_c_Set_Oimage_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000t__a, % 127.77/18.21 gsy_c_Set_Oimage_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Com__Opnam, % 127.77/18.21 gsy_c_Set_Oimage_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000t__a, % 127.77/18.21 gsy_c_Set_Oimage_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Com__Opname, % 127.77/18.21 gsy_c_Set_Oinsert_000t__a, gsy_c_Set_Oinsert_000tc__Com__Opname, % 127.77/18.21 gsy_c_Set_Oinsert_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_Set_Oinsert_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, gsy_c_fFalse, % 127.77/18.21 gsy_c_fTrue, gsy_c_hAPP_000t__a_000t__a, gsy_c_hAPP_000t__a_000tc__Com__Opname, % 127.77/18.21 gsy_c_hAPP_000t__a_000tc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000t__a_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000t__a_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000t__a_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__H, % 127.77/18.21 gsy_c_hAPP_000tc__Com__Opname_000t__a, % 127.77/18.21 gsy_c_hAPP_000tc__Com__Opname_000tc__Com__Opname, % 127.77/18.21 gsy_c_hAPP_000tc__Com__Opname_000tc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000tc__Com__Opname_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__H, % 127.77/18.21 gsy_c_hAPP_000tc__Com__Opname_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obo, % 127.77/18.21 gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000tc__Nat__Onat_000t__a, % 127.77/18.21 gsy_c_hAPP_000tc__Nat__Onat_000tc__Com__Opname, % 127.77/18.21 gsy_c_hAPP_000tc__Nat__Onat_000tc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL, % 127.77/18.21 gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opname, % 127.77/18.21 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HOL__Obool_J, % 127.77/18.21 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__Com__Opname_Mtc__H, % 127.77/18.21 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__a_Mtc__HOL, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Com__Opname, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__H, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_Itc__Com__Op, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_Itc, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Com__Opname, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obool, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HOL, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__Com__Opna, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_000tc__, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_000tc___001, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL__Oboo, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL__Oboo_002, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HOL__Obool_, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__, % 127.77/18.21 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HO, % 127.77/18.21 gsy_v_G, gsy_v_P, gsy_v_mgt, gsy_v_pn, gsy_v_wt, % 127.77/18.21 help_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000t__a_U, % 127.77/18.21 help_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opna, % 127.77/18.21 help_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Nat__Onat, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_006, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_008, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_011, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_015, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob_017, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000t__a_U, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Opname_U, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Nat__Onat_U, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_It__a_Mtc__H, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Com__Op, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Nat__On, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_004, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_007, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_010, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_013, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_016, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__003, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__005, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__009, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__012, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool__014, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It___018, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It___019, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_023, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_025, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__020, % 127.77/18.21 help_COMBB_1_1_COMBB_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__022, % 127.77/18.21 help_COMBC_1_1_COMBC_000t__a_000t__a_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000t__a_000tc__Com__Opname_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000t__a_000tc__Nat__Onat_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Oboo, % 127.77/18.21 help_COMBC_1_1_COMBC_000t__a_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc, % 127.77/18.21 help_COMBC_1_1_COMBC_000t__a_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Com__Opname_000t__a_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__Com__Opname_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__Nat__Onat_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Oboo, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000t__a_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__Com__Opname_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__Nat__Onat_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Oboo, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opname_000tc, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Nat__Onat_000tc__, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HO, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Com__O, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Nat__O, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_024, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Com__Opn, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Nat__Ona, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__021, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc_, % 127.77/18.21 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__H, % 127.77/18.21 help_COMBK_1_1_COMBK_000t__a_000tc__Com__Opname_U, % 127.77/18.21 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000t__a_U, % 127.77/18.21 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Opname_U, % 127.77/18.21 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Nat__Onat_U, % 127.77/18.21 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__fun_It__a_Mtc__HOL__Obool_J_U, % 127.77/18.21 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obo, % 127.77/18.21 help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool, % 127.77/18.21 help_COMBS_1_1_COMBS_000t__a_000tc__HOL__Obool_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBS_1_1_COMBS_000tc__Com__Opname_000tc__HOL__Obool_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBS_1_1_COMBS_000tc__Nat__Onat_000tc__HOL__Obool_000tc__HOL__Obool_U, % 127.77/18.21 help_COMBS_1_1_COMBS_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool_000tc_, % 127.77/18.21 help_COMBS_1_1_COMBS_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__O, % 127.77/18.21 help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obo, % 127.77/18.21 help_fFalse_1_1_T, help_fFalse_1_1_U, help_fNot_1_1_U, help_fNot_2_1_U, % 127.77/18.21 help_fconj_1_1_U, help_fconj_2_1_U, help_fconj_3_1_U, help_fdisj_1_1_U, % 127.77/18.21 help_fdisj_2_1_U, help_fdisj_3_1_U, help_fequal_1_1_fequal_000t__a_T, % 127.77/18.21 help_fequal_1_1_fequal_000tc__Com__Opname_T, % 127.77/18.21 help_fequal_1_1_fequal_000tc__Nat__Onat_T, % 127.77/18.21 help_fequal_1_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T, % 127.77/18.21 help_fequal_1_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T, % 127.77/18.21 help_fequal_1_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 127.77/18.21 help_fequal_2_1_fequal_000t__a_T, help_fequal_2_1_fequal_000tc__Com__Opname_T, % 127.77/18.21 help_fequal_2_1_fequal_000tc__Nat__Onat_T, % 127.77/18.21 help_fequal_2_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T, % 127.77/18.21 help_fequal_2_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T, % 127.77/18.21 help_fequal_2_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 127.77/18.21 help_fimplies_1_1_U, help_fimplies_2_1_U, help_fimplies_3_1_U % 127.77/18.21 % 127.77/18.21 Those formulas are unsatisfiable: % 127.77/18.21 --------------------------------- % 127.77/18.21 % 127.77/18.21 Begin of proof % 127.77/18.21 | % 127.77/18.21 | ALPHA: (gsy_v_U) implies: % 127.77/18.22 | (1) is_fun_pname_bool(u) % 127.77/18.22 | % 127.77/18.22 | ALPHA: (fact_64_card__insert__if) implies: % 128.07/18.22 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 128.07/18.22 | (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 128.07/18.22 | (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ % 128.07/18.22 | $i(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? % 128.07/18.22 | [v8: $i] : ((hAPP_f1664156314l_bool(finite_finite_pname, v1) = v4 & % 128.07/18.22 | $i(v4) & ~ hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 128.07/18.22 | hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 128.07/18.22 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v6 & % 128.07/18.22 | insert_pname(v0, v1) = v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | % 128.07/18.22 | (v8 = v6 & hAPP_nat_nat(suc, v7) = v6 & % 128.07/18.22 | hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 128.07/18.22 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v7 & % 128.07/18.22 | insert_pname(v0, v1) = v5 & $i(v7) & $i(v6) & $i(v5)))))) % 128.07/18.22 | % 128.07/18.22 | ALPHA: (fact_65_card__insert__if) implies: % 128.07/18.22 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 128.07/18.22 | (hAPP_fun_a_bool_bool(v2, v1) = v3) | ~ % 128.07/18.22 | (hAPP_a85458249l_bool(member_a, v0) = v2) | ~ $i(v1) | ~ $i(v0) | % 128.07/18.22 | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 128.07/18.22 | ((hAPP_fun_a_bool_bool(finite_finite_a, v1) = v4 & $i(v4) & ~ % 128.07/18.22 | hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 128.07/18.22 | hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 & % 128.07/18.22 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v6 & insert_a(v0, % 128.07/18.22 | v1) = v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | (v8 = v6 & % 128.07/18.22 | hAPP_nat_nat(suc, v7) = v6 & % 128.07/18.22 | hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 & % 128.07/18.22 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v7 & insert_a(v0, % 128.07/18.22 | v1) = v5 & $i(v7) & $i(v6) & $i(v5)))))) % 128.07/18.22 | % 128.07/18.22 | ALPHA: (fact_154_finite__surj) implies: % 128.07/18.22 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 128.07/18.22 | ! [v5: $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v0) = % 128.07/18.22 | v3) | ~ (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ % 128.07/18.22 | (image_pname_a(v1, v2) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 128.07/18.22 | hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : % 128.07/18.22 | ((hAPP_f1664156314l_bool(finite_finite_pname, v2) = v6 & $i(v6) & ~ % 128.07/18.22 | hBOOL(v6)) | (hAPP_fun_a_bool_bool(finite_finite_a, v0) = v7 & % 128.07/18.22 | $i(v7) & hBOOL(v7)))) % 128.07/18.22 | % 128.07/18.22 | ALPHA: (fact_264_insert__absorb) implies: % 128.07/18.22 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 128.07/18.22 | (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 128.07/18.22 | (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ % 128.07/18.22 | $i(v0) | ~ hBOOL(v3) | ~ is_fun_pname_bool(v1) | insert_pname(v0, % 128.07/18.22 | v1) = v1) % 128.07/18.22 | % 128.07/18.22 | ALPHA: (fact_312_rev__image__eqI) implies: % 128.07/18.22 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 128.07/18.22 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 128.07/18.22 | (hAPP_f1664156314l_bool(v4, v3) = v5) | ~ (hAPP_fun_a_bool_bool(v6, % 128.07/18.22 | v7) = v8) | ~ (hAPP_p338031245l_bool(member_pname, v2) = v4) | % 128.07/18.22 | ~ (hAPP_a85458249l_bool(member_a, v0) = v6) | ~ (image_pname_a(v1, % 128.07/18.22 | v3) = v7) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 128.07/18.22 | hBOOL(v5) | hBOOL(v8) | ? [v9: $i] : ( ~ (v9 = v0) & % 128.07/18.22 | hAPP_pname_a(v1, v2) = v9 & $i(v9))) % 128.07/18.22 | % 128.07/18.22 | ALPHA: (fact_324_insert__subset) implies: % 128.07/18.22 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 128.07/18.22 | ! [v5: $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = % 128.07/18.22 | v4) | ~ (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ (insert_a(v0, v1) % 128.07/18.22 | = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | hBOOL(v5) | ? [v6: $i] % 128.07/18.22 | : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 128.07/18.22 | ((hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v8 & % 128.07/18.22 | hAPP_fun_a_bool_bool(v8, v2) = v9 & $i(v9) & $i(v8) & ~ % 128.07/18.22 | hBOOL(v9)) | (hAPP_fun_a_bool_bool(v6, v2) = v7 & % 128.07/18.22 | hAPP_a85458249l_bool(member_a, v0) = v6 & $i(v7) & $i(v6) & ~ % 128.07/18.22 | hBOOL(v7)))) % 128.07/18.22 | % 128.07/18.22 | ALPHA: (fact_359_subsetI) implies: % 128.07/18.22 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 128.07/18.22 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2) | ~ % 128.07/18.22 | (hAPP_fun_a_bool_bool(v2, v0) = v3) | ~ $i(v1) | ~ $i(v0) | % 128.07/18.22 | hBOOL(v3) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 128.07/18.22 | (hAPP_fun_a_bool_bool(v5, v1) = v6 & hAPP_fun_a_bool_bool(v5, v0) = % 128.07/18.22 | v7 & hAPP_a85458249l_bool(member_a, v4) = v5 & $i(v7) & $i(v6) & % 128.07/18.22 | $i(v5) & $i(v4) & hBOOL(v6) & is_a(v4) & ~ hBOOL(v7))) % 128.07/18.22 | % 128.07/18.22 | ALPHA: (conj_0) implies: % 128.07/18.22 | (9) ? [v0: $i] : (hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & % 128.07/18.22 | $i(v0) & hBOOL(v0)) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (conj_1) implies: % 128.07/18.23 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 128.07/18.23 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = v0 & % 128.07/18.23 | hAPP_fun_a_bool_bool(v0, v1) = v2 & image_pname_a(mgt_call, u) = v1 % 128.07/18.23 | & $i(v2) & $i(v1) & $i(v0) & hBOOL(v2)) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (conj_2) implies: % 128.07/18.23 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 128.07/18.23 | (hAPP_nat_nat(suc, na) = v0 & hAPP_fun_a_bool_nat(finite_card_a, v2) = % 128.07/18.23 | v3 & hAPP_n1699378549t_bool(ord_less_eq_nat, v0) = v1 & % 128.07/18.23 | hAPP_nat_bool(v1, v3) = v4 & image_pname_a(mgt_call, u) = v2 & % 128.07/18.23 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & hBOOL(v4)) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (conj_3) implies: % 128.07/18.23 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 128.07/18.23 | (minus_minus_nat(v2) = v3 & hAPP_nat_nat(v3, v4) = v0 & % 128.07/18.23 | hAPP_nat_nat(suc, na) = v4 & hAPP_fun_a_bool_nat(finite_card_a, v1) % 128.07/18.23 | = v2 & hAPP_fun_a_bool_nat(finite_card_a, g) = v0 & % 128.07/18.23 | image_pname_a(mgt_call, u) = v1 & $i(v4) & $i(v3) & $i(v2) & $i(v1) % 128.07/18.23 | & $i(v0)) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (conj_4) implies: % 128.07/18.23 | (13) ? [v0: $i] : ? [v1: $i] : (hAPP_f1664156314l_bool(v0, u) = v1 & % 128.07/18.23 | hAPP_p338031245l_bool(member_pname, pn) = v0 & $i(v1) & $i(v0) & % 128.07/18.23 | hBOOL(v1)) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (conj_5) implies: % 128.07/18.23 | (14) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (hAPP_fun_a_bool_bool(v1, g) % 128.07/18.23 | = v2 & hAPP_pname_a(mgt_call, pn) = v0 & % 128.07/18.23 | hAPP_a85458249l_bool(member_a, v0) = v1 & $i(v2) & $i(v1) & $i(v0) & % 128.07/18.23 | ~ hBOOL(v2)) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (conj_6) implies: % 128.07/18.23 | (15) $i(g) % 128.07/18.23 | (16) $i(u) % 128.07/18.23 | (17) $i(pn) % 128.07/18.23 | (18) $i(mgt_call) % 128.07/18.23 | (19) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 128.07/18.23 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2 & % 128.07/18.23 | hAPP_fun_a_bool_bool(v2, v3) = v4 & hAPP_pname_a(mgt_call, pn) = v0 % 128.07/18.23 | & insert_a(v0, g) = v1 & image_pname_a(mgt_call, u) = v3 & $i(v4) & % 128.07/18.23 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ hBOOL(v4)) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (function-axioms) implies: % 128.07/18.23 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 128.07/18.23 | (image_pname_a(v3, v2) = v1) | ~ (image_pname_a(v3, v2) = v0)) % 128.07/18.23 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 128.07/18.23 | (insert_pname(v3, v2) = v1) | ~ (insert_pname(v3, v2) = v0)) % 128.07/18.23 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 128.07/18.23 | (hAPP_a85458249l_bool(v3, v2) = v1) | ~ (hAPP_a85458249l_bool(v3, % 128.07/18.23 | v2) = v0)) % 128.07/18.23 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 128.07/18.23 | (hAPP_pname_a(v3, v2) = v1) | ~ (hAPP_pname_a(v3, v2) = v0)) % 128.07/18.23 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 128.07/18.23 | (hAPP_fun_a_bool_bool(v3, v2) = v1) | ~ (hAPP_fun_a_bool_bool(v3, % 128.07/18.23 | v2) = v0)) % 128.07/18.23 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 128.07/18.23 | (hAPP_f1631501043l_bool(v3, v2) = v1) | ~ % 128.07/18.23 | (hAPP_f1631501043l_bool(v3, v2) = v0)) % 128.07/18.23 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 128.07/18.23 | (hAPP_f1664156314l_bool(v3, v2) = v1) | ~ % 128.07/18.23 | (hAPP_f1664156314l_bool(v3, v2) = v0)) % 128.07/18.23 | % 128.07/18.23 | DELTA: instantiating (9) with fresh symbol all_802_0 gives: % 128.07/18.23 | (27) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_802_0 & % 128.07/18.23 | $i(all_802_0) & hBOOL(all_802_0) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (27) implies: % 128.07/18.23 | (28) hBOOL(all_802_0) % 128.07/18.23 | (29) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_802_0 % 128.07/18.23 | % 128.07/18.23 | DELTA: instantiating (13) with fresh symbols all_823_0, all_823_1 gives: % 128.07/18.23 | (30) hAPP_f1664156314l_bool(all_823_1, u) = all_823_0 & % 128.07/18.23 | hAPP_p338031245l_bool(member_pname, pn) = all_823_1 & $i(all_823_0) & % 128.07/18.23 | $i(all_823_1) & hBOOL(all_823_0) % 128.07/18.23 | % 128.07/18.23 | ALPHA: (30) implies: % 128.07/18.24 | (31) hBOOL(all_823_0) % 128.07/18.24 | (32) hAPP_p338031245l_bool(member_pname, pn) = all_823_1 % 128.07/18.24 | (33) hAPP_f1664156314l_bool(all_823_1, u) = all_823_0 % 128.07/18.24 | % 128.07/18.24 | DELTA: instantiating (10) with fresh symbols all_879_0, all_879_1, all_879_2 % 128.07/18.24 | gives: % 128.07/18.24 | (34) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_879_2 & % 128.07/18.24 | hAPP_fun_a_bool_bool(all_879_2, all_879_1) = all_879_0 & % 128.07/18.24 | image_pname_a(mgt_call, u) = all_879_1 & $i(all_879_0) & $i(all_879_1) % 128.07/18.24 | & $i(all_879_2) & hBOOL(all_879_0) % 128.07/18.24 | % 128.07/18.24 | ALPHA: (34) implies: % 128.07/18.24 | (35) hBOOL(all_879_0) % 128.07/18.24 | (36) image_pname_a(mgt_call, u) = all_879_1 % 128.07/18.24 | (37) hAPP_fun_a_bool_bool(all_879_2, all_879_1) = all_879_0 % 128.07/18.24 | (38) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_879_2 % 128.07/18.24 | % 128.07/18.24 | DELTA: instantiating (14) with fresh symbols all_886_0, all_886_1, all_886_2 % 128.07/18.24 | gives: % 128.07/18.24 | (39) hAPP_fun_a_bool_bool(all_886_1, g) = all_886_0 & % 128.07/18.24 | hAPP_pname_a(mgt_call, pn) = all_886_2 & % 128.07/18.24 | hAPP_a85458249l_bool(member_a, all_886_2) = all_886_1 & $i(all_886_0) % 128.07/18.24 | & $i(all_886_1) & $i(all_886_2) & ~ hBOOL(all_886_0) % 128.07/18.24 | % 128.07/18.24 | ALPHA: (39) implies: % 128.07/18.24 | (40) ~ hBOOL(all_886_0) % 128.07/18.24 | (41) hAPP_a85458249l_bool(member_a, all_886_2) = all_886_1 % 128.07/18.24 | (42) hAPP_pname_a(mgt_call, pn) = all_886_2 % 128.07/18.24 | (43) hAPP_fun_a_bool_bool(all_886_1, g) = all_886_0 % 128.07/18.24 | % 128.07/18.24 | DELTA: instantiating (19) with fresh symbols all_899_0, all_899_1, all_899_2, % 128.07/18.24 | all_899_3, all_899_4 gives: % 128.07/18.24 | (44) hAPP_f1631501043l_bool(ord_le1311769555a_bool, all_899_3) = all_899_2 % 128.07/18.24 | & hAPP_fun_a_bool_bool(all_899_2, all_899_1) = all_899_0 & % 128.07/18.24 | hAPP_pname_a(mgt_call, pn) = all_899_4 & insert_a(all_899_4, g) = % 128.07/18.24 | all_899_3 & image_pname_a(mgt_call, u) = all_899_1 & $i(all_899_0) & % 128.07/18.24 | $i(all_899_1) & $i(all_899_2) & $i(all_899_3) & $i(all_899_4) & ~ % 128.07/18.24 | hBOOL(all_899_0) % 128.07/18.24 | % 128.07/18.24 | ALPHA: (44) implies: % 128.07/18.24 | (45) ~ hBOOL(all_899_0) % 128.07/18.24 | (46) $i(all_899_4) % 128.07/18.24 | (47) $i(all_899_3) % 128.07/18.24 | (48) $i(all_899_1) % 128.07/18.24 | (49) image_pname_a(mgt_call, u) = all_899_1 % 128.07/18.24 | (50) insert_a(all_899_4, g) = all_899_3 % 128.07/18.24 | (51) hAPP_pname_a(mgt_call, pn) = all_899_4 % 128.07/18.24 | (52) hAPP_fun_a_bool_bool(all_899_2, all_899_1) = all_899_0 % 128.07/18.24 | (53) hAPP_f1631501043l_bool(ord_le1311769555a_bool, all_899_3) = all_899_2 % 128.07/18.24 | % 128.07/18.24 | DELTA: instantiating (12) with fresh symbols all_901_0, all_901_1, all_901_2, % 128.07/18.24 | all_901_3, all_901_4 gives: % 128.07/18.24 | (54) minus_minus_nat(all_901_2) = all_901_1 & hAPP_nat_nat(all_901_1, % 128.07/18.24 | all_901_0) = all_901_4 & hAPP_nat_nat(suc, na) = all_901_0 & % 128.07/18.24 | hAPP_fun_a_bool_nat(finite_card_a, all_901_3) = all_901_2 & % 128.07/18.24 | hAPP_fun_a_bool_nat(finite_card_a, g) = all_901_4 & % 128.07/18.24 | image_pname_a(mgt_call, u) = all_901_3 & $i(all_901_0) & $i(all_901_1) % 128.07/18.24 | & $i(all_901_2) & $i(all_901_3) & $i(all_901_4) % 128.07/18.24 | % 128.07/18.24 | ALPHA: (54) implies: % 128.07/18.24 | (55) image_pname_a(mgt_call, u) = all_901_3 % 128.07/18.24 | % 128.07/18.24 | DELTA: instantiating (11) with fresh symbols all_903_0, all_903_1, all_903_2, % 128.07/18.24 | all_903_3, all_903_4 gives: % 128.07/18.24 | (56) hAPP_nat_nat(suc, na) = all_903_4 & hAPP_fun_a_bool_nat(finite_card_a, % 128.07/18.24 | all_903_2) = all_903_1 & hAPP_n1699378549t_bool(ord_less_eq_nat, % 128.07/18.24 | all_903_4) = all_903_3 & hAPP_nat_bool(all_903_3, all_903_1) = % 128.07/18.24 | all_903_0 & image_pname_a(mgt_call, u) = all_903_2 & $i(all_903_0) & % 128.07/18.24 | $i(all_903_1) & $i(all_903_2) & $i(all_903_3) & $i(all_903_4) & % 128.07/18.24 | hBOOL(all_903_0) % 128.07/18.24 | % 128.07/18.24 | ALPHA: (56) implies: % 128.07/18.24 | (57) image_pname_a(mgt_call, u) = all_903_2 % 128.07/18.24 | % 128.07/18.24 | GROUND_INST: instantiating (20) with all_879_1, all_901_3, u, mgt_call, % 128.07/18.24 | simplifying with (36), (55) gives: % 128.07/18.24 | (58) all_901_3 = all_879_1 % 128.07/18.24 | % 128.07/18.24 | GROUND_INST: instantiating (20) with all_901_3, all_903_2, u, mgt_call, % 128.07/18.24 | simplifying with (55), (57) gives: % 128.07/18.24 | (59) all_903_2 = all_901_3 % 128.07/18.24 | % 128.07/18.24 | GROUND_INST: instantiating (20) with all_899_1, all_903_2, u, mgt_call, % 128.07/18.24 | simplifying with (49), (57) gives: % 128.07/18.24 | (60) all_903_2 = all_899_1 % 128.07/18.24 | % 128.07/18.24 | GROUND_INST: instantiating (23) with all_886_2, all_899_4, pn, mgt_call, % 128.07/18.24 | simplifying with (42), (51) gives: % 128.07/18.24 | (61) all_899_4 = all_886_2 % 128.07/18.24 | % 128.07/18.24 | COMBINE_EQS: (59), (60) imply: % 128.07/18.24 | (62) all_901_3 = all_899_1 % 128.07/18.24 | % 128.07/18.24 | SIMP: (62) implies: % 128.07/18.24 | (63) all_901_3 = all_899_1 % 128.07/18.24 | % 128.07/18.24 | COMBINE_EQS: (58), (63) imply: % 128.07/18.24 | (64) all_899_1 = all_879_1 % 128.07/18.24 | % 128.07/18.24 | REDUCE: (52), (64) imply: % 128.07/18.24 | (65) hAPP_fun_a_bool_bool(all_899_2, all_879_1) = all_899_0 % 128.07/18.24 | % 128.07/18.24 | REDUCE: (50), (61) imply: % 128.07/18.24 | (66) insert_a(all_886_2, g) = all_899_3 % 128.07/18.24 | % 128.07/18.24 | REDUCE: (48), (64) imply: % 128.07/18.24 | (67) $i(all_879_1) % 128.07/18.24 | % 128.07/18.24 | REDUCE: (46), (61) imply: % 128.07/18.24 | (68) $i(all_886_2) % 128.07/18.24 | % 128.07/18.24 | GROUND_INST: instantiating (3) with all_886_2, g, all_886_1, all_886_0, % 128.07/18.24 | simplifying with (15), (41), (43), (68) gives: % 128.07/18.24 | (69) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 128.07/18.24 | ((hAPP_fun_a_bool_bool(finite_finite_a, g) = v0 & $i(v0) & ~ % 128.07/18.24 | hBOOL(v0)) | (( ~ hBOOL(all_886_0) | (v3 = v2 & % 128.07/18.24 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 128.07/18.24 | hAPP_fun_a_bool_nat(finite_card_a, g) = v2 & % 128.07/18.24 | insert_a(all_886_2, g) = v1 & $i(v2) & $i(v1))) & % 128.07/18.24 | (hBOOL(all_886_0) | (v4 = v2 & hAPP_nat_nat(suc, v3) = v2 & % 128.07/18.24 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 128.07/18.24 | hAPP_fun_a_bool_nat(finite_card_a, g) = v3 & % 128.07/18.24 | insert_a(all_886_2, g) = v1 & $i(v3) & $i(v2) & $i(v1))))) % 128.07/18.24 | % 128.07/18.25 | GROUND_INST: instantiating (4) with g, mgt_call, u, all_879_2, all_879_1, % 128.07/18.25 | all_879_0, simplifying with (15), (16), (18), (35), (36), (37), % 128.07/18.25 | (38) gives: % 128.07/18.25 | (70) ? [v0: $i] : ? [v1: $i] : % 128.07/18.25 | ((hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & $i(v0) & ~ % 128.07/18.25 | hBOOL(v0)) | (hAPP_fun_a_bool_bool(finite_finite_a, g) = v1 & % 128.07/18.25 | $i(v1) & hBOOL(v1))) % 128.07/18.25 | % 128.07/18.25 | GROUND_INST: instantiating (7) with all_886_2, g, all_879_1, all_899_3, % 128.07/18.25 | all_899_2, all_899_0, simplifying with (15), (45), (53), (65), % 128.07/18.25 | (66), (67), (68) gives: % 128.07/18.25 | (71) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 128.07/18.25 | ((hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = v2 & % 128.07/18.25 | hAPP_fun_a_bool_bool(v2, all_879_1) = v3 & $i(v3) & $i(v2) & ~ % 128.07/18.25 | hBOOL(v3)) | (hAPP_fun_a_bool_bool(v0, all_879_1) = v1 & % 128.07/18.25 | hAPP_a85458249l_bool(member_a, all_886_2) = v0 & $i(v1) & $i(v0) & % 128.07/18.25 | ~ hBOOL(v1))) % 128.07/18.25 | % 128.07/18.25 | GROUND_INST: instantiating (8) with all_879_1, all_899_3, all_899_2, % 128.07/18.25 | all_899_0, simplifying with (45), (47), (53), (65), (67) gives: % 128.07/18.25 | (72) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 128.07/18.25 | (hAPP_fun_a_bool_bool(v1, all_899_3) = v2 & hAPP_fun_a_bool_bool(v1, % 128.07/18.25 | all_879_1) = v3 & hAPP_a85458249l_bool(member_a, v0) = v1 & $i(v3) % 128.07/18.25 | & $i(v2) & $i(v1) & $i(v0) & hBOOL(v2) & is_a(v0) & ~ hBOOL(v3)) % 128.07/18.25 | % 128.07/18.25 | GROUND_INST: instantiating (5) with pn, u, all_823_1, all_823_0, simplifying % 128.07/18.25 | with (1), (16), (17), (31), (32), (33) gives: % 128.07/18.25 | (73) insert_pname(pn, u) = u % 128.07/18.25 | % 128.07/18.25 | GROUND_INST: instantiating (2) with pn, u, all_823_1, all_823_0, simplifying % 128.07/18.25 | with (16), (17), (32), (33) gives: % 128.07/18.25 | (74) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 128.07/18.25 | ((hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & $i(v0) & ~ % 128.07/18.25 | hBOOL(v0)) | (( ~ hBOOL(all_823_0) | (v3 = v2 & % 128.07/18.25 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v2 & % 128.07/18.25 | hAPP_f921600141ol_nat(finite_card_pname, u) = v2 & % 128.07/18.25 | insert_pname(pn, u) = v1 & $i(v2) & $i(v1))) & % 128.07/18.25 | (hBOOL(all_823_0) | (v4 = v2 & hAPP_nat_nat(suc, v3) = v2 & % 128.07/18.25 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v2 & % 128.07/18.25 | hAPP_f921600141ol_nat(finite_card_pname, u) = v3 & % 128.07/18.25 | insert_pname(pn, u) = v1 & $i(v3) & $i(v2) & $i(v1))))) % 128.07/18.25 | % 128.07/18.25 | DELTA: instantiating (70) with fresh symbols all_1147_0, all_1147_1 gives: % 128.07/18.25 | (75) (hAPP_f1664156314l_bool(finite_finite_pname, u) = all_1147_1 & % 128.07/18.25 | $i(all_1147_1) & ~ hBOOL(all_1147_1)) | % 128.07/18.25 | (hAPP_fun_a_bool_bool(finite_finite_a, g) = all_1147_0 & % 128.07/18.25 | $i(all_1147_0) & hBOOL(all_1147_0)) % 128.07/18.25 | % 128.07/18.25 | DELTA: instantiating (72) with fresh symbols all_1159_0, all_1159_1, % 128.07/18.25 | all_1159_2, all_1159_3 gives: % 128.07/18.25 | (76) hAPP_fun_a_bool_bool(all_1159_2, all_899_3) = all_1159_1 & % 128.07/18.25 | hAPP_fun_a_bool_bool(all_1159_2, all_879_1) = all_1159_0 & % 128.07/18.25 | hAPP_a85458249l_bool(member_a, all_1159_3) = all_1159_2 & % 128.07/18.25 | $i(all_1159_0) & $i(all_1159_1) & $i(all_1159_2) & $i(all_1159_3) & % 128.07/18.25 | hBOOL(all_1159_1) & is_a(all_1159_3) & ~ hBOOL(all_1159_0) % 128.07/18.25 | % 128.07/18.25 | ALPHA: (76) implies: % 128.07/18.25 | (77) ~ hBOOL(all_1159_0) % 128.07/18.25 | (78) $i(all_1159_3) % 128.07/18.25 | (79) hAPP_a85458249l_bool(member_a, all_1159_3) = all_1159_2 % 128.07/18.25 | (80) hAPP_fun_a_bool_bool(all_1159_2, all_879_1) = all_1159_0 % 128.07/18.25 | % 128.07/18.25 | DELTA: instantiating (71) with fresh symbols all_1161_0, all_1161_1, % 128.07/18.25 | all_1161_2, all_1161_3 gives: % 128.07/18.25 | (81) (hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_1161_1 & % 128.07/18.25 | hAPP_fun_a_bool_bool(all_1161_1, all_879_1) = all_1161_0 & % 128.07/18.25 | $i(all_1161_0) & $i(all_1161_1) & ~ hBOOL(all_1161_0)) | % 128.07/18.25 | (hAPP_fun_a_bool_bool(all_1161_3, all_879_1) = all_1161_2 & % 128.07/18.25 | hAPP_a85458249l_bool(member_a, all_886_2) = all_1161_3 & % 128.07/18.25 | $i(all_1161_2) & $i(all_1161_3) & ~ hBOOL(all_1161_2)) % 128.07/18.25 | % 128.07/18.25 | DELTA: instantiating (69) with fresh symbols all_1168_0, all_1168_1, % 128.07/18.25 | all_1168_2, all_1168_3, all_1168_4 gives: % 128.07/18.25 | (82) (hAPP_fun_a_bool_bool(finite_finite_a, g) = all_1168_4 & % 128.07/18.25 | $i(all_1168_4) & ~ hBOOL(all_1168_4)) | (( ~ hBOOL(all_886_0) | % 128.07/18.25 | (all_1168_1 = all_1168_2 & hAPP_fun_a_bool_nat(finite_card_a, % 128.07/18.25 | all_1168_3) = all_1168_2 & hAPP_fun_a_bool_nat(finite_card_a, % 128.07/18.25 | g) = all_1168_2 & insert_a(all_886_2, g) = all_1168_3 & % 128.07/18.25 | $i(all_1168_2) & $i(all_1168_3))) & (hBOOL(all_886_0) | % 128.07/18.25 | (all_1168_0 = all_1168_2 & hAPP_nat_nat(suc, all_1168_1) = % 128.07/18.25 | all_1168_2 & hAPP_fun_a_bool_nat(finite_card_a, all_1168_3) = % 128.07/18.25 | all_1168_2 & hAPP_fun_a_bool_nat(finite_card_a, g) = all_1168_1 % 128.07/18.25 | & insert_a(all_886_2, g) = all_1168_3 & $i(all_1168_1) & % 128.07/18.25 | $i(all_1168_2) & $i(all_1168_3)))) % 128.07/18.25 | % 128.07/18.25 | DELTA: instantiating (74) with fresh symbols all_1169_0, all_1169_1, % 128.07/18.25 | all_1169_2, all_1169_3, all_1169_4 gives: % 128.07/18.25 | (83) (hAPP_f1664156314l_bool(finite_finite_pname, u) = all_1169_4 & % 128.07/18.25 | $i(all_1169_4) & ~ hBOOL(all_1169_4)) | (( ~ hBOOL(all_823_0) | % 128.07/18.25 | (all_1169_1 = all_1169_2 & % 128.07/18.25 | hAPP_f921600141ol_nat(finite_card_pname, all_1169_3) = % 128.07/18.25 | all_1169_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 128.07/18.25 | all_1169_2 & insert_pname(pn, u) = all_1169_3 & $i(all_1169_2) & % 128.07/18.25 | $i(all_1169_3))) & (hBOOL(all_823_0) | (all_1169_0 = all_1169_2 % 128.07/18.25 | & hAPP_nat_nat(suc, all_1169_1) = all_1169_2 & % 128.07/18.25 | hAPP_f921600141ol_nat(finite_card_pname, all_1169_3) = % 128.07/18.25 | all_1169_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 128.07/18.25 | all_1169_1 & insert_pname(pn, u) = all_1169_3 & $i(all_1169_1) & % 128.07/18.25 | $i(all_1169_2) & $i(all_1169_3)))) % 128.07/18.25 | % 128.07/18.25 | BETA: splitting (83) gives: % 128.07/18.25 | % 128.07/18.25 | Case 1: % 128.07/18.25 | | % 128.07/18.25 | | (84) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_1169_4 & % 128.07/18.25 | | $i(all_1169_4) & ~ hBOOL(all_1169_4) % 128.07/18.25 | | % 128.07/18.25 | | ALPHA: (84) implies: % 128.07/18.26 | | (85) ~ hBOOL(all_1169_4) % 128.07/18.26 | | (86) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_1169_4 % 128.07/18.26 | | % 128.07/18.26 | | GROUND_INST: instantiating (26) with all_802_0, all_1169_4, u, % 128.07/18.26 | | finite_finite_pname, simplifying with (29), (86) gives: % 128.07/18.26 | | (87) all_1169_4 = all_802_0 % 128.07/18.26 | | % 128.07/18.26 | | REDUCE: (85), (87) imply: % 128.07/18.26 | | (88) ~ hBOOL(all_802_0) % 128.07/18.26 | | % 128.07/18.26 | | PRED_UNIFY: (28), (88) imply: % 128.07/18.26 | | (89) $false % 128.07/18.26 | | % 128.07/18.26 | | CLOSE: (89) is inconsistent. % 128.07/18.26 | | % 128.07/18.26 | Case 2: % 128.07/18.26 | | % 128.07/18.26 | | (90) ( ~ hBOOL(all_823_0) | (all_1169_1 = all_1169_2 & % 128.07/18.26 | | hAPP_f921600141ol_nat(finite_card_pname, all_1169_3) = % 128.07/18.26 | | all_1169_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 128.07/18.26 | | all_1169_2 & insert_pname(pn, u) = all_1169_3 & $i(all_1169_2) & % 128.07/18.26 | | $i(all_1169_3))) & (hBOOL(all_823_0) | (all_1169_0 = all_1169_2 % 128.07/18.26 | | & hAPP_nat_nat(suc, all_1169_1) = all_1169_2 & % 128.07/18.26 | | hAPP_f921600141ol_nat(finite_card_pname, all_1169_3) = % 128.07/18.26 | | all_1169_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 128.07/18.26 | | all_1169_1 & insert_pname(pn, u) = all_1169_3 & $i(all_1169_1) & % 128.07/18.26 | | $i(all_1169_2) & $i(all_1169_3))) % 128.07/18.26 | | % 128.07/18.26 | | ALPHA: (90) implies: % 128.07/18.26 | | (91) ~ hBOOL(all_823_0) | (all_1169_1 = all_1169_2 & % 128.07/18.26 | | hAPP_f921600141ol_nat(finite_card_pname, all_1169_3) = all_1169_2 % 128.07/18.26 | | & hAPP_f921600141ol_nat(finite_card_pname, u) = all_1169_2 & % 128.07/18.26 | | insert_pname(pn, u) = all_1169_3 & $i(all_1169_2) & % 128.07/18.26 | | $i(all_1169_3)) % 128.07/18.26 | | % 128.07/18.26 | | BETA: splitting (75) gives: % 128.07/18.26 | | % 128.07/18.26 | | Case 1: % 128.07/18.26 | | | % 128.25/18.26 | | | (92) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_1147_1 & % 128.25/18.26 | | | $i(all_1147_1) & ~ hBOOL(all_1147_1) % 128.25/18.26 | | | % 128.25/18.26 | | | ALPHA: (92) implies: % 128.25/18.26 | | | (93) ~ hBOOL(all_1147_1) % 128.25/18.26 | | | (94) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_1147_1 % 128.25/18.26 | | | % 128.25/18.26 | | | GROUND_INST: instantiating (26) with all_802_0, all_1147_1, u, % 128.25/18.26 | | | finite_finite_pname, simplifying with (29), (94) gives: % 128.25/18.26 | | | (95) all_1147_1 = all_802_0 % 128.25/18.26 | | | % 128.25/18.26 | | | REDUCE: (93), (95) imply: % 128.25/18.26 | | | (96) ~ hBOOL(all_802_0) % 128.25/18.26 | | | % 128.25/18.26 | | | PRED_UNIFY: (28), (96) imply: % 128.25/18.26 | | | (97) $false % 128.25/18.26 | | | % 128.25/18.26 | | | CLOSE: (97) is inconsistent. % 128.25/18.26 | | | % 128.25/18.26 | | Case 2: % 128.25/18.26 | | | % 128.25/18.26 | | | (98) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_1147_0 & % 128.25/18.26 | | | $i(all_1147_0) & hBOOL(all_1147_0) % 128.25/18.26 | | | % 128.25/18.26 | | | ALPHA: (98) implies: % 128.25/18.26 | | | (99) hBOOL(all_1147_0) % 128.25/18.26 | | | (100) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_1147_0 % 128.25/18.26 | | | % 128.25/18.26 | | | BETA: splitting (81) gives: % 128.25/18.26 | | | % 128.25/18.26 | | | Case 1: % 128.25/18.26 | | | | % 128.25/18.26 | | | | (101) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_1161_1 % 128.25/18.26 | | | | & hAPP_fun_a_bool_bool(all_1161_1, all_879_1) = all_1161_0 & % 128.25/18.26 | | | | $i(all_1161_0) & $i(all_1161_1) & ~ hBOOL(all_1161_0) % 128.25/18.26 | | | | % 128.25/18.26 | | | | ALPHA: (101) implies: % 128.25/18.26 | | | | (102) ~ hBOOL(all_1161_0) % 128.25/18.26 | | | | (103) hAPP_fun_a_bool_bool(all_1161_1, all_879_1) = all_1161_0 % 128.25/18.26 | | | | (104) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_1161_1 % 128.25/18.26 | | | | % 128.25/18.26 | | | | GROUND_INST: instantiating (25) with all_879_2, all_1161_1, g, % 128.25/18.26 | | | | ord_le1311769555a_bool, simplifying with (38), (104) gives: % 128.25/18.26 | | | | (105) all_1161_1 = all_879_2 % 128.25/18.26 | | | | % 128.25/18.26 | | | | REDUCE: (103), (105) imply: % 128.25/18.26 | | | | (106) hAPP_fun_a_bool_bool(all_879_2, all_879_1) = all_1161_0 % 128.25/18.26 | | | | % 128.25/18.26 | | | | GROUND_INST: instantiating (24) with all_879_0, all_1161_0, all_879_1, % 128.25/18.26 | | | | all_879_2, simplifying with (37), (106) gives: % 128.25/18.26 | | | | (107) all_1161_0 = all_879_0 % 128.25/18.26 | | | | % 128.25/18.26 | | | | REDUCE: (102), (107) imply: % 128.25/18.26 | | | | (108) ~ hBOOL(all_879_0) % 128.25/18.26 | | | | % 128.25/18.26 | | | | PRED_UNIFY: (35), (108) imply: % 128.25/18.26 | | | | (109) $false % 128.25/18.26 | | | | % 128.25/18.26 | | | | CLOSE: (109) is inconsistent. % 128.25/18.26 | | | | % 128.25/18.26 | | | Case 2: % 128.25/18.26 | | | | % 128.25/18.26 | | | | (110) hAPP_fun_a_bool_bool(all_1161_3, all_879_1) = all_1161_2 & % 128.25/18.26 | | | | hAPP_a85458249l_bool(member_a, all_886_2) = all_1161_3 & % 128.25/18.26 | | | | $i(all_1161_2) & $i(all_1161_3) & ~ hBOOL(all_1161_2) % 128.25/18.26 | | | | % 128.25/18.26 | | | | ALPHA: (110) implies: % 128.25/18.26 | | | | (111) ~ hBOOL(all_1161_2) % 128.25/18.26 | | | | (112) hAPP_a85458249l_bool(member_a, all_886_2) = all_1161_3 % 128.25/18.26 | | | | (113) hAPP_fun_a_bool_bool(all_1161_3, all_879_1) = all_1161_2 % 128.25/18.26 | | | | % 128.25/18.26 | | | | BETA: splitting (91) gives: % 128.25/18.26 | | | | % 128.25/18.26 | | | | Case 1: % 128.25/18.26 | | | | | % 128.25/18.26 | | | | | (114) ~ hBOOL(all_823_0) % 128.25/18.26 | | | | | % 128.25/18.26 | | | | | PRED_UNIFY: (31), (114) imply: % 128.25/18.26 | | | | | (115) $false % 128.25/18.26 | | | | | % 128.25/18.26 | | | | | CLOSE: (115) is inconsistent. % 128.25/18.26 | | | | | % 128.25/18.26 | | | | Case 2: % 128.25/18.26 | | | | | % 128.25/18.26 | | | | | (116) all_1169_1 = all_1169_2 & % 128.25/18.26 | | | | | hAPP_f921600141ol_nat(finite_card_pname, all_1169_3) = % 128.25/18.26 | | | | | all_1169_2 & hAPP_f921600141ol_nat(finite_card_pname, u) = % 128.25/18.26 | | | | | all_1169_2 & insert_pname(pn, u) = all_1169_3 & % 128.25/18.26 | | | | | $i(all_1169_2) & $i(all_1169_3) % 128.25/18.26 | | | | | % 128.25/18.26 | | | | | ALPHA: (116) implies: % 128.25/18.26 | | | | | (117) $i(all_1169_3) % 128.25/18.26 | | | | | (118) insert_pname(pn, u) = all_1169_3 % 128.25/18.26 | | | | | % 128.25/18.26 | | | | | BETA: splitting (82) gives: % 128.25/18.26 | | | | | % 128.25/18.26 | | | | | Case 1: % 128.25/18.26 | | | | | | % 128.25/18.26 | | | | | | (119) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_1168_4 & % 128.25/18.26 | | | | | | $i(all_1168_4) & ~ hBOOL(all_1168_4) % 128.25/18.26 | | | | | | % 128.25/18.26 | | | | | | ALPHA: (119) implies: % 128.25/18.26 | | | | | | (120) ~ hBOOL(all_1168_4) % 128.25/18.26 | | | | | | (121) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_1168_4 % 128.25/18.26 | | | | | | % 128.25/18.26 | | | | | | GROUND_INST: instantiating (24) with all_1147_0, all_1168_4, g, % 128.25/18.26 | | | | | | finite_finite_a, simplifying with (100), (121) gives: % 128.25/18.26 | | | | | | (122) all_1168_4 = all_1147_0 % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | | REDUCE: (120), (122) imply: % 128.25/18.27 | | | | | | (123) ~ hBOOL(all_1147_0) % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | | PRED_UNIFY: (99), (123) imply: % 128.25/18.27 | | | | | | (124) $false % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | | CLOSE: (124) is inconsistent. % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | Case 2: % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | | (125) ( ~ hBOOL(all_886_0) | (all_1168_1 = all_1168_2 & % 128.25/18.27 | | | | | | hAPP_fun_a_bool_nat(finite_card_a, all_1168_3) = % 128.25/18.27 | | | | | | all_1168_2 & hAPP_fun_a_bool_nat(finite_card_a, g) = % 128.25/18.27 | | | | | | all_1168_2 & insert_a(all_886_2, g) = all_1168_3 & % 128.25/18.27 | | | | | | $i(all_1168_2) & $i(all_1168_3))) & (hBOOL(all_886_0) | % 128.25/18.27 | | | | | | (all_1168_0 = all_1168_2 & hAPP_nat_nat(suc, all_1168_1) % 128.25/18.27 | | | | | | = all_1168_2 & hAPP_fun_a_bool_nat(finite_card_a, % 128.25/18.27 | | | | | | all_1168_3) = all_1168_2 & % 128.25/18.27 | | | | | | hAPP_fun_a_bool_nat(finite_card_a, g) = all_1168_1 & % 128.25/18.27 | | | | | | insert_a(all_886_2, g) = all_1168_3 & $i(all_1168_1) & % 128.25/18.27 | | | | | | $i(all_1168_2) & $i(all_1168_3))) % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | | ALPHA: (125) implies: % 128.25/18.27 | | | | | | (126) hBOOL(all_886_0) | (all_1168_0 = all_1168_2 & % 128.25/18.27 | | | | | | hAPP_nat_nat(suc, all_1168_1) = all_1168_2 & % 128.25/18.27 | | | | | | hAPP_fun_a_bool_nat(finite_card_a, all_1168_3) = % 128.25/18.27 | | | | | | all_1168_2 & hAPP_fun_a_bool_nat(finite_card_a, g) = % 128.25/18.27 | | | | | | all_1168_1 & insert_a(all_886_2, g) = all_1168_3 & % 128.25/18.27 | | | | | | $i(all_1168_1) & $i(all_1168_2) & $i(all_1168_3)) % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | | BETA: splitting (126) gives: % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | | Case 1: % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | (127) hBOOL(all_886_0) % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | PRED_UNIFY: (40), (127) imply: % 128.25/18.27 | | | | | | | (128) $false % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | CLOSE: (128) is inconsistent. % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | Case 2: % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | GROUND_INST: instantiating (21) with u, all_1169_3, u, pn, % 128.25/18.27 | | | | | | | simplifying with (73), (118) gives: % 128.25/18.27 | | | | | | | (129) all_1169_3 = u % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | GROUND_INST: instantiating (22) with all_886_1, all_1161_3, % 128.25/18.27 | | | | | | | all_886_2, member_a, simplifying with (41), (112) % 128.25/18.27 | | | | | | | gives: % 128.25/18.27 | | | | | | | (130) all_1161_3 = all_886_1 % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | REDUCE: (113), (130) imply: % 128.25/18.27 | | | | | | | (131) hAPP_fun_a_bool_bool(all_886_1, all_879_1) = all_1161_2 % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | GROUND_INST: instantiating (6) with all_886_2, mgt_call, pn, u, % 128.25/18.27 | | | | | | | all_823_1, all_823_0, all_886_1, all_879_1, % 128.25/18.27 | | | | | | | all_1161_2, simplifying with (16), (17), (18), (31), % 128.25/18.27 | | | | | | | (32), (33), (36), (41), (68), (111), (131) gives: % 128.25/18.27 | | | | | | | (132) ? [v0: any] : ( ~ (v0 = all_886_2) & % 128.25/18.27 | | | | | | | hAPP_pname_a(mgt_call, pn) = v0 & $i(v0)) % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | GROUND_INST: instantiating (6) with all_1159_3, mgt_call, pn, u, % 128.25/18.27 | | | | | | | all_823_1, all_823_0, all_1159_2, all_879_1, % 128.25/18.27 | | | | | | | all_1159_0, simplifying with (16), (17), (18), (31), % 128.25/18.27 | | | | | | | (32), (33), (36), (77), (78), (79), (80) gives: % 128.25/18.27 | | | | | | | (133) ? [v0: any] : ( ~ (v0 = all_1159_3) & % 128.25/18.27 | | | | | | | hAPP_pname_a(mgt_call, pn) = v0 & $i(v0)) % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | DELTA: instantiating (132) with fresh symbol all_1262_0 gives: % 128.25/18.27 | | | | | | | (134) ~ (all_1262_0 = all_886_2) & hAPP_pname_a(mgt_call, pn) % 128.25/18.27 | | | | | | | = all_1262_0 & $i(all_1262_0) % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | ALPHA: (134) implies: % 128.25/18.27 | | | | | | | (135) ~ (all_1262_0 = all_886_2) % 128.25/18.27 | | | | | | | (136) hAPP_pname_a(mgt_call, pn) = all_1262_0 % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | DELTA: instantiating (133) with fresh symbol all_1280_0 gives: % 128.25/18.27 | | | | | | | (137) ~ (all_1280_0 = all_1159_3) & hAPP_pname_a(mgt_call, pn) % 128.25/18.27 | | | | | | | = all_1280_0 & $i(all_1280_0) % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | ALPHA: (137) implies: % 128.25/18.27 | | | | | | | (138) hAPP_pname_a(mgt_call, pn) = all_1280_0 % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | GROUND_INST: instantiating (23) with all_886_2, all_1280_0, pn, % 128.25/18.27 | | | | | | | mgt_call, simplifying with (42), (138) gives: % 128.25/18.27 | | | | | | | (139) all_1280_0 = all_886_2 % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | GROUND_INST: instantiating (23) with all_1262_0, all_1280_0, pn, % 128.25/18.27 | | | | | | | mgt_call, simplifying with (136), (138) gives: % 128.25/18.27 | | | | | | | (140) all_1280_0 = all_1262_0 % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | COMBINE_EQS: (139), (140) imply: % 128.25/18.27 | | | | | | | (141) all_1262_0 = all_886_2 % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | REDUCE: (135), (141) imply: % 128.25/18.27 | | | | | | | (142) $false % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | | CLOSE: (142) is inconsistent. % 128.25/18.27 | | | | | | | % 128.25/18.27 | | | | | | End of split % 128.25/18.27 | | | | | | % 128.25/18.27 | | | | | End of split % 128.25/18.27 | | | | | % 128.25/18.27 | | | | End of split % 128.25/18.27 | | | | % 128.25/18.27 | | | End of split % 128.25/18.27 | | | % 128.25/18.27 | | End of split % 128.25/18.27 | | % 128.25/18.27 | End of split % 128.25/18.27 | % 128.25/18.27 End of proof % 128.25/18.27 % SZS output end Proof for theBenchmark % 128.25/18.27 % 128.25/18.27 17676ms %------------------------------------------------------------------------------