%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW473+1 : TPTP v8.1.2. Released v5.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n001.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:17 EDT 2023 % Result : Theorem 35.58s 5.54s % Output : Proof 65.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWW473+1 : TPTP v8.1.2. Released v5.3.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n001.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Sun Aug 27 20:09:33 EDT 2023 % 0.20/0.35 % CPUTime : % 0.21/0.62 ________ _____ % 0.21/0.62 ___ __ \_________(_)________________________________ % 0.21/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.62 % 0.21/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.62 (2023-06-19) % 0.21/0.62 % 0.21/0.62 (c) Philipp Rümmer, 2009-2023 % 0.21/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.62 Amanda Stjerna. % 0.21/0.62 Free software under BSD-3-Clause. % 0.21/0.62 % 0.21/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.62 % 0.21/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.63 Running up to 7 provers in parallel. % 0.21/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.76/2.08 Prover 1: Preprocessing ... % 9.76/2.09 Prover 4: Preprocessing ... % 9.76/2.12 Prover 5: Preprocessing ... % 9.76/2.12 Prover 6: Preprocessing ... % 9.76/2.12 Prover 3: Preprocessing ... % 9.76/2.12 Prover 0: Preprocessing ... % 9.76/2.12 Prover 2: Preprocessing ... % 26.43/4.40 Prover 1: Warning: ignoring some quantifiers % 26.43/4.48 Prover 3: Warning: ignoring some quantifiers % 28.25/4.55 Prover 3: Constructing countermodel ... % 28.25/4.56 Prover 1: Constructing countermodel ... % 29.28/4.71 Prover 4: Warning: ignoring some quantifiers % 29.85/4.75 Prover 6: Proving ... % 31.15/4.94 Prover 4: Constructing countermodel ... % 31.58/5.02 Prover 5: Proving ... % 32.40/5.21 Prover 0: Proving ... % 34.97/5.53 Prover 3: proved (4876ms) % 35.58/5.53 % 35.58/5.54 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.58/5.54 % 35.58/5.55 Prover 6: stopped % 35.58/5.55 Prover 0: stopped % 35.58/5.56 Prover 5: stopped % 35.90/5.58 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 35.90/5.58 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 35.90/5.58 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 35.90/5.58 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 39.88/6.18 Prover 7: Preprocessing ... % 40.41/6.21 Prover 10: Preprocessing ... % 41.07/6.30 Prover 11: Preprocessing ... % 41.28/6.35 Prover 2: Proving ... % 41.28/6.35 Prover 2: stopped % 41.28/6.35 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 41.28/6.35 Prover 8: Preprocessing ... % 44.00/6.70 Prover 13: Preprocessing ... % 48.98/7.35 Prover 10: Warning: ignoring some quantifiers % 48.98/7.37 Prover 8: Warning: ignoring some quantifiers % 50.03/7.48 Prover 8: Constructing countermodel ... % 50.03/7.52 Prover 10: Constructing countermodel ... % 51.86/7.78 Prover 7: Warning: ignoring some quantifiers % 51.86/7.83 Prover 7: Constructing countermodel ... % 54.51/8.06 Prover 11: Warning: ignoring some quantifiers % 55.08/8.16 Prover 11: Constructing countermodel ... % 56.18/8.30 Prover 13: Warning: ignoring some quantifiers % 56.85/8.41 Prover 13: Constructing countermodel ... % 63.60/9.41 Prover 10: Found proof (size 118) % 63.60/9.41 Prover 10: proved (3843ms) % 63.60/9.41 Prover 11: stopped % 63.60/9.41 Prover 13: stopped % 63.60/9.41 Prover 1: stopped % 63.60/9.41 Prover 4: stopped % 63.60/9.41 Prover 8: stopped % 63.60/9.41 Prover 7: stopped % 63.60/9.41 % 63.60/9.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.60/9.41 % 64.77/9.43 % SZS output start Proof for theBenchmark % 64.77/9.44 Assumptions after simplification: % 64.77/9.44 --------------------------------- % 64.77/9.45 % 64.77/9.45 (conj_0) % 64.77/9.47 $i(u) & $i(finite_finite_pname) & ? [v0: $i] : % 64.77/9.47 (hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & $i(v0) & hBOOL(v0)) % 64.77/9.47 % 64.77/9.47 (conj_1) % 64.77/9.47 $i(mgt_call) & $i(ord_le1311769555a_bool) & $i(u) & $i(g) & ? [v0: $i] : ? % 64.77/9.47 [v1: $i] : ? [v2: $i] : (hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = % 64.77/9.47 v0 & hAPP_fun_a_bool_bool(v0, v1) = v2 & image_pname_a(mgt_call, u) = v1 & % 64.77/9.47 $i(v2) & $i(v1) & $i(v0) & hBOOL(v2)) % 64.77/9.47 % 64.77/9.47 (conj_2) % 64.77/9.47 $i(na) & $i(mgt_call) & $i(suc) & $i(finite_card_a) & $i(ord_less_eq_nat) & % 64.77/9.47 $i(u) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 64.77/9.47 (hAPP_nat_nat(suc, na) = v0 & hAPP_fun_a_bool_nat(finite_card_a, v2) = v3 & % 64.77/9.47 hAPP_n1699378549t_bool(ord_less_eq_nat, v0) = v1 & hAPP_nat_bool(v1, v3) = % 64.77/9.47 v4 & image_pname_a(mgt_call, u) = v2 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 64.77/9.47 $i(v0) & hBOOL(v4)) % 64.77/9.47 % 64.77/9.47 (conj_3) % 64.77/9.47 $i(na) & $i(mgt_call) & $i(suc) & $i(finite_card_a) & $i(u) & $i(g) & ? [v0: % 64.77/9.48 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 64.77/9.48 (minus_minus_nat(v2) = v3 & hAPP_nat_nat(v3, v4) = v0 & hAPP_nat_nat(suc, na) % 64.77/9.48 = v4 & hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 64.77/9.48 hAPP_fun_a_bool_nat(finite_card_a, g) = v0 & image_pname_a(mgt_call, u) = v1 % 64.77/9.48 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 64.77/9.48 % 64.77/9.48 (conj_4) % 64.77/9.48 $i(member_pname) & $i(pn) & $i(u) & ? [v0: $i] : ? [v1: $i] : % 64.77/9.48 (hAPP_f1664156314l_bool(v0, u) = v1 & hAPP_p338031245l_bool(member_pname, pn) % 64.77/9.48 = v0 & $i(v1) & $i(v0) & hBOOL(v1)) % 64.77/9.48 % 64.77/9.48 (conj_5) % 64.77/9.48 $i(mgt_call) & $i(member_a) & $i(pn) & $i(g) & ? [v0: $i] : ? [v1: $i] : ? % 64.77/9.48 [v2: $i] : (hAPP_fun_a_bool_bool(v1, g) = v2 & hAPP_pname_a(mgt_call, pn) = v0 % 64.77/9.48 & hAPP_a85458249l_bool(member_a, v0) = v1 & $i(v2) & $i(v1) & $i(v0) & ~ % 64.77/9.48 hBOOL(v2)) % 64.77/9.48 % 64.77/9.48 (conj_6) % 64.77/9.48 $i(mgt_call) & $i(ord_le1311769555a_bool) & $i(pn) & $i(u) & $i(g) & ? [v0: % 64.77/9.48 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 64.77/9.48 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2 & % 64.77/9.48 hAPP_fun_a_bool_bool(v2, v3) = v4 & hAPP_pname_a(mgt_call, pn) = v0 & % 64.77/9.48 insert_a(v0, g) = v1 & image_pname_a(mgt_call, u) = v3 & $i(v4) & $i(v3) & % 64.77/9.48 $i(v2) & $i(v1) & $i(v0) & ~ hBOOL(v4)) % 64.77/9.48 % 64.77/9.48 (fact_102_card__insert__if) % 64.77/9.48 $i(member_pname) & $i(suc) & $i(finite_card_pname) & $i(finite_finite_pname) & % 64.77/9.48 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 64.77/9.48 (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 64.77/9.48 (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? % 64.77/9.48 [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 64.77/9.48 ((hAPP_f1664156314l_bool(finite_finite_pname, v1) = v4 & $i(v4) & ~ % 64.77/9.48 hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 64.77/9.48 hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 64.77/9.48 hAPP_f921600141ol_nat(finite_card_pname, v1) = v6 & insert_pname(v0, % 64.77/9.48 v1) = v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | (v8 = v6 & % 64.77/9.48 hAPP_nat_nat(suc, v7) = v6 & % 64.77/9.48 hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 64.77/9.48 hAPP_f921600141ol_nat(finite_card_pname, v1) = v7 & insert_pname(v0, % 64.77/9.48 v1) = v5 & $i(v7) & $i(v6) & $i(v5)))))) % 64.77/9.48 % 64.77/9.48 (fact_103_card__insert__if) % 64.77/9.49 $i(member_a) & $i(suc) & $i(finite_card_a) & $i(finite_finite_a) & ! [v0: $i] % 64.77/9.49 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (hAPP_fun_a_bool_bool(v2, v1) % 64.77/9.49 = v3) | ~ (hAPP_a85458249l_bool(member_a, v0) = v2) | ~ $i(v1) | ~ % 64.77/9.49 $i(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] % 64.77/9.49 : ((hAPP_fun_a_bool_bool(finite_finite_a, v1) = v4 & $i(v4) & ~ hBOOL(v4)) % 64.77/9.49 | (( ~ hBOOL(v3) | (v7 = v6 & hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 % 64.77/9.49 & hAPP_fun_a_bool_nat(finite_card_a, v1) = v6 & insert_a(v0, v1) = % 64.77/9.49 v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | (v8 = v6 & hAPP_nat_nat(suc, % 64.77/9.49 v7) = v6 & hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 & % 64.77/9.49 hAPP_fun_a_bool_nat(finite_card_a, v1) = v7 & insert_a(v0, v1) = v5 % 64.77/9.49 & $i(v7) & $i(v6) & $i(v5)))))) % 64.77/9.49 % 64.77/9.49 (fact_169_finite__surj) % 64.77/9.49 $i(ord_le1311769555a_bool) & $i(finite_finite_pname) & $i(finite_finite_a) & % 64.77/9.49 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 64.77/9.49 $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v0) = v3) | ~ % 64.77/9.49 (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ (image_pname_a(v1, v2) = v4) | ~ % 64.77/9.49 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : % 64.77/9.49 ((hAPP_f1664156314l_bool(finite_finite_pname, v2) = v6 & $i(v6) & ~ % 64.77/9.49 hBOOL(v6)) | (hAPP_fun_a_bool_bool(finite_finite_a, v0) = v7 & $i(v7) & % 64.77/9.49 hBOOL(v7)))) % 64.77/9.49 % 64.77/9.49 (fact_223_insert__absorb) % 64.77/9.49 $i(member_pname) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 64.77/9.49 (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 64.77/9.49 (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 64.77/9.49 hBOOL(v3) | ~ is_fun_pname_bool(v1) | insert_pname(v0, v1) = v1) % 64.77/9.49 % 64.77/9.49 (fact_262_rev__image__eqI) % 64.77/9.49 $i(member_a) & $i(member_pname) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 64.77/9.49 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 64.77/9.49 : ( ~ (hAPP_f1664156314l_bool(v4, v3) = v5) | ~ (hAPP_fun_a_bool_bool(v6, v7) % 64.77/9.49 = v8) | ~ (hAPP_p338031245l_bool(member_pname, v2) = v4) | ~ % 64.77/9.49 (hAPP_a85458249l_bool(member_a, v0) = v6) | ~ (image_pname_a(v1, v3) = v7) % 64.77/9.49 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ hBOOL(v5) | hBOOL(v8) | % 64.77/9.49 ? [v9: $i] : ( ~ (v9 = v0) & hAPP_pname_a(v1, v2) = v9 & $i(v9))) % 64.77/9.49 % 64.77/9.49 (fact_274_insert__subset) % 65.14/9.50 $i(member_a) & $i(ord_le1311769555a_bool) & ! [v0: $i] : ! [v1: $i] : ! % 65.14/9.50 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 65.14/9.50 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = v4) | ~ % 65.14/9.50 (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ (insert_a(v0, v1) = v3) | ~ $i(v2) % 65.14/9.50 | ~ $i(v1) | ~ $i(v0) | ~ hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : ? [v8: % 65.14/9.50 $i] : ? [v9: $i] : (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = % 65.14/9.50 v8 & hAPP_fun_a_bool_bool(v8, v2) = v9 & hAPP_fun_a_bool_bool(v6, v2) = v7 % 65.14/9.50 & hAPP_a85458249l_bool(member_a, v0) = v6 & $i(v9) & $i(v8) & $i(v7) & % 65.14/9.50 $i(v6) & hBOOL(v9) & hBOOL(v7))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.50 : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 65.14/9.50 (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = v4) | ~ % 65.14/9.50 (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ (insert_a(v0, v1) = v3) | ~ $i(v2) % 65.14/9.50 | ~ $i(v1) | ~ $i(v0) | hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : ? [v8: % 65.14/9.50 $i] : ? [v9: $i] : ((hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = % 65.14/9.50 v8 & hAPP_fun_a_bool_bool(v8, v2) = v9 & $i(v9) & $i(v8) & ~ hBOOL(v9)) % 65.14/9.50 | (hAPP_fun_a_bool_bool(v6, v2) = v7 & hAPP_a85458249l_bool(member_a, v0) % 65.14/9.50 = v6 & $i(v7) & $i(v6) & ~ hBOOL(v7)))) % 65.14/9.50 % 65.14/9.50 (fact_290_subsetI) % 65.14/9.50 $i(member_a) & $i(ord_le1311769555a_bool) & ! [v0: $i] : ! [v1: $i] : ! % 65.14/9.50 [v2: $i] : ! [v3: $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, % 65.14/9.50 v1) = v2) | ~ (hAPP_fun_a_bool_bool(v2, v0) = v3) | ~ $i(v1) | ~ % 65.14/9.50 $i(v0) | hBOOL(v3) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 65.14/9.50 (hAPP_fun_a_bool_bool(v5, v1) = v6 & hAPP_fun_a_bool_bool(v5, v0) = v7 & % 65.14/9.50 hAPP_a85458249l_bool(member_a, v4) = v5 & $i(v7) & $i(v6) & $i(v5) & % 65.14/9.50 $i(v4) & hBOOL(v6) & is_a(v4) & ~ hBOOL(v7))) % 65.14/9.50 % 65.14/9.50 (gsy_v_U) % 65.14/9.50 $i(u) & is_fun_pname_bool(u) % 65.14/9.50 % 65.14/9.50 (function-axioms) % 65.14/9.54 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.54 (hAPP_f1476298914l_bool(v3, v2) = v1) | ~ (hAPP_f1476298914l_bool(v3, v2) = % 65.14/9.54 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 65.14/9.54 ~ (hAPP_f1748468828l_bool(v3, v2) = v1) | ~ (hAPP_f1748468828l_bool(v3, v2) % 65.14/9.54 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 65.14/9.54 | ~ (hAPP_f198738859l_bool(v3, v2) = v1) | ~ (hAPP_f198738859l_bool(v3, % 65.14/9.54 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 65.14/9.54 = v0 | ~ (hAPP_p393069232l_bool(v3, v2) = v1) | ~ % 65.14/9.54 (hAPP_p393069232l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n1006566506l_bool(v3, v2) = v1) | ~ % 65.14/9.54 (hAPP_n1006566506l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_a_fun_bool_bool(v3, v2) = v1) | ~ % 65.14/9.54 (hAPP_a_fun_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_b589554111l_bool(v3, v2) = v1) | ~ % 65.14/9.54 (hAPP_b589554111l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_238756964t_bool(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_238756964t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_bool_bool_nat(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_bool_bool_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1246832597l_bool(v3, v2) = v1) | ~ % 65.14/9.54 (hAPP_f1246832597l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f800510211t_bool(v3, v2) = v1) | ~ % 65.14/9.54 (hAPP_f800510211t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1897541054_pname(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_1897541054_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1015721476ol_nat(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_1015721476ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_nat_bool_bool(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBS_nat_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_675860798_pname(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_675860798_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_1972296269bool_a(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_1972296269bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_338059395a_bool(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_338059395a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_2095475776e_bool(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_2095475776e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_444170502t_bool(v3, v2) = v1) | ~ % 65.14/9.54 (cOMBB_444170502t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.54 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_1187019125l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBS_1187019125l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n215258509l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_n215258509l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f285962445l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f285962445l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f556039215l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f556039215l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1951378235l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1951378235l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_nat_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_nat_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 65.14/9.55 [v3: $i] : (v1 = v0 | ~ (hAPP_f1253658590ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1253658590ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f98387925ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f98387925ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1690079119ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1690079119ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f2009550088ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f2009550088ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f55526627ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f55526627ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f696928925ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f696928925ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_fun_a_bool_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_fun_a_bool_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f22106695ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f22106695ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n1699378549t_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_n1699378549t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f921600141ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f921600141ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (insert_fun_nat_bool(v3, v2) = v1) | ~ % 65.14/9.55 (insert_fun_nat_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (insert1457093509l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (insert1457093509l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (insert1117693814l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (insert1117693814l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (insert2003652156l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (insert2003652156l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (insert_nat(v3, v2) = v1) | ~ % 65.14/9.55 (insert_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 65.14/9.55 [v3: $i] : (v1 = v0 | ~ (image_pname_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_pname_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 65.14/9.55 ! [v3: $i] : (v1 = v0 | ~ (image_2129980159t_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_2129980159t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1420695166l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_1420695166l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1642285373l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_1642285373l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1154884483l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_1154884483l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_26036933t_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_26036933t_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1208015684l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_1208015684l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1874789623l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_1874789623l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1607900221l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_1607900221l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_a_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_a_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 65.14/9.55 [v3: $i] : (v1 = v0 | ~ (image_496248727ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_496248727ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1551609309ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_1551609309ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_fun_a_bool_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_fun_a_bool_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1802975832ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_1802975832ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1079571347ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_1079571347ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_2089570637ol_nat(v3, v2) = v1) | ~ % 65.14/9.55 (image_2089570637ol_nat(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1772781669l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1772781669l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f510955609l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f510955609l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1434722111l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1434722111l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1050622307l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1050622307l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1759205631l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1759205631l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f760187903l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f760187903l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f103356543l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f103356543l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1295398978l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1295398978l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f595608956l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f595608956l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1363661463l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1363661463l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f937997336l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f937997336l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f389811538l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f389811538l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f292226953l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f292226953l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1637334154l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1637334154l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f559147733l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f559147733l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1935102916l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1935102916l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f2117159681l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f2117159681l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f621171935l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f621171935l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f54304608l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f54304608l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f434788991l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f434788991l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f759274231e_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f759274231e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1664156314l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1664156314l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f1631501043l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f1631501043l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_f2050579477a_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_f2050579477a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_fun_a_bool_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_fun_a_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_n1025906991e_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_n1025906991e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_nat_fun_a_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_nat_fun_a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_nat_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_nat_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 65.14/9.55 [v3: $i] : (v1 = v0 | ~ (hAPP_bool_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 65.14/9.55 ! [v3: $i] : (v1 = v0 | ~ (hAPP_p338031245l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_p338031245l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_p61793385e_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_p61793385e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_p1534023578a_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_p1534023578a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (hAPP_pname_bool(v3, v2) = v1) | ~ % 65.14/9.55 (hAPP_pname_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 65.14/9.55 ! [v3: $i] : (v1 = v0 | ~ (hAPP_pname_a(v3, v2) = v1) | ~ (hAPP_pname_a(v3, % 65.14/9.55 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 65.14/9.55 = v0 | ~ (hAPP_a85458249l_bool(v3, v2) = v1) | ~ (hAPP_a85458249l_bool(v3, % 65.14/9.55 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 65.14/9.55 = v0 | ~ (hAPP_a93125764e_bool(v3, v2) = v1) | ~ (hAPP_a93125764e_bool(v3, % 65.14/9.55 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 65.14/9.55 = v0 | ~ (hAPP_a_fun_a_bool(v3, v2) = v1) | ~ (hAPP_a_fun_a_bool(v3, v2) = % 65.14/9.55 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 65.14/9.55 ~ (hAPP_a_bool(v3, v2) = v1) | ~ (hAPP_a_bool(v3, v2) = v0)) & ! [v0: $i] % 65.14/9.55 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.55 (insert1325755072e_bool(v3, v2) = v1) | ~ (insert1325755072e_bool(v3, v2) = % 65.14/9.55 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 65.14/9.55 ~ (insert_fun_a_bool(v3, v2) = v1) | ~ (insert_fun_a_bool(v3, v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.55 (insert_pname(v3, v2) = v1) | ~ (insert_pname(v3, v2) = v0)) & ! [v0: $i] % 65.14/9.55 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (insert_a(v3, v2) = % 65.14/9.55 v1) | ~ (insert_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1604018183_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_1604018183_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_526090948bool_a(v3, v2) = v1) | ~ % 65.14/9.55 (image_526090948bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1705983821_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_1705983821_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_349102846bool_a(v3, v2) = v1) | ~ % 65.14/9.55 (image_349102846bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_990671762_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_990671762_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_573985017bool_a(v3, v2) = v1) | ~ % 65.14/9.55 (image_573985017bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1921560913_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_1921560913_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_fun_nat_bool_a(v3, v2) = v1) | ~ % 65.14/9.55 (image_fun_nat_bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1283814551_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_1283814551_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_876012084bool_a(v3, v2) = v1) | ~ % 65.14/9.55 (image_876012084bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_1854862208_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_1854862208_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_fun_a_bool_a(v3, v2) = v1) | ~ % 65.14/9.55 (image_fun_a_bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : ! [v3: $i] : (v1 = v0 | ~ (image_1655916159e_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_1655916159e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_nat_fun_a_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_nat_fun_a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_nat_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_nat_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 65.14/9.55 ! [v3: $i] : (v1 = v0 | ~ (image_nat_a(v3, v2) = v1) | ~ (image_nat_a(v3, % 65.14/9.55 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 65.14/9.55 = v0 | ~ (image_47868345e_bool(v3, v2) = v1) | ~ (image_47868345e_bool(v3, % 65.14/9.55 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 65.14/9.55 = v0 | ~ (image_112932426a_bool(v3, v2) = v1) | ~ % 65.14/9.55 (image_112932426a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (image_pname_pname(v3, v2) = v1) | ~ % 65.14/9.55 (image_pname_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : ! [v3: $i] : (v1 = v0 | ~ (image_pname_a(v3, v2) = v1) | ~ % 65.14/9.55 (image_pname_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 65.14/9.55 [v3: $i] : (v1 = v0 | ~ (image_a_pname(v3, v2) = v1) | ~ (image_a_pname(v3, % 65.14/9.55 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 65.14/9.55 = v0 | ~ (image_a_a(v3, v2) = v1) | ~ (image_a_a(v3, v2) = v0)) & ! [v0: % 65.14/9.55 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (fun(v3, v2) = % 65.14/9.55 v1) | ~ (fun(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 65.14/9.55 ! [v3: $i] : (v1 = v0 | ~ (cOMBS_350070575l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBS_350070575l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_1035972772l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBS_1035972772l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_568398431l_bool(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBS_568398431l_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBS_a_bool_bool(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBS_a_bool_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_307249310e_bool(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBB_307249310e_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_2140588453a_bool(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBB_2140588453a_bool(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_647938656_pname(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBB_647938656_pname(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : ! [v3: $i] : (v1 = v0 | ~ (cOMBB_bool_bool_a(v3, v2) = v1) | ~ % 65.14/9.55 (cOMBB_bool_bool_a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : (v1 = v0 | ~ (cOMBC_1880041174l_bool(v2) = v1) | ~ % 65.14/9.55 (cOMBC_1880041174l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : (v1 = v0 | ~ (cOMBC_1988546018l_bool(v2) = v1) | ~ % 65.14/9.55 (cOMBC_1988546018l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : (v1 = v0 | ~ (cOMBC_1245412066l_bool(v2) = v1) | ~ % 65.14/9.55 (cOMBC_1245412066l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : (v1 = v0 | ~ (cOMBC_a_a_bool(v2) = v1) | ~ (cOMBC_a_a_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_1355376034l_bool(v2) = v1) | ~ (cOMBC_1355376034l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_1149511130e_bool(v2) = v1) | ~ (cOMBC_1149511130e_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_226598744l_bool(v2) = v1) | ~ (cOMBC_226598744l_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_1058051404l_bool(v2) = v1) | ~ (cOMBC_1058051404l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (cOMBC_pname_a_bool(v2) % 65.14/9.55 = v1) | ~ (cOMBC_pname_a_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 65.14/9.55 [v2: $i] : (v1 = v0 | ~ (cOMBC_nat_nat_bool(v2) = v1) | ~ % 65.14/9.55 (cOMBC_nat_nat_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 65.14/9.55 (v1 = v0 | ~ (minus_minus_nat(v2) = v1) | ~ (minus_minus_nat(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (collect_nat(v2) = v1) | % 65.14/9.55 ~ (collect_nat(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 65.14/9.55 v0 | ~ (cOMBC_595898202l_bool(v2) = v1) | ~ (cOMBC_595898202l_bool(v2) = % 65.14/9.55 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collec1015864663l_bool(v2) = v1) | ~ (collec1015864663l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_7971162l_bool(v2) = v1) | ~ (cOMBC_7971162l_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collec1613912337l_bool(v2) = v1) | ~ (collec1613912337l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_331553030l_bool(v2) = v1) | ~ (cOMBC_331553030l_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collec707592106l_bool(v2) = v1) | ~ (collec707592106l_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_636888218l_bool(v2) = v1) | ~ (cOMBC_636888218l_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collec1635217238l_bool(v2) = v1) | ~ (collec1635217238l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_336095980l_bool(v2) = v1) | ~ (cOMBC_336095980l_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collec792590109l_bool(v2) = v1) | ~ (collec792590109l_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_1269652216l_bool(v2) = v1) | ~ (cOMBC_1269652216l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collec1874991203l_bool(v2) = v1) | ~ (collec1874991203l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_1732670874l_bool(v2) = v1) | ~ (cOMBC_1732670874l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_1284144636l_bool(v2) = v1) | ~ (cOMBC_1284144636l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (cOMBC_1693257480l_bool(v2) = v1) | ~ (cOMBC_1693257480l_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collect_fun_nat_bool(v2) = v1) | ~ (collect_fun_nat_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) % 65.14/9.55 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collec1974731493e_bool(v2) = v1) | ~ (collec1974731493e_bool(v2) = v0)) & % 65.14/9.55 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (collect_fun_a_bool(v2) % 65.14/9.55 = v1) | ~ (collect_fun_a_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 65.14/9.55 [v2: $i] : (v1 = v0 | ~ (collect_pname(v2) = v1) | ~ (collect_pname(v2) = % 65.14/9.55 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (collect_a(v2) = v1) | ~ (collect_a(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 65.14/9.55 : ! [v2: $i] : (v1 = v0 | ~ (undefi64961550l_bool(v2) = v1) | ~ % 65.14/9.55 (undefi64961550l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 65.14/9.55 (v1 = v0 | ~ (undefi1699038445l_bool(v2) = v1) | ~ % 65.14/9.55 (undefi1699038445l_bool(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 65.14/9.55 : (v1 = v0 | ~ (undefi17486888e_bool(v2) = v1) | ~ (undefi17486888e_bool(v2) % 65.14/9.55 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 65.14/9.55 (undefined_fun_a_bool(v2) = v1) | ~ (undefined_fun_a_bool(v2) = v0)) & ! % 65.14/9.55 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (undefined_pname(v2) = % 65.14/9.55 v1) | ~ (undefined_pname(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 65.14/9.55 $i] : (v1 = v0 | ~ (undefined_a(v2) = v1) | ~ (undefined_a(v2) = v0)) % 65.14/9.55 % 65.14/9.55 Further assumptions not needed in the proof: % 65.14/9.55 -------------------------------------------- % 65.14/9.55 fact_0_assms_I1_J, fact_100_card__insert__if, fact_101_card__insert__if, % 65.14/9.55 fact_104_card__insert__disjoint, fact_105_card__insert__disjoint, % 65.14/9.55 fact_106_card__insert__disjoint, fact_107_card__insert__disjoint, % 65.14/9.55 fact_108_card__insert__disjoint, fact_109_card__insert__disjoint, % 65.14/9.55 fact_10_finite__imageI, fact_110_finite__Collect__conjI, % 65.14/9.55 fact_111_finite__Collect__conjI, fact_112_finite__Collect__conjI, % 65.14/9.55 fact_113_finite__Collect__conjI, fact_114_finite__Collect__conjI, % 65.14/9.55 fact_115_finite__Collect__conjI, fact_116_Suc__diff__le, % 65.14/9.55 fact_117_finite__Collect__le__nat, fact_118_card__Collect__le__nat, % 65.14/9.55 fact_119_Suc__inject, fact_11_finite__imageI, fact_120_nat_Oinject, % 65.14/9.55 fact_121_Suc__n__not__n, fact_122_n__not__Suc__n, fact_123_le__antisym, % 65.14/9.55 fact_124_le__trans, fact_125_eq__imp__le, fact_126_nat__le__linear, % 65.14/9.55 fact_127_le__refl, fact_128_diff__commute, fact_129_finite__Collect__disjI, % 65.14/9.55 fact_12_finite__imageI, fact_130_finite__Collect__disjI, % 65.14/9.55 fact_131_finite__Collect__disjI, fact_132_finite__Collect__disjI, % 65.14/9.55 fact_133_finite__Collect__disjI, fact_134_finite__Collect__disjI, % 65.14/9.55 fact_135_finite__insert, fact_136_finite__insert, fact_137_finite__insert, % 65.14/9.55 fact_138_finite__insert, fact_139_finite__insert, fact_13_finite__imageI, % 65.14/9.55 fact_140_finite__insert, fact_141_finite__subset, fact_142_finite__subset, % 65.14/9.55 fact_143_finite__subset, fact_144_finite__subset, fact_145_finite__subset, % 65.14/9.55 fact_146_finite__subset, fact_147_rev__finite__subset, % 65.14/9.55 fact_148_rev__finite__subset, fact_149_rev__finite__subset, % 65.14/9.55 fact_14_finite__imageI, fact_150_rev__finite__subset, % 65.14/9.55 fact_151_rev__finite__subset, fact_152_rev__finite__subset, fact_153_Suc__leD, % 65.14/9.55 fact_154_le__SucE, fact_155_le__SucI, fact_156_Suc__le__mono, % 65.14/9.55 fact_157_le__Suc__eq, fact_158_not__less__eq__eq, fact_159_Suc__n__not__le__n, % 65.14/9.55 fact_15_finite__imageI, fact_160_Suc__diff__diff, fact_161_diff__Suc__Suc, % 65.14/9.55 fact_162_le__diff__iff, fact_163_Nat_Odiff__diff__eq, fact_164_eq__diff__iff, % 65.14/9.55 fact_165_diff__diff__cancel, fact_166_diff__le__mono, fact_167_diff__le__mono2, % 65.14/9.55 fact_168_diff__le__self, fact_16_finite__imageI, fact_170_finite__subset__image, % 65.14/9.55 fact_171_lift__Suc__mono__le, fact_172_lift__Suc__mono__le, % 65.14/9.55 fact_173_lift__Suc__mono__le, fact_174_lift__Suc__mono__le, % 65.14/9.55 fact_175_pigeonhole__infinite, fact_176_image__eqI, fact_177_equalityI, % 65.14/9.55 fact_178_equalityI, fact_179_equalityI, fact_17_finite__imageI, % 65.14/9.55 fact_180_subsetD, fact_181_subsetD, fact_182_subsetD, fact_183_insertCI, % 65.14/9.55 fact_184_insertCI, fact_185_insertCI, fact_186_insertE, fact_187_insertE, % 65.14/9.55 fact_188_insertE, fact_189_insertI1, fact_18_finite__imageI, fact_190_insertI1, % 65.14/9.55 fact_191_insertI1, fact_192_insert__compr, fact_193_insert__compr, % 65.14/9.55 fact_194_insert__compr, fact_195_insert__compr, fact_196_insert__compr, % 65.14/9.55 fact_197_insert__compr, fact_198_insert__Collect, fact_199_insert__Collect, % 65.14/9.55 fact_19_finite__imageI, fact_1_finite__Collect__subsets, % 65.14/9.55 fact_200_insert__Collect, fact_201_insert__Collect, fact_202_insert__Collect, % 65.14/9.55 fact_203_insert__Collect, fact_204_insert__absorb2, fact_205_insert__absorb2, % 65.14/9.55 fact_206_insert__absorb2, fact_207_insert__commute, fact_208_insert__commute, % 65.14/9.55 fact_209_insert__commute, fact_20_finite__imageI, fact_210_insert__iff, % 65.14/9.55 fact_211_insert__iff, fact_212_insert__iff, fact_213_insert__code, % 65.14/9.55 fact_214_insert__code, fact_215_insert__code, fact_216_insert__ident, % 65.14/9.55 fact_217_insert__ident, fact_218_insert__ident, fact_219_insertI2, % 65.14/9.55 fact_21_finite__imageI, fact_220_insertI2, fact_221_insertI2, % 65.14/9.55 fact_222_insert__absorb, fact_224_insert__absorb, fact_225_subset__refl, % 65.14/9.55 fact_226_subset__refl, fact_227_subset__refl, fact_228_set__eq__subset, % 65.14/9.55 fact_229_set__eq__subset, fact_22_finite__imageI, fact_230_set__eq__subset, % 65.14/9.55 fact_231_equalityD1, fact_232_equalityD1, fact_233_equalityD1, % 65.14/9.55 fact_234_equalityD2, fact_235_equalityD2, fact_236_equalityD2, % 65.14/9.55 fact_237_in__mono, fact_238_in__mono, fact_239_in__mono, fact_23_finite__imageI, % 65.14/9.55 fact_240_set__rev__mp, fact_241_set__rev__mp, fact_242_set__rev__mp, % 65.14/9.55 fact_243_set__mp, fact_244_set__mp, fact_245_set__mp, fact_246_subset__trans, % 65.14/9.55 fact_247_subset__trans, fact_248_subset__trans, fact_249_equalityE, % 65.14/9.55 fact_24_finite__imageI, fact_250_equalityE, fact_251_equalityE, % 65.14/9.55 fact_252_mem__def, fact_253_mem__def, fact_254_mem__def, fact_255_Collect__def, % 65.14/9.55 fact_256_Collect__def, fact_257_Collect__def, fact_258_Collect__def, % 65.14/9.55 fact_259_Collect__def, fact_25_finite__imageI, fact_260_image__iff, % 65.14/9.55 fact_261_imageI, fact_263_insert__compr__raw, fact_264_insert__compr__raw, % 65.14/9.55 fact_265_insert__compr__raw, fact_266_insert__compr__raw, % 65.14/9.55 fact_267_insert__compr__raw, fact_268_insert__compr__raw, % 65.14/9.55 fact_269_subset__insertI, fact_26_finite__imageI, fact_270_subset__insertI, % 65.14/9.55 fact_271_subset__insertI, fact_272_insert__subset, fact_273_insert__subset, % 65.14/9.55 fact_275_subset__insert, fact_276_subset__insert, fact_277_subset__insert, % 65.14/9.55 fact_278_subset__insertI2, fact_279_subset__insertI2, fact_27_finite__imageI, % 65.14/9.55 fact_280_subset__insertI2, fact_281_insert__mono, fact_282_insert__mono, % 65.14/9.55 fact_283_insert__mono, fact_284_image__insert, fact_285_insert__image, % 65.14/9.55 fact_286_subset__image__iff, fact_287_image__mono, fact_288_imageE, % 65.14/9.55 fact_289_subsetI, fact_28_finite__imageI, fact_291_subsetI, % 65.14/9.55 fact_292_zero__induct__lemma, fact_293_Suc__le__D, fact_294_image__subsetI, % 65.14/9.55 fact_295_order__refl, fact_296_order__refl, fact_297_order__refl, % 65.14/9.55 fact_298_order__refl, fact_299_finite__nat__set__iff__bounded__le, % 65.14/9.55 fact_29_finite__imageI, fact_2_finite__Collect__subsets, fact_30_finite__imageI, % 65.14/9.55 fact_31_finite__imageI, fact_32_finite__imageI, fact_33_finite__imageI, % 65.14/9.55 fact_34_finite__imageI, fact_35_finite__imageI, fact_36_finite__imageI, % 65.14/9.55 fact_37_finite__imageI, fact_38_finite__imageI, fact_39_finite__imageI, % 65.14/9.55 fact_3_finite__Collect__subsets, fact_40_finite__imageI, fact_41_finite__imageI, % 65.14/9.55 fact_42_finite__imageI, fact_43_finite__imageI, fact_44_finite__imageI, % 65.14/9.55 fact_45_finite_OinsertI, fact_46_finite_OinsertI, fact_47_finite_OinsertI, % 65.14/9.55 fact_48_finite_OinsertI, fact_49_finite_OinsertI, % 65.14/9.55 fact_4_finite__Collect__subsets, fact_50_finite_OinsertI, % 65.14/9.55 fact_51_finite_OinsertI, fact_52_finite_OinsertI, fact_53_finite_OinsertI, % 65.14/9.55 fact_54_card__image__le, fact_55_card__image__le, fact_56_card__image__le, % 65.14/9.55 fact_57_card__image__le, fact_58_card__image__le, fact_59_card__image__le, % 65.14/9.55 fact_5_finite__Collect__subsets, fact_60_card__image__le, % 65.14/9.55 fact_61_card__image__le, fact_62_card__image__le, fact_63_card__image__le, % 65.14/9.55 fact_64_card__image__le, fact_65_card__image__le, fact_66_card__image__le, % 65.14/9.55 fact_67_card__image__le, fact_68_card__image__le, fact_69_card__image__le, % 65.14/9.55 fact_6_finite__Collect__subsets, fact_70_card__image__le, % 65.14/9.55 fact_71_card__image__le, fact_72_card__image__le, fact_73_card__image__le, % 65.14/9.55 fact_74_card__image__le, fact_75_card__image__le, fact_76_card__image__le, % 65.14/9.55 fact_77_card__image__le, fact_78_card__image__le, fact_79_card__image__le, % 65.14/9.55 fact_7_finite__Collect__subsets, fact_80_card__mono, fact_81_card__mono, % 65.14/9.55 fact_82_card__mono, fact_83_card__mono, fact_84_card__mono, fact_85_card__mono, % 65.14/9.55 fact_86_card__seteq, fact_87_card__seteq, fact_88_card__seteq, % 65.14/9.55 fact_89_card__seteq, fact_8_finite__Collect__subsets, fact_90_card__seteq, % 65.14/9.55 fact_91_card__seteq, fact_92_card__insert__le, fact_93_card__insert__le, % 65.14/9.55 fact_94_card__insert__le, fact_95_card__insert__le, fact_96_card__insert__le, % 65.14/9.55 fact_97_card__insert__le, fact_98_card__insert__if, fact_99_card__insert__if, % 65.14/9.55 fact_9_finite__Collect__subsets, % 65.14/9.55 gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000t__a, % 65.14/9.55 gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Opname, % 65.14/9.55 gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_It__a_Mtc__HOL__Obool, % 65.14/9.55 gsy_c_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Com__Opname_Mtc_, % 65.14/9.55 gsy_c_COMBS_000t__a_000tc__HOL__Obool_000tc__HOL__Obool, % 65.14/9.55 gsy_c_COMBS_000tc__Com__Opname_000tc__HOL__Obool_000tc__HOL__Obool, % 65.14/9.55 gsy_c_COMBS_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool_000tc__HOL__Obo, % 65.14/9.55 gsy_c_COMBS_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__Obool_000t, % 65.14/9.55 gsy_c_Finite__Set_Ofinite_000t__a, gsy_c_Finite__Set_Ofinite_000tc__Com__Opname, % 65.14/9.55 gsy_c_HOL_Oundefined_000t__a, gsy_c_HOL_Oundefined_000tc__Com__Opname, % 65.14/9.55 gsy_c_HOL_Oundefined_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.55 gsy_c_HOL_Oundefined_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 65.14/9.55 gsy_c_HOL_Oundefined_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool, % 65.14/9.55 gsy_c_HOL_Oundefined_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc_, % 65.14/9.55 gsy_c_Set_OCollect_000t__a, gsy_c_Set_OCollect_000tc__Com__Opname, % 65.14/9.55 gsy_c_Set_OCollect_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.55 gsy_c_Set_OCollect_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_Set_Oimage_000t__a_000t__a, gsy_c_Set_Oimage_000t__a_000tc__Com__Opname, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Com__Opname_000t__a, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Com__Opname_000tc__Com__Opname, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Nat__Onat_000t__a, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__Com__Opname, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_Set_Oimage_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_It__a_Mtc__HOL__Obool_J_000t__a, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opname, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000t__a, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__Com__Opnam, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000t__a, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__Com__Opname, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_0, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_0_001, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL_002, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HOL__, % 65.14/9.56 gsy_c_Set_Oimage_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HOL___003, % 65.14/9.56 gsy_c_Set_Oinsert_000t__a, gsy_c_Set_Oinsert_000tc__Com__Opname, % 65.14/9.56 gsy_c_Set_Oinsert_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_Set_Oinsert_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000t__a_000tc__HOL__Obool, % 65.14/9.56 gsy_c_hAPP_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000t__a_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000t__a_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000tc__Com__Opname_000t__a, % 65.14/9.56 gsy_c_hAPP_000tc__Com__Opname_000tc__HOL__Obool, % 65.14/9.56 gsy_c_hAPP_000tc__Com__Opname_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000tc__Com__Opname_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obo, % 65.14/9.56 gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool, % 65.14/9.56 gsy_c_hAPP_000tc__Nat__Onat_000tc__HOL__Obool, % 65.14/9.56 gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000tc__Nat__Onat_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool, % 65.14/9.56 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HOL__Obool_J, % 65.14/9.56 gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__a_Mtc__HOL, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__Obool, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_Itc__Com__Op, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_Itc, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obool, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_000tc__, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J_000tc___004, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL__Oboo, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__HOL__Oboo_005, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HOL__Obool_, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc__, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__HO, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HO, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Oboo, % 65.14/9.56 gsy_c_hAPP_000tc__fun_Itc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_, % 65.14/9.56 gsy_v_G, gsy_v_P, gsy_v_pn, % 65.14/9.56 help_COMBB_1_1_COMBB_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__Com__Opna, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000t__a_U, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Com__Opname_U, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Nat__Onat_U, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_It__a_Mtc__H, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Com__Op, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__fun_Itc__Nat__On, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_006, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_007, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_008, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_009, % 65.14/9.56 help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__fun_Itc__HOL__Obool_Mtc__HOL__Oboo_010, % 65.14/9.56 help_COMBC_1_1_COMBC_000t__a_000t__a_000tc__HOL__Obool_U, % 65.14/9.56 help_COMBC_1_1_COMBC_000t__a_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Oboo, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__Com__Opname_000t__a_000tc__HOL__Obool_U, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__Com__Opname_000tc__HOL__Obool_U, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__Com__Opname_000tc__fun_Itc__Com__Opname_Mtc__HOL__Ob, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__Nat__Onat_000tc__HOL__Obool_U, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__Nat__Onat_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_It__a_Mtc__HO, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__fun_Itc__fun_It__, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__fun_It_012, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc_, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__fun_Itc__011, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_Mtc_, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_Mtc__H, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__H, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_Itc__Com__Opname_Mtc__HOL__Obo, % 65.14/9.56 help_COMBC_1_1_COMBC_000tc__fun_Itc__fun_Itc__fun_Itc__Nat__Onat_Mtc__HOL__Obool, % 65.14/9.56 help_COMBS_1_1_COMBS_000t__a_000tc__HOL__Obool_000tc__HOL__Obool_U, % 65.14/9.56 help_COMBS_1_1_COMBS_000tc__Com__Opname_000tc__HOL__Obool_000tc__HOL__Obool_U, % 65.14/9.56 help_COMBS_1_1_COMBS_000tc__Nat__Onat_000tc__HOL__Obool_000tc__HOL__Obool_U, % 65.14/9.56 help_COMBS_1_1_COMBS_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool_000tc_, % 65.14/9.56 help_COMBS_1_1_COMBS_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_000tc__HOL__O, % 65.14/9.56 help_COMBS_1_1_COMBS_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_000tc__HOL__Obo, % 65.14/9.56 help_fNot_1_1_U, help_fNot_2_1_U, help_fconj_1_1_U, help_fconj_2_1_U, % 65.14/9.56 help_fconj_3_1_U, help_fdisj_1_1_U, help_fdisj_2_1_U, help_fdisj_3_1_U, % 65.14/9.56 help_fequal_1_1_fequal_000t__a_T, help_fequal_1_1_fequal_000tc__Com__Opname_T, % 65.14/9.56 help_fequal_1_1_fequal_000tc__Nat__Onat_T, % 65.14/9.56 help_fequal_1_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T, % 65.14/9.56 help_fequal_1_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T, % 65.14/9.56 help_fequal_1_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 65.14/9.56 help_fequal_2_1_fequal_000t__a_T, help_fequal_2_1_fequal_000tc__Com__Opname_T, % 65.14/9.56 help_fequal_2_1_fequal_000tc__Nat__Onat_T, % 65.14/9.56 help_fequal_2_1_fequal_000tc__fun_It__a_Mtc__HOL__Obool_J_T, % 65.14/9.56 help_fequal_2_1_fequal_000tc__fun_Itc__Com__Opname_Mtc__HOL__Obool_J_T, % 65.14/9.56 help_fequal_2_1_fequal_000tc__fun_Itc__Nat__Onat_Mtc__HOL__Obool_J_T, % 65.14/9.56 help_fimplies_1_1_U, help_fimplies_2_1_U, help_fimplies_3_1_U % 65.14/9.56 % 65.14/9.56 Those formulas are unsatisfiable: % 65.14/9.56 --------------------------------- % 65.14/9.56 % 65.14/9.56 Begin of proof % 65.14/9.56 | % 65.14/9.56 | ALPHA: (gsy_v_U) implies: % 65.14/9.56 | (1) is_fun_pname_bool(u) % 65.14/9.56 | % 65.14/9.56 | ALPHA: (fact_102_card__insert__if) implies: % 65.14/9.56 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 65.14/9.56 | (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 65.14/9.56 | (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ % 65.14/9.56 | $i(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? % 65.14/9.56 | [v8: $i] : ((hAPP_f1664156314l_bool(finite_finite_pname, v1) = v4 & % 65.14/9.56 | $i(v4) & ~ hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 65.14/9.56 | hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 65.14/9.56 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v6 & % 65.14/9.56 | insert_pname(v0, v1) = v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | % 65.14/9.56 | (v8 = v6 & hAPP_nat_nat(suc, v7) = v6 & % 65.14/9.56 | hAPP_f921600141ol_nat(finite_card_pname, v5) = v6 & % 65.14/9.56 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v7 & % 65.14/9.56 | insert_pname(v0, v1) = v5 & $i(v7) & $i(v6) & $i(v5)))))) % 65.14/9.56 | % 65.14/9.56 | ALPHA: (fact_103_card__insert__if) implies: % 65.14/9.56 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 65.14/9.56 | (hAPP_fun_a_bool_bool(v2, v1) = v3) | ~ % 65.14/9.56 | (hAPP_a85458249l_bool(member_a, v0) = v2) | ~ $i(v1) | ~ $i(v0) | % 65.14/9.56 | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 65.14/9.56 | ((hAPP_fun_a_bool_bool(finite_finite_a, v1) = v4 & $i(v4) & ~ % 65.14/9.56 | hBOOL(v4)) | (( ~ hBOOL(v3) | (v7 = v6 & % 65.14/9.56 | hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 & % 65.14/9.56 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v6 & insert_a(v0, % 65.14/9.56 | v1) = v5 & $i(v6) & $i(v5))) & (hBOOL(v3) | (v8 = v6 & % 65.14/9.56 | hAPP_nat_nat(suc, v7) = v6 & % 65.14/9.56 | hAPP_fun_a_bool_nat(finite_card_a, v5) = v6 & % 65.14/9.56 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v7 & insert_a(v0, % 65.14/9.56 | v1) = v5 & $i(v7) & $i(v6) & $i(v5)))))) % 65.14/9.56 | % 65.14/9.56 | ALPHA: (fact_169_finite__surj) implies: % 65.14/9.56 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 65.14/9.56 | ! [v5: $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v0) = % 65.14/9.56 | v3) | ~ (hAPP_fun_a_bool_bool(v3, v4) = v5) | ~ % 65.14/9.56 | (image_pname_a(v1, v2) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 65.14/9.56 | hBOOL(v5) | ? [v6: $i] : ? [v7: $i] : % 65.14/9.56 | ((hAPP_f1664156314l_bool(finite_finite_pname, v2) = v6 & $i(v6) & ~ % 65.14/9.56 | hBOOL(v6)) | (hAPP_fun_a_bool_bool(finite_finite_a, v0) = v7 & % 65.14/9.56 | $i(v7) & hBOOL(v7)))) % 65.14/9.56 | % 65.14/9.56 | ALPHA: (fact_223_insert__absorb) implies: % 65.14/9.57 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 65.14/9.57 | (hAPP_f1664156314l_bool(v2, v1) = v3) | ~ % 65.14/9.57 | (hAPP_p338031245l_bool(member_pname, v0) = v2) | ~ $i(v1) | ~ % 65.14/9.57 | $i(v0) | ~ hBOOL(v3) | ~ is_fun_pname_bool(v1) | insert_pname(v0, % 65.14/9.57 | v1) = v1) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (fact_262_rev__image__eqI) implies: % 65.14/9.57 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 65.14/9.57 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 65.14/9.57 | (hAPP_f1664156314l_bool(v4, v3) = v5) | ~ (hAPP_fun_a_bool_bool(v6, % 65.14/9.57 | v7) = v8) | ~ (hAPP_p338031245l_bool(member_pname, v2) = v4) | % 65.14/9.57 | ~ (hAPP_a85458249l_bool(member_a, v0) = v6) | ~ (image_pname_a(v1, % 65.14/9.57 | v3) = v7) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 65.14/9.57 | hBOOL(v5) | hBOOL(v8) | ? [v9: $i] : ( ~ (v9 = v0) & % 65.14/9.57 | hAPP_pname_a(v1, v2) = v9 & $i(v9))) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (fact_274_insert__subset) implies: % 65.14/9.57 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 65.14/9.57 | ! [v5: $i] : ( ~ (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v3) = % 65.14/9.57 | v4) | ~ (hAPP_fun_a_bool_bool(v4, v2) = v5) | ~ (insert_a(v0, v1) % 65.14/9.57 | = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | hBOOL(v5) | ? [v6: $i] % 65.14/9.57 | : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 65.14/9.57 | ((hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v8 & % 65.14/9.57 | hAPP_fun_a_bool_bool(v8, v2) = v9 & $i(v9) & $i(v8) & ~ % 65.14/9.57 | hBOOL(v9)) | (hAPP_fun_a_bool_bool(v6, v2) = v7 & % 65.14/9.57 | hAPP_a85458249l_bool(member_a, v0) = v6 & $i(v7) & $i(v6) & ~ % 65.14/9.57 | hBOOL(v7)))) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (fact_290_subsetI) implies: % 65.14/9.57 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 65.14/9.57 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2) | ~ % 65.14/9.57 | (hAPP_fun_a_bool_bool(v2, v0) = v3) | ~ $i(v1) | ~ $i(v0) | % 65.14/9.57 | hBOOL(v3) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 65.14/9.57 | (hAPP_fun_a_bool_bool(v5, v1) = v6 & hAPP_fun_a_bool_bool(v5, v0) = % 65.14/9.57 | v7 & hAPP_a85458249l_bool(member_a, v4) = v5 & $i(v7) & $i(v6) & % 65.14/9.57 | $i(v5) & $i(v4) & hBOOL(v6) & is_a(v4) & ~ hBOOL(v7))) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (conj_0) implies: % 65.14/9.57 | (9) ? [v0: $i] : (hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & % 65.14/9.57 | $i(v0) & hBOOL(v0)) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (conj_1) implies: % 65.14/9.57 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 65.14/9.57 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = v0 & % 65.14/9.57 | hAPP_fun_a_bool_bool(v0, v1) = v2 & image_pname_a(mgt_call, u) = v1 % 65.14/9.57 | & $i(v2) & $i(v1) & $i(v0) & hBOOL(v2)) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (conj_2) implies: % 65.14/9.57 | (11) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 65.14/9.57 | (hAPP_nat_nat(suc, na) = v0 & hAPP_fun_a_bool_nat(finite_card_a, v2) = % 65.14/9.57 | v3 & hAPP_n1699378549t_bool(ord_less_eq_nat, v0) = v1 & % 65.14/9.57 | hAPP_nat_bool(v1, v3) = v4 & image_pname_a(mgt_call, u) = v2 & % 65.14/9.57 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & hBOOL(v4)) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (conj_3) implies: % 65.14/9.57 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 65.14/9.57 | (minus_minus_nat(v2) = v3 & hAPP_nat_nat(v3, v4) = v0 & % 65.14/9.57 | hAPP_nat_nat(suc, na) = v4 & hAPP_fun_a_bool_nat(finite_card_a, v1) % 65.14/9.57 | = v2 & hAPP_fun_a_bool_nat(finite_card_a, g) = v0 & % 65.14/9.57 | image_pname_a(mgt_call, u) = v1 & $i(v4) & $i(v3) & $i(v2) & $i(v1) % 65.14/9.57 | & $i(v0)) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (conj_4) implies: % 65.14/9.57 | (13) ? [v0: $i] : ? [v1: $i] : (hAPP_f1664156314l_bool(v0, u) = v1 & % 65.14/9.57 | hAPP_p338031245l_bool(member_pname, pn) = v0 & $i(v1) & $i(v0) & % 65.14/9.57 | hBOOL(v1)) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (conj_5) implies: % 65.14/9.57 | (14) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (hAPP_fun_a_bool_bool(v1, g) % 65.14/9.57 | = v2 & hAPP_pname_a(mgt_call, pn) = v0 & % 65.14/9.57 | hAPP_a85458249l_bool(member_a, v0) = v1 & $i(v2) & $i(v1) & $i(v0) & % 65.14/9.57 | ~ hBOOL(v2)) % 65.14/9.57 | % 65.14/9.57 | ALPHA: (conj_6) implies: % 65.14/9.58 | (15) $i(g) % 65.14/9.58 | (16) $i(u) % 65.14/9.58 | (17) $i(pn) % 65.14/9.58 | (18) $i(mgt_call) % 65.14/9.58 | (19) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 65.14/9.58 | (hAPP_f1631501043l_bool(ord_le1311769555a_bool, v1) = v2 & % 65.14/9.58 | hAPP_fun_a_bool_bool(v2, v3) = v4 & hAPP_pname_a(mgt_call, pn) = v0 % 65.14/9.58 | & insert_a(v0, g) = v1 & image_pname_a(mgt_call, u) = v3 & $i(v4) & % 65.14/9.58 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & ~ hBOOL(v4)) % 65.14/9.58 | % 65.14/9.58 | ALPHA: (function-axioms) implies: % 65.14/9.58 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.58 | (image_pname_a(v3, v2) = v1) | ~ (image_pname_a(v3, v2) = v0)) % 65.14/9.58 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.58 | (insert_pname(v3, v2) = v1) | ~ (insert_pname(v3, v2) = v0)) % 65.14/9.58 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.58 | (hAPP_a85458249l_bool(v3, v2) = v1) | ~ (hAPP_a85458249l_bool(v3, % 65.14/9.58 | v2) = v0)) % 65.14/9.58 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.58 | (hAPP_pname_a(v3, v2) = v1) | ~ (hAPP_pname_a(v3, v2) = v0)) % 65.14/9.58 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.58 | (hAPP_fun_a_bool_bool(v3, v2) = v1) | ~ (hAPP_fun_a_bool_bool(v3, % 65.14/9.58 | v2) = v0)) % 65.14/9.58 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.58 | (hAPP_f1631501043l_bool(v3, v2) = v1) | ~ % 65.14/9.58 | (hAPP_f1631501043l_bool(v3, v2) = v0)) % 65.14/9.58 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 65.14/9.58 | (hAPP_f1664156314l_bool(v3, v2) = v1) | ~ % 65.14/9.58 | (hAPP_f1664156314l_bool(v3, v2) = v0)) % 65.14/9.58 | % 65.56/9.58 | DELTA: instantiating (9) with fresh symbol all_407_0 gives: % 65.56/9.58 | (27) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_407_0 & % 65.56/9.58 | $i(all_407_0) & hBOOL(all_407_0) % 65.56/9.58 | % 65.56/9.58 | ALPHA: (27) implies: % 65.56/9.58 | (28) hBOOL(all_407_0) % 65.56/9.58 | (29) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_407_0 % 65.56/9.58 | % 65.56/9.58 | DELTA: instantiating (13) with fresh symbols all_411_0, all_411_1 gives: % 65.56/9.58 | (30) hAPP_f1664156314l_bool(all_411_1, u) = all_411_0 & % 65.56/9.58 | hAPP_p338031245l_bool(member_pname, pn) = all_411_1 & $i(all_411_0) & % 65.56/9.58 | $i(all_411_1) & hBOOL(all_411_0) % 65.56/9.58 | % 65.56/9.58 | ALPHA: (30) implies: % 65.56/9.58 | (31) hBOOL(all_411_0) % 65.56/9.58 | (32) hAPP_p338031245l_bool(member_pname, pn) = all_411_1 % 65.56/9.58 | (33) hAPP_f1664156314l_bool(all_411_1, u) = all_411_0 % 65.56/9.58 | % 65.56/9.58 | DELTA: instantiating (10) with fresh symbols all_417_0, all_417_1, all_417_2 % 65.56/9.58 | gives: % 65.56/9.58 | (34) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_417_2 & % 65.56/9.58 | hAPP_fun_a_bool_bool(all_417_2, all_417_1) = all_417_0 & % 65.56/9.58 | image_pname_a(mgt_call, u) = all_417_1 & $i(all_417_0) & $i(all_417_1) % 65.56/9.58 | & $i(all_417_2) & hBOOL(all_417_0) % 65.56/9.58 | % 65.56/9.58 | ALPHA: (34) implies: % 65.56/9.58 | (35) hBOOL(all_417_0) % 65.56/9.58 | (36) image_pname_a(mgt_call, u) = all_417_1 % 65.56/9.58 | (37) hAPP_fun_a_bool_bool(all_417_2, all_417_1) = all_417_0 % 65.56/9.58 | (38) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_417_2 % 65.56/9.58 | % 65.56/9.58 | DELTA: instantiating (14) with fresh symbols all_421_0, all_421_1, all_421_2 % 65.56/9.58 | gives: % 65.56/9.58 | (39) hAPP_fun_a_bool_bool(all_421_1, g) = all_421_0 & % 65.56/9.58 | hAPP_pname_a(mgt_call, pn) = all_421_2 & % 65.56/9.58 | hAPP_a85458249l_bool(member_a, all_421_2) = all_421_1 & $i(all_421_0) % 65.56/9.58 | & $i(all_421_1) & $i(all_421_2) & ~ hBOOL(all_421_0) % 65.56/9.58 | % 65.56/9.58 | ALPHA: (39) implies: % 65.56/9.58 | (40) ~ hBOOL(all_421_0) % 65.56/9.58 | (41) hAPP_a85458249l_bool(member_a, all_421_2) = all_421_1 % 65.56/9.58 | (42) hAPP_pname_a(mgt_call, pn) = all_421_2 % 65.56/9.59 | (43) hAPP_fun_a_bool_bool(all_421_1, g) = all_421_0 % 65.56/9.59 | % 65.56/9.59 | DELTA: instantiating (12) with fresh symbols all_431_0, all_431_1, all_431_2, % 65.56/9.59 | all_431_3, all_431_4 gives: % 65.56/9.59 | (44) minus_minus_nat(all_431_2) = all_431_1 & hAPP_nat_nat(all_431_1, % 65.56/9.59 | all_431_0) = all_431_4 & hAPP_nat_nat(suc, na) = all_431_0 & % 65.56/9.59 | hAPP_fun_a_bool_nat(finite_card_a, all_431_3) = all_431_2 & % 65.56/9.59 | hAPP_fun_a_bool_nat(finite_card_a, g) = all_431_4 & % 65.56/9.59 | image_pname_a(mgt_call, u) = all_431_3 & $i(all_431_0) & $i(all_431_1) % 65.56/9.59 | & $i(all_431_2) & $i(all_431_3) & $i(all_431_4) % 65.56/9.59 | % 65.56/9.59 | ALPHA: (44) implies: % 65.56/9.59 | (45) $i(all_431_3) % 65.56/9.59 | (46) image_pname_a(mgt_call, u) = all_431_3 % 65.56/9.59 | % 65.56/9.59 | DELTA: instantiating (19) with fresh symbols all_433_0, all_433_1, all_433_2, % 65.56/9.59 | all_433_3, all_433_4 gives: % 65.56/9.59 | (47) hAPP_f1631501043l_bool(ord_le1311769555a_bool, all_433_3) = all_433_2 % 65.56/9.59 | & hAPP_fun_a_bool_bool(all_433_2, all_433_1) = all_433_0 & % 65.56/9.59 | hAPP_pname_a(mgt_call, pn) = all_433_4 & insert_a(all_433_4, g) = % 65.56/9.59 | all_433_3 & image_pname_a(mgt_call, u) = all_433_1 & $i(all_433_0) & % 65.56/9.59 | $i(all_433_1) & $i(all_433_2) & $i(all_433_3) & $i(all_433_4) & ~ % 65.56/9.59 | hBOOL(all_433_0) % 65.56/9.59 | % 65.56/9.59 | ALPHA: (47) implies: % 65.56/9.59 | (48) ~ hBOOL(all_433_0) % 65.56/9.59 | (49) $i(all_433_4) % 65.56/9.59 | (50) $i(all_433_3) % 65.56/9.59 | (51) image_pname_a(mgt_call, u) = all_433_1 % 65.56/9.59 | (52) insert_a(all_433_4, g) = all_433_3 % 65.56/9.59 | (53) hAPP_pname_a(mgt_call, pn) = all_433_4 % 65.56/9.59 | (54) hAPP_fun_a_bool_bool(all_433_2, all_433_1) = all_433_0 % 65.56/9.59 | (55) hAPP_f1631501043l_bool(ord_le1311769555a_bool, all_433_3) = all_433_2 % 65.56/9.59 | % 65.56/9.59 | DELTA: instantiating (11) with fresh symbols all_435_0, all_435_1, all_435_2, % 65.56/9.59 | all_435_3, all_435_4 gives: % 65.56/9.59 | (56) hAPP_nat_nat(suc, na) = all_435_4 & hAPP_fun_a_bool_nat(finite_card_a, % 65.56/9.59 | all_435_2) = all_435_1 & hAPP_n1699378549t_bool(ord_less_eq_nat, % 65.56/9.59 | all_435_4) = all_435_3 & hAPP_nat_bool(all_435_3, all_435_1) = % 65.56/9.59 | all_435_0 & image_pname_a(mgt_call, u) = all_435_2 & $i(all_435_0) & % 65.56/9.59 | $i(all_435_1) & $i(all_435_2) & $i(all_435_3) & $i(all_435_4) & % 65.56/9.59 | hBOOL(all_435_0) % 65.56/9.59 | % 65.56/9.59 | ALPHA: (56) implies: % 65.56/9.59 | (57) image_pname_a(mgt_call, u) = all_435_2 % 65.56/9.59 | % 65.56/9.59 | GROUND_INST: instantiating (20) with all_433_1, all_435_2, u, mgt_call, % 65.56/9.59 | simplifying with (51), (57) gives: % 65.56/9.59 | (58) all_435_2 = all_433_1 % 65.56/9.59 | % 65.56/9.59 | GROUND_INST: instantiating (20) with all_431_3, all_435_2, u, mgt_call, % 65.56/9.59 | simplifying with (46), (57) gives: % 65.56/9.59 | (59) all_435_2 = all_431_3 % 65.56/9.59 | % 65.56/9.59 | GROUND_INST: instantiating (20) with all_417_1, all_435_2, u, mgt_call, % 65.56/9.59 | simplifying with (36), (57) gives: % 65.56/9.59 | (60) all_435_2 = all_417_1 % 65.56/9.59 | % 65.56/9.59 | GROUND_INST: instantiating (23) with all_421_2, all_433_4, pn, mgt_call, % 65.56/9.59 | simplifying with (42), (53) gives: % 65.56/9.59 | (61) all_433_4 = all_421_2 % 65.56/9.59 | % 65.56/9.59 | COMBINE_EQS: (58), (60) imply: % 65.56/9.59 | (62) all_433_1 = all_417_1 % 65.56/9.59 | % 65.56/9.59 | COMBINE_EQS: (58), (59) imply: % 65.56/9.59 | (63) all_433_1 = all_431_3 % 65.56/9.59 | % 65.56/9.59 | COMBINE_EQS: (62), (63) imply: % 65.56/9.59 | (64) all_431_3 = all_417_1 % 65.56/9.59 | % 65.56/9.59 | SIMP: (64) implies: % 65.56/9.59 | (65) all_431_3 = all_417_1 % 65.56/9.59 | % 65.56/9.59 | REDUCE: (54), (62) imply: % 65.56/9.59 | (66) hAPP_fun_a_bool_bool(all_433_2, all_417_1) = all_433_0 % 65.56/9.59 | % 65.56/9.59 | REDUCE: (52), (61) imply: % 65.56/9.59 | (67) insert_a(all_421_2, g) = all_433_3 % 65.56/9.59 | % 65.56/9.59 | REDUCE: (49), (61) imply: % 65.56/9.59 | (68) $i(all_421_2) % 65.56/9.59 | % 65.56/9.59 | REDUCE: (45), (65) imply: % 65.56/9.59 | (69) $i(all_417_1) % 65.56/9.59 | % 65.56/9.59 | GROUND_INST: instantiating (3) with all_421_2, g, all_421_1, all_421_0, % 65.56/9.59 | simplifying with (15), (41), (43), (68) gives: % 65.56/9.59 | (70) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 65.56/9.59 | ((hAPP_fun_a_bool_bool(finite_finite_a, g) = v0 & $i(v0) & ~ % 65.56/9.59 | hBOOL(v0)) | (( ~ hBOOL(all_421_0) | (v3 = v2 & % 65.56/9.59 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 65.56/9.59 | hAPP_fun_a_bool_nat(finite_card_a, g) = v2 & % 65.56/9.59 | insert_a(all_421_2, g) = v1 & $i(v2) & $i(v1))) & % 65.56/9.59 | (hBOOL(all_421_0) | (v4 = v2 & hAPP_nat_nat(suc, v3) = v2 & % 65.56/9.59 | hAPP_fun_a_bool_nat(finite_card_a, v1) = v2 & % 65.56/9.59 | hAPP_fun_a_bool_nat(finite_card_a, g) = v3 & % 65.56/9.59 | insert_a(all_421_2, g) = v1 & $i(v3) & $i(v2) & $i(v1))))) % 65.56/9.59 | % 65.56/9.60 | GROUND_INST: instantiating (4) with g, mgt_call, u, all_417_2, all_417_1, % 65.56/9.60 | all_417_0, simplifying with (15), (16), (18), (35), (36), (37), % 65.56/9.60 | (38) gives: % 65.56/9.60 | (71) ? [v0: $i] : ? [v1: $i] : % 65.56/9.60 | ((hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & $i(v0) & ~ % 65.56/9.60 | hBOOL(v0)) | (hAPP_fun_a_bool_bool(finite_finite_a, g) = v1 & % 65.56/9.60 | $i(v1) & hBOOL(v1))) % 65.56/9.60 | % 65.56/9.60 | GROUND_INST: instantiating (7) with all_421_2, g, all_417_1, all_433_3, % 65.56/9.60 | all_433_2, all_433_0, simplifying with (15), (48), (55), (66), % 65.56/9.60 | (67), (68), (69) gives: % 65.56/9.60 | (72) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 65.56/9.60 | ((hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = v2 & % 65.56/9.60 | hAPP_fun_a_bool_bool(v2, all_417_1) = v3 & $i(v3) & $i(v2) & ~ % 65.56/9.60 | hBOOL(v3)) | (hAPP_fun_a_bool_bool(v0, all_417_1) = v1 & % 65.56/9.60 | hAPP_a85458249l_bool(member_a, all_421_2) = v0 & $i(v1) & $i(v0) & % 65.56/9.60 | ~ hBOOL(v1))) % 65.56/9.60 | % 65.64/9.60 | GROUND_INST: instantiating (8) with all_417_1, all_433_3, all_433_2, % 65.64/9.60 | all_433_0, simplifying with (48), (50), (55), (66), (69) gives: % 65.64/9.60 | (73) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 65.64/9.60 | (hAPP_fun_a_bool_bool(v1, all_433_3) = v2 & hAPP_fun_a_bool_bool(v1, % 65.64/9.60 | all_417_1) = v3 & hAPP_a85458249l_bool(member_a, v0) = v1 & $i(v3) % 65.64/9.60 | & $i(v2) & $i(v1) & $i(v0) & hBOOL(v2) & is_a(v0) & ~ hBOOL(v3)) % 65.64/9.60 | % 65.64/9.60 | GROUND_INST: instantiating (5) with pn, u, all_411_1, all_411_0, simplifying % 65.64/9.60 | with (1), (16), (17), (31), (32), (33) gives: % 65.64/9.60 | (74) insert_pname(pn, u) = u % 65.64/9.60 | % 65.64/9.60 | GROUND_INST: instantiating (2) with pn, u, all_411_1, all_411_0, simplifying % 65.64/9.60 | with (16), (17), (32), (33) gives: % 65.64/9.60 | (75) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 65.64/9.60 | ((hAPP_f1664156314l_bool(finite_finite_pname, u) = v0 & $i(v0) & ~ % 65.64/9.60 | hBOOL(v0)) | (( ~ hBOOL(all_411_0) | (v3 = v2 & % 65.64/9.60 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v2 & % 65.64/9.60 | hAPP_f921600141ol_nat(finite_card_pname, u) = v2 & % 65.64/9.60 | insert_pname(pn, u) = v1 & $i(v2) & $i(v1))) & % 65.64/9.60 | (hBOOL(all_411_0) | (v4 = v2 & hAPP_nat_nat(suc, v3) = v2 & % 65.64/9.60 | hAPP_f921600141ol_nat(finite_card_pname, v1) = v2 & % 65.64/9.60 | hAPP_f921600141ol_nat(finite_card_pname, u) = v3 & % 65.64/9.60 | insert_pname(pn, u) = v1 & $i(v3) & $i(v2) & $i(v1))))) % 65.64/9.60 | % 65.64/9.60 | DELTA: instantiating (71) with fresh symbols all_550_0, all_550_1 gives: % 65.64/9.60 | (76) (hAPP_f1664156314l_bool(finite_finite_pname, u) = all_550_1 & % 65.64/9.60 | $i(all_550_1) & ~ hBOOL(all_550_1)) | % 65.64/9.60 | (hAPP_fun_a_bool_bool(finite_finite_a, g) = all_550_0 & $i(all_550_0) % 65.64/9.60 | & hBOOL(all_550_0)) % 65.64/9.60 | % 65.64/9.60 | DELTA: instantiating (73) with fresh symbols all_556_0, all_556_1, all_556_2, % 65.64/9.60 | all_556_3 gives: % 65.64/9.60 | (77) hAPP_fun_a_bool_bool(all_556_2, all_433_3) = all_556_1 & % 65.64/9.60 | hAPP_fun_a_bool_bool(all_556_2, all_417_1) = all_556_0 & % 65.64/9.60 | hAPP_a85458249l_bool(member_a, all_556_3) = all_556_2 & $i(all_556_0) % 65.64/9.60 | & $i(all_556_1) & $i(all_556_2) & $i(all_556_3) & hBOOL(all_556_1) & % 65.64/9.60 | is_a(all_556_3) & ~ hBOOL(all_556_0) % 65.64/9.60 | % 65.64/9.60 | ALPHA: (77) implies: % 65.64/9.60 | (78) ~ hBOOL(all_556_0) % 65.64/9.60 | (79) $i(all_556_3) % 65.64/9.60 | (80) hAPP_a85458249l_bool(member_a, all_556_3) = all_556_2 % 65.64/9.60 | (81) hAPP_fun_a_bool_bool(all_556_2, all_417_1) = all_556_0 % 65.64/9.60 | % 65.64/9.60 | DELTA: instantiating (72) with fresh symbols all_558_0, all_558_1, all_558_2, % 65.64/9.60 | all_558_3 gives: % 65.64/9.60 | (82) (hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_558_1 & % 65.64/9.60 | hAPP_fun_a_bool_bool(all_558_1, all_417_1) = all_558_0 & % 65.64/9.60 | $i(all_558_0) & $i(all_558_1) & ~ hBOOL(all_558_0)) | % 65.64/9.60 | (hAPP_fun_a_bool_bool(all_558_3, all_417_1) = all_558_2 & % 65.64/9.60 | hAPP_a85458249l_bool(member_a, all_421_2) = all_558_3 & % 65.64/9.60 | $i(all_558_2) & $i(all_558_3) & ~ hBOOL(all_558_2)) % 65.64/9.60 | % 65.64/9.60 | DELTA: instantiating (70) with fresh symbols all_562_0, all_562_1, all_562_2, % 65.64/9.60 | all_562_3, all_562_4 gives: % 65.64/9.60 | (83) (hAPP_fun_a_bool_bool(finite_finite_a, g) = all_562_4 & $i(all_562_4) % 65.64/9.60 | & ~ hBOOL(all_562_4)) | (( ~ hBOOL(all_421_0) | (all_562_1 = % 65.64/9.60 | all_562_2 & hAPP_fun_a_bool_nat(finite_card_a, all_562_3) = % 65.64/9.60 | all_562_2 & hAPP_fun_a_bool_nat(finite_card_a, g) = all_562_2 & % 65.64/9.60 | insert_a(all_421_2, g) = all_562_3 & $i(all_562_2) & % 65.64/9.60 | $i(all_562_3))) & (hBOOL(all_421_0) | (all_562_0 = all_562_2 & % 65.64/9.60 | hAPP_nat_nat(suc, all_562_1) = all_562_2 & % 65.64/9.60 | hAPP_fun_a_bool_nat(finite_card_a, all_562_3) = all_562_2 & % 65.64/9.60 | hAPP_fun_a_bool_nat(finite_card_a, g) = all_562_1 & % 65.64/9.60 | insert_a(all_421_2, g) = all_562_3 & $i(all_562_1) & % 65.64/9.60 | $i(all_562_2) & $i(all_562_3)))) % 65.64/9.60 | % 65.64/9.60 | DELTA: instantiating (75) with fresh symbols all_563_0, all_563_1, all_563_2, % 65.64/9.60 | all_563_3, all_563_4 gives: % 65.64/9.60 | (84) (hAPP_f1664156314l_bool(finite_finite_pname, u) = all_563_4 & % 65.64/9.60 | $i(all_563_4) & ~ hBOOL(all_563_4)) | (( ~ hBOOL(all_411_0) | % 65.64/9.60 | (all_563_1 = all_563_2 & hAPP_f921600141ol_nat(finite_card_pname, % 65.64/9.60 | all_563_3) = all_563_2 & % 65.64/9.60 | hAPP_f921600141ol_nat(finite_card_pname, u) = all_563_2 & % 65.64/9.60 | insert_pname(pn, u) = all_563_3 & $i(all_563_2) & % 65.64/9.60 | $i(all_563_3))) & (hBOOL(all_411_0) | (all_563_0 = all_563_2 & % 65.64/9.60 | hAPP_nat_nat(suc, all_563_1) = all_563_2 & % 65.64/9.60 | hAPP_f921600141ol_nat(finite_card_pname, all_563_3) = all_563_2 % 65.64/9.60 | & hAPP_f921600141ol_nat(finite_card_pname, u) = all_563_1 & % 65.64/9.60 | insert_pname(pn, u) = all_563_3 & $i(all_563_1) & $i(all_563_2) % 65.64/9.60 | & $i(all_563_3)))) % 65.64/9.60 | % 65.64/9.60 | BETA: splitting (84) gives: % 65.64/9.60 | % 65.64/9.60 | Case 1: % 65.64/9.60 | | % 65.64/9.60 | | (85) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_563_4 & % 65.64/9.60 | | $i(all_563_4) & ~ hBOOL(all_563_4) % 65.64/9.60 | | % 65.64/9.60 | | ALPHA: (85) implies: % 65.64/9.60 | | (86) ~ hBOOL(all_563_4) % 65.64/9.60 | | (87) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_563_4 % 65.64/9.60 | | % 65.64/9.60 | | GROUND_INST: instantiating (26) with all_407_0, all_563_4, u, % 65.64/9.60 | | finite_finite_pname, simplifying with (29), (87) gives: % 65.64/9.61 | | (88) all_563_4 = all_407_0 % 65.64/9.61 | | % 65.64/9.61 | | REDUCE: (86), (88) imply: % 65.64/9.61 | | (89) ~ hBOOL(all_407_0) % 65.64/9.61 | | % 65.64/9.61 | | PRED_UNIFY: (28), (89) imply: % 65.64/9.61 | | (90) $false % 65.64/9.61 | | % 65.64/9.61 | | CLOSE: (90) is inconsistent. % 65.64/9.61 | | % 65.64/9.61 | Case 2: % 65.64/9.61 | | % 65.64/9.61 | | (91) ( ~ hBOOL(all_411_0) | (all_563_1 = all_563_2 & % 65.64/9.61 | | hAPP_f921600141ol_nat(finite_card_pname, all_563_3) = all_563_2 % 65.64/9.61 | | & hAPP_f921600141ol_nat(finite_card_pname, u) = all_563_2 & % 65.64/9.61 | | insert_pname(pn, u) = all_563_3 & $i(all_563_2) & % 65.64/9.61 | | $i(all_563_3))) & (hBOOL(all_411_0) | (all_563_0 = all_563_2 & % 65.64/9.61 | | hAPP_nat_nat(suc, all_563_1) = all_563_2 & % 65.64/9.61 | | hAPP_f921600141ol_nat(finite_card_pname, all_563_3) = all_563_2 % 65.64/9.61 | | & hAPP_f921600141ol_nat(finite_card_pname, u) = all_563_1 & % 65.64/9.61 | | insert_pname(pn, u) = all_563_3 & $i(all_563_1) & $i(all_563_2) % 65.64/9.61 | | & $i(all_563_3))) % 65.64/9.61 | | % 65.64/9.61 | | ALPHA: (91) implies: % 65.64/9.61 | | (92) ~ hBOOL(all_411_0) | (all_563_1 = all_563_2 & % 65.64/9.61 | | hAPP_f921600141ol_nat(finite_card_pname, all_563_3) = all_563_2 & % 65.64/9.61 | | hAPP_f921600141ol_nat(finite_card_pname, u) = all_563_2 & % 65.64/9.61 | | insert_pname(pn, u) = all_563_3 & $i(all_563_2) & $i(all_563_3)) % 65.64/9.61 | | % 65.64/9.61 | | BETA: splitting (92) gives: % 65.64/9.61 | | % 65.64/9.61 | | Case 1: % 65.64/9.61 | | | % 65.64/9.61 | | | (93) ~ hBOOL(all_411_0) % 65.64/9.61 | | | % 65.64/9.61 | | | PRED_UNIFY: (31), (93) imply: % 65.64/9.61 | | | (94) $false % 65.64/9.61 | | | % 65.64/9.61 | | | CLOSE: (94) is inconsistent. % 65.64/9.61 | | | % 65.64/9.61 | | Case 2: % 65.64/9.61 | | | % 65.64/9.61 | | | (95) all_563_1 = all_563_2 & hAPP_f921600141ol_nat(finite_card_pname, % 65.64/9.61 | | | all_563_3) = all_563_2 & % 65.64/9.61 | | | hAPP_f921600141ol_nat(finite_card_pname, u) = all_563_2 & % 65.64/9.61 | | | insert_pname(pn, u) = all_563_3 & $i(all_563_2) & $i(all_563_3) % 65.64/9.61 | | | % 65.64/9.61 | | | ALPHA: (95) implies: % 65.64/9.61 | | | (96) $i(all_563_3) % 65.64/9.61 | | | (97) insert_pname(pn, u) = all_563_3 % 65.64/9.61 | | | % 65.64/9.61 | | | BETA: splitting (76) gives: % 65.64/9.61 | | | % 65.64/9.61 | | | Case 1: % 65.64/9.61 | | | | % 65.64/9.61 | | | | (98) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_550_1 & % 65.64/9.61 | | | | $i(all_550_1) & ~ hBOOL(all_550_1) % 65.64/9.61 | | | | % 65.64/9.61 | | | | ALPHA: (98) implies: % 65.64/9.61 | | | | (99) ~ hBOOL(all_550_1) % 65.64/9.61 | | | | (100) hAPP_f1664156314l_bool(finite_finite_pname, u) = all_550_1 % 65.64/9.61 | | | | % 65.64/9.61 | | | | GROUND_INST: instantiating (26) with all_407_0, all_550_1, u, % 65.64/9.61 | | | | finite_finite_pname, simplifying with (29), (100) gives: % 65.64/9.61 | | | | (101) all_550_1 = all_407_0 % 65.64/9.61 | | | | % 65.64/9.61 | | | | REDUCE: (99), (101) imply: % 65.64/9.61 | | | | (102) ~ hBOOL(all_407_0) % 65.64/9.61 | | | | % 65.64/9.61 | | | | PRED_UNIFY: (28), (102) imply: % 65.64/9.61 | | | | (103) $false % 65.64/9.61 | | | | % 65.64/9.61 | | | | CLOSE: (103) is inconsistent. % 65.64/9.61 | | | | % 65.64/9.61 | | | Case 2: % 65.64/9.61 | | | | % 65.64/9.61 | | | | (104) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_550_0 & % 65.64/9.61 | | | | $i(all_550_0) & hBOOL(all_550_0) % 65.64/9.61 | | | | % 65.64/9.61 | | | | ALPHA: (104) implies: % 65.64/9.61 | | | | (105) hBOOL(all_550_0) % 65.64/9.61 | | | | (106) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_550_0 % 65.64/9.61 | | | | % 65.64/9.61 | | | | BETA: splitting (82) gives: % 65.64/9.61 | | | | % 65.64/9.61 | | | | Case 1: % 65.64/9.61 | | | | | % 65.64/9.61 | | | | | (107) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_558_1 % 65.64/9.61 | | | | | & hAPP_fun_a_bool_bool(all_558_1, all_417_1) = all_558_0 & % 65.64/9.61 | | | | | $i(all_558_0) & $i(all_558_1) & ~ hBOOL(all_558_0) % 65.64/9.61 | | | | | % 65.64/9.61 | | | | | ALPHA: (107) implies: % 65.64/9.61 | | | | | (108) ~ hBOOL(all_558_0) % 65.64/9.61 | | | | | (109) hAPP_fun_a_bool_bool(all_558_1, all_417_1) = all_558_0 % 65.64/9.61 | | | | | (110) hAPP_f1631501043l_bool(ord_le1311769555a_bool, g) = all_558_1 % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | GROUND_INST: instantiating (25) with all_417_2, all_558_1, g, % 65.71/9.61 | | | | | ord_le1311769555a_bool, simplifying with (38), (110) % 65.71/9.61 | | | | | gives: % 65.71/9.61 | | | | | (111) all_558_1 = all_417_2 % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | REDUCE: (109), (111) imply: % 65.71/9.61 | | | | | (112) hAPP_fun_a_bool_bool(all_417_2, all_417_1) = all_558_0 % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | GROUND_INST: instantiating (24) with all_417_0, all_558_0, all_417_1, % 65.71/9.61 | | | | | all_417_2, simplifying with (37), (112) gives: % 65.71/9.61 | | | | | (113) all_558_0 = all_417_0 % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | REDUCE: (108), (113) imply: % 65.71/9.61 | | | | | (114) ~ hBOOL(all_417_0) % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | PRED_UNIFY: (35), (114) imply: % 65.71/9.61 | | | | | (115) $false % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | CLOSE: (115) is inconsistent. % 65.71/9.61 | | | | | % 65.71/9.61 | | | | Case 2: % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | (116) hAPP_fun_a_bool_bool(all_558_3, all_417_1) = all_558_2 & % 65.71/9.61 | | | | | hAPP_a85458249l_bool(member_a, all_421_2) = all_558_3 & % 65.71/9.61 | | | | | $i(all_558_2) & $i(all_558_3) & ~ hBOOL(all_558_2) % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | ALPHA: (116) implies: % 65.71/9.61 | | | | | (117) ~ hBOOL(all_558_2) % 65.71/9.61 | | | | | (118) hAPP_a85458249l_bool(member_a, all_421_2) = all_558_3 % 65.71/9.61 | | | | | (119) hAPP_fun_a_bool_bool(all_558_3, all_417_1) = all_558_2 % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | BETA: splitting (83) gives: % 65.71/9.61 | | | | | % 65.71/9.61 | | | | | Case 1: % 65.71/9.61 | | | | | | % 65.71/9.61 | | | | | | (120) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_562_4 & % 65.71/9.61 | | | | | | $i(all_562_4) & ~ hBOOL(all_562_4) % 65.71/9.61 | | | | | | % 65.71/9.61 | | | | | | ALPHA: (120) implies: % 65.71/9.61 | | | | | | (121) ~ hBOOL(all_562_4) % 65.71/9.61 | | | | | | (122) hAPP_fun_a_bool_bool(finite_finite_a, g) = all_562_4 % 65.71/9.61 | | | | | | % 65.71/9.61 | | | | | | GROUND_INST: instantiating (24) with all_550_0, all_562_4, g, % 65.71/9.61 | | | | | | finite_finite_a, simplifying with (106), (122) gives: % 65.71/9.61 | | | | | | (123) all_562_4 = all_550_0 % 65.71/9.61 | | | | | | % 65.71/9.61 | | | | | | REDUCE: (121), (123) imply: % 65.71/9.61 | | | | | | (124) ~ hBOOL(all_550_0) % 65.71/9.61 | | | | | | % 65.71/9.61 | | | | | | PRED_UNIFY: (105), (124) imply: % 65.71/9.61 | | | | | | (125) $false % 65.71/9.61 | | | | | | % 65.71/9.61 | | | | | | CLOSE: (125) is inconsistent. % 65.71/9.61 | | | | | | % 65.71/9.61 | | | | | Case 2: % 65.71/9.61 | | | | | | % 65.71/9.62 | | | | | | (126) ( ~ hBOOL(all_421_0) | (all_562_1 = all_562_2 & % 65.71/9.62 | | | | | | hAPP_fun_a_bool_nat(finite_card_a, all_562_3) = % 65.71/9.62 | | | | | | all_562_2 & hAPP_fun_a_bool_nat(finite_card_a, g) = % 65.71/9.62 | | | | | | all_562_2 & insert_a(all_421_2, g) = all_562_3 & % 65.71/9.62 | | | | | | $i(all_562_2) & $i(all_562_3))) & (hBOOL(all_421_0) | % 65.71/9.62 | | | | | | (all_562_0 = all_562_2 & hAPP_nat_nat(suc, all_562_1) = % 65.71/9.62 | | | | | | all_562_2 & hAPP_fun_a_bool_nat(finite_card_a, % 65.71/9.62 | | | | | | all_562_3) = all_562_2 & % 65.71/9.62 | | | | | | hAPP_fun_a_bool_nat(finite_card_a, g) = all_562_1 & % 65.71/9.62 | | | | | | insert_a(all_421_2, g) = all_562_3 & $i(all_562_1) & % 65.71/9.62 | | | | | | $i(all_562_2) & $i(all_562_3))) % 65.71/9.62 | | | | | | % 65.71/9.62 | | | | | | ALPHA: (126) implies: % 65.71/9.62 | | | | | | (127) hBOOL(all_421_0) | (all_562_0 = all_562_2 & % 65.71/9.62 | | | | | | hAPP_nat_nat(suc, all_562_1) = all_562_2 & % 65.71/9.62 | | | | | | hAPP_fun_a_bool_nat(finite_card_a, all_562_3) = all_562_2 % 65.71/9.62 | | | | | | & hAPP_fun_a_bool_nat(finite_card_a, g) = all_562_1 & % 65.71/9.62 | | | | | | insert_a(all_421_2, g) = all_562_3 & $i(all_562_1) & % 65.71/9.62 | | | | | | $i(all_562_2) & $i(all_562_3)) % 65.71/9.62 | | | | | | % 65.71/9.62 | | | | | | BETA: splitting (127) gives: % 65.71/9.62 | | | | | | % 65.71/9.62 | | | | | | Case 1: % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | (128) hBOOL(all_421_0) % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | PRED_UNIFY: (40), (128) imply: % 65.71/9.62 | | | | | | | (129) $false % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | CLOSE: (129) is inconsistent. % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | Case 2: % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | GROUND_INST: instantiating (21) with u, all_563_3, u, pn, % 65.71/9.62 | | | | | | | simplifying with (74), (97) gives: % 65.71/9.62 | | | | | | | (130) all_563_3 = u % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | GROUND_INST: instantiating (22) with all_421_1, all_558_3, % 65.71/9.62 | | | | | | | all_421_2, member_a, simplifying with (41), (118) % 65.71/9.62 | | | | | | | gives: % 65.71/9.62 | | | | | | | (131) all_558_3 = all_421_1 % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | REDUCE: (119), (131) imply: % 65.71/9.62 | | | | | | | (132) hAPP_fun_a_bool_bool(all_421_1, all_417_1) = all_558_2 % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | GROUND_INST: instantiating (6) with all_421_2, mgt_call, pn, u, % 65.71/9.62 | | | | | | | all_411_1, all_411_0, all_421_1, all_417_1, % 65.71/9.62 | | | | | | | all_558_2, simplifying with (16), (17), (18), (31), % 65.71/9.62 | | | | | | | (32), (33), (36), (41), (68), (117), (132) gives: % 65.71/9.62 | | | | | | | (133) ? [v0: any] : ( ~ (v0 = all_421_2) & % 65.71/9.62 | | | | | | | hAPP_pname_a(mgt_call, pn) = v0 & $i(v0)) % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | GROUND_INST: instantiating (6) with all_556_3, mgt_call, pn, u, % 65.71/9.62 | | | | | | | all_411_1, all_411_0, all_556_2, all_417_1, % 65.71/9.62 | | | | | | | all_556_0, simplifying with (16), (17), (18), (31), % 65.71/9.62 | | | | | | | (32), (33), (36), (78), (79), (80), (81) gives: % 65.71/9.62 | | | | | | | (134) ? [v0: any] : ( ~ (v0 = all_556_3) & % 65.71/9.62 | | | | | | | hAPP_pname_a(mgt_call, pn) = v0 & $i(v0)) % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | DELTA: instantiating (133) with fresh symbol all_620_0 gives: % 65.71/9.62 | | | | | | | (135) ~ (all_620_0 = all_421_2) & hAPP_pname_a(mgt_call, pn) = % 65.71/9.62 | | | | | | | all_620_0 & $i(all_620_0) % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | ALPHA: (135) implies: % 65.71/9.62 | | | | | | | (136) ~ (all_620_0 = all_421_2) % 65.71/9.62 | | | | | | | (137) hAPP_pname_a(mgt_call, pn) = all_620_0 % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | DELTA: instantiating (134) with fresh symbol all_624_0 gives: % 65.71/9.62 | | | | | | | (138) ~ (all_624_0 = all_556_3) & hAPP_pname_a(mgt_call, pn) = % 65.71/9.62 | | | | | | | all_624_0 & $i(all_624_0) % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | ALPHA: (138) implies: % 65.71/9.62 | | | | | | | (139) hAPP_pname_a(mgt_call, pn) = all_624_0 % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | GROUND_INST: instantiating (23) with all_421_2, all_624_0, pn, % 65.71/9.62 | | | | | | | mgt_call, simplifying with (42), (139) gives: % 65.71/9.62 | | | | | | | (140) all_624_0 = all_421_2 % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | GROUND_INST: instantiating (23) with all_620_0, all_624_0, pn, % 65.71/9.62 | | | | | | | mgt_call, simplifying with (137), (139) gives: % 65.71/9.62 | | | | | | | (141) all_624_0 = all_620_0 % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | COMBINE_EQS: (140), (141) imply: % 65.71/9.62 | | | | | | | (142) all_620_0 = all_421_2 % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | REDUCE: (136), (142) imply: % 65.71/9.62 | | | | | | | (143) $false % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | | CLOSE: (143) is inconsistent. % 65.71/9.62 | | | | | | | % 65.71/9.62 | | | | | | End of split % 65.71/9.62 | | | | | | % 65.71/9.62 | | | | | End of split % 65.71/9.62 | | | | | % 65.71/9.62 | | | | End of split % 65.71/9.62 | | | | % 65.71/9.62 | | | End of split % 65.71/9.62 | | | % 65.71/9.62 | | End of split % 65.71/9.62 | | % 65.71/9.62 | End of split % 65.71/9.62 | % 65.71/9.62 End of proof % 65.71/9.62 % SZS output end Proof for theBenchmark % 65.71/9.62 % 65.71/9.62 9001ms %------------------------------------------------------------------------------