%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n032.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 : Thu Aug 31 04:11:38 EDT 2023 % Result : Theorem 65.88s 9.76s % Output : Proof 104.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.00/0.09 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.28 % Computer : n032.cluster.edu % 0.10/0.28 % Model : x86_64 x86_64 % 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.28 % Memory : 8042.1875MB % 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.28 % CPULimit : 300 % 0.10/0.28 % WCLimit : 300 % 0.10/0.28 % DateTime : Sun Aug 27 12:54:45 EDT 2023 % 0.10/0.28 % CPUTime : % 0.12/0.58 ________ _____ % 0.12/0.58 ___ __ \_________(_)________________________________ % 0.12/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.12/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.12/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.12/0.58 % 0.12/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.12/0.58 (2023-06-19) % 0.12/0.58 % 0.12/0.58 (c) Philipp Rümmer, 2009-2023 % 0.12/0.58 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.12/0.58 Amanda Stjerna. % 0.12/0.58 Free software under BSD-3-Clause. % 0.12/0.58 % 0.12/0.58 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.12/0.58 % 0.12/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.12/0.60 Running up to 7 provers in parallel. % 0.12/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.12/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.12/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.12/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.12/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.12/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.12/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 23.92/4.15 Prover 1: Preprocessing ... % 24.47/4.24 Prover 2: Preprocessing ... % 24.47/4.24 Prover 5: Preprocessing ... % 26.10/4.51 Prover 6: Preprocessing ... % 26.10/4.58 Prover 4: Preprocessing ... % 26.10/4.61 Prover 3: Preprocessing ... % 26.10/4.69 Prover 0: Preprocessing ... % 56.39/8.49 Prover 1: Warning: ignoring some quantifiers % 57.77/8.71 Prover 3: Warning: ignoring some quantifiers % 58.74/8.88 Prover 1: Constructing countermodel ... % 58.74/8.88 Prover 3: Constructing countermodel ... % 61.38/9.19 Prover 6: Proving ... % 65.88/9.75 Prover 3: proved (9136ms) % 65.88/9.75 % 65.88/9.76 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.88/9.76 % 65.88/9.77 Prover 6: stopped % 65.88/9.77 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 65.88/9.79 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 66.68/9.85 Prover 4: Warning: ignoring some quantifiers % 69.04/10.23 Prover 4: Constructing countermodel ... % 71.23/10.48 Prover 5: Proving ... % 71.23/10.48 Prover 5: stopped % 71.23/10.50 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 71.94/10.60 Prover 0: Proving ... % 72.41/10.60 Prover 0: stopped % 72.41/10.62 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 72.82/10.67 Prover 8: Preprocessing ... % 74.66/10.92 Prover 7: Preprocessing ... % 79.77/11.59 Prover 10: Preprocessing ... % 80.56/11.76 Prover 11: Preprocessing ... % 87.38/12.59 Prover 2: Proving ... % 87.38/12.59 Prover 2: stopped % 87.38/12.60 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 89.22/12.85 Prover 8: Warning: ignoring some quantifiers % 91.07/13.11 Prover 8: Constructing countermodel ... % 94.00/13.43 Prover 7: Warning: ignoring some quantifiers % 94.00/13.44 Prover 13: Preprocessing ... % 96.58/13.76 Prover 7: Constructing countermodel ... % 97.17/13.86 Prover 10: Warning: ignoring some quantifiers % 99.49/14.17 Prover 10: Constructing countermodel ... % 99.49/14.17 Prover 1: Found proof (size 54) % 99.49/14.17 Prover 1: proved (13561ms) % 99.49/14.17 Prover 8: stopped % 99.49/14.18 Prover 4: stopped % 99.49/14.18 Prover 7: stopped % 99.49/14.18 Prover 13: stopped % 99.49/14.19 Prover 10: stopped % 101.43/14.80 Prover 11: Warning: ignoring some quantifiers % 103.07/15.00 Prover 11: Constructing countermodel ... % 103.23/15.01 Prover 11: stopped % 103.23/15.01 % 103.23/15.02 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 103.23/15.02 % 103.23/15.03 % SZS output start Proof for theBenchmark % 103.38/15.08 Assumptions after simplification: % 103.38/15.08 --------------------------------- % 103.38/15.08 % 103.38/15.08 (axiom221) % 103.38/15.10 fun_app$c(isZFfun$, f$) = 0 & ZF$(f$) & ZF_bool_fun$(isZFfun$) % 103.38/15.10 % 103.38/15.10 (axiom222) % 103.38/15.10 ZF$(f$) & ZF_ZF_fun$(domain$) & ZF_ZF_fun$(zFfunDom$) & ZF_ZF_fun$(snd$) & ? % 103.38/15.10 [v0: ZF$] : ? [v1: ZF$] : (fun_app$(domain$, v1) = v0 & fun_app$(zFfunDom$, % 103.38/15.10 f$) = v0 & fun_app$(snd$, f$) = v1 & ZF$(v1) & ZF$(v0)) % 103.38/15.10 % 103.38/15.10 (axiom223) % 103.38/15.10 ZF$(f$) & ZF_bool_fun$(isFun$) & ZF_ZF_fun$(snd$) & ? [v0: ZF$] : % 103.38/15.10 (fun_app$c(isFun$, v0) = 0 & fun_app$(snd$, f$) = v0 & ZF$(v0)) % 103.38/15.10 % 103.38/15.10 (axiom226) % 103.38/15.10 ZF$(f$) & ZF_ZF_fun$(fst$) & ZF_ZF_fun$(snd$) & ZF_ZF_ZF_fun_fun$(opair$) & ? % 103.38/15.10 [v0: ZF$] : ? [v1: ZF$] : ? [v2: ZF_ZF_fun$] : ? [v3: ZF$] : ? [v4: ZF$] : % 103.38/15.10 ? [v5: ZF_ZF_fun$] : ? [v6: ZF$] : (fun_app$t(opair$, v4) = v5 & % 103.38/15.10 fun_app$t(opair$, v1) = v2 & fun_app$(v5, v6) = f$ & fun_app$(v2, v3) = v4 & % 103.38/15.10 fun_app$(fst$, v0) = v1 & fun_app$(fst$, f$) = v0 & fun_app$(snd$, v0) = v3 % 103.38/15.10 & fun_app$(snd$, f$) = v6 & ZF$(v6) & ZF$(v4) & ZF$(v3) & ZF$(v1) & ZF$(v0) % 103.38/15.10 & ZF_ZF_fun$(v5) & ZF_ZF_fun$(v2)) % 103.38/15.10 % 103.38/15.10 (axiom228) % 103.38/15.11 ZF$(f$) & ZF_ZF_fun$(zFfunDom$) & ZF_ZF_fun$(snd$) & ZF_ZF_fun$(zFfunCod$) & % 103.38/15.11 ZF_ZF_ZF_fun_fun$(opair$) & ? [v0: ZF$] : ? [v1: ZF_ZF_fun$] : ? [v2: ZF$] % 103.38/15.11 : ? [v3: ZF$] : ? [v4: ZF_ZF_fun$] : ? [v5: ZF$] : (fun_app$t(opair$, v3) = % 103.38/15.11 v4 & fun_app$t(opair$, v0) = v1 & fun_app$(v4, v5) = f$ & fun_app$(v1, v2) = % 103.38/15.11 v3 & fun_app$(zFfunDom$, f$) = v0 & fun_app$(snd$, f$) = v5 & % 103.38/15.11 fun_app$(zFfunCod$, f$) = v2 & ZF$(v5) & ZF$(v3) & ZF$(v2) & ZF$(v0) & % 103.38/15.11 ZF_ZF_fun$(v4) & ZF_ZF_fun$(v1)) % 103.38/15.11 % 103.38/15.11 (axiom245) % 103.38/15.12 ZF_ZF_bool_fun_fun$(subset$) & ZF_bool_fun$(isZFfun$) & ZF_bool_fun$(isFun$) & % 103.38/15.12 ZF_bool_fun$(isOpair$) & ZF_ZF_fun$(domain$) & ZF_ZF_fun$(range$) & % 103.38/15.12 ZF_ZF_fun$(zFfunDom$) & ZF_ZF_fun$(fst$) & ZF_ZF_fun$(snd$) & % 103.38/15.12 ZF_ZF_fun$(zFfunCod$) & ZF_ZF_ZF_fun_fun$(cartProd$) & ! [v0: ZF$] : ! [v1: % 103.38/15.12 ZF$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF$] : ! [v4: ZF_ZF_fun$] : ! [v5: % 103.38/15.12 ZF$] : ! [v6: ZF$] : ! [v7: any] : ( ~ (fun_app$t(cartProd$, v3) = v4) | % 103.38/15.12 ~ (fun_app$h(subset$, v1) = v2) | ~ (fun_app$c(v2, v6) = v7) | ~ % 103.38/15.12 (fun_app$(v4, v5) = v6) | ~ (fun_app$(domain$, v1) = v3) | ~ % 103.38/15.12 (fun_app$(range$, v1) = v5) | ~ (fun_app$(snd$, v0) = v1) | ~ ZF$(v0) | ? % 103.38/15.12 [v8: any] : ? [v9: any] : ? [v10: ZF$] : ? [v11: any] : ? [v12: any] : % 103.38/15.12 ? [v13: ZF$] : ? [v14: ZF_bool_fun$] : ? [v15: ZF$] : ? [v16: any] : % 103.38/15.12 (fun_app$h(subset$, v5) = v14 & fun_app$c(v14, v15) = v16 & % 103.38/15.12 fun_app$c(isZFfun$, v0) = v8 & fun_app$c(isFun$, v1) = v12 & % 103.38/15.12 fun_app$c(isOpair$, v10) = v11 & fun_app$c(isOpair$, v0) = v9 & % 103.38/15.12 fun_app$(zFfunDom$, v0) = v13 & fun_app$(fst$, v0) = v10 & % 103.38/15.12 fun_app$(zFfunCod$, v0) = v15 & ZF$(v15) & ZF$(v13) & ZF$(v10) & % 103.38/15.12 ZF_bool_fun$(v14) & ( ~ (v8 = 0) | (v16 = 0 & v13 = v3 & v12 = 0 & v11 = 0 % 103.38/15.12 & v9 = 0 & v7 = 0)))) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: % 103.38/15.12 ZF_bool_fun$] : ! [v3: ZF$] : ! [v4: ZF_ZF_fun$] : ! [v5: ZF$] : ! [v6: % 103.38/15.12 ZF$] : ( ~ (fun_app$t(cartProd$, v3) = v4) | ~ (fun_app$h(subset$, v1) = % 103.38/15.12 v2) | ~ (fun_app$c(v2, v6) = 0) | ~ (fun_app$(v4, v5) = v6) | ~ % 103.38/15.12 (fun_app$(domain$, v1) = v3) | ~ (fun_app$(range$, v1) = v5) | ~ % 103.38/15.12 (fun_app$(snd$, v0) = v1) | ~ ZF$(v0) | ? [v7: any] : ? [v8: ZF$] : ? % 103.38/15.12 [v9: any] : ? [v10: any] : ? [v11: ZF$] : ? [v12: ZF_bool_fun$] : ? % 103.38/15.12 [v13: ZF$] : ? [v14: any] : ? [v15: any] : (fun_app$h(subset$, v5) = v12 & % 103.38/15.12 fun_app$c(v12, v13) = v14 & fun_app$c(isZFfun$, v0) = v15 & % 103.38/15.12 fun_app$c(isFun$, v1) = v10 & fun_app$c(isOpair$, v8) = v9 & % 103.38/15.12 fun_app$c(isOpair$, v0) = v7 & fun_app$(zFfunDom$, v0) = v11 & % 103.38/15.12 fun_app$(fst$, v0) = v8 & fun_app$(zFfunCod$, v0) = v13 & ZF$(v13) & % 103.38/15.12 ZF$(v11) & ZF$(v8) & ZF_bool_fun$(v12) & ( ~ (v14 = 0) | ~ (v11 = v3) | % 103.38/15.12 ~ (v10 = 0) | ~ (v9 = 0) | ~ (v7 = 0) | v15 = 0))) % 103.38/15.12 % 103.38/15.12 (axiom252) % 103.38/15.12 ZF$(f$) & ZF_ZF_fun$(snd$) & ZF_ZF_ZF_fun_fun$(zFfunApp$) & % 103.38/15.12 ZF_ZF_ZF_fun_fun$(app$) & ? [v0: ZF_ZF_fun$] : ? [v1: ZF$] : ? [v2: % 103.38/15.12 ZF_ZF_fun$] : (fun_app$t(zFfunApp$, f$) = v0 & fun_app$t(app$, v1) = v2 & % 103.38/15.12 fun_app$(snd$, f$) = v1 & ZF$(v1) & ZF_ZF_fun$(v2) & ZF_ZF_fun$(v0) & ! % 103.38/15.12 [v3: ZF$] : ! [v4: ZF$] : ( ~ (fun_app$(v2, v3) = v4) | ~ ZF$(v3) | % 103.38/15.12 (fun_app$(v0, v3) = v4 & ZF$(v4)))) % 103.38/15.12 % 103.38/15.12 (conjecture220) % 103.38/15.12 ZF_ZF_bool_fun_fun$(subset$) & ZF$(f$) & ZF_ZF_fun$(domain$) & % 103.38/15.12 ZF_ZF_fun$(range$) & ZF_ZF_fun$(snd$) & ZF_ZF_ZF_fun_fun$(cartProd$) & ? [v0: % 103.38/15.12 ZF$] : ? [v1: ZF_bool_fun$] : ? [v2: ZF$] : ? [v3: ZF_ZF_fun$] : ? [v4: % 103.38/15.12 ZF$] : ? [v5: ZF$] : ? [v6: int] : ( ~ (v6 = 0) & fun_app$t(cartProd$, v2) % 103.38/15.12 = v3 & fun_app$h(subset$, v0) = v1 & fun_app$c(v1, v5) = v6 & fun_app$(v3, % 103.38/15.12 v4) = v5 & fun_app$(domain$, v0) = v2 & fun_app$(range$, v0) = v4 & % 103.38/15.12 fun_app$(snd$, f$) = v0 & ZF$(v5) & ZF$(v4) & ZF$(v2) & ZF$(v0) & % 103.38/15.12 ZF_bool_fun$(v1) & ZF_ZF_fun$(v3)) % 103.38/15.12 % 103.38/15.12 (function-axioms) % 104.07/15.23 ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: ZF_ZF_unit_Category_ext$] : ! % 104.07/15.23 [v2: Unit$] : ! [v3: ZF_ZF_ZF_fun_fun$] : ! [v4: ZF_ZF_fun$] : ! [v5: % 104.07/15.23 ZF_ZF_fun$] : ! [v6: ZF_ZF_fun$] : ! [v7: ZF_set$] : ! [v8: ZF_set$] : % 104.07/15.23 (v1 = v0 | ~ (category_ext$(v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 104.07/15.23 (category_ext$(v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: tlbool] : ! % 104.07/15.23 [v1: tlbool] : ! [v2: ZF$] : ! [v3: ZF$] : ! [v4: ZF_ZF_bool_fun_fun$] : % 104.07/15.23 (v1 = v0 | ~ (def_8(v4, v3, v2) = v1) | ~ (def_8(v4, v3, v2) = v0)) & ! % 104.07/15.23 [v0: tlbool] : ! [v1: tlbool] : ! [v2: ZF_ZF_bool_fun_fun$] : ! [v3: ZF$] : % 104.07/15.23 ! [v4: ZF$] : (v1 = v0 | ~ (def_6(v4, v3, v2) = v1) | ~ (def_6(v4, v3, v2) % 104.07/15.23 = v0)) & ! [v0: Nat_nat_prod_set$] : ! [v1: Nat_nat_prod_set$] : ! [v2: % 104.07/15.23 Nat_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_prod_set$] : ! [v4: Nat_set$] : % 104.07/15.23 (v1 = v0 | ~ (relInvImage$d(v4, v3, v2) = v1) | ~ (relInvImage$d(v4, v3, v2) % 104.07/15.23 = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: % 104.07/15.23 ZF_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_prod_set$] : ! [v4: ZF_set$] : (v1 % 104.07/15.23 = v0 | ~ (relInvImage$c(v4, v3, v2) = v1) | ~ (relInvImage$c(v4, v3, v2) = % 104.07/15.23 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: Nat$] : ! [v3: % 104.07/15.23 Nat_bool_fun$] : ! [v4: tlbool] : (v1 = v0 | ~ (def_4(v4, v3, v2) = v1) | % 104.07/15.23 ~ (def_4(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.23 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF_ZF_prod_set$] : ! [v4: % 104.07/15.23 ZF_set$] : (v1 = v0 | ~ (relInvImage$b(v4, v3, v2) = v1) | ~ % 104.07/15.23 (relInvImage$b(v4, v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod_set$] : ! % 104.07/15.23 [v1: ZF_set_ZF_set_prod_set$] : ! [v2: ZF_set_ZF_fun$] : ! [v3: % 104.07/15.23 ZF_ZF_prod_set$] : ! [v4: ZF_set_set$] : (v1 = v0 | ~ (relInvImage$a(v4, % 104.07/15.23 v3, v2) = v1) | ~ (relInvImage$a(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.23 ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_prod_set$] % 104.07/15.23 : ! [v2: ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_prod_set$] : ! [v4: % 104.07/15.23 ZF_ZF_prod_set$] : (v1 = v0 | ~ (relInvImage$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (relInvImage$(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.23 ZF_ZF_prod_set$] : ! [v2: ZF_set_ZF_fun$] : ! [v3: ZF_set_ZF_fun$] : ! % 104.07/15.23 [v4: ZF_set_set$] : (v1 = v0 | ~ (image2$b(v4, v3, v2) = v1) | ~ % 104.07/15.23 (image2$b(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.23 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF_ZF_fun$] : ! [v4: % 104.07/15.23 ZF_set$] : (v1 = v0 | ~ (image2$a(v4, v3, v2) = v1) | ~ (image2$a(v4, v3, % 104.07/15.23 v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! % 104.07/15.23 [v2: ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_prod_ZF_fun$] : ! [v4: % 104.07/15.23 ZF_ZF_prod_set$] : (v1 = v0 | ~ (image2$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (image2$(v4, v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] % 104.07/15.23 : ! [v2: tlbool] : ! [v3: ZF$] : ! [v4: ZF$] : (v1 = v0 | ~ % 104.07/15.23 (rec_set_bool$(v4, v3, v2) = v1) | ~ (rec_set_bool$(v4, v3, v2) = v0)) & ! % 104.07/15.23 [v0: ZF_set_ZF_set_prod_bool_fun$] : ! [v1: ZF_set_ZF_set_prod_bool_fun$] : % 104.07/15.23 ! [v2: ZF_set_ZF_fun$] : ! [v3: ZF_ZF_prod_set$] : ! [v4: ZF_set_set$] : (v1 % 104.07/15.23 = v0 | ~ (uvu$(v4, v3, v2) = v1) | ~ (uvu$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.23 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_fun$] % 104.07/15.23 : ! [v3: ZF_ZF_prod_set$] : ! [v4: ZF_set$] : (v1 = v0 | ~ (uvv$(v4, v3, % 104.07/15.23 v2) = v1) | ~ (uvv$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.23 ZF_ZF_prod_ZF_ZF_prod_prod_bool_fun$] : ! [v1: % 104.07/15.23 ZF_ZF_prod_ZF_ZF_prod_prod_bool_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : ! % 104.07/15.23 [v3: ZF_ZF_prod_set$] : ! [v4: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uvt$(v4, v3, % 104.07/15.23 v2) = v1) | ~ (uvt$(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] % 104.07/15.23 : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_set_ZF_fun$] : ! [v3: % 104.07/15.23 ZF_set_ZF_fun$] : ! [v4: ZF_set_set$] : (v1 = v0 | ~ (uvr$(v4, v3, v2) = % 104.07/15.23 v1) | ~ (uvr$(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! % 104.07/15.23 [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF_ZF_fun$] : ! % 104.07/15.23 [v4: ZF_set$] : (v1 = v0 | ~ (uvq$(v4, v3, v2) = v1) | ~ (uvq$(v4, v3, v2) = % 104.07/15.23 v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! % 104.07/15.23 [v2: ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_prod_ZF_fun$] : ! [v4: % 104.07/15.23 ZF_ZF_prod_set$] : (v1 = v0 | ~ (uvp$(v4, v3, v2) = v1) | ~ (uvp$(v4, v3, % 104.07/15.23 v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: ZF$] : ! [v3: % 104.07/15.23 ZF$] : ! [v4: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (def_3(v4, v3, v2) = v1) % 104.07/15.23 | ~ (def_3(v4, v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 104.07/15.23 ZF$] : ! [v3: ZF$] : ! [v4: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ % 104.07/15.23 (def_2(v4, v3, v2) = v1) | ~ (def_2(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.23 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: ZF_set_bool_fun$] : ! % 104.07/15.23 [v3: Nat_set$] : ! [v4: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uwp$(v4, v3, v2) = % 104.07/15.23 v1) | ~ (uwp$(v4, v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.23 ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : ! [v3: ZF_set_set$] : ! % 104.07/15.23 [v4: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ (uwr$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (uwr$(v4, v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.23 ZF_set_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF_set_set$] : ! [v4: % 104.07/15.23 ZF_set_ZF_fun$] : (v1 = v0 | ~ (uwx$(v4, v3, v2) = v1) | ~ (uwx$(v4, v3, % 104.07/15.23 v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! % 104.07/15.23 [v2: ZF_ZF_prod_bool_fun$] : ! [v3: ZF_set_set$] : ! [v4: % 104.07/15.23 ZF_set_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (uxd$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (uxd$(v4, v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : % 104.07/15.23 ! [v2: ZF_set_bool_fun$] : ! [v3: ZF_set$] : ! [v4: ZF_ZF_set_fun$] : (v1 = % 104.07/15.23 v0 | ~ (uwt$(v4, v3, v2) = v1) | ~ (uwt$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.23 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 104.07/15.23 ZF_set$] : ! [v4: ZF_ZF_fun$] : (v1 = v0 | ~ (uwz$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (uwz$(v4, v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : % 104.07/15.23 ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: ZF_set$] : ! [v4: ZF_ZF_ZF_prod_fun$] % 104.07/15.23 : (v1 = v0 | ~ (uxf$(v4, v3, v2) = v1) | ~ (uxf$(v4, v3, v2) = v0)) & ! % 104.07/15.23 [v0: ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.23 ZF_set_bool_fun$] : ! [v3: ZF_ZF_prod_set$] : ! [v4: % 104.07/15.23 ZF_ZF_prod_ZF_set_fun$] : (v1 = v0 | ~ (uwv$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (uwv$(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.23 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF_ZF_prod_set$] : % 104.07/15.23 ! [v4: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uxb$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (uxb$(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.23 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: % 104.07/15.23 ZF_ZF_prod_set$] : ! [v4: ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ % 104.07/15.23 (uxh$(v4, v3, v2) = v1) | ~ (uxh$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.23 ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : % 104.07/15.23 ! [v3: Nat_set$] : ! [v4: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uwo$(v4, v3, v2) % 104.07/15.23 = v1) | ~ (uwo$(v4, v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.23 ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : ! [v3: ZF_set_set$] : ! % 104.07/15.23 [v4: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ (uwq$(v4, v3, v2) = v1) | ~ % 104.07/15.23 (uwq$(v4, v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : % 104.07/15.23 ! [v2: ZF_bool_fun$] : ! [v3: ZF_set_set$] : ! [v4: ZF_set_ZF_fun$] : (v1 = % 104.07/15.23 v0 | ~ (uww$(v4, v3, v2) = v1) | ~ (uww$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.23 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.23 ZF_ZF_prod_bool_fun$] : ! [v3: ZF_set_set$] : ! [v4: % 104.07/15.23 ZF_set_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (uxc$(v4, v3, v2) = v1) | ~ % 104.07/15.24 (uxc$(v4, v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.24 ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : ! [v3: ZF_set$] : ! [v4: % 104.07/15.24 ZF_ZF_set_fun$] : (v1 = v0 | ~ (uws$(v4, v3, v2) = v1) | ~ (uws$(v4, v3, % 104.07/15.24 v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 104.07/15.24 ZF_bool_fun$] : ! [v3: ZF_set$] : ! [v4: ZF_ZF_fun$] : (v1 = v0 | ~ % 104.07/15.24 (uwy$(v4, v3, v2) = v1) | ~ (uwy$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v3: ZF_set$] : ! [v4: ZF_ZF_ZF_prod_fun$] : (v1 % 104.07/15.24 = v0 | ~ (uxe$(v4, v3, v2) = v1) | ~ (uxe$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : % 104.07/15.24 ! [v3: ZF_ZF_prod_set$] : ! [v4: ZF_ZF_prod_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (uwu$(v4, v3, v2) = v1) | ~ (uwu$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v4: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uxa$(v4, v3, % 104.07/15.24 v2) = v1) | ~ (uxa$(v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] % 104.07/15.24 : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v4: ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ % 104.07/15.24 (uxg$(v4, v3, v2) = v1) | ~ (uxg$(v4, v3, v2) = v0)) & ! [v0: ZF$] : ! % 104.07/15.24 [v1: ZF$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF$] : ! [v4: ZF$] : (v1 = v0 | ~ % 104.07/15.24 (zFfun$(v4, v3, v2) = v1) | ~ (zFfun$(v4, v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set$] : ! % 104.07/15.24 [v3: Nat_ZF_fun$] : (v1 = v0 | ~ (inj_on$(v3, v2) = v1) | ~ (inj_on$(v3, v2) % 104.07/15.24 = v0)) & ! [v0: ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! % 104.07/15.24 [v2: Nat_set$] : ! [v3: Nat_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (image$ad(v3, v2) = v1) | ~ (image$ad(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set_ZF_set_fun$] : ! [v1: ZF_set_set_ZF_set_fun$] : ! [v2: % 104.07/15.24 ZF_set_set_ZF_set_set_fun$] : ! [v3: ZF_set_set_ZF_set_fun$] : (v1 = v0 | % 104.07/15.24 ~ (comp$h(v3, v2) = v1) | ~ (comp$h(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set_ZF_set_fun$] : ! [v1: ZF_set_set_ZF_set_fun$] : ! [v2: % 104.07/15.24 ZF_set_set_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (comp$i(v3, v2) = v1) | ~ (comp$i(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set_set_ZF_set_fun$] : ! [v1: ZF_ZF_prod_set_set_ZF_set_fun$] : % 104.07/15.24 ! [v2: ZF_ZF_prod_set_set_ZF_set_set_fun$] : ! [v3: ZF_set_set_ZF_set_fun$] : % 104.07/15.24 (v1 = v0 | ~ (comp$f(v3, v2) = v1) | ~ (comp$f(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set_set_ZF_set_fun$] : ! [v1: ZF_ZF_prod_set_set_ZF_set_fun$] : % 104.07/15.24 ! [v2: ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_set_ZF_set_fun$] : (v1 = v0 | ~ (comp$g(v3, v2) = v1) | ~ % 104.07/15.24 (comp$g(v3, v2) = v0)) & ! [v0: ZF_set_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 ZF_set_set_ZF_set_set_fun$] : ! [v2: ZF_set_set_ZF_set_set_set_fun$] : ! % 104.07/15.24 [v3: ZF_set_set_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$d(v3, v2) = v1) | % 104.07/15.24 ~ (comp$d(v3, v2) = v0)) & ! [v0: ZF_set_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 ZF_set_set_ZF_set_set_fun$] : ! [v2: ZF_set_set_ZF_set_fun$] : ! [v3: % 104.07/15.24 ZF_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$e(v3, v2) = v1) | ~ % 104.07/15.24 (comp$e(v3, v2) = v0)) & ! [v0: Nat_set_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 Nat_set_set_ZF_set_set_fun$] : ! [v2: Nat_set_set_ZF_set_set_set_fun$] : ! % 104.07/15.24 [v3: ZF_set_set_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$b(v3, v2) = v1) | % 104.07/15.24 ~ (comp$b(v3, v2) = v0)) & ! [v0: Nat_set_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 Nat_set_set_ZF_set_set_fun$] : ! [v2: Nat_set_set_nat_set_fun$] : ! [v3: % 104.07/15.24 Nat_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$c(v3, v2) = v1) | ~ % 104.07/15.24 (comp$c(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! % 104.07/15.24 [v2: ZF_ZF_prod_set_set$] : ! [v3: ZF_ZF_prod_set_set_ZF_set_set_fun$] : (v1 % 104.07/15.24 = v0 | ~ (fun_app$bg(v3, v2) = v1) | ~ (fun_app$bg(v3, v2) = v0)) & ! % 104.07/15.24 [v0: ZF_set_set_set$] : ! [v1: ZF_set_set_set$] : ! [v2: Nat_set_set$] : ! % 104.07/15.24 [v3: Nat_set_set_ZF_set_set_set_fun$] : (v1 = v0 | ~ (fun_app$bf(v3, v2) = % 104.07/15.24 v1) | ~ (fun_app$bf(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: % 104.07/15.24 ZF_set_set$] : ! [v2: Nat_set_set$] : ! [v3: Nat_set_ZF_set_fun$] : (v1 = % 104.07/15.24 v0 | ~ (image$aa(v3, v2) = v1) | ~ (image$aa(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_set_set$] : ! [v1: Nat_set_set$] : ! [v2: Nat_set$] : ! [v3: % 104.07/15.24 Nat_nat_set_fun$] : (v1 = v0 | ~ (image$z(v3, v2) = v1) | ~ (image$z(v3, % 104.07/15.24 v2) = v0)) & ! [v0: Nat_set_set$] : ! [v1: Nat_set_set$] : ! [v2: % 104.07/15.24 ZF_set$] : ! [v3: ZF_nat_set_fun$] : (v1 = v0 | ~ (image$y(v3, v2) = v1) | % 104.07/15.24 ~ (image$y(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 104.07/15.24 Nat_set_set$] : ! [v3: Nat_set_set_nat_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$be(v3, v2) = v1) | ~ (fun_app$be(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: % 104.07/15.24 Nat_nat_prod_set$] : ! [v3: Nat_nat_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | % 104.07/15.24 ~ (image$x(v3, v2) = v1) | ~ (image$x(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: % 104.07/15.24 Nat_ZF_prod_set$] : ! [v3: Nat_ZF_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (image$w(v3, v2) = v1) | ~ (image$w(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: % 104.07/15.24 ZF_nat_prod_set$] : ! [v3: ZF_nat_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (image$v(v3, v2) = v1) | ~ (image$v(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set_set$] : ! [v1: ZF_set_set_set$] : ! [v2: ZF_set_set$] : ! [v3: % 104.07/15.24 ZF_set_set_ZF_set_set_set_fun$] : (v1 = v0 | ~ (fun_app$bd(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$bd(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set_set$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set_set$] : ! [v2: ZF_set_set$] : ! [v3: % 104.07/15.24 ZF_set_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (image$t(v3, v2) = v1) | ~ % 104.07/15.24 (image$t(v3, v2) = v0)) & ! [v0: ZF_set_set_set$] : ! [v1: % 104.07/15.24 ZF_set_set_set$] : ! [v2: ZF_ZF_prod_set$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_set_set_fun$] : (v1 = v0 | ~ (image$s(v3, v2) = v1) | ~ % 104.07/15.24 (image$s(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set_set$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set_set$] : ! [v2: ZF_ZF_prod_set$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (image$r(v3, v2) = v1) | ~ % 104.07/15.24 (image$r(v3, v2) = v0)) & ! [v0: ZF_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_set_set_fun$] : ! [v2: ZF$] : ! [v3: ZF_ZF_ZF_set_set_fun_fun$] : % 104.07/15.24 (v1 = v0 | ~ (fun_app$bc(v3, v2) = v1) | ~ (fun_app$bc(v3, v2) = v0)) & ! % 104.07/15.24 [v0: ZF_set_set_set$] : ! [v1: ZF_set_set_set$] : ! [v2: Nat_set$] : ! [v3: % 104.07/15.24 Nat_ZF_set_set_fun$] : (v1 = v0 | ~ (image$q(v3, v2) = v1) | ~ % 104.07/15.24 (image$q(v3, v2) = v0)) & ! [v0: ZF_set_set_set$] : ! [v1: % 104.07/15.24 ZF_set_set_set$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_set_fun$] : (v1 = v0 % 104.07/15.24 | ~ (image$p(v3, v2) = v1) | ~ (image$p(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF_set_set_set$] : ! [v3: % 104.07/15.24 ZF_set_set_set_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$bb(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$bb(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_set_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 104.07/15.24 (bind$c(v3, v2) = v1) | ~ (bind$c(v3, v2) = v0)) & ! [v0: ZF_set$] : ! % 104.07/15.24 [v1: ZF_set$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_set$] : (v1 = v0 | ~ % 104.07/15.24 (bind$b(v3, v2) = v1) | ~ (bind$b(v3, v2) = v0)) & ! [v0: ZF_set_set$] : % 104.07/15.24 ! [v1: ZF_set_set$] : ! [v2: Nat_ZF_set_set_fun$] : ! [v3: Nat_set$] : (v1 = % 104.07/15.24 v0 | ~ (bind$a(v3, v2) = v1) | ~ (bind$a(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF_ZF_set_set_fun$] : ! [v3: % 104.07/15.24 ZF_set$] : (v1 = v0 | ~ (bind$(v3, v2) = v1) | ~ (bind$(v3, v2) = v0)) & % 104.07/15.24 ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: ZF_ZF_prod$] : ! [v3: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (def_10(v3, v2) = v1) | ~ (def_10(v3, % 104.07/15.24 v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: ZF_ZF_prod$] : % 104.07/15.24 ! [v3: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (def_9(v3, v2) = v1) | ~ % 104.07/15.24 (def_9(v3, v2) = v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: % 104.07/15.24 ZF_ZF_prod$] : ! [v3: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (def_7(v3, v2) = % 104.07/15.24 v1) | ~ (def_7(v3, v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : % 104.07/15.24 ! [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ % 104.07/15.24 (image$o(v3, v2) = v1) | ~ (image$o(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Bool_set$] : ! % 104.07/15.24 [v3: tlbool] : (v1 = v0 | ~ (member$d(v3, v2) = v1) | ~ (member$d(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: % 104.07/15.24 Nat_set$] : ! [v3: Nat_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (image$n(v3, v2) = % 104.07/15.24 v1) | ~ (image$n(v3, v2) = v0)) & ! [v0: Nat_nat_prod_set$] : ! [v1: % 104.07/15.24 Nat_nat_prod_set$] : ! [v2: Nat_nat_set_fun$] : ! [v3: Nat_set$] : (v1 = % 104.07/15.24 v0 | ~ (sigma$k(v3, v2) = v1) | ~ (sigma$k(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_prod_set$] : ! [v1: Nat_ZF_prod_set$] : ! [v2: Nat_ZF_set_fun$] : % 104.07/15.24 ! [v3: Nat_set$] : (v1 = v0 | ~ (sigma$j(v3, v2) = v1) | ~ (sigma$j(v3, v2) % 104.07/15.24 = v0)) & ! [v0: ZF_nat_prod_set$] : ! [v1: ZF_nat_prod_set$] : ! [v2: % 104.07/15.24 ZF_nat_set_fun$] : ! [v3: ZF_set$] : (v1 = v0 | ~ (sigma$i(v3, v2) = v1) | % 104.07/15.24 ~ (sigma$i(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF_set$] : (v1 = v0 | ~ % 104.07/15.24 (gr$c(v3, v2) = v1) | ~ (gr$c(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_prod_set$] : ! [v1: ZF_ZF_prod_ZF_prod_set$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (gr$b(v3, v2) % 104.07/15.24 = v1) | ~ (gr$b(v3, v2) = v0)) & ! [v0: Nat_ZF_set_prod_set$] : ! [v1: % 104.07/15.24 Nat_ZF_set_prod_set$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: Nat_set$] : (v1 = % 104.07/15.24 v0 | ~ (gr$a(v3, v2) = v1) | ~ (gr$a(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_set_prod_set$] : ! [v1: Nat_ZF_set_prod_set$] : ! [v2: % 104.07/15.24 Nat_ZF_set_set_fun$] : ! [v3: Nat_set$] : (v1 = v0 | ~ (sigma$h(v3, v2) = % 104.07/15.24 v1) | ~ (sigma$h(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 104.07/15.24 MultipleValueBool] : ! [v2: Nat_ZF_set_prod_set$] : ! [v3: % 104.07/15.24 Nat_ZF_set_prod_set$] : (v1 = v0 | ~ (less_eq$n(v3, v2) = v1) | ~ % 104.07/15.24 (less_eq$n(v3, v2) = v0)) & ! [v0: ZF_ZF_set_prod_set$] : ! [v1: % 104.07/15.24 ZF_ZF_set_prod_set$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_set$] : (v1 = v0 % 104.07/15.24 | ~ (gr$(v3, v2) = v1) | ~ (gr$(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! % 104.07/15.24 [v1: ZF_ZF_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_set$] : (v1 = v0 | ~ % 104.07/15.24 (subsetFn$a(v3, v2) = v1) | ~ (subsetFn$a(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (subsetFn$(v3, % 104.07/15.24 v2) = v1) | ~ (subsetFn$(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: % 104.07/15.24 Nat_set$] : ! [v2: Nat_set$] : ! [v3: Nat_nat_fun$] : (v1 = v0 | ~ % 104.07/15.24 (image$m(v3, v2) = v1) | ~ (image$m(v3, v2) = v0)) & ! [v0: Nat_set$] : ! % 104.07/15.24 [v1: Nat_set$] : ! [v2: ZF_set$] : ! [v3: ZF_nat_fun$] : (v1 = v0 | ~ % 104.07/15.24 (image$l(v3, v2) = v1) | ~ (image$l(v3, v2) = v0)) & ! [v0: ZF_set$] : ! % 104.07/15.24 [v1: ZF_set$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_fun$] : (v1 = v0 | ~ % 104.07/15.24 (image$k(v3, v2) = v1) | ~ (image$k(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_ZF_fun$] : % 104.07/15.24 ! [v3: ZF_ZF_prod_ZF_ZF_prod_prod_set$] : (v1 = v0 | ~ (relImage$c(v3, v2) = % 104.07/15.24 v1) | ~ (relImage$c(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod_set$] : % 104.07/15.24 ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: % 104.07/15.24 Nat_nat_prod_set$] : (v1 = v0 | ~ (relImage$b(v3, v2) = v1) | ~ % 104.07/15.24 (relImage$b(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod_set$] : ! [v1: % 104.07/15.24 ZF_set_ZF_set_prod_set$] : ! [v2: ZF_set_ZF_set_set_fun$] : ! [v3: % 104.07/15.24 ZF_set_set$] : (v1 = v0 | ~ (sigma$g(v3, v2) = v1) | ~ (sigma$g(v3, v2) = % 104.07/15.24 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_set_ZF_set_prod_set$] : ! [v3: ZF_set_ZF_set_prod_set$] : (v1 = v0 | ~ % 104.07/15.24 (less_eq$m(v3, v2) = v1) | ~ (less_eq$m(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_ZF_set_prod_set$] : ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (relImage$a(v3, % 104.07/15.24 v2) = v1) | ~ (relImage$a(v3, v2) = v0)) & ! [v0: ZF_ZF_set_prod_set$] % 104.07/15.24 : ! [v1: ZF_ZF_set_prod_set$] : ! [v2: ZF_ZF_set_set_fun$] : ! [v3: % 104.07/15.24 ZF_set$] : (v1 = v0 | ~ (sigma$f(v3, v2) = v1) | ~ (sigma$f(v3, v2) = v0)) % 104.07/15.24 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_set_prod_set$] : ! [v3: ZF_ZF_set_prod_set$] : (v1 = v0 | ~ % 104.07/15.24 (less_eq$l(v3, v2) = v1) | ~ (less_eq$l(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_set_prod_set$] : ! [v1: ZF_ZF_prod_ZF_set_prod_set$] : ! % 104.07/15.24 [v2: ZF_ZF_prod_ZF_set_set_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 104.07/15.24 (sigma$e(v3, v2) = v1) | ~ (sigma$e(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_set_prod_set$] : ! [v3: ZF_ZF_prod_ZF_set_prod_set$] : (v1 = % 104.07/15.24 v0 | ~ (less_eq$k(v3, v2) = v1) | ~ (less_eq$k(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_ZF_prod_set$] : ! [v1: ZF_set_ZF_prod_set$] : ! [v2: % 104.07/15.24 ZF_set_ZF_set_fun$] : ! [v3: ZF_set_set$] : (v1 = v0 | ~ (sigma$d(v3, v2) % 104.07/15.24 = v1) | ~ (sigma$d(v3, v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_prod_set$] : ! % 104.07/15.24 [v1: ZF_ZF_ZF_prod_prod_set$] : ! [v2: ZF_ZF_ZF_prod_set_fun$] : ! [v3: % 104.07/15.24 ZF_set$] : (v1 = v0 | ~ (sigma$c(v3, v2) = v1) | ~ (sigma$c(v3, v2) = v0)) % 104.07/15.24 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_ZF_prod_prod_set$] : ! [v3: ZF_ZF_ZF_prod_prod_set$] : (v1 = v0 | ~ % 104.07/15.24 (less_eq$j(v3, v2) = v1) | ~ (less_eq$j(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_prod_set$] : ! [v1: ZF_ZF_prod_ZF_prod_set$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_set_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 104.07/15.24 (sigma$b(v3, v2) = v1) | ~ (sigma$b(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_prod_set$] : (v1 = v0 | ~ % 104.07/15.24 (less_eq$i(v3, v2) = v1) | ~ (less_eq$i(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_prod_set$] % 104.07/15.24 : ! [v2: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = % 104.07/15.24 v0 | ~ (sigma$a(v3, v2) = v1) | ~ (sigma$a(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v3: ZF_ZF_prod_ZF_ZF_prod_prod_set$] % 104.07/15.24 : (v1 = v0 | ~ (less_eq$h(v3, v2) = v1) | ~ (less_eq$h(v3, v2) = v0)) & ! % 104.07/15.24 [v0: tlbool] : ! [v1: tlbool] : ! [v2: tlbool] : ! [v3: Bool_bool_fun$] : % 104.07/15.24 (v1 = v0 | ~ (def_5(v3, v2) = v1) | ~ (def_5(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: % 104.07/15.24 tlbool] : (v1 = v0 | ~ (case_nat$(v3, v2) = v1) | ~ (case_nat$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: % 104.07/15.24 ZF_ZF_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (relImage$(v3, v2) = % 104.07/15.24 v1) | ~ (relImage$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 104.07/15.24 MultipleValueBool] : ! [v2: ZF_bool_fun$] : ! [v3: ZF_bool_fun$] : (v1 = % 104.07/15.24 v0 | ~ (less_eq$g(v3, v2) = v1) | ~ (less_eq$g(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ % 104.07/15.24 (less_eq$f(v3, v2) = v1) | ~ (less_eq$f(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF_set_bool_fun$] % 104.07/15.24 : ! [v3: ZF_set_bool_fun$] : (v1 = v0 | ~ (less_eq$d(v3, v2) = v1) | ~ % 104.07/15.24 (less_eq$d(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 104.07/15.24 MultipleValueBool] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_set$] : (v1 = v0 % 104.07/15.24 | ~ (less_eq$e(v3, v2) = v1) | ~ (less_eq$e(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : ! [v3: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ % 104.07/15.24 (less_eq$c(v3, v2) = v1) | ~ (less_eq$c(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Bool_ZF_fun$] : ! [v1: Bool_ZF_fun$] : ! [v2: ZF$] : ! [v3: ZF$] : (v1 = % 104.07/15.24 v0 | ~ (rec_bool$(v3, v2) = v1) | ~ (rec_bool$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF$] : ! [v1: ZF$] : ! [v2: Unit$] : ! [v3: ZF$] : (v1 = v0 | ~ % 104.07/15.24 (rec_unit$(v3, v2) = v1) | ~ (rec_unit$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: Unit$] : ! [v3: ZF$] : (v1 % 104.07/15.24 = v0 | ~ (rec_set_unit$(v3, v2) = v1) | ~ (rec_set_unit$(v3, v2) = v0)) & % 104.07/15.24 ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: ZF_bool_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (least$(v3, v2) = v1) | ~ (least$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: Nat_ZF_fun$] : ! [v1: Nat_ZF_fun$] : ! [v2: ZF$] % 104.07/15.24 : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (ext_ZF_n$(v3, v2) = v1) | ~ % 104.07/15.24 (ext_ZF_n$(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! % 104.07/15.24 [v2: ZF_nat_fun$] : ! [v3: Nat_ZF_fun$] : (v1 = v0 | ~ (comp$a(v3, v2) = v1) % 104.07/15.24 | ~ (comp$a(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! % 104.07/15.24 [v2: ZF_ZF_fun$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (comp$(v3, v2) = v1) | % 104.07/15.24 ~ (comp$(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: ZF_ZF_fun$] % 104.07/15.24 : ! [v3: ZF$] : (v1 = v0 | ~ (lambda$(v3, v2) = v1) | ~ (lambda$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF$] % 104.07/15.24 : (v1 = v0 | ~ (sep$(v3, v2) = v1) | ~ (sep$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF_ZF_prod$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$ba(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$ba(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 104.07/15.24 MultipleValueBool] : ! [v2: ZF_set_ZF_set_prod$] : ! [v3: % 104.07/15.24 ZF_set_ZF_set_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$az(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$az(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod$] : ! [v1: % 104.07/15.24 ZF_set_ZF_set_prod$] : ! [v2: ZF_set$] : ! [v3: ZF_set$] : (v1 = v0 | ~ % 104.07/15.24 (pair$b(v3, v2) = v1) | ~ (pair$b(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_prod$] : ! [v3: ZF_ZF_prod_ZF_ZF_prod_prod_bool_fun$] % 104.07/15.24 : (v1 = v0 | ~ (fun_app$ay(v3, v2) = v1) | ~ (fun_app$ay(v3, v2) = v0)) & ! % 104.07/15.24 [v0: ZF_ZF_prod_ZF_ZF_prod_prod$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_prod$] : ! % 104.07/15.24 [v2: ZF_ZF_prod$] : ! [v3: ZF_ZF_prod$] : (v1 = v0 | ~ (pair$a(v3, v2) = v1) % 104.07/15.24 | ~ (pair$a(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_bool_fun_fun$] : ! [v3: % 104.07/15.24 Bool_bool_fun$] : (v1 = v0 | ~ (uzr$(v3, v2) = v1) | ~ (uzr$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : ! [v3: Bool_ZF_fun$] : (v1 = v0 | ~ (uzq$(v3, v2) = % 104.07/15.24 v1) | ~ (uzq$(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: % 104.07/15.24 tlbool] : ! [v3: Bool_ZF_fun$] : (v1 = v0 | ~ (fun_app$ax(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$ax(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_ZF_fun_fun$] : ! [v3: ZF_bool_fun$] : % 104.07/15.24 (v1 = v0 | ~ (uzp$(v3, v2) = v1) | ~ (uzp$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_ZF_fun_fun$] : ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: ZF_ZF_ZF_fun_fun$] % 104.07/15.24 : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (uzo$(v3, v2) = v1) | ~ (uzo$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_bool_fun_fun$] : ! % 104.07/15.24 [v2: ZF_bool_fun$] : ! [v3: ZF_bool_fun$] : (v1 = v0 | ~ (vag$(v3, v2) = v1) % 104.07/15.24 | ~ (vag$(v3, v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_bool_fun_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_ZF_prod_bool_fun_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: % 104.07/15.24 ZF_bool_fun$] : (v1 = v0 | ~ (vaa$(v3, v2) = v1) | ~ (vaa$(v3, v2) = v0)) % 104.07/15.24 & ! [v0: ZF_ZF_prod_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_prod_ZF_bool_fun_fun$] % 104.07/15.24 : ! [v2: ZF_bool_fun$] : ! [v3: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ % 104.07/15.24 (vac$(v3, v2) = v1) | ~ (vac$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! % 104.07/15.24 [v3: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (vae$(v3, v2) = v1) | ~ (vae$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: Nat_nat_ZF_ZF_prod_set_fun_fun$] : ! [v1: % 104.07/15.24 Nat_nat_ZF_ZF_prod_set_fun_fun$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: % 104.07/15.24 Nat_ZF_set_fun$] : (v1 = v0 | ~ (vax$(v3, v2) = v1) | ~ (vax$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: Nat_ZF_ZF_prod_set_fun$] : ! [v1: Nat_ZF_ZF_prod_set_fun$] % 104.07/15.24 : ! [v2: Nat$] : ! [v3: Nat_nat_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$aw(v3, v2) = v1) | ~ (fun_app$aw(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_nat_ZF_ZF_prod_set_fun_fun$] : ! [v1: ZF_nat_ZF_ZF_prod_set_fun_fun$] : % 104.07/15.24 ! [v2: Nat_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (var$(v3, % 104.07/15.24 v2) = v1) | ~ (var$(v3, v2) = v0)) & ! [v0: Nat_ZF_ZF_prod_set_fun$] : % 104.07/15.24 ! [v1: Nat_ZF_ZF_prod_set_fun$] : ! [v2: ZF$] : ! [v3: % 104.07/15.24 ZF_nat_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (fun_app$av(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$av(v3, v2) = v0)) & ! [v0: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : ! % 104.07/15.24 [v1: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: % 104.07/15.24 Nat_ZF_set_fun$] : (v1 = v0 | ~ (vav$(v3, v2) = v1) | ~ (vav$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_ZF_prod_set_fun$] : % 104.07/15.24 ! [v2: Nat$] : ! [v3: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$au(v3, v2) = v1) | ~ (fun_app$au(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_ZF_ZF_prod_set_fun_fun$] : ! [v1: ZF_ZF_ZF_ZF_prod_set_fun_fun$] : ! % 104.07/15.24 [v2: ZF_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (vaz$(v3, v2) = % 104.07/15.24 v1) | ~ (vaz$(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_bool_fun_fun$] : ! [v3: ZF_bool_fun$] % 104.07/15.24 : (v1 = v0 | ~ (vby$(v3, v2) = v1) | ~ (vby$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_ZF_prod_bool_fun_fun$] : ! [v1: ZF_ZF_ZF_prod_bool_fun_fun$] : ! % 104.07/15.24 [v2: ZF_ZF_ZF_prod_bool_fun_fun$] : ! [v3: ZF_bool_fun$] : (v1 = v0 | ~ % 104.07/15.24 (vbs$(v3, v2) = v1) | ~ (vbs$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_prod_ZF_bool_fun_fun$] : ! % 104.07/15.24 [v2: ZF_ZF_prod_ZF_bool_fun_fun$] : ! [v3: ZF_ZF_prod_bool_fun$] : (v1 = v0 | % 104.07/15.24 ~ (vbu$(v3, v2) = v1) | ~ (vbu$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : ! [v3: ZF_ZF_prod_bool_fun$] : (v1 = % 104.07/15.24 v0 | ~ (vbw$(v3, v2) = v1) | ~ (vbw$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_bool_fun_fun$] : ! [v2: ZF$] : ! [v3: % 104.07/15.24 ZF$] : (v1 = v0 | ~ (uzz$(v3, v2) = v1) | ~ (uzz$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF_set_set$] : ! [v3: % 104.07/15.24 ZF_set_set_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$at(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$at(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.24 ZF_set_set$] : ! [v3: ZF_set_ZF_fun$] : (v1 = v0 | ~ (image$i(v3, v2) = % 104.07/15.24 v1) | ~ (image$i(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_ZF_ZF_prod_fun$] : % 104.07/15.24 (v1 = v0 | ~ (image$h(v3, v2) = v1) | ~ (image$h(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF_ZF_prod_set$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_set_fun$] : (v1 = v0 | ~ (image$f(v3, v2) = v1) | ~ % 104.07/15.24 (image$f(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (image$e(v3, v2) = v1) | ~ % 104.07/15.24 (image$e(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : ! [v2: ZF$] : ! [v3: tlbool] : (v1 = v0 | ~ % 104.07/15.24 (uun$(v3, v2) = v1) | ~ (uun$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_fun$] % 104.07/15.24 : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uvs$(v3, v2) = v1) | ~ (uvs$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! % 104.07/15.24 [v2: Nat_bool_fun$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uya$(v3, v2) = % 104.07/15.24 v1) | ~ (uya$(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.24 ZF_set_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = % 104.07/15.24 v0 | ~ (uyb$(v3, v2) = v1) | ~ (uyb$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_fun$] : (v1 = v0 | ~ (uyc$(v3, v2) = v1) | ~ (uyc$(v3, v2) = v0)) & % 104.07/15.24 ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_bool_fun$] : ! [v3: ZF_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (uye$(v3, v2) = % 104.07/15.24 v1) | ~ (uye$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: % 104.07/15.24 ZF_bool_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod_ZF_fun$] % 104.07/15.24 : (v1 = v0 | ~ (uyd$(v3, v2) = v1) | ~ (uyd$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ % 104.07/15.24 (uyf$(v3, v2) = v1) | ~ (uyf$(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : % 104.07/15.24 ! [v1: ZF_set_bool_fun$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_set_fun$] : (v1 % 104.07/15.24 = v0 | ~ (uxs$(v3, v2) = v1) | ~ (uxs$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set$] : ! % 104.07/15.24 [v3: Nat$] : (v1 = v0 | ~ (member$c(v3, v2) = v1) | ~ (member$c(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 104.07/15.24 ZF_set_set$] : ! [v3: ZF_set_ZF_fun$] : (v1 = v0 | ~ (uxw$(v3, v2) = v1) | % 104.07/15.24 ~ (uxw$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_set_set$] : ! [v3: % 104.07/15.24 ZF_set_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (uxz$(v3, v2) = v1) | ~ (uxz$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : ! [v2: % 104.07/15.24 ZF_set$] : ! [v3: ZF_set_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (fun_app$as(v3, % 104.07/15.24 v2) = v1) | ~ (fun_app$as(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : % 104.07/15.24 ! [v1: ZF_set_bool_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_fun$] : (v1 = % 104.07/15.24 v0 | ~ (uxt$(v3, v2) = v1) | ~ (uxt$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_set$] : ! [v3: % 104.07/15.24 ZF_ZF_fun$] : (v1 = v0 | ~ (uxv$(v3, v2) = v1) | ~ (uxv$(v3, v2) = v0)) & % 104.07/15.24 ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_set$] : ! [v3: ZF_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (uxy$(v3, v2) = v1) | % 104.07/15.24 ~ (uxy$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! % 104.07/15.24 [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uxu$(v3, % 104.07/15.24 v2) = v1) | ~ (uxu$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! % 104.07/15.24 [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_set$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (uxx$(v3, v2) = v1) | ~ % 104.07/15.24 (uxx$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : ! [v2: % 104.07/15.24 ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$ar(v3, v2) = v1) | ~ (fun_app$ar(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_fun$] % 104.07/15.24 : ! [v3: ZF_set$] : (v1 = v0 | ~ (uyx$(v3, v2) = v1) | ~ (uyx$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 104.07/15.24 Nat_set$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (vat$(v3, v2) = v1) | % 104.07/15.24 ~ (vat$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : % 104.07/15.24 ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (vaw$(v3, v2) = v1) % 104.07/15.24 | ~ (vaw$(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 104.07/15.24 Nat$] : ! [v3: Nat_nat_set_fun$] : (v1 = v0 | ~ (fun_app$aq(v3, v2) = v1) % 104.07/15.24 | ~ (fun_app$aq(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v2: Nat_nat_set_fun$] : ! [v3: Nat_ZF_set_fun$] : % 104.07/15.24 (v1 = v0 | ~ (vbb$(v3, v2) = v1) | ~ (vbb$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_set$] : ! [v1: Nat_set$] : ! [v2: ZF$] : ! [v3: ZF_nat_set_fun$] : % 104.07/15.24 (v1 = v0 | ~ (fun_app$ap(v3, v2) = v1) | ~ (fun_app$ap(v3, v2) = v0)) & ! % 104.07/15.24 [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_nat_set_fun$] : ! % 104.07/15.24 [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (vba$(v3, v2) = v1) | ~ (vba$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (vbd$(v3, v2) = % 104.07/15.24 v1) | ~ (vbd$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = % 104.07/15.24 v0 | ~ (vbc$(v3, v2) = v1) | ~ (vbc$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_set$] : ! [v3: % 104.07/15.24 Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (vbp$(v3, v2) = v1) | ~ (vbp$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! % 104.07/15.24 [v2: ZF_set$] : ! [v3: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vbm$(v3, v2) % 104.07/15.24 = v1) | ~ (vbm$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v2: Nat_set$] : ! [v3: ZF_nat_ZF_set_fun_fun$] : (v1 % 104.07/15.24 = v0 | ~ (vbj$(v3, v2) = v1) | ~ (vbj$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: % 104.07/15.24 ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vbg$(v3, v2) = v1) | ~ (vbg$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 104.07/15.24 ZF_set$] : ! [v3: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vbi$(v3, v2) = % 104.07/15.24 v1) | ~ (vbi$(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_nat_ZF_set_fun_fun$] : (v1 % 104.07/15.24 = v0 | ~ (vbl$(v3, v2) = v1) | ~ (vbl$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: Nat_set$] : ! [v3: % 104.07/15.24 Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vbo$(v3, v2) = v1) | ~ (vbo$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! % 104.07/15.24 [v2: Nat_set$] : ! [v3: Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (vbr$(v3, % 104.07/15.24 v2) = v1) | ~ (vbr$(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! % 104.07/15.24 [v2: Nat$] : ! [v3: Nat_nat_fun$] : (v1 = v0 | ~ (fun_app$ao(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$ao(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v2: Nat_nat_fun$] : ! [v3: Nat_ZF_set_fun$] : (v1 = % 104.07/15.24 v0 | ~ (uxn$(v3, v2) = v1) | ~ (uxn$(v3, v2) = v0)) & ! [v0: Nat$] : ! % 104.07/15.24 [v1: Nat$] : ! [v2: ZF$] : ! [v3: ZF_nat_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$an(v3, v2) = v1) | ~ (fun_app$an(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_nat_fun$] : ! [v3: % 104.07/15.24 Nat_ZF_set_fun$] : (v1 = v0 | ~ (uxm$(v3, v2) = v1) | ~ (uxm$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ (uxp$(v3, v2) % 104.07/15.24 = v1) | ~ (uxp$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_fun$] : % 104.07/15.24 (v1 = v0 | ~ (uxo$(v3, v2) = v1) | ~ (uxo$(v3, v2) = v0)) & ! [v0: ZF$] : % 104.07/15.24 ! [v1: ZF$] : ! [v2: ZF_set$] : ! [v3: ZF_set_ZF_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$am(v3, v2) = v1) | ~ (fun_app$am(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: % 104.07/15.24 ZF_set_ZF_fun$] : (v1 = v0 | ~ (uxj$(v3, v2) = v1) | ~ (uxj$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: Nat$] : ! [v3: % 104.07/15.24 Nat_bool_fun$] : (v1 = v0 | ~ (def_1(v3, v2) = v1) | ~ (def_1(v3, v2) = % 104.07/15.24 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 tlbool] : ! [v3: Bool_bool_fun$] : (v1 = v0 | ~ (fun_app$al(v3, v2) = v1) % 104.07/15.24 | ~ (fun_app$al(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 104.07/15.24 Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: Bool_bool_fun$] : (v1 = v0 % 104.07/15.24 | ~ (uvz$(v3, v2) = v1) | ~ (uvz$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_ZF_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_set_fun$] : (v1 = v0 | ~ (uxk$(v3, v2) = v1) | ~ (uxk$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uxl$(v3, v2) = v1) | % 104.07/15.24 ~ (uxl$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_ZF_set_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_set_fun$] : (v1 = v0 | ~ (vcd$(v3, v2) = v1) | ~ (vcd$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: Nat_ZF_fun$] : ! [v1: Nat_ZF_fun$] : ! [v2: Nat_ZF_fun$] % 104.07/15.24 : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (uyp$(v3, v2) = v1) | ~ (uyp$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: ZF_ZF_fun$] : % 104.07/15.24 ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (uxi$(v3, v2) = v1) | ~ (uxi$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_prod_ZF_fun$] : ! [v1: ZF_ZF_prod_ZF_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (uxq$(v3, v2) = % 104.07/15.24 v1) | ~ (uxq$(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] % 104.07/15.24 : ! [v2: ZF_ZF_ZF_prod_fun$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 104.07/15.24 (uxr$(v3, v2) = v1) | ~ (uxr$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_ZF_set_set_fun$] : ! [v1: ZF_set_ZF_set_set_fun$] : ! [v2: % 104.07/15.24 Nat_set$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uwl$(v3, v2) = v1) | % 104.07/15.24 ~ (uwl$(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 ZF_set_ZF_set_set_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_fun$] : (v1 = % 104.07/15.24 v0 | ~ (uwk$(v3, v2) = v1) | ~ (uwk$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: % 104.07/15.24 ZF_ZF_fun$] : (v1 = v0 | ~ (uwm$(v3, v2) = v1) | ~ (uwm$(v3, v2) = v0)) & % 104.07/15.24 ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_ZF_prod_set$] : % 104.07/15.24 ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uwn$(v3, v2) = v1) | ~ (uwn$(v3, % 104.07/15.24 v2) = v0)) & ! [v0: Nat_ZF_set_set_fun$] : ! [v1: Nat_ZF_set_set_fun$] % 104.07/15.24 : ! [v2: Nat_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (vch$(v3, % 104.07/15.24 v2) = v1) | ~ (vch$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_set_fun$] : ! % 104.07/15.24 [v1: ZF_ZF_set_set_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : % 104.07/15.24 (v1 = v0 | ~ (vcg$(v3, v2) = v1) | ~ (vcg$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_ZF_set_fun$] : ! % 104.07/15.24 [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (vcj$(v3, v2) = v1) | ~ (vcj$(v3, v2) = v0)) % 104.07/15.24 & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_ZF_set_fun$] % 104.07/15.24 : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (vci$(v3, v2) = v1) | ~ (vci$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: Nat$] % 104.07/15.24 : ! [v3: Nat_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$ak(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$ak(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v2: Nat_ZF_ZF_prod_set_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (vcf$(v3, v2) = v1) | ~ (vcf$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: ZF_ZF_prod_set$] : ! % 104.07/15.24 [v3: ZF_ZF_prod_set_ZF_set_fun$] : (v1 = v0 | ~ (fun_app$aj(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$aj(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v2: ZF_ZF_ZF_prod_set_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (vce$(v3, v2) = v1) | ~ (vce$(v3, v2) = % 104.07/15.24 v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (van$(v3, v2) = v1) | ~ % 104.07/15.24 (van$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : % 104.07/15.24 ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (vao$(v3, v2) = v1) | ~ % 104.07/15.24 (vao$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! % 104.07/15.24 [v2: ZF_bool_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (uzj$(v3, v2) = v1) | ~ % 104.07/15.24 (uzj$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod$] % 104.07/15.24 : (v1 = v0 | ~ (uzk$(v3, v2) = v1) | ~ (uzk$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (uva$(v3, v2) = v1) | ~ (uva$(v3, v2) % 104.07/15.24 = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 104.07/15.24 ZF_bool_fun$] : ! [v3: ZF_bool_fun$] : (v1 = v0 | ~ (uvo$(v3, v2) = v1) | % 104.07/15.24 ~ (uvo$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (uvn$(v3, v2) = v1) | ~ (uvn$(v3, v2) % 104.07/15.24 = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 104.07/15.24 ZF_bool_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (uze$(v3, v2) = v1) | ~ % 104.07/15.24 (uze$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod$] % 104.07/15.24 : (v1 = v0 | ~ (uzd$(v3, v2) = v1) | ~ (uzd$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF$] % 104.07/15.24 : (v1 = v0 | ~ (uzg$(v3, v2) = v1) | ~ (uzg$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod$] : (v1 = v0 | ~ (uzf$(v3, v2) = % 104.07/15.24 v1) | ~ (uzf$(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.24 ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : ! [v3: ZF_set_set$] : (v1 = % 104.07/15.24 v0 | ~ (uuq$(v3, v2) = v1) | ~ (uuq$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 104.07/15.24 ZF_set$] : (v1 = v0 | ~ (uur$(v3, v2) = v1) | ~ (uur$(v3, v2) = v0)) & ! % 104.07/15.24 [v0: ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uup$(v3, % 104.07/15.24 v2) = v1) | ~ (uup$(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! % 104.07/15.24 [v1: ZF_set_bool_fun$] : ! [v2: ZF_set_set$] : ! [v3: ZF_set$] : (v1 = v0 | % 104.07/15.24 ~ (uzl$(v3, v2) = v1) | ~ (uzl$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! % 104.07/15.24 [v1: ZF_bool_fun$] : ! [v2: ZF_set$] : ! [v3: ZF$] : (v1 = v0 | ~ (uzm$(v3, % 104.07/15.24 v2) = v1) | ~ (uzm$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! % 104.07/15.24 [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod$] : % 104.07/15.24 (v1 = v0 | ~ (uzn$(v3, v2) = v1) | ~ (uzn$(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat$] : ! [v3: % 104.07/15.24 Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (fun_app$ai(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$ai(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_set_fun$] : ! [v2: Nat$] : ! [v3: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 % 104.07/15.24 | ~ (fun_app$ag(v3, v2) = v1) | ~ (fun_app$ag(v3, v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: ZF$] : ! [v3: % 104.07/15.24 ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (fun_app$ah(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$ah(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : % 104.07/15.24 ! [v2: ZF_bool_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (uul$(v3, v2) = v1) | ~ % 104.07/15.24 (uul$(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: % 104.07/15.24 ZF_bool_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (uum$(v3, v2) = v1) | ~ % 104.07/15.24 (uum$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : % 104.07/15.24 ! [v2: ZF$] : ! [v3: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (fun_app$af(v3, % 104.07/15.24 v2) = v1) | ~ (fun_app$af(v3, v2) = v0)) & ! [v0: ZF_ZF_prod$] : ! % 104.07/15.24 [v1: ZF_ZF_prod$] : ! [v2: Nat$] : ! [v3: Nat_ZF_ZF_prod_fun$] : (v1 = v0 | % 104.07/15.24 ~ (fun_app$ae(v3, v2) = v1) | ~ (fun_app$ae(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF$] : ! % 104.07/15.24 [v3: ZF_ZF_ZF_prod_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$ad(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] % 104.07/15.24 : ! [v2: ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_ZF_bool_fun_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$ac(v3, v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$ab(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$ab(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.24 Nat_set$] : ! [v3: Nat_set_ZF_set_fun$] : (v1 = v0 | ~ (fun_app$z(v3, v2) % 104.07/15.24 = v1) | ~ (fun_app$z(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: % 104.07/15.24 ZF_set_set$] : ! [v2: Nat_set$] : ! [v3: Nat_set_ZF_set_set_fun$] : (v1 = % 104.07/15.24 v0 | ~ (fun_app$aa(v3, v2) = v1) | ~ (fun_app$aa(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF_set$] : ! [v3: % 104.07/15.24 ZF_set_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$y(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$y(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.24 ZF_set_set$] : ! [v3: ZF_set_set_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$x(v3, v2) = v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: ZF_set$] : ! % 104.07/15.24 [v3: ZF_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (image$(v3, v2) = v1) | ~ % 104.07/15.24 (image$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] % 104.07/15.24 : ! [v2: ZF_ZF_prod_set_set$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$w(v3, v2) = % 104.07/15.24 v1) | ~ (fun_app$w(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! % 104.07/15.24 [v1: ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod$] : ! [v3: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$v(v3, v2) = % 104.07/15.24 v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 104.07/15.24 MultipleValueBool] : ! [v2: ZF_set_set$] : ! [v3: ZF_set$] : (v1 = v0 | ~ % 104.07/15.24 (member$b(v3, v2) = v1) | ~ (member$b(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_set$] : ! [v3: % 104.07/15.24 ZF_set_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$u(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$u(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_set$] : (v1 = v0 | % 104.07/15.24 ~ (sigma$(v3, v2) = v1) | ~ (sigma$(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: % 104.07/15.24 ZF$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (repl$(v3, v2) = % 104.07/15.24 v1) | ~ (repl$(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] % 104.07/15.24 : ! [v2: ZF$] : ! [v3: ZF_ZF_ZF_fun_fun$] : (v1 = v0 | ~ (fun_app$t(v3, v2) % 104.07/15.24 = v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: % 104.07/15.24 ZF_set_set$] : ! [v2: Nat$] : ! [v3: Nat_ZF_set_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$s(v3, v2) = v1) | ~ (fun_app$s(v3, v2) = v0)) & ! [v0: ZF_set$] : % 104.07/15.24 ! [v1: ZF_set$] : ! [v2: Nat$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF$] : ! [v3: % 104.07/15.24 ZF_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$q(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! % 104.07/15.24 [v2: ZF_set_set$] : ! [v3: ZF_set$] : (v1 = v0 | ~ (insert$b(v3, v2) = v1) | % 104.07/15.24 ~ (insert$b(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.24 ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$o(v3, v2) = v1) | ~ (fun_app$o(v3, v2) = v0)) & ! [v0: ZF$] : ! % 104.07/15.24 [v1: ZF$] : ! [v2: ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$p(v3, v2) = v1) | ~ (fun_app$p(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: % 104.07/15.24 Int_bool_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | ~ (fun_app$n(v3, % 104.07/15.24 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 104.07/15.24 ! [v2: Nat$] : ! [v3: Nat_bool_fun$] : (v1 = v0 | ~ (fun_app$m(v3, v2) = v1) % 104.07/15.24 | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 104.07/15.24 MultipleValueBool] : ! [v2: ZF_set$] : ! [v3: ZF_set_bool_fun$] : (v1 = v0 % 104.07/15.24 | ~ (fun_app$l(v3, v2) = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF_ZF_prod_set$] : % 104.07/15.24 ! [v3: ZF_ZF_prod_set_bool_fun$] : (v1 = v0 | ~ (fun_app$k(v3, v2) = v1) | % 104.07/15.24 ~ (fun_app$k(v3, v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_ZF_prod_set_fun$] : ! [v2: ZF$] : ! [v3: % 104.07/15.24 ZF_ZF_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$j(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v2: ZF$] : ! [v3: ZF_ZF_ZF_prod_set_fun$] : (v1 = v0 % 104.07/15.24 | ~ (fun_app$i(v3, v2) = v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set$] : ! % 104.07/15.24 [v3: ZF_ZF_prod$] : (v1 = v0 | ~ (insert$a(v3, v2) = v1) | ~ (insert$a(v3, % 104.07/15.24 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 104.07/15.24 ! [v2: ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_ZF_prod_fun$] : ! [v1: ZF_ZF_ZF_prod_fun$] : ! [v2: ZF$] : ! [v3: % 104.07/15.24 ZF_ZF_ZF_ZF_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$g(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$g(v3, v2) = v0)) & ! [v0: ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : ! % 104.07/15.24 [v2: ZF$] : ! [v3: ZF_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (fun_app$f(v3, v2) = % 104.07/15.24 v1) | ~ (fun_app$f(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: % 104.07/15.24 ZF_bool_fun$] : ! [v2: ZF$] : ! [v3: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ % 104.07/15.24 (fun_app$h(v3, v2) = v1) | ~ (fun_app$h(v3, v2) = v0)) & ! [v0: % 104.07/15.24 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF$] : ! [v3: % 104.07/15.24 ZF_bool_fun$] : (v1 = v0 | ~ (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, % 104.07/15.24 v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: Nat$] : ! [v3: % 104.07/15.24 Nat_ZF_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, % 104.07/15.24 v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: ZF$] : ! % 104.07/15.24 [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (fun_app$a(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$a(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.24 ZF_set$] : ! [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = % 104.07/15.24 v1) | ~ (fun_app$b(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: % 104.07/15.24 ZF$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (fun_app$(v3, v2) = v1) | ~ % 104.07/15.24 (fun_app$(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.24 ZF_set_bool_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ (inj_on$a(v2) = % 104.07/15.24 v1) | ~ (inj_on$a(v2) = v0)) & ! [v0: ZF_set_ZF_set_fun$] : ! [v1: % 104.07/15.24 ZF_set_ZF_set_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (sup$d(v2) = v1) | ~ % 104.07/15.24 (sup$d(v2) = v0)) & ! [v0: ZF_ZF_prod_set_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_set_set_ZF_set_set_fun$] : ! [v2: ZF_ZF_prod_set_ZF_set_fun$] : % 104.07/15.24 (v1 = v0 | ~ (image$ac(v2) = v1) | ~ (image$ac(v2) = v0)) & ! [v0: % 104.07/15.24 Nat_set_set_ZF_set_set_set_fun$] : ! [v1: Nat_set_set_ZF_set_set_set_fun$] % 104.07/15.24 : ! [v2: Nat_set_ZF_set_set_fun$] : (v1 = v0 | ~ (image$ab(v2) = v1) | ~ % 104.07/15.24 (image$ab(v2) = v0)) & ! [v0: Nat_nat_prod_ZF_ZF_prod_set_fun$] : ! [v1: % 104.07/15.24 Nat_nat_prod_ZF_ZF_prod_set_fun$] : ! [v2: Nat_nat_ZF_ZF_prod_set_fun_fun$] % 104.07/15.24 : (v1 = v0 | ~ (case_prod$k(v2) = v1) | ~ (case_prod$k(v2) = v0)) & ! [v0: % 104.07/15.24 Nat_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: Nat_ZF_prod_ZF_ZF_prod_set_fun$] % 104.07/15.24 : ! [v2: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (case_prod$j(v2) = % 104.07/15.24 v1) | ~ (case_prod$j(v2) = v0)) & ! [v0: % 104.07/15.24 ZF_nat_prod_ZF_ZF_prod_set_fun$] : ! [v1: ZF_nat_prod_ZF_ZF_prod_set_fun$] % 104.07/15.24 : ! [v2: ZF_nat_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (case_prod$i(v2) = % 104.07/15.24 v1) | ~ (case_prod$i(v2) = v0)) & ! [v0: ZF_set_set_ZF_set_set_set_fun$] % 104.07/15.24 : ! [v1: ZF_set_set_ZF_set_set_set_fun$] : ! [v2: ZF_set_ZF_set_set_fun$] : % 104.07/15.24 (v1 = v0 | ~ (image$u(v2) = v1) | ~ (image$u(v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_prod_bool_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : (v1 = v0 | ~ (case_prod$h(v2) = v1) % 104.07/15.24 | ~ (case_prod$h(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_prod_bool_fun$] : ! % 104.07/15.24 [v1: ZF_ZF_prod_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_ZF_bool_fun_fun$] : % 104.07/15.24 (v1 = v0 | ~ (case_prod$g(v2) = v1) | ~ (case_prod$g(v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_prod_set$] : ! [v1: ZF_ZF_prod_ZF_prod_set$] : ! [v2: % 104.07/15.24 ZF_ZF_prod_ZF_prod_bool_fun$] : (v1 = v0 | ~ (collect$g(v2) = v1) | ~ % 104.07/15.24 (collect$g(v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_prod_bool_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_ZF_prod_prod_bool_fun$] : ! [v2: ZF_ZF_ZF_prod_bool_fun_fun$] : (v1 = % 104.07/15.24 v0 | ~ (case_prod$f(v2) = v1) | ~ (case_prod$f(v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_ZF_prod_prod_set$] : ! [v1: ZF_ZF_ZF_prod_prod_set$] : ! [v2: % 104.07/15.24 ZF_ZF_ZF_prod_prod_bool_fun$] : (v1 = v0 | ~ (collect$f(v2) = v1) | ~ % 104.07/15.24 (collect$f(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_set_set_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_ZF_set_set_fun$] : ! [v2: ZF_ZF_ZF_set_set_fun_fun$] : (v1 = v0 % 104.07/15.24 | ~ (case_prod$e(v2) = v1) | ~ (case_prod$e(v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : % 104.07/15.24 ! [v2: ZF_ZF_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (case_prod$d(v2) = v1) | % 104.07/15.24 ~ (case_prod$d(v2) = v0)) & ! [v0: ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : % 104.07/15.24 ! [v2: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (the$e(v2) = v1) | ~ (the$e(v2) % 104.07/15.24 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_bool_fun$] : (v1 = v0 | ~ (uniq$b(v2) = v1) | ~ (uniq$b(v2) = v0)) & ! % 104.07/15.24 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (uniq$a(v2) = v1) | ~ (uniq$a(v2) = % 104.07/15.24 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 104.07/15.24 ZF_set_bool_fun$] : (v1 = v0 | ~ (uniq$(v2) = v1) | ~ (uniq$(v2) = v0)) & % 104.07/15.24 ! [v0: ZF_ZF_prod_ZF_set_fun$] : ! [v1: ZF_ZF_prod_ZF_set_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (case_prod$c(v2) = v1) | ~ % 104.07/15.24 (case_prod$c(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v2: ZF_ZF_ZF_ZF_prod_fun_fun$] : (v1 = v0 % 104.07/15.24 | ~ (case_prod$b(v2) = v1) | ~ (case_prod$b(v2) = v0)) & ! [v0: % 104.07/15.24 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.24 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (case_prod$a(v2) = v1) | ~ % 104.07/15.24 (case_prod$a(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_fun$] : ! [v1: % 104.07/15.24 ZF_ZF_prod_ZF_fun$] : ! [v2: ZF_ZF_ZF_fun_fun$] : (v1 = v0 | ~ % 104.07/15.25 (case_prod$(v2) = v1) | ~ (case_prod$(v2) = v0)) & ! [v0: Nat_set$] : ! % 104.07/15.25 [v1: Nat_set$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ (collect$e(v2) = v1) | % 104.07/15.25 ~ (collect$e(v2) = v0)) & ! [v0: ZF_set_ZF_ZF_prod_set_fun$] : ! [v1: % 104.07/15.25 ZF_set_ZF_ZF_prod_set_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ % 104.07/15.25 (product$a(v2) = v1) | ~ (product$a(v2) = v0)) & ! [v0: ZF_set$] : ! [v1: % 104.07/15.25 ZF_set$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (domain$a(v2) = v1) | ~ % 104.07/15.25 (domain$a(v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: % 104.07/15.25 ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | % 104.07/15.25 ~ (makeCat$(v2) = v1) | ~ (makeCat$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_set_ZF_set_prod_set$] : ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: % 104.07/15.25 ZF_set_ZF_set_prod_bool_fun$] : (v1 = v0 | ~ (collect$d(v2) = v1) | ~ % 104.07/15.25 (collect$d(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_ZF_ZF_prod_prod_bool_fun$] : (v1 = v0 | ~ (collect$c(v2) = v1) | % 104.07/15.25 ~ (collect$c(v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (trancl$(v2) = % 104.07/15.25 v1) | ~ (trancl$(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_set_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (ext$(v2) = v1) | % 104.07/15.25 ~ (ext$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_bool_fun$] % 104.07/15.25 : (v1 = v0 | ~ (least$d(v2) = v1) | ~ (least$d(v2) = v0)) & ! [v0: ZF_set$] % 104.07/15.25 : ! [v1: ZF_set$] : ! [v2: ZF_set_bool_fun$] : (v1 = v0 | ~ (least$c(v2) = % 104.07/15.25 v1) | ~ (least$c(v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set_bool_fun$] : (v1 = v0 | ~ % 104.07/15.25 (least$b(v2) = v1) | ~ (least$b(v2) = v0)) & ! [v0: int] : ! [v1: int] : % 104.07/15.25 ! [v2: Int_bool_fun$] : (v1 = v0 | ~ (least$a(v2) = v1) | ~ (least$a(v2) = % 104.07/15.25 v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | % 104.07/15.25 ~ (greatest$c(v2) = v1) | ~ (greatest$c(v2) = v0)) & ! [v0: Nat$] : ! % 104.07/15.25 [v1: Nat$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ (the$d(v2) = v1) | ~ % 104.07/15.25 (the$d(v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.25 ZF_set_bool_fun$] : (v1 = v0 | ~ (greatest$b(v2) = v1) | ~ (greatest$b(v2) % 104.07/15.25 = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: ZF_set_bool_fun$] : % 104.07/15.25 (v1 = v0 | ~ (the$c(v2) = v1) | ~ (the$c(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_set_bool_fun$] : (v1 = v0 | ~ (greatest$a(v2) = v1) | ~ % 104.07/15.25 (greatest$a(v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] % 104.07/15.25 : ! [v2: ZF_ZF_prod_set_bool_fun$] : (v1 = v0 | ~ (the$b(v2) = v1) | ~ % 104.07/15.25 (the$b(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: Int_bool_fun$] : % 104.07/15.25 (v1 = v0 | ~ (greatest$(v2) = v1) | ~ (greatest$(v2) = v0)) & ! [v0: int] : % 104.07/15.25 ! [v1: int] : ! [v2: Int_bool_fun$] : (v1 = v0 | ~ (the$a(v2) = v1) | ~ % 104.07/15.25 (the$a(v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_set$] : (v1 = v0 | ~ (ext_ZF_hull$(v2) = v1) | ~ % 104.07/15.25 (ext_ZF_hull$(v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! % 104.07/15.25 [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (ext_ZF$(v2) = v1) | ~ (ext_ZF$(v2) = % 104.07/15.25 v0)) & ! [v0: Nat_ZF_fun$] : ! [v1: Nat_ZF_fun$] : ! [v2: Nat$] : (v1 = % 104.07/15.25 v0 | ~ (natInterval$(v2) = v1) | ~ (natInterval$(v2) = v0)) & ! [v0: ZF$] % 104.07/15.25 : ! [v1: ZF$] : ! [v2: Nat_ZF_fun$] : (v1 = v0 | ~ (seqSum$(v2) = v1) | ~ % 104.07/15.25 (seqSum$(v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.25 ZF_set_bool_fun$] : (v1 = v0 | ~ (eps$b(v2) = v1) | ~ (eps$b(v2) = v0)) & % 104.07/15.25 ! [v0: ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : ! [v2: ZF_ZF_prod_bool_fun$] : % 104.07/15.25 (v1 = v0 | ~ (eps$a(v2) = v1) | ~ (eps$a(v2) = v0)) & ! [v0: ZF$] : ! [v1: % 104.07/15.25 ZF$] : ! [v2: ZF_bool_fun$] : (v1 = v0 | ~ (the$(v2) = v1) | ~ (the$(v2) % 104.07/15.25 = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: % 104.07/15.25 ZF_set_bool_fun$] : (v1 = v0 | ~ (collect$b(v2) = v1) | ~ (collect$b(v2) = % 104.07/15.25 v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: % 104.07/15.25 ZF$] : (v1 = v0 | ~ (zFTriple$(v2) = v1) | ~ (zFTriple$(v2) = v0)) & ! % 104.07/15.25 [v0: Nat_nat_set_fun$] : ! [v1: Nat_nat_set_fun$] : ! [v2: Nat_set$] : (v1 = % 104.07/15.25 v0 | ~ (vay$(v2) = v1) | ~ (vay$(v2) = v0)) & ! [v0: ZF_nat_set_fun$] : % 104.07/15.25 ! [v1: ZF_nat_set_fun$] : ! [v2: Nat_set$] : (v1 = v0 | ~ (vas$(v2) = v1) | % 104.07/15.25 ~ (vas$(v2) = v0)) & ! [v0: Nat_ZF_set_set_fun$] : ! [v1: % 104.07/15.25 Nat_ZF_set_set_fun$] : ! [v2: ZF_set_set$] : (v1 = v0 | ~ (uyg$(v2) = v1) % 104.07/15.25 | ~ (uyg$(v2) = v0)) & ! [v0: ZF_ZF_set_set_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_set_set_fun$] : ! [v2: ZF_set_set$] : (v1 = v0 | ~ (uwj$(v2) = v1) | % 104.07/15.25 ~ (uwj$(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_set_set_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_ZF_set_set_fun$] : ! [v2: ZF_set_set$] : (v1 = v0 | ~ (uwi$(v2) % 104.07/15.25 = v1) | ~ (uwi$(v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 104.07/15.25 Nat_ZF_set_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (uzc$(v2) = v1) | ~ % 104.07/15.25 (uzc$(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! % 104.07/15.25 [v2: ZF_set$] : (v1 = v0 | ~ (uwf$(v2) = v1) | ~ (uwf$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_prod_ZF_set_fun$] : ! [v1: ZF_ZF_prod_ZF_set_fun$] : ! [v2: ZF_set$] % 104.07/15.25 : (v1 = v0 | ~ (uwd$(v2) = v1) | ~ (uwd$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_ZF_prod_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_set$] : (v1 = v0 | ~ (uwe$(v2) = v1) | ~ (uwe$(v2) = v0)) & ! % 104.07/15.25 [v0: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_set_fun$] % 104.07/15.25 : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uwc$(v2) = v1) | ~ (uwc$(v2) = % 104.07/15.25 v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: tlbool] : % 104.07/15.25 (v1 = v0 | ~ (uyj$(v2) = v1) | ~ (uyj$(v2) = v0)) & ! [v0: ZF_bool_fun$] : % 104.07/15.25 ! [v1: ZF_bool_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ (uyi$(v2) = v1) | ~ % 104.07/15.25 (uyi$(v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_bool_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ (uyh$(v2) = v1) | ~ % 104.07/15.25 (uyh$(v2) = v0)) & ! [v0: Nat_ZF_fun$] : ! [v1: Nat_ZF_fun$] : ! [v2: % 104.07/15.25 ZF$] : (v1 = v0 | ~ (uux$(v2) = v1) | ~ (uux$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_set_ZF_fun$] : ! [v1: ZF_set_ZF_fun$] : ! [v2: ZF$] : (v1 = v0 | ~ % 104.07/15.25 (uzs$(v2) = v1) | ~ (uzs$(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_fun$] : ! % 104.07/15.25 [v1: ZF_ZF_prod_ZF_fun$] : ! [v2: ZF$] : (v1 = v0 | ~ (uzb$(v2) = v1) | ~ % 104.07/15.25 (uzb$(v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_bool_fun_fun$] : ! [v2: tlbool] : (v1 = v0 | ~ (vak$(v2) = v1) | ~ % 104.07/15.25 (vak$(v2) = v0)) & ! [v0: ZF_set_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.25 ZF_set_set_ZF_set_set_fun$] : ! [v2: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.25 (image$j(v2) = v1) | ~ (image$j(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_set_ZF_ZF_prod_set_fun$] : ! [v1: ZF_set_ZF_ZF_prod_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (image$g(v2) = v1) | ~ (image$g(v2) = % 104.07/15.25 v0)) & ! [v0: Nat_ZF_ZF_set_fun_fun$] : ! [v1: Nat_ZF_ZF_set_fun_fun$] : % 104.07/15.25 ! [v2: Nat_ZF_set_fun$] : (v1 = v0 | ~ (vaq$(v2) = v1) | ~ (vaq$(v2) = v0)) % 104.07/15.25 & ! [v0: ZF_ZF_ZF_set_fun_fun$] : ! [v1: ZF_ZF_ZF_set_fun_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_set_fun$] : (v1 = v0 | ~ (vau$(v2) = v1) | ~ (vau$(v2) = v0)) & ! % 104.07/15.25 [v0: ZF_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_bool_fun_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (uzi$(v2) = v1) | ~ (uzi$(v2) = v0)) % 104.07/15.25 & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uzh$(v2) = v1) | ~ (uzh$(v2) = v0)) & % 104.07/15.25 ! [v0: ZF_set_ZF_set_fun$] : ! [v1: ZF_set_ZF_set_fun$] : ! [v2: ZF_ZF_fun$] % 104.07/15.25 : (v1 = v0 | ~ (image$d(v2) = v1) | ~ (image$d(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_prod_set_ZF_set_fun$] : ! [v1: ZF_ZF_prod_set_ZF_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (image$c(v2) = v1) | ~ (image$c(v2) = % 104.07/15.25 v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: % 104.07/15.25 ZF$] : (v1 = v0 | ~ (uuc$(v2) = v1) | ~ (uuc$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_bool_fun_fun$] : ! [v2: ZF$] : (v1 = % 104.07/15.25 v0 | ~ (uui$(v2) = v1) | ~ (uui$(v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] % 104.07/15.25 : ! [v1: ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 104.07/15.25 (uvm$(v2) = v1) | ~ (uvm$(v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! % 104.07/15.25 [v1: ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uvl$(v2) % 104.07/15.25 = v1) | ~ (uvl$(v2) = v0)) & ! [v0: Nat_nat_ZF_set_fun_fun$] : ! [v1: % 104.07/15.25 Nat_nat_ZF_set_fun_fun$] : ! [v2: Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 104.07/15.25 (vbq$(v2) = v1) | ~ (vbq$(v2) = v0)) & ! [v0: ZF_nat_ZF_set_fun_fun$] : ! % 104.07/15.25 [v1: ZF_nat_ZF_set_fun_fun$] : ! [v2: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 104.07/15.25 (vbn$(v2) = v1) | ~ (vbn$(v2) = v0)) & ! [v0: Nat_ZF_ZF_set_fun_fun$] : ! % 104.07/15.25 [v1: Nat_ZF_ZF_set_fun_fun$] : ! [v2: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 104.07/15.25 (vbk$(v2) = v1) | ~ (vbk$(v2) = v0)) & ! [v0: ZF_ZF_ZF_set_fun_fun$] : ! % 104.07/15.25 [v1: ZF_ZF_ZF_set_fun_fun$] : ! [v2: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 104.07/15.25 (vbh$(v2) = v1) | ~ (vbh$(v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! % 104.07/15.25 [v2: ZF_bool_fun$] : (v1 = v0 | ~ (eps$(v2) = v1) | ~ (eps$(v2) = v0)) & ! % 104.07/15.25 [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: ZF$] : (v1 = v0 % 104.07/15.25 | ~ (uuh$(v2) = v1) | ~ (uuh$(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! % 104.07/15.25 [v1: ZF_ZF_set_fun$] : ! [v2: ZF_bool_fun$] : (v1 = v0 | ~ (vah$(v2) = v1) | % 104.07/15.25 ~ (vah$(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_set_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_ZF_set_fun$] : ! [v2: ZF_bool_fun$] : (v1 = v0 | ~ (vad$(v2) = % 104.07/15.25 v1) | ~ (vad$(v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_set_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_ZF_prod_set_fun$] : ! [v2: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ % 104.07/15.25 (vab$(v2) = v1) | ~ (vab$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : % 104.07/15.25 ! [v2: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (vaf$(v2) = v1) | ~ (vaf$(v2) = % 104.07/15.25 v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: % 104.07/15.25 Nat_ZF_set_fun$] : (v1 = v0 | ~ (uyu$(v2) = v1) | ~ (uyu$(v2) = v0)) & ! % 104.07/15.25 [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: Nat_ZF_fun$] : (v1 = v0 | % 104.07/15.25 ~ (uyv$(v2) = v1) | ~ (uyv$(v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : % 104.07/15.25 ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: Nat_ZF_ZF_prod_fun$] : (v1 = v0 | ~ % 104.07/15.25 (uyw$(v2) = v1) | ~ (uyw$(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.25 ZF_set_bool_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uyr$(v2) = v1) % 104.07/15.25 | ~ (uyr$(v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! % 104.07/15.25 [v2: ZF_ZF_fun$] : (v1 = v0 | ~ (uys$(v2) = v1) | ~ (uys$(v2) = v0)) & ! % 104.07/15.25 [v0: ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (uyt$(v2) = v1) | ~ (uyt$(v2) = v0)) & % 104.07/15.25 ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : % 104.07/15.25 (v1 = v0 | ~ (uyq$(v2) = v1) | ~ (uyq$(v2) = v0)) & ! [v0: ZF_bool_fun$] : % 104.07/15.25 ! [v1: ZF_bool_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uwg$(v2) = % 104.07/15.25 v1) | ~ (uwg$(v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] % 104.07/15.25 : ! [v2: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (vaj$(v2) = v1) | ~ (vaj$(v2) % 104.07/15.25 = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 104.07/15.25 ZF_bool_fun$] : (v1 = v0 | ~ (uuo$(v2) = v1) | ~ (uuo$(v2) = v0)) & ! % 104.07/15.25 [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_ZF_bool_fun_fun$] % 104.07/15.25 : (v1 = v0 | ~ (vbz$(v2) = v1) | ~ (vbz$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_ZF_prod_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_ZF_prod_bool_fun_fun$] : (v1 = v0 | ~ (vbt$(v2) = v1) | ~ (vbt$(v2) % 104.07/15.25 = v0)) & ! [v0: ZF_ZF_prod_ZF_set_fun$] : ! [v1: ZF_ZF_prod_ZF_set_fun$] % 104.07/15.25 : ! [v2: ZF_ZF_prod_ZF_bool_fun_fun$] : (v1 = v0 | ~ (vbv$(v2) = v1) | ~ % 104.07/15.25 (vbv$(v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 104.07/15.25 ZF_bool_fun$] : (v1 = v0 | ~ (collect$a(v2) = v1) | ~ (collect$a(v2) = % 104.07/15.25 v0)) & ! [v0: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_ZF_ZF_prod_bool_fun_fun$] : (v1 = v0 | ~ (vbx$(v2) = v1) | ~ % 104.07/15.25 (vbx$(v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! % 104.07/15.25 [v2: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (collect$(v2) = v1) | ~ % 104.07/15.25 (collect$(v2) = v0)) & ! [v0: Nat_set_ZF_set_fun$] : ! [v1: % 104.07/15.25 Nat_set_ZF_set_fun$] : ! [v2: Nat_ZF_set_fun$] : (v1 = v0 | ~ (vbe$(v2) = % 104.07/15.25 v1) | ~ (vbe$(v2) = v0)) & ! [v0: Nat_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.25 Nat_set_ZF_set_set_fun$] : ! [v2: Nat_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.25 (image$b(v2) = v1) | ~ (image$b(v2) = v0)) & ! [v0: ZF_set_ZF_set_fun$] : % 104.07/15.25 ! [v1: ZF_set_ZF_set_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ (vbf$(v2) % 104.07/15.25 = v1) | ~ (vbf$(v2) = v0)) & ! [v0: ZF_set_ZF_set_set_fun$] : ! [v1: % 104.07/15.25 ZF_set_ZF_set_set_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ % 104.07/15.25 (image$a(v2) = v1) | ~ (image$a(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_ZF_prod_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_set_fun$] : (v1 = v0 | ~ (vcb$(v2) = v1) | ~ (vcb$(v2) = v0)) & ! % 104.07/15.25 [v0: int] : ! [v1: int] : ! [v2: Nat$] : (v1 = v0 | ~ (of_nat$(v2) = v1) | % 104.07/15.25 ~ (of_nat$(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : (v1 = % 104.07/15.25 v0 | ~ (nat$(v2) = v1) | ~ (nat$(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! % 104.07/15.25 [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ (uvj$(v2) = v1) | % 104.07/15.25 ~ (uvj$(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] % 104.07/15.25 : ! [v2: ZF_set_set$] : (v1 = v0 | ~ (uu$(v2) = v1) | ~ (uu$(v2) = v0)) & % 104.07/15.25 ! [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: ZF$] : (v1 = v0 % 104.07/15.25 | ~ (member$a(v2) = v1) | ~ (member$a(v2) = v0)) & ! [v0: ZF_bool_fun$] : % 104.07/15.25 ! [v1: ZF_bool_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (uua$(v2) = v1) | ~ % 104.07/15.25 (uua$(v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uub$(v2) = % 104.07/15.25 v1) | ~ (uub$(v2) = v0)) & ! [v0: ZF_ZF_prod_set_bool_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_set_bool_fun$] : ! [v2: ZF_ZF_prod$] : (v1 = v0 | ~ % 104.07/15.25 (member$(v2) = v1) | ~ (member$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_set_ZF_ZF_prod_set_fun$] : ! [v1: ZF_set_ZF_ZF_prod_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_set_fun$] : (v1 = v0 | ~ (vap$(v2) = v1) | ~ (vap$(v2) = v0)) & ! % 104.07/15.25 [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: ZF_ZF_fun$] : (v1 = v0 | ~ % 104.07/15.25 (uuf$(v2) = v1) | ~ (uuf$(v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: % 104.07/15.25 ZF_bool_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (uzt$(v2) = v1) | ~ % 104.07/15.25 (uzt$(v2) = v0)) & ! [v0: Nat_ZF_set_set_fun$] : ! [v1: % 104.07/15.25 Nat_ZF_set_set_fun$] : ! [v2: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uzv$(v2) = % 104.07/15.25 v1) | ~ (uzv$(v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 104.07/15.25 Nat_ZF_set_fun$] : ! [v2: Nat_ZF_fun$] : (v1 = v0 | ~ (uzy$(v2) = v1) | ~ % 104.07/15.25 (uzy$(v2) = v0)) & ! [v0: ZF_ZF_set_set_fun$] : ! [v1: ZF_ZF_set_set_fun$] % 104.07/15.25 : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uzu$(v2) = v1) | ~ (uzu$(v2) = % 104.07/15.25 v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_fun$] : (v1 = v0 | ~ (uzw$(v2) = v1) | ~ (uzw$(v2) = v0)) & ! [v0: % 104.07/15.25 ZF_ZF_prod_ZF_set_fun$] : ! [v1: ZF_ZF_prod_ZF_set_fun$] : ! [v2: % 104.07/15.25 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uzx$(v2) = v1) | ~ (uzx$(v2) = v0)) & % 104.07/15.25 ! [v0: Int_bool_fun$] : ! [v1: Int_bool_fun$] : ! [v2: Int_bool_fun$] : (v1 % 104.07/15.25 = v0 | ~ (uvb$(v2) = v1) | ~ (uvb$(v2) = v0)) & ! [v0: Nat_bool_fun$] : % 104.07/15.25 ! [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ (uve$(v2) = v1) % 104.07/15.25 | ~ (uve$(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.25 ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : (v1 = v0 | ~ (uvd$(v2) = % 104.07/15.25 v1) | ~ (uvd$(v2) = v0)) & ! [v0: ZF_ZF_prod_set_bool_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_set_bool_fun$] : ! [v2: ZF_ZF_prod_set_bool_fun$] : (v1 = v0 | % 104.07/15.25 ~ (uvc$(v2) = v1) | ~ (uvc$(v2) = v0)) & ! [v0: Int_bool_fun$] : ! [v1: % 104.07/15.25 Int_bool_fun$] : ! [v2: Int_bool_fun$] : (v1 = v0 | ~ (uvf$(v2) = v1) | ~ % 104.07/15.25 (uvf$(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: % 104.07/15.25 Nat_bool_fun$] : (v1 = v0 | ~ (uvi$(v2) = v1) | ~ (uvi$(v2) = v0)) & ! % 104.07/15.25 [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ % 104.07/15.25 (less_eq$b(v2) = v1) | ~ (less_eq$b(v2) = v0)) & ! [v0: ZF_set_bool_fun$] % 104.07/15.25 : ! [v1: ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] : (v1 = v0 | ~ % 104.07/15.25 (uvh$(v2) = v1) | ~ (uvh$(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 104.07/15.25 ZF_set_bool_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (less_eq$a(v2) = v1) | % 104.07/15.25 ~ (less_eq$a(v2) = v0)) & ! [v0: ZF_ZF_prod_set_bool_fun$] : ! [v1: % 104.07/15.25 ZF_ZF_prod_set_bool_fun$] : ! [v2: ZF_ZF_prod_set_bool_fun$] : (v1 = v0 | % 104.07/15.25 ~ (uvg$(v2) = v1) | ~ (uvg$(v2) = v0)) & ! [v0: ZF_ZF_prod_set_bool_fun$] % 104.07/15.25 : ! [v1: ZF_ZF_prod_set_bool_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 104.07/15.25 (less_eq$(v2) = v1) | ~ (less_eq$(v2) = v0)) & ! [v0: ZF_set_ZF_set_fun$] % 104.07/15.25 : ! [v1: ZF_set_ZF_set_fun$] : ! [v2: ZF$] : (v1 = v0 | ~ (insert$(v2) = % 104.07/15.25 v1) | ~ (insert$(v2) = v0)) % 104.07/15.25 % 104.07/15.25 Further assumptions not needed in the proof: % 104.07/15.25 -------------------------------------------- % 104.07/15.25 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 104.07/15.25 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 104.07/15.25 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, % 104.07/15.25 axiom12, axiom120, axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, % 104.07/15.25 axiom127, axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, % 104.07/15.25 axiom134, axiom135, axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, % 104.07/15.25 axiom141, axiom142, axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, % 104.07/15.25 axiom149, axiom15, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, % 104.07/15.25 axiom156, axiom157, axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, % 104.07/15.25 axiom163, axiom164, axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, % 104.07/15.25 axiom170, axiom171, axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, % 104.07/15.25 axiom178, axiom179, axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, % 104.07/15.25 axiom185, axiom186, axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, % 104.07/15.25 axiom192, axiom193, axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, % 104.07/15.25 axiom2, axiom20, axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, % 104.07/15.25 axiom206, axiom207, axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, % 104.07/15.25 axiom213, axiom214, axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, % 104.07/15.25 axiom224, axiom225, axiom227, axiom229, axiom23, axiom230, axiom231, axiom232, % 104.07/15.25 axiom233, axiom234, axiom235, axiom236, axiom237, axiom238, axiom239, axiom24, % 104.07/15.25 axiom240, axiom241, axiom242, axiom243, axiom244, axiom246, axiom247, axiom248, % 104.07/15.25 axiom249, axiom25, axiom250, axiom251, axiom253, axiom254, axiom255, axiom256, % 104.07/15.25 axiom257, axiom258, axiom259, axiom26, axiom260, axiom261, axiom262, axiom263, % 104.07/15.25 axiom264, axiom265, axiom266, axiom267, axiom268, axiom269, axiom27, axiom270, % 104.07/15.25 axiom271, axiom272, axiom273, axiom274, axiom275, axiom276, axiom277, axiom278, % 104.07/15.25 axiom279, axiom28, axiom280, axiom281, axiom282, axiom283, axiom284, axiom285, % 104.07/15.25 axiom286, axiom287, axiom288, axiom289, axiom29, axiom290, axiom291, axiom292, % 104.07/15.25 axiom293, axiom294, axiom295, axiom296, axiom297, axiom298, axiom299, axiom3, % 104.07/15.25 axiom30, axiom300, axiom301, axiom302, axiom303, axiom304, axiom305, axiom306, % 104.07/15.25 axiom307, axiom308, axiom309, axiom31, axiom310, axiom311, axiom312, axiom313, % 104.07/15.25 axiom314, axiom315, axiom316, axiom317, axiom318, axiom319, axiom32, axiom320, % 104.07/15.25 axiom321, axiom322, axiom323, axiom324, axiom325, axiom326, axiom327, axiom328, % 104.07/15.25 axiom329, axiom33, axiom330, axiom331, axiom332, axiom333, axiom334, axiom335, % 104.07/15.25 axiom336, axiom337, axiom338, axiom339, axiom34, axiom340, axiom341, axiom342, % 104.07/15.25 axiom343, axiom344, axiom345, axiom346, axiom347, axiom348, axiom349, axiom35, % 104.07/15.25 axiom350, axiom351, axiom352, axiom353, axiom354, axiom355, axiom356, axiom357, % 104.07/15.25 axiom358, axiom359, axiom36, axiom360, axiom361, axiom362, axiom363, axiom364, % 104.07/15.25 axiom365, axiom366, axiom367, axiom368, axiom369, axiom37, axiom370, axiom371, % 104.07/15.25 axiom372, axiom373, axiom374, axiom375, axiom376, axiom377, axiom378, axiom379, % 104.07/15.25 axiom38, axiom380, axiom381, axiom382, axiom383, axiom384, axiom385, axiom386, % 104.07/15.25 axiom387, axiom388, axiom389, axiom39, axiom390, axiom391, axiom392, axiom393, % 104.07/15.25 axiom394, axiom395, axiom396, axiom397, axiom398, axiom399, axiom4, axiom40, % 104.07/15.25 axiom400, axiom401, axiom402, axiom403, axiom404, axiom405, axiom406, axiom407, % 104.07/15.25 axiom408, axiom409, axiom41, axiom410, axiom411, axiom412, axiom413, axiom414, % 104.07/15.25 axiom415, axiom416, axiom417, axiom418, axiom419, axiom42, axiom420, axiom421, % 104.07/15.25 axiom422, axiom423, axiom424, axiom425, axiom426, axiom427, axiom428, axiom429, % 104.07/15.25 axiom43, axiom430, axiom431, axiom432, axiom433, axiom434, axiom435, axiom436, % 104.07/15.25 axiom437, axiom438, axiom439, axiom44, axiom440, axiom441, axiom442, axiom443, % 104.07/15.25 axiom444, axiom445, axiom446, axiom447, axiom448, axiom449, axiom45, axiom450, % 104.07/15.25 axiom451, axiom452, axiom453, axiom454, axiom455, axiom456, axiom457, axiom458, % 104.07/15.25 axiom459, axiom46, axiom460, axiom461, axiom462, axiom463, axiom464, axiom465, % 104.07/15.25 axiom466, axiom467, axiom468, axiom469, axiom47, axiom470, axiom471, axiom472, % 104.07/15.25 axiom473, axiom474, axiom475, axiom476, axiom477, axiom478, axiom479, axiom48, % 104.07/15.25 axiom480, axiom481, axiom482, axiom483, axiom484, axiom485, axiom486, axiom487, % 104.07/15.25 axiom488, axiom489, axiom49, axiom490, axiom491, axiom492, axiom493, axiom494, % 104.07/15.25 axiom495, axiom496, axiom497, axiom498, axiom499, axiom5, axiom50, axiom500, % 104.07/15.25 axiom501, axiom502, axiom503, axiom504, axiom505, axiom506, axiom507, axiom508, % 104.07/15.25 axiom509, axiom51, axiom510, axiom511, axiom512, axiom513, axiom514, axiom515, % 104.07/15.25 axiom516, axiom517, axiom518, axiom519, axiom52, axiom520, axiom521, axiom522, % 104.07/15.25 axiom523, axiom524, axiom525, axiom526, axiom527, axiom528, axiom529, axiom53, % 104.07/15.25 axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, axiom536, axiom537, % 104.07/15.25 axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, axiom543, axiom544, % 104.07/15.25 axiom545, axiom546, axiom547, axiom548, axiom549, axiom55, axiom550, axiom551, % 104.07/15.25 axiom552, axiom553, axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, % 104.07/15.25 axiom56, axiom560, axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, % 104.07/15.25 axiom567, axiom568, axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, % 104.07/15.25 axiom574, axiom575, axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, % 104.07/15.25 axiom581, axiom582, axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, % 104.07/15.25 axiom589, axiom59, axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, % 104.07/15.25 axiom596, axiom597, axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, % 104.07/15.25 axiom602, axiom603, axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, % 104.07/15.25 axiom61, axiom610, axiom611, axiom612, axiom613, axiom614, axiom615, axiom616, % 104.07/15.25 axiom617, axiom618, axiom619, axiom62, axiom620, axiom621, axiom622, axiom623, % 104.07/15.25 axiom624, axiom625, axiom626, axiom627, axiom628, axiom629, axiom63, axiom630, % 104.07/15.25 axiom631, axiom632, axiom633, axiom634, axiom635, axiom636, axiom637, axiom638, % 104.07/15.25 axiom639, axiom64, axiom640, axiom641, axiom642, axiom643, axiom644, axiom645, % 104.07/15.25 axiom646, axiom647, axiom648, axiom649, axiom65, axiom650, axiom651, axiom652, % 104.07/15.25 axiom653, axiom654, axiom655, axiom656, axiom657, axiom658, axiom659, axiom66, % 104.07/15.25 axiom660, axiom661, axiom662, axiom663, axiom664, axiom665, axiom666, axiom667, % 104.07/15.25 axiom668, axiom669, axiom67, axiom670, axiom671, axiom672, axiom673, axiom674, % 104.07/15.25 axiom675, axiom676, axiom677, axiom678, axiom679, axiom68, axiom680, axiom681, % 104.07/15.25 axiom682, axiom683, axiom684, axiom685, axiom686, axiom687, axiom688, axiom689, % 104.07/15.25 axiom69, axiom690, axiom691, axiom692, axiom693, axiom694, axiom695, axiom696, % 104.07/15.25 axiom697, axiom698, axiom699, axiom7, axiom70, axiom700, axiom701, axiom702, % 104.07/15.25 axiom703, axiom704, axiom705, axiom706, axiom707, axiom708, axiom709, axiom71, % 104.07/15.25 axiom710, axiom711, axiom712, axiom713, axiom714, axiom715, axiom716, axiom717, % 104.07/15.25 axiom718, axiom719, axiom72, axiom720, axiom721, axiom722, axiom723, axiom724, % 104.07/15.25 axiom725, axiom726, axiom727, axiom728, axiom729, axiom73, axiom730, axiom731, % 104.07/15.25 axiom732, axiom733, axiom734, axiom735, axiom736, axiom737, axiom738, axiom739, % 104.07/15.25 axiom74, axiom740, axiom741, axiom742, axiom743, axiom744, axiom745, axiom746, % 104.07/15.25 axiom747, axiom748, axiom749, axiom75, axiom750, axiom751, axiom752, axiom753, % 104.07/15.25 axiom754, axiom755, axiom756, axiom757, axiom758, axiom759, axiom76, axiom760, % 104.07/15.25 axiom761, axiom762, axiom763, axiom764, axiom765, axiom766, axiom767, axiom768, % 104.07/15.25 axiom769, axiom77, axiom770, axiom771, axiom772, axiom773, axiom774, axiom775, % 104.07/15.25 axiom776, axiom777, axiom778, axiom779, axiom78, axiom780, axiom781, axiom782, % 104.07/15.25 axiom783, axiom784, axiom785, axiom786, axiom787, axiom788, axiom789, axiom79, % 104.07/15.25 axiom790, axiom791, axiom792, axiom793, axiom794, axiom795, axiom796, axiom797, % 104.07/15.25 axiom798, axiom799, axiom8, axiom80, axiom800, axiom801, axiom802, axiom803, % 104.07/15.25 axiom804, axiom805, axiom806, axiom807, axiom808, axiom809, axiom81, axiom810, % 104.07/15.25 axiom811, axiom812, axiom813, axiom814, axiom815, axiom816, axiom817, axiom818, % 104.07/15.25 axiom819, axiom82, axiom820, axiom821, axiom822, axiom823, axiom824, axiom825, % 104.07/15.25 axiom826, axiom827, axiom828, axiom829, axiom83, axiom830, axiom831, axiom832, % 104.07/15.25 axiom833, axiom834, axiom835, axiom836, axiom837, axiom838, axiom839, axiom84, % 104.07/15.25 axiom840, axiom841, axiom842, axiom843, axiom844, axiom845, axiom846, axiom847, % 104.07/15.25 axiom848, axiom849, axiom85, axiom850, axiom851, axiom852, axiom853, axiom86, % 104.07/15.25 axiom87, axiom88, axiom89, axiom9, axiom90, axiom91, axiom92, axiom93, axiom94, % 104.07/15.25 axiom95, axiom96, axiom97, axiom98, axiom99, formula_855, formula_856, % 104.07/15.25 formula_857, formula_858, formula_859, formula_860, formula_861, formula_862, % 104.07/15.25 formula_863, formula_864, formula_865, formula_866 % 104.07/15.25 % 104.07/15.25 Those formulas are unsatisfiable: % 104.07/15.25 --------------------------------- % 104.07/15.25 % 104.07/15.25 Begin of proof % 104.07/15.25 | % 104.07/15.25 | ALPHA: (axiom221) implies: % 104.07/15.25 | (1) fun_app$c(isZFfun$, f$) = 0 % 104.07/15.25 | % 104.07/15.25 | ALPHA: (axiom222) implies: % 104.07/15.26 | (2) ? [v0: ZF$] : ? [v1: ZF$] : (fun_app$(domain$, v1) = v0 & % 104.07/15.26 | fun_app$(zFfunDom$, f$) = v0 & fun_app$(snd$, f$) = v1 & ZF$(v1) & % 104.07/15.26 | ZF$(v0)) % 104.07/15.26 | % 104.07/15.26 | ALPHA: (axiom223) implies: % 104.37/15.26 | (3) ? [v0: ZF$] : (fun_app$c(isFun$, v0) = 0 & fun_app$(snd$, f$) = v0 & % 104.37/15.26 | ZF$(v0)) % 104.37/15.26 | % 104.37/15.26 | ALPHA: (axiom226) implies: % 104.37/15.26 | (4) ? [v0: ZF$] : ? [v1: ZF$] : ? [v2: ZF_ZF_fun$] : ? [v3: ZF$] : ? % 104.37/15.26 | [v4: ZF$] : ? [v5: ZF_ZF_fun$] : ? [v6: ZF$] : (fun_app$t(opair$, v4) % 104.37/15.26 | = v5 & fun_app$t(opair$, v1) = v2 & fun_app$(v5, v6) = f$ & % 104.37/15.26 | fun_app$(v2, v3) = v4 & fun_app$(fst$, v0) = v1 & fun_app$(fst$, f$) % 104.37/15.26 | = v0 & fun_app$(snd$, v0) = v3 & fun_app$(snd$, f$) = v6 & ZF$(v6) & % 104.37/15.26 | ZF$(v4) & ZF$(v3) & ZF$(v1) & ZF$(v0) & ZF_ZF_fun$(v5) & % 104.37/15.26 | ZF_ZF_fun$(v2)) % 104.37/15.26 | % 104.37/15.26 | ALPHA: (axiom228) implies: % 104.37/15.26 | (5) ? [v0: ZF$] : ? [v1: ZF_ZF_fun$] : ? [v2: ZF$] : ? [v3: ZF$] : ? % 104.37/15.26 | [v4: ZF_ZF_fun$] : ? [v5: ZF$] : (fun_app$t(opair$, v3) = v4 & % 104.37/15.26 | fun_app$t(opair$, v0) = v1 & fun_app$(v4, v5) = f$ & fun_app$(v1, v2) % 104.37/15.26 | = v3 & fun_app$(zFfunDom$, f$) = v0 & fun_app$(snd$, f$) = v5 & % 104.37/15.26 | fun_app$(zFfunCod$, f$) = v2 & ZF$(v5) & ZF$(v3) & ZF$(v2) & ZF$(v0) % 104.37/15.26 | & ZF_ZF_fun$(v4) & ZF_ZF_fun$(v1)) % 104.37/15.26 | % 104.37/15.26 | ALPHA: (axiom245) implies: % 104.37/15.26 | (6) ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF$] : ! % 104.37/15.26 | [v4: ZF_ZF_fun$] : ! [v5: ZF$] : ! [v6: ZF$] : ! [v7: any] : ( ~ % 104.37/15.26 | (fun_app$t(cartProd$, v3) = v4) | ~ (fun_app$h(subset$, v1) = v2) | % 104.37/15.26 | ~ (fun_app$c(v2, v6) = v7) | ~ (fun_app$(v4, v5) = v6) | ~ % 104.37/15.26 | (fun_app$(domain$, v1) = v3) | ~ (fun_app$(range$, v1) = v5) | ~ % 104.37/15.26 | (fun_app$(snd$, v0) = v1) | ~ ZF$(v0) | ? [v8: any] : ? [v9: any] % 104.37/15.26 | : ? [v10: ZF$] : ? [v11: any] : ? [v12: any] : ? [v13: ZF$] : ? % 104.37/15.26 | [v14: ZF_bool_fun$] : ? [v15: ZF$] : ? [v16: any] : % 104.37/15.26 | (fun_app$h(subset$, v5) = v14 & fun_app$c(v14, v15) = v16 & % 104.37/15.26 | fun_app$c(isZFfun$, v0) = v8 & fun_app$c(isFun$, v1) = v12 & % 104.37/15.26 | fun_app$c(isOpair$, v10) = v11 & fun_app$c(isOpair$, v0) = v9 & % 104.37/15.26 | fun_app$(zFfunDom$, v0) = v13 & fun_app$(fst$, v0) = v10 & % 104.37/15.26 | fun_app$(zFfunCod$, v0) = v15 & ZF$(v15) & ZF$(v13) & ZF$(v10) & % 104.37/15.26 | ZF_bool_fun$(v14) & ( ~ (v8 = 0) | (v16 = 0 & v13 = v3 & v12 = 0 & % 104.37/15.26 | v11 = 0 & v9 = 0 & v7 = 0)))) % 104.37/15.26 | % 104.37/15.26 | ALPHA: (axiom252) implies: % 104.37/15.26 | (7) ? [v0: ZF_ZF_fun$] : ? [v1: ZF$] : ? [v2: ZF_ZF_fun$] : % 104.37/15.26 | (fun_app$t(zFfunApp$, f$) = v0 & fun_app$t(app$, v1) = v2 & % 104.37/15.26 | fun_app$(snd$, f$) = v1 & ZF$(v1) & ZF_ZF_fun$(v2) & ZF_ZF_fun$(v0) & % 104.37/15.26 | ! [v3: ZF$] : ! [v4: ZF$] : ( ~ (fun_app$(v2, v3) = v4) | ~ % 104.37/15.26 | ZF$(v3) | (fun_app$(v0, v3) = v4 & ZF$(v4)))) % 104.37/15.26 | % 104.37/15.26 | ALPHA: (conjecture220) implies: % 104.37/15.26 | (8) ZF$(f$) % 104.37/15.26 | (9) ? [v0: ZF$] : ? [v1: ZF_bool_fun$] : ? [v2: ZF$] : ? [v3: % 104.37/15.26 | ZF_ZF_fun$] : ? [v4: ZF$] : ? [v5: ZF$] : ? [v6: int] : ( ~ (v6 = % 104.37/15.26 | 0) & fun_app$t(cartProd$, v2) = v3 & fun_app$h(subset$, v0) = v1 & % 104.37/15.26 | fun_app$c(v1, v5) = v6 & fun_app$(v3, v4) = v5 & fun_app$(domain$, % 104.37/15.26 | v0) = v2 & fun_app$(range$, v0) = v4 & fun_app$(snd$, f$) = v0 & % 104.37/15.26 | ZF$(v5) & ZF$(v4) & ZF$(v2) & ZF$(v0) & ZF_bool_fun$(v1) & % 104.37/15.26 | ZF_ZF_fun$(v3)) % 104.37/15.26 | % 104.37/15.26 | ALPHA: (function-axioms) implies: % 104.37/15.26 | (10) ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: ZF$] : ! [v3: ZF_ZF_fun$] : (v1 % 104.37/15.26 | = v0 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) = v0)) % 104.37/15.27 | (11) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF$] % 104.37/15.27 | : ! [v3: ZF_bool_fun$] : (v1 = v0 | ~ (fun_app$c(v3, v2) = v1) | ~ % 104.37/15.27 | (fun_app$c(v3, v2) = v0)) % 104.37/15.27 | % 104.41/15.27 | DELTA: instantiating (3) with fresh symbol all_986_0 gives: % 104.41/15.27 | (12) fun_app$c(isFun$, all_986_0) = 0 & fun_app$(snd$, f$) = all_986_0 & % 104.41/15.27 | ZF$(all_986_0) % 104.41/15.27 | % 104.41/15.27 | ALPHA: (12) implies: % 104.41/15.27 | (13) fun_app$(snd$, f$) = all_986_0 % 104.41/15.27 | % 104.41/15.27 | DELTA: instantiating (2) with fresh symbols all_1014_0, all_1014_1 gives: % 104.41/15.27 | (14) fun_app$(domain$, all_1014_0) = all_1014_1 & fun_app$(zFfunDom$, f$) = % 104.41/15.27 | all_1014_1 & fun_app$(snd$, f$) = all_1014_0 & ZF$(all_1014_0) & % 104.41/15.27 | ZF$(all_1014_1) % 104.41/15.27 | % 104.41/15.27 | ALPHA: (14) implies: % 104.41/15.27 | (15) fun_app$(snd$, f$) = all_1014_0 % 104.41/15.27 | (16) fun_app$(domain$, all_1014_0) = all_1014_1 % 104.41/15.27 | % 104.41/15.27 | DELTA: instantiating (7) with fresh symbols all_1040_0, all_1040_1, all_1040_2 % 104.41/15.27 | gives: % 104.41/15.27 | (17) fun_app$t(zFfunApp$, f$) = all_1040_2 & fun_app$t(app$, all_1040_1) = % 104.41/15.27 | all_1040_0 & fun_app$(snd$, f$) = all_1040_1 & ZF$(all_1040_1) & % 104.41/15.27 | ZF_ZF_fun$(all_1040_0) & ZF_ZF_fun$(all_1040_2) & ! [v0: ZF$] : ! % 104.41/15.27 | [v1: ZF$] : ( ~ (fun_app$(all_1040_0, v0) = v1) | ~ ZF$(v0) | % 104.41/15.27 | (fun_app$(all_1040_2, v0) = v1 & ZF$(v1))) % 104.41/15.27 | % 104.41/15.27 | ALPHA: (17) implies: % 104.41/15.27 | (18) fun_app$(snd$, f$) = all_1040_1 % 104.41/15.27 | % 104.41/15.27 | DELTA: instantiating (5) with fresh symbols all_1069_0, all_1069_1, % 104.41/15.27 | all_1069_2, all_1069_3, all_1069_4, all_1069_5 gives: % 104.41/15.27 | (19) fun_app$t(opair$, all_1069_2) = all_1069_1 & fun_app$t(opair$, % 104.41/15.27 | all_1069_5) = all_1069_4 & fun_app$(all_1069_1, all_1069_0) = f$ & % 104.41/15.27 | fun_app$(all_1069_4, all_1069_3) = all_1069_2 & fun_app$(zFfunDom$, % 104.41/15.27 | f$) = all_1069_5 & fun_app$(snd$, f$) = all_1069_0 & % 104.41/15.27 | fun_app$(zFfunCod$, f$) = all_1069_3 & ZF$(all_1069_0) & % 104.41/15.27 | ZF$(all_1069_2) & ZF$(all_1069_3) & ZF$(all_1069_5) & % 104.41/15.27 | ZF_ZF_fun$(all_1069_1) & ZF_ZF_fun$(all_1069_4) % 104.41/15.27 | % 104.41/15.27 | ALPHA: (19) implies: % 104.41/15.27 | (20) fun_app$(snd$, f$) = all_1069_0 % 104.41/15.27 | % 104.41/15.27 | DELTA: instantiating (9) with fresh symbols all_1071_0, all_1071_1, % 104.41/15.27 | all_1071_2, all_1071_3, all_1071_4, all_1071_5, all_1071_6 gives: % 104.41/15.27 | (21) ~ (all_1071_0 = 0) & fun_app$t(cartProd$, all_1071_4) = all_1071_3 & % 104.41/15.27 | fun_app$h(subset$, all_1071_6) = all_1071_5 & fun_app$c(all_1071_5, % 104.41/15.27 | all_1071_1) = all_1071_0 & fun_app$(all_1071_3, all_1071_2) = % 104.41/15.27 | all_1071_1 & fun_app$(domain$, all_1071_6) = all_1071_4 & % 104.41/15.27 | fun_app$(range$, all_1071_6) = all_1071_2 & fun_app$(snd$, f$) = % 104.41/15.27 | all_1071_6 & ZF$(all_1071_1) & ZF$(all_1071_2) & ZF$(all_1071_4) & % 104.41/15.27 | ZF$(all_1071_6) & ZF_bool_fun$(all_1071_5) & ZF_ZF_fun$(all_1071_3) % 104.41/15.27 | % 104.41/15.27 | ALPHA: (21) implies: % 104.41/15.27 | (22) ~ (all_1071_0 = 0) % 104.41/15.27 | (23) fun_app$(snd$, f$) = all_1071_6 % 104.41/15.27 | (24) fun_app$(range$, all_1071_6) = all_1071_2 % 104.41/15.27 | (25) fun_app$(domain$, all_1071_6) = all_1071_4 % 104.41/15.27 | (26) fun_app$(all_1071_3, all_1071_2) = all_1071_1 % 104.41/15.27 | (27) fun_app$c(all_1071_5, all_1071_1) = all_1071_0 % 104.41/15.27 | (28) fun_app$h(subset$, all_1071_6) = all_1071_5 % 104.41/15.27 | (29) fun_app$t(cartProd$, all_1071_4) = all_1071_3 % 104.41/15.27 | % 104.41/15.27 | DELTA: instantiating (4) with fresh symbols all_1078_0, all_1078_1, % 104.41/15.27 | all_1078_2, all_1078_3, all_1078_4, all_1078_5, all_1078_6 gives: % 104.41/15.27 | (30) fun_app$t(opair$, all_1078_2) = all_1078_1 & fun_app$t(opair$, % 104.41/15.27 | all_1078_5) = all_1078_4 & fun_app$(all_1078_1, all_1078_0) = f$ & % 104.41/15.27 | fun_app$(all_1078_4, all_1078_3) = all_1078_2 & fun_app$(fst$, % 104.41/15.27 | all_1078_6) = all_1078_5 & fun_app$(fst$, f$) = all_1078_6 & % 104.41/15.27 | fun_app$(snd$, all_1078_6) = all_1078_3 & fun_app$(snd$, f$) = % 104.41/15.27 | all_1078_0 & ZF$(all_1078_0) & ZF$(all_1078_2) & ZF$(all_1078_3) & % 104.41/15.27 | ZF$(all_1078_5) & ZF$(all_1078_6) & ZF_ZF_fun$(all_1078_1) & % 104.41/15.27 | ZF_ZF_fun$(all_1078_4) % 104.41/15.27 | % 104.41/15.27 | ALPHA: (30) implies: % 104.41/15.27 | (31) fun_app$(snd$, f$) = all_1078_0 % 104.41/15.27 | % 104.41/15.27 | GROUND_INST: instantiating (10) with all_1014_0, all_1040_1, f$, snd$, % 104.41/15.27 | simplifying with (15), (18) gives: % 104.41/15.27 | (32) all_1040_1 = all_1014_0 % 104.41/15.27 | % 104.41/15.27 | GROUND_INST: instantiating (10) with all_986_0, all_1071_6, f$, snd$, % 104.41/15.27 | simplifying with (13), (23) gives: % 104.41/15.27 | (33) all_1071_6 = all_986_0 % 104.41/15.27 | % 104.41/15.27 | GROUND_INST: instantiating (10) with all_1071_6, all_1078_0, f$, snd$, % 104.41/15.27 | simplifying with (23), (31) gives: % 104.41/15.27 | (34) all_1078_0 = all_1071_6 % 104.41/15.27 | % 104.41/15.27 | GROUND_INST: instantiating (10) with all_1069_0, all_1078_0, f$, snd$, % 104.41/15.27 | simplifying with (20), (31) gives: % 104.41/15.27 | (35) all_1078_0 = all_1069_0 % 104.41/15.27 | % 104.41/15.28 | GROUND_INST: instantiating (10) with all_1040_1, all_1078_0, f$, snd$, % 104.41/15.28 | simplifying with (18), (31) gives: % 104.41/15.28 | (36) all_1078_0 = all_1040_1 % 104.41/15.28 | % 104.41/15.28 | COMBINE_EQS: (34), (35) imply: % 104.41/15.28 | (37) all_1071_6 = all_1069_0 % 104.41/15.28 | % 104.41/15.28 | SIMP: (37) implies: % 104.41/15.28 | (38) all_1071_6 = all_1069_0 % 104.41/15.28 | % 104.41/15.28 | COMBINE_EQS: (35), (36) imply: % 104.41/15.28 | (39) all_1069_0 = all_1040_1 % 104.41/15.28 | % 104.41/15.28 | COMBINE_EQS: (33), (38) imply: % 104.41/15.28 | (40) all_1069_0 = all_986_0 % 104.41/15.28 | % 104.41/15.28 | SIMP: (40) implies: % 104.41/15.28 | (41) all_1069_0 = all_986_0 % 104.41/15.28 | % 104.41/15.28 | COMBINE_EQS: (39), (41) imply: % 104.41/15.28 | (42) all_1040_1 = all_986_0 % 104.41/15.28 | % 104.41/15.28 | SIMP: (42) implies: % 104.41/15.28 | (43) all_1040_1 = all_986_0 % 104.41/15.28 | % 104.41/15.28 | COMBINE_EQS: (32), (43) imply: % 104.41/15.28 | (44) all_1014_0 = all_986_0 % 104.41/15.28 | % 104.41/15.28 | SIMP: (44) implies: % 104.41/15.28 | (45) all_1014_0 = all_986_0 % 104.41/15.28 | % 104.41/15.28 | REDUCE: (28), (33) imply: % 104.41/15.28 | (46) fun_app$h(subset$, all_986_0) = all_1071_5 % 104.41/15.28 | % 104.41/15.28 | REDUCE: (25), (33) imply: % 104.41/15.28 | (47) fun_app$(domain$, all_986_0) = all_1071_4 % 104.41/15.28 | % 104.41/15.28 | REDUCE: (16), (45) imply: % 104.41/15.28 | (48) fun_app$(domain$, all_986_0) = all_1014_1 % 104.41/15.28 | % 104.41/15.28 | REDUCE: (24), (33) imply: % 104.41/15.28 | (49) fun_app$(range$, all_986_0) = all_1071_2 % 104.41/15.28 | % 104.41/15.28 | GROUND_INST: instantiating (10) with all_1014_1, all_1071_4, all_986_0, % 104.41/15.28 | domain$, simplifying with (47), (48) gives: % 104.41/15.28 | (50) all_1071_4 = all_1014_1 % 104.41/15.28 | % 104.41/15.28 | REDUCE: (29), (50) imply: % 104.41/15.28 | (51) fun_app$t(cartProd$, all_1014_1) = all_1071_3 % 104.41/15.28 | % 104.41/15.28 | GROUND_INST: instantiating (6) with f$, all_986_0, all_1071_5, all_1014_1, % 104.41/15.28 | all_1071_3, all_1071_2, all_1071_1, all_1071_0, simplifying with % 104.41/15.28 | (8), (13), (26), (27), (46), (48), (49), (51) gives: % 104.41/15.28 | (52) ? [v0: any] : ? [v1: any] : ? [v2: ZF$] : ? [v3: any] : ? [v4: % 104.41/15.28 | any] : ? [v5: ZF$] : ? [v6: ZF_bool_fun$] : ? [v7: ZF$] : ? [v8: % 104.41/15.28 | any] : (fun_app$h(subset$, all_1071_2) = v6 & fun_app$c(v6, v7) = v8 % 104.41/15.28 | & fun_app$c(isZFfun$, f$) = v0 & fun_app$c(isFun$, all_986_0) = v4 & % 104.41/15.28 | fun_app$c(isOpair$, v2) = v3 & fun_app$c(isOpair$, f$) = v1 & % 104.41/15.28 | fun_app$(zFfunDom$, f$) = v5 & fun_app$(fst$, f$) = v2 & % 104.41/15.28 | fun_app$(zFfunCod$, f$) = v7 & ZF$(v7) & ZF$(v5) & ZF$(v2) & % 104.41/15.28 | ZF_bool_fun$(v6) & ( ~ (v0 = 0) | (v8 = 0 & v5 = all_1014_1 & v4 = 0 % 104.41/15.28 | & v3 = 0 & v1 = 0 & all_1071_0 = 0))) % 104.41/15.28 | % 104.41/15.28 | DELTA: instantiating (52) with fresh symbols all_1210_0, all_1210_1, % 104.41/15.28 | all_1210_2, all_1210_3, all_1210_4, all_1210_5, all_1210_6, all_1210_7, % 104.41/15.28 | all_1210_8 gives: % 104.41/15.28 | (53) fun_app$h(subset$, all_1071_2) = all_1210_2 & fun_app$c(all_1210_2, % 104.41/15.28 | all_1210_1) = all_1210_0 & fun_app$c(isZFfun$, f$) = all_1210_8 & % 104.41/15.28 | fun_app$c(isFun$, all_986_0) = all_1210_4 & fun_app$c(isOpair$, % 104.41/15.28 | all_1210_6) = all_1210_5 & fun_app$c(isOpair$, f$) = all_1210_7 & % 104.41/15.28 | fun_app$(zFfunDom$, f$) = all_1210_3 & fun_app$(fst$, f$) = all_1210_6 % 104.41/15.28 | & fun_app$(zFfunCod$, f$) = all_1210_1 & ZF$(all_1210_1) & % 104.41/15.28 | ZF$(all_1210_3) & ZF$(all_1210_6) & ZF_bool_fun$(all_1210_2) & ( ~ % 104.41/15.28 | (all_1210_8 = 0) | (all_1210_0 = 0 & all_1210_3 = all_1014_1 & % 104.41/15.28 | all_1210_4 = 0 & all_1210_5 = 0 & all_1210_7 = 0 & all_1071_0 = % 104.41/15.28 | 0)) % 104.41/15.28 | % 104.41/15.28 | ALPHA: (53) implies: % 104.41/15.28 | (54) fun_app$c(isZFfun$, f$) = all_1210_8 % 104.41/15.28 | (55) ~ (all_1210_8 = 0) | (all_1210_0 = 0 & all_1210_3 = all_1014_1 & % 104.41/15.28 | all_1210_4 = 0 & all_1210_5 = 0 & all_1210_7 = 0 & all_1071_0 = 0) % 104.41/15.28 | % 104.41/15.28 | BETA: splitting (55) gives: % 104.41/15.28 | % 104.41/15.28 | Case 1: % 104.41/15.28 | | % 104.41/15.28 | | (56) ~ (all_1210_8 = 0) % 104.41/15.28 | | % 104.41/15.28 | | GROUND_INST: instantiating (11) with 0, all_1210_8, f$, isZFfun$, % 104.41/15.28 | | simplifying with (1), (54) gives: % 104.41/15.28 | | (57) all_1210_8 = 0 % 104.41/15.28 | | % 104.41/15.28 | | REDUCE: (56), (57) imply: % 104.41/15.28 | | (58) $false % 104.41/15.28 | | % 104.41/15.28 | | CLOSE: (58) is inconsistent. % 104.41/15.28 | | % 104.41/15.28 | Case 2: % 104.41/15.28 | | % 104.41/15.28 | | (59) all_1210_0 = 0 & all_1210_3 = all_1014_1 & all_1210_4 = 0 & % 104.41/15.28 | | all_1210_5 = 0 & all_1210_7 = 0 & all_1071_0 = 0 % 104.41/15.28 | | % 104.41/15.28 | | ALPHA: (59) implies: % 104.41/15.28 | | (60) all_1071_0 = 0 % 104.41/15.28 | | % 104.41/15.28 | | REDUCE: (22), (60) imply: % 104.41/15.28 | | (61) $false % 104.41/15.28 | | % 104.41/15.28 | | CLOSE: (61) is inconsistent. % 104.41/15.28 | | % 104.41/15.28 | End of split % 104.41/15.28 | % 104.41/15.28 End of proof % 104.41/15.29 % SZS output end Proof for theBenchmark % 104.41/15.29 % 104.41/15.29 14700ms %------------------------------------------------------------------------------