%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP302_1 : TPTP v8.1.2. Released v8.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n002.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:39 EDT 2023 % Result : Theorem 61.49s 8.71s % Output : Proof 95.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : ITP302_1 : TPTP v8.1.2. Released v8.0.0. % 0.12/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n002.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Sun Aug 27 13:12:48 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.62 ________ _____ % 0.20/0.62 ___ __ \_________(_)________________________________ % 0.20/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.62 % 0.20/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.62 (2023-06-19) % 0.20/0.62 % 0.20/0.62 (c) Philipp Rümmer, 2009-2023 % 0.20/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.62 Amanda Stjerna. % 0.20/0.62 Free software under BSD-3-Clause. % 0.20/0.62 % 0.20/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.62 % 0.20/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 18.88/3.24 Prover 5: Preprocessing ... % 18.88/3.25 Prover 0: Preprocessing ... % 18.88/3.26 Prover 1: Preprocessing ... % 18.88/3.29 Prover 4: Preprocessing ... % 20.70/3.43 Prover 3: Preprocessing ... % 20.70/3.43 Prover 2: Preprocessing ... % 20.70/3.47 Prover 6: Preprocessing ... % 49.98/7.22 Prover 1: Warning: ignoring some quantifiers % 50.13/7.31 Prover 3: Warning: ignoring some quantifiers % 52.05/7.50 Prover 3: Constructing countermodel ... % 52.48/7.56 Prover 1: Constructing countermodel ... % 54.03/7.76 Prover 6: Proving ... % 61.49/8.70 Prover 3: proved (8061ms) % 61.49/8.71 % 61.49/8.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 61.49/8.71 % 61.49/8.72 Prover 6: stopped % 61.67/8.73 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 61.67/8.73 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 67.24/9.53 Prover 4: Warning: ignoring some quantifiers % 72.16/10.12 Prover 4: Constructing countermodel ... % 72.16/10.13 Prover 8: Preprocessing ... % 72.77/10.16 Prover 7: Preprocessing ... % 77.87/10.88 Prover 5: Proving ... % 77.87/10.88 Prover 5: stopped % 77.87/10.88 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 79.35/11.00 Prover 0: Proving ... % 79.35/11.01 Prover 0: stopped % 79.35/11.01 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 82.21/11.47 Prover 1: Found proof (size 30) % 82.21/11.47 Prover 1: proved (10828ms) % 82.21/11.47 Prover 4: stopped % 87.44/12.07 Prover 10: Preprocessing ... % 87.44/12.08 Prover 8: Warning: ignoring some quantifiers % 88.05/12.20 Prover 11: Preprocessing ... % 89.88/12.35 Prover 8: Constructing countermodel ... % 89.88/12.38 Prover 8: stopped % 89.88/12.38 Prover 10: stopped % 91.24/12.56 Prover 2: Proving ... % 91.24/12.56 Prover 2: stopped % 91.53/12.64 Prover 11: stopped % 93.05/12.98 Prover 7: Warning: ignoring some quantifiers % 93.73/13.20 Prover 7: Constructing countermodel ... % 93.73/13.21 Prover 7: stopped % 93.73/13.21 % 93.73/13.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 93.73/13.22 % 93.73/13.23 % SZS output start Proof for theBenchmark % 94.18/13.29 Assumptions after simplification: % 94.18/13.29 --------------------------------- % 94.18/13.29 % 94.18/13.29 (axiom186) % 94.47/13.34 lSCategory$(c$) = 0 & A_b_b_c_LSCategory_ext_Category_ext$(c$) % 94.47/13.34 % 94.47/13.34 (axiom187) % 94.47/13.34 B$(f$) & A_b_b_c_LSCategory_ext_Category_ext$(c$) & ? [v0: B_set_bool_fun$] : % 94.47/13.34 ? [v1: B_set$] : (mor$(c$) = v1 & member$b(f$) = v0 & fun_app$m(v0, v1) = 0 & % 94.47/13.34 B_set_bool_fun$(v0) & B_set$(v1)) % 94.47/13.34 % 94.47/13.34 (axiom188) % 94.47/13.34 B$(g$) & A_b_b_c_LSCategory_ext_Category_ext$(c$) & ? [v0: B_set_bool_fun$] : % 94.47/13.34 ? [v1: B_set$] : (mor$(c$) = v1 & member$b(g$) = v0 & fun_app$m(v0, v1) = 0 & % 94.47/13.34 B_set_bool_fun$(v0) & B_set$(v1)) % 94.47/13.34 % 94.47/13.35 (axiom203) % 94.47/13.35 ! [v0: A_b_b_c_LSCategory_ext_Category_ext$] : ! [v1: B$] : ! [v2: % 94.47/13.35 B_a_fun$] : ! [v3: A$] : ! [v4: A_set_bool_fun$] : ! [v5: A_set$] : ! % 94.47/13.35 [v6: int] : (v6 = 0 | ~ (dom$(v0) = v2) | ~ (obj$(v0) = v5) | ~ % 94.47/13.35 (fun_app$bk(v2, v1) = v3) | ~ (member$c(v3) = v4) | ~ (fun_app$p(v4, v5) = % 94.47/13.35 v6) | ~ B$(v1) | ~ A_b_b_c_LSCategory_ext_Category_ext$(v0) | ? [v7: % 94.47/13.35 any] : ? [v8: B_set_bool_fun$] : ? [v9: B_set$] : ? [v10: any] : % 94.47/13.35 (category$(v0) = v7 & mor$(v0) = v9 & member$b(v1) = v8 & fun_app$m(v8, v9) % 94.47/13.35 = v10 & B_set_bool_fun$(v8) & B_set$(v9) & ( ~ (v10 = 0) | ~ (v7 = 0)))) % 94.47/13.35 % 94.47/13.35 (axiom212) % 94.47/13.35 ! [v0: A_b_b_c_LSCategory_ext_Category_ext$] : ( ~ (lSCategory$(v0) = 0) | ~ % 94.47/13.35 A_b_b_c_LSCategory_ext_Category_ext$(v0) | category$(v0) = 0) % 94.47/13.35 % 94.47/13.35 (conjecture185) % 94.47/13.36 B$(f$) & A_b_b_c_LSCategory_ext_Category_ext$(c$) & ? [v0: B_a_fun$] : ? % 94.47/13.36 [v1: A$] : ? [v2: A_set_bool_fun$] : ? [v3: A_set$] : ? [v4: int] : ( ~ (v4 % 94.47/13.36 = 0) & dom$(c$) = v0 & obj$(c$) = v3 & fun_app$bk(v0, f$) = v1 & % 94.47/13.36 member$c(v1) = v2 & fun_app$p(v2, v3) = v4 & A_set_bool_fun$(v2) & A$(v1) & % 94.47/13.36 A_set$(v3) & B_a_fun$(v0)) % 94.47/13.36 % 94.47/13.36 (function-axioms) % 95.22/13.51 ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: ZF_ZF_unit_Category_ext$] : ! % 95.22/13.51 [v2: Unit$] : ! [v3: ZF_ZF_ZF_fun_fun$] : ! [v4: ZF_ZF_fun$] : ! [v5: % 95.22/13.51 ZF_ZF_fun$] : ! [v6: ZF_ZF_fun$] : ! [v7: ZF_set$] : ! [v8: ZF_set$] : % 95.22/13.51 (v1 = v0 | ~ (category_ext$a(v8, v7, v6, v5, v4, v3, v2) = v1) | ~ % 95.22/13.51 (category_ext$a(v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: % 95.22/13.51 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v1: % 95.22/13.51 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v2: B_c_LSCategory_ext$] : ! % 95.22/13.51 [v3: B_b_b_fun_fun$] : ! [v4: A_b_fun$] : ! [v5: B_a_fun$] : ! [v6: % 95.22/13.51 B_a_fun$] : ! [v7: B_set$] : ! [v8: A_set$] : (v1 = v0 | ~ % 95.22/13.51 (category_ext$(v8, v7, v6, v5, v4, v3, v2) = v1) | ~ (category_ext$(v8, v7, % 95.22/13.51 v6, v5, v4, v3, v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_ZF_prod_prod_set$] : % 95.22/13.51 ! [v1: ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v2: ZF_ZF_prod_ZF_fun$] : ! % 95.22/13.51 [v3: ZF_ZF_prod_set$] : ! [v4: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 95.22/13.51 (relInvImage$b(v4, v3, v2) = v1) | ~ (relInvImage$b(v4, v3, v2) = v0)) & ! % 95.22/13.51 [v0: Nat_nat_prod_set$] : ! [v1: Nat_nat_prod_set$] : ! [v2: % 95.22/13.51 Nat_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_prod_set$] : ! [v4: Nat_set$] : % 95.22/13.51 (v1 = v0 | ~ (relInvImage$a(v4, v3, v2) = v1) | ~ (relInvImage$a(v4, v3, v2) % 95.22/13.51 = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: % 95.22/13.51 ZF_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_prod_set$] : ! [v4: ZF_set$] : (v1 % 95.22/13.51 = v0 | ~ (relInvImage$(v4, v3, v2) = v1) | ~ (relInvImage$(v4, v3, v2) = % 95.22/13.51 v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: tlbool] : % 95.22/13.51 ! [v3: ZF$] : ! [v4: ZF$] : (v1 = v0 | ~ (rec_set_bool$(v4, v3, v2) = v1) | % 95.22/13.51 ~ (rec_set_bool$(v4, v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: % 95.22/13.51 tlbool] : ! [v3: ZF$] : ! [v4: ZF$] : (v1 = v0 | ~ (rec_bool$(v4, v3, v2) % 95.22/13.51 = v1) | ~ (rec_bool$(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 95.22/13.51 [v1: MultipleValueBool] : ! [v2: ZF_ZF_unit_Category_ext$] : ! [v3: % 95.22/13.51 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v4: % 95.22/13.51 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.51 (functor_abbrev$(v4, v3, v2) = v1) | ~ (functor_abbrev$(v4, v3, v2) = v0)) % 95.22/13.51 & ! [v0: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.51 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v2: ZF$] : ! [v3: % 95.22/13.51 ZF_ZF_unit_Category_ext$] : ! [v4: ZF_ZF_unit_Category_ext$] : (v1 = v0 | % 95.22/13.51 ~ (constFunctor$e(v4, v3, v2) = v1) | ~ (constFunctor$e(v4, v3, v2) = v0)) % 95.22/13.51 & ! [v0: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v1: % 95.22/13.51 ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v2: A$] : ! [v3: % 95.22/13.51 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v4: ZF_ZF_unit_Category_ext$] : % 95.22/13.51 (v1 = v0 | ~ (constFunctor$d(v4, v3, v2) = v1) | ~ (constFunctor$d(v4, v3, % 95.22/13.51 v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: A$] : % 95.22/13.51 ! [v3: B$] : ! [v4: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ % 95.22/13.51 (mapsTo$(v4, v3, v2) = v1) | ~ (mapsTo$(v4, v3, v2) = v0)) & ! [v0: % 95.22/13.51 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.51 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v2: ZF$] : ! [v3: % 95.22/13.51 ZF_ZF_unit_Category_ext$] : ! [v4: ZF_ZF_unit_Category_ext$] : (v1 = v0 | % 95.22/13.51 ~ (constFunctor$c(v4, v3, v2) = v1) | ~ (constFunctor$c(v4, v3, v2) = v0)) % 95.22/13.51 & ! [v0: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v1: % 95.22/13.51 ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v2: A$] : ! [v3: % 95.22/13.51 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v4: ZF_ZF_unit_Category_ext$] : % 95.22/13.51 (v1 = v0 | ~ (constFunctor$b(v4, v3, v2) = v1) | ~ (constFunctor$b(v4, v3, % 95.22/13.51 v2) = v0)) & ! [v0: % 95.22/13.51 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.51 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v2: ZF$] : ! % 95.22/13.51 [v3: ZF_ZF_unit_Category_ext$] : ! [v4: A_b_b_c_LSCategory_ext_Category_ext$] % 95.22/13.51 : (v1 = v0 | ~ (constFunctor$a(v4, v3, v2) = v1) | ~ (constFunctor$a(v4, v3, % 95.22/13.51 v2) = v0)) & ! [v0: % 95.22/13.51 A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v1: % 95.22/13.51 A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v2: % 95.22/13.51 A$] : ! [v3: A_b_b_c_LSCategory_ext_Category_ext$] : ! [v4: % 95.22/13.51 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (constFunctor$(v4, v3, % 95.22/13.51 v2) = v1) | ~ (constFunctor$(v4, v3, v2) = v0)) & ! [v0: A_bool_fun$] % 95.22/13.51 : ! [v1: A_bool_fun$] : ! [v2: A_bool_fun$] : ! [v3: A_set$] : ! [v4: % 95.22/13.51 A_a_fun$] : (v1 = v0 | ~ (uvm$(v4, v3, v2) = v1) | ~ (uvm$(v4, v3, v2) = % 95.22/13.52 v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: B_bool_fun$] % 95.22/13.52 : ! [v3: A_set$] : ! [v4: A_b_fun$] : (v1 = v0 | ~ (uvq$(v4, v3, v2) = v1) % 95.22/13.52 | ~ (uvq$(v4, v3, v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] % 95.22/13.52 : ! [v2: ZF_bool_fun$] : ! [v3: A_set$] : ! [v4: A_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uvy$(v4, v3, v2) = v1) | ~ (uvy$(v4, v3, v2) = v0)) & ! [v0: B_bool_fun$] % 95.22/13.52 : ! [v1: B_bool_fun$] : ! [v2: A_bool_fun$] : ! [v3: B_set$] : ! [v4: % 95.22/13.52 B_a_fun$] : (v1 = v0 | ~ (uvo$(v4, v3, v2) = v1) | ~ (uvo$(v4, v3, v2) = % 95.22/13.52 v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! [v2: B_bool_fun$] % 95.22/13.52 : ! [v3: B_set$] : ! [v4: B_b_fun$] : (v1 = v0 | ~ (uvs$(v4, v3, v2) = v1) % 95.22/13.52 | ~ (uvs$(v4, v3, v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] % 95.22/13.52 : ! [v2: ZF_bool_fun$] : ! [v3: B_set$] : ! [v4: B_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uwa$(v4, v3, v2) = v1) | ~ (uwa$(v4, v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: A_bool_fun$] : ! % 95.22/13.52 [v3: ZF_set_set$] : ! [v4: ZF_set_a_fun$] : (v1 = v0 | ~ (uwe$(v4, v3, v2) = % 95.22/13.52 v1) | ~ (uwe$(v4, v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: % 95.22/13.52 ZF_bool_fun$] : ! [v2: A_bool_fun$] : ! [v3: ZF_set$] : ! [v4: ZF_a_fun$] % 95.22/13.52 : (v1 = v0 | ~ (uvu$(v4, v3, v2) = v1) | ~ (uvu$(v4, v3, v2) = v0)) & ! % 95.22/13.52 [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: B_bool_fun$] : ! [v3: % 95.22/13.52 ZF_set$] : ! [v4: ZF_b_fun$] : (v1 = v0 | ~ (uvw$(v4, v3, v2) = v1) | ~ % 95.22/13.52 (uvw$(v4, v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : % 95.22/13.52 ! [v2: ZF_bool_fun$] : ! [v3: ZF_set$] : ! [v4: ZF_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uwc$(v4, v3, v2) = v1) | ~ (uwc$(v4, v3, v2) = v0)) & ! [v0: A_bool_fun$] % 95.22/13.52 : ! [v1: A_bool_fun$] : ! [v2: A_bool_fun$] : ! [v3: A_set$] : ! [v4: % 95.22/13.52 A_a_fun$] : (v1 = v0 | ~ (uvl$(v4, v3, v2) = v1) | ~ (uvl$(v4, v3, v2) = % 95.22/13.52 v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! [v2: B_bool_fun$] % 95.22/13.52 : ! [v3: A_set$] : ! [v4: A_b_fun$] : (v1 = v0 | ~ (uvp$(v4, v3, v2) = v1) % 95.22/13.52 | ~ (uvp$(v4, v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: % 95.22/13.52 ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: A_set$] : ! [v4: A_ZF_fun$] % 95.22/13.52 : (v1 = v0 | ~ (uvx$(v4, v3, v2) = v1) | ~ (uvx$(v4, v3, v2) = v0)) & ! % 95.22/13.52 [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: A_bool_fun$] : ! [v3: % 95.22/13.52 B_set$] : ! [v4: B_a_fun$] : (v1 = v0 | ~ (uvn$(v4, v3, v2) = v1) | ~ % 95.22/13.52 (uvn$(v4, v3, v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! % 95.22/13.52 [v2: B_bool_fun$] : ! [v3: B_set$] : ! [v4: B_b_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uvr$(v4, v3, v2) = v1) | ~ (uvr$(v4, v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 95.22/13.52 B_set$] : ! [v4: B_ZF_fun$] : (v1 = v0 | ~ (uvz$(v4, v3, v2) = v1) | ~ % 95.22/13.52 (uvz$(v4, v3, v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! % 95.22/13.52 [v2: A_bool_fun$] : ! [v3: ZF_set_set$] : ! [v4: ZF_set_a_fun$] : (v1 = v0 | % 95.22/13.52 ~ (uwd$(v4, v3, v2) = v1) | ~ (uwd$(v4, v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: A_bool_fun$] : ! [v3: % 95.22/13.52 ZF_set$] : ! [v4: ZF_a_fun$] : (v1 = v0 | ~ (uvt$(v4, v3, v2) = v1) | ~ % 95.22/13.52 (uvt$(v4, v3, v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! % 95.22/13.52 [v2: B_bool_fun$] : ! [v3: ZF_set$] : ! [v4: ZF_b_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uvv$(v4, v3, v2) = v1) | ~ (uvv$(v4, v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 95.22/13.52 ZF_set$] : ! [v4: ZF_ZF_fun$] : (v1 = v0 | ~ (uwb$(v4, v3, v2) = v1) | ~ % 95.22/13.52 (uwb$(v4, v3, v2) = v0)) & ! [v0: B$] : ! [v1: B$] : ! [v2: B_b_prod$] : % 95.22/13.52 ! [v3: B_b_prod_set$] : ! [v4: B_b_prod_b_fun$] : (v1 = v0 | ~ % 95.22/13.52 (restrict$a(v4, v3, v2) = v1) | ~ (restrict$a(v4, v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF$] : ! [v1: ZF$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF$] : ! [v4: ZF$] : % 95.22/13.52 (v1 = v0 | ~ (zFfun$(v4, v3, v2) = v1) | ~ (zFfun$(v4, v3, v2) = v0)) & ! % 95.22/13.52 [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: Nat_nat_fun_set$] : ! [v3: % 95.22/13.52 Nat_nat_fun_ZF_set_fun$] : (v1 = v0 | ~ (image$bq(v3, v2) = v1) | ~ % 95.22/13.52 (image$bq(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! % 95.22/13.52 [v2: ZF_nat_fun_set$] : ! [v3: ZF_nat_fun_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$bp(v3, v2) = v1) | ~ (image$bp(v3, v2) = v0)) & ! [v0: ZF_set_set$] % 95.22/13.52 : ! [v1: ZF_set_set$] : ! [v2: Nat_ZF_fun_set$] : ! [v3: % 95.22/13.52 Nat_ZF_fun_ZF_set_fun$] : (v1 = v0 | ~ (image$bo(v3, v2) = v1) | ~ % 95.22/13.52 (image$bo(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! % 95.22/13.52 [v2: ZF_ZF_fun_set$] : ! [v3: ZF_ZF_fun_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$bn(v3, v2) = v1) | ~ (image$bn(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF_set_bool_fun$] % 95.22/13.52 : ! [v3: ZF_set_bool_fun$] : (v1 = v0 | ~ (less_eq$m(v3, v2) = v1) | ~ % 95.22/13.52 (less_eq$m(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.52 MultipleValueBool] : ! [v2: ZF_bool_fun$] : ! [v3: ZF_bool_fun$] : (v1 = % 95.22/13.52 v0 | ~ (less_eq$l(v3, v2) = v1) | ~ (less_eq$l(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: B_bool_fun$] : ! % 95.22/13.52 [v3: B_bool_fun$] : (v1 = v0 | ~ (less_eq$k(v3, v2) = v1) | ~ (less_eq$k(v3, % 95.22/13.52 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 95.22/13.52 ! [v2: A_bool_fun$] : ! [v3: A_bool_fun$] : (v1 = v0 | ~ (less_eq$j(v3, v2) % 95.22/13.52 = v1) | ~ (less_eq$j(v3, v2) = v0)) & ! [v0: ZF_bool_fun_set$] : ! [v1: % 95.22/13.52 ZF_bool_fun_set$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_bool_fun_fun$] : (v1 % 95.22/13.52 = v0 | ~ (image$bm(v3, v2) = v1) | ~ (image$bm(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_bool_fun_set$] : ! [v1: ZF_bool_fun_set$] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.52 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (image$bl(v3, v2) = v1) | ~ % 95.22/13.52 (image$bl(v3, v2) = v0)) & ! [v0: ZF_bool_fun_set$] : ! [v1: % 95.22/13.52 ZF_bool_fun_set$] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_ZF_bool_fun_fun$] % 95.22/13.52 : (v1 = v0 | ~ (image$bk(v3, v2) = v1) | ~ (image$bk(v3, v2) = v0)) & ! % 95.22/13.52 [v0: ZF_set_bool_fun_set$] : ! [v1: ZF_set_bool_fun_set$] : ! [v2: % 95.22/13.52 ZF_set_set_set$] : ! [v3: ZF_set_set_ZF_set_bool_fun_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$bj(v3, v2) = v1) | ~ (image$bj(v3, v2) = v0)) & ! [v0: % 95.22/13.52 B_bool_fun_set$] : ! [v1: B_bool_fun_set$] : ! [v2: B_set_set$] : ! [v3: % 95.22/13.52 B_set_b_bool_fun_fun$] : (v1 = v0 | ~ (image$bi(v3, v2) = v1) | ~ % 95.22/13.52 (image$bi(v3, v2) = v0)) & ! [v0: A_bool_fun_set$] : ! [v1: % 95.22/13.52 A_bool_fun_set$] : ! [v2: A_set_set$] : ! [v3: A_set_a_bool_fun_fun$] : % 95.22/13.52 (v1 = v0 | ~ (image$bh(v3, v2) = v1) | ~ (image$bh(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$bg(v3, v2) = v1) | ~ (image$bg(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: % 95.22/13.52 Nat_nat_prod_set$] : ! [v3: Nat_nat_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | % 95.22/13.52 ~ (image$bf(v3, v2) = v1) | ~ (image$bf(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: % 95.22/13.52 Nat_ZF_prod_set$] : ! [v3: Nat_ZF_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$be(v3, v2) = v1) | ~ (image$be(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: % 95.22/13.52 ZF_nat_prod_set$] : ! [v3: ZF_nat_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$bd(v3, v2) = v1) | ~ (image$bd(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_set_set$] : ! [v1: ZF_set_set_set$] : ! [v2: ZF_set_set$] : ! [v3: % 95.22/13.52 ZF_set_set_ZF_set_set_set_fun$] : (v1 = v0 | ~ (fun_app$dd(v3, v2) = v1) | % 95.22/13.52 ~ (fun_app$dd(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : % 95.22/13.52 ! [v2: ZF_ZF_prod_set_set$] : ! [v3: ZF_ZF_prod_set_set_ZF_set_set_fun$] : % 95.22/13.52 (v1 = v0 | ~ (fun_app$dc(v3, v2) = v1) | ~ (fun_app$dc(v3, v2) = v0)) & ! % 95.22/13.52 [v0: ZF_set_set_set$] : ! [v1: ZF_set_set_set$] : ! [v2: Nat_set_set$] : ! % 95.22/13.52 [v3: Nat_set_set_ZF_set_set_set_fun$] : (v1 = v0 | ~ (fun_app$db(v3, v2) = % 95.22/13.52 v1) | ~ (fun_app$db(v3, v2) = v0)) & ! [v0: ZF_set_set_set$] : ! [v1: % 95.22/13.52 ZF_set_set_set$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_set_set_fun$] : (v1 = % 95.22/13.52 v0 | ~ (image$bc(v3, v2) = v1) | ~ (image$bc(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_set_set$] : ! [v1: ZF_set_set_set$] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.52 ZF_ZF_set_set_fun$] : (v1 = v0 | ~ (image$bb(v3, v2) = v1) | ~ % 95.22/13.52 (image$bb(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! % 95.22/13.52 [v2: ZF_set_set_set$] : ! [v3: ZF_set_set_set_ZF_set_set_fun$] : (v1 = v0 | % 95.22/13.52 ~ (fun_app$da(v3, v2) = v1) | ~ (fun_app$da(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set_set$] : ! [v1: ZF_ZF_prod_set_set$] : ! [v2: Nat_set$] : ! % 95.22/13.52 [v3: Nat_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (image$ba(v3, v2) = v1) | ~ % 95.22/13.52 (image$ba(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set_set$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_set_set$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_ZF_prod_set_fun$] : % 95.22/13.52 (v1 = v0 | ~ (image$az(v3, v2) = v1) | ~ (image$az(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: Nat_set_set$] : ! [v3: % 95.22/13.52 Nat_set_ZF_set_fun$] : (v1 = v0 | ~ (image$ay(v3, v2) = v1) | ~ % 95.22/13.52 (image$ay(v3, v2) = v0)) & ! [v0: Nat_set_set$] : ! [v1: Nat_set_set$] : % 95.22/13.52 ! [v2: Nat_set$] : ! [v3: Nat_nat_set_fun$] : (v1 = v0 | ~ (image$ax(v3, v2) % 95.22/13.52 = v1) | ~ (image$ax(v3, v2) = v0)) & ! [v0: Nat_set_set$] : ! [v1: % 95.22/13.52 Nat_set_set$] : ! [v2: ZF_set$] : ! [v3: ZF_nat_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$aw(v3, v2) = v1) | ~ (image$aw(v3, v2) = v0)) & ! [v0: Nat_set$] : % 95.22/13.52 ! [v1: Nat_set$] : ! [v2: Nat_set_set$] : ! [v3: Nat_set_set_nat_set_fun$] : % 95.22/13.52 (v1 = v0 | ~ (fun_app$cz(v3, v2) = v1) | ~ (fun_app$cz(v3, v2) = v0)) & ! % 95.22/13.52 [v0: ZF_set_set_ZF_set_fun$] : ! [v1: ZF_set_set_ZF_set_fun$] : ! [v2: % 95.22/13.52 ZF_set_set_ZF_set_set_fun$] : ! [v3: ZF_set_set_ZF_set_fun$] : (v1 = v0 | % 95.22/13.52 ~ (comp$i(v3, v2) = v1) | ~ (comp$i(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_set_ZF_set_fun$] : ! [v1: ZF_set_set_ZF_set_fun$] : ! [v2: % 95.22/13.52 ZF_set_set_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (comp$j(v3, v2) = v1) | ~ (comp$j(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set_set_ZF_set_fun$] : ! [v1: ZF_ZF_prod_set_set_ZF_set_fun$] : % 95.22/13.52 ! [v2: ZF_ZF_prod_set_set_ZF_set_set_fun$] : ! [v3: ZF_set_set_ZF_set_fun$] : % 95.22/13.52 (v1 = v0 | ~ (comp$g(v3, v2) = v1) | ~ (comp$g(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set_set_ZF_set_fun$] : ! [v1: ZF_ZF_prod_set_set_ZF_set_fun$] : % 95.22/13.52 ! [v2: ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_set_ZF_set_fun$] : (v1 = v0 | ~ (comp$h(v3, v2) = v1) | ~ % 95.22/13.52 (comp$h(v3, v2) = v0)) & ! [v0: ZF_set_set_ZF_set_set_fun$] : ! [v1: % 95.22/13.52 ZF_set_set_ZF_set_set_fun$] : ! [v2: ZF_set_set_ZF_set_set_set_fun$] : ! % 95.22/13.52 [v3: ZF_set_set_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$e(v3, v2) = v1) | % 95.22/13.52 ~ (comp$e(v3, v2) = v0)) & ! [v0: ZF_set_set_ZF_set_set_fun$] : ! [v1: % 95.22/13.52 ZF_set_set_ZF_set_set_fun$] : ! [v2: ZF_set_set_ZF_set_fun$] : ! [v3: % 95.22/13.52 ZF_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$f(v3, v2) = v1) | ~ % 95.22/13.52 (comp$f(v3, v2) = v0)) & ! [v0: Nat_set_set_ZF_set_set_fun$] : ! [v1: % 95.22/13.52 Nat_set_set_ZF_set_set_fun$] : ! [v2: Nat_set_set_ZF_set_set_set_fun$] : ! % 95.22/13.52 [v3: ZF_set_set_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$c(v3, v2) = v1) | % 95.22/13.52 ~ (comp$c(v3, v2) = v0)) & ! [v0: Nat_set_set_ZF_set_set_fun$] : ! [v1: % 95.22/13.52 Nat_set_set_ZF_set_set_fun$] : ! [v2: Nat_set_set_nat_set_fun$] : ! [v3: % 95.22/13.52 Nat_set_ZF_set_set_fun$] : (v1 = v0 | ~ (comp$d(v3, v2) = v1) | ~ % 95.22/13.52 (comp$d(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set_set$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_set_set$] : ! [v2: ZF_set_set$] : ! [v3: % 95.22/13.52 ZF_set_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (image$as(v3, v2) = v1) | ~ % 95.22/13.52 (image$as(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set_set$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$cy(v3, v2) % 95.22/13.52 = v1) | ~ (fun_app$cy(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 95.22/13.52 [v1: MultipleValueBool] : ! [v2: Nat_set$] : ! [v3: Nat_set$] : (v1 = v0 | % 95.22/13.52 ~ (less_eq$i(v3, v2) = v1) | ~ (less_eq$i(v3, v2) = v0)) & ! [v0: ZF_set$] % 95.22/13.52 : ! [v1: ZF_set$] : ! [v2: B$] : ! [v3: B_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (fun_app$cx(v3, v2) = v1) | ~ (fun_app$cx(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: B_set$] : ! [v3: % 95.22/13.52 B_ZF_set_fun$] : (v1 = v0 | ~ (image$ar(v3, v2) = v1) | ~ (image$ar(v3, % 95.22/13.52 v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: % 95.22/13.52 A_set$] : ! [v3: A_ZF_set_fun$] : (v1 = v0 | ~ (image$aq(v3, v2) = v1) | % 95.22/13.52 ~ (image$aq(v3, v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.52 ZF$] : ! [v3: ZF_b_set_fun$] : (v1 = v0 | ~ (fun_app$cw(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$cw(v3, v2) = v0)) & ! [v0: B_set_set$] : ! [v1: B_set_set$] : ! % 95.22/13.52 [v2: ZF_set$] : ! [v3: ZF_b_set_fun$] : (v1 = v0 | ~ (image$ap(v3, v2) = v1) % 95.22/13.52 | ~ (image$ap(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 95.22/13.52 ZF$] : ! [v3: ZF_a_set_fun$] : (v1 = v0 | ~ (fun_app$cv(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$cv(v3, v2) = v0)) & ! [v0: A_set_set$] : ! [v1: A_set_set$] : ! % 95.22/13.52 [v2: ZF_set$] : ! [v3: ZF_a_set_fun$] : (v1 = v0 | ~ (image$ao(v3, v2) = v1) % 95.22/13.52 | ~ (image$ao(v3, v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.52 B$] : ! [v3: B_b_set_fun$] : (v1 = v0 | ~ (fun_app$cu(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$cu(v3, v2) = v0)) & ! [v0: B_set_set$] : ! [v1: B_set_set$] : ! % 95.22/13.52 [v2: B_set$] : ! [v3: B_b_set_fun$] : (v1 = v0 | ~ (image$an(v3, v2) = v1) | % 95.22/13.52 ~ (image$an(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 95.22/13.52 B$] : ! [v3: B_a_set_fun$] : (v1 = v0 | ~ (fun_app$ct(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$ct(v3, v2) = v0)) & ! [v0: A_set_set$] : ! [v1: A_set_set$] : ! % 95.22/13.52 [v2: B_set$] : ! [v3: B_a_set_fun$] : (v1 = v0 | ~ (image$am(v3, v2) = v1) | % 95.22/13.52 ~ (image$am(v3, v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.52 A$] : ! [v3: A_b_set_fun$] : (v1 = v0 | ~ (fun_app$cs(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$cs(v3, v2) = v0)) & ! [v0: B_set_set$] : ! [v1: B_set_set$] : ! % 95.22/13.52 [v2: A_set$] : ! [v3: A_b_set_fun$] : (v1 = v0 | ~ (image$al(v3, v2) = v1) | % 95.22/13.52 ~ (image$al(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 95.22/13.52 A$] : ! [v3: A_a_set_fun$] : (v1 = v0 | ~ (fun_app$cr(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$cr(v3, v2) = v0)) & ! [v0: A_set_set$] : ! [v1: A_set_set$] : ! % 95.22/13.52 [v2: A_set$] : ! [v3: A_a_set_fun$] : (v1 = v0 | ~ (image$ak(v3, v2) = v1) | % 95.22/13.52 ~ (image$ak(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: % 95.22/13.52 ZF_ZF_fun$] : ! [v3: ZF$] : (v1 = v0 | ~ (lambda$(v3, v2) = v1) | ~ % 95.22/13.52 (lambda$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v2: ZF_set$] : ! [v3: ZF_set$] : (v1 = v0 | ~ % 95.22/13.52 (product$(v3, v2) = v1) | ~ (product$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_fun$] : ! [v3: % 95.22/13.52 ZF_set$] : (v1 = v0 | ~ (gr$c(v3, v2) = v1) | ~ (gr$c(v3, v2) = v0)) & ! % 95.22/13.52 [v0: Nat_ZF_set_prod_set$] : ! [v1: Nat_ZF_set_prod_set$] : ! [v2: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v3: Nat_set$] : (v1 = v0 | ~ (gr$b(v3, v2) = v1) | % 95.22/13.52 ~ (gr$b(v3, v2) = v0)) & ! [v0: Nat_ZF_set_prod_set$] : ! [v1: % 95.22/13.52 Nat_ZF_set_prod_set$] : ! [v2: Nat_ZF_set_set_fun$] : ! [v3: Nat_set$] : % 95.22/13.52 (v1 = v0 | ~ (sigma$l(v3, v2) = v1) | ~ (sigma$l(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.52 Nat_ZF_set_prod_set$] : ! [v3: Nat_ZF_set_prod_set$] : (v1 = v0 | ~ % 95.22/13.52 (less_eq$h(v3, v2) = v1) | ~ (less_eq$h(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_ZF_prod_set$] : ! [v1: ZF_ZF_prod_ZF_prod_set$] : ! [v2: % 95.22/13.52 ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (gr$a(v3, v2) % 95.22/13.52 = v1) | ~ (gr$a(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.52 MultipleValueBool] : ! [v2: ZF_ZF_prod_ZF_prod_set$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_prod_set$] : (v1 = v0 | ~ (less_eq$g(v3, v2) = v1) | ~ % 95.22/13.52 (less_eq$g(v3, v2) = v0)) & ! [v0: ZF_ZF_set_prod_set$] : ! [v1: % 95.22/13.52 ZF_ZF_set_prod_set$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_set$] : (v1 = v0 % 95.22/13.52 | ~ (gr$(v3, v2) = v1) | ~ (gr$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.52 ZF_ZF_set_prod_set$] : ! [v3: ZF_ZF_set_prod_set$] : (v1 = v0 | ~ % 95.22/13.52 (less_eq$f(v3, v2) = v1) | ~ (less_eq$f(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_ZF_set_prod_set$] : ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_set_ZF_set_prod_fun$] : (v1 = v0 | % 95.22/13.52 ~ (image$aj(v3, v2) = v1) | ~ (image$aj(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_prod_set$] % 95.22/13.52 : ! [v2: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = % 95.22/13.52 v0 | ~ (sigma$k(v3, v2) = v1) | ~ (sigma$k(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_prod_set$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (image$ai(v3, % 95.22/13.52 v2) = v1) | ~ (image$ai(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_ZF_set_prod_set$] : ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: % 95.22/13.52 Nat_nat_prod_set$] : ! [v3: Nat_nat_prod_ZF_set_ZF_set_prod_fun$] : (v1 = % 95.22/13.52 v0 | ~ (image$ah(v3, v2) = v1) | ~ (image$ah(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_ZF_prod_prod_set$] : ! [v1: Nat_ZF_ZF_prod_prod_set$] : ! [v2: % 95.22/13.52 Nat_ZF_ZF_prod_set_fun$] : ! [v3: Nat_set$] : (v1 = v0 | ~ (sigma$j(v3, % 95.22/13.52 v2) = v1) | ~ (sigma$j(v3, v2) = v0)) & ! [v0: ZF_set_ZF_prod_set$] : % 95.22/13.52 ! [v1: ZF_set_ZF_prod_set$] : ! [v2: Nat_ZF_ZF_prod_prod_set$] : ! [v3: % 95.22/13.52 Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$] : (v1 = v0 | ~ (image$ag(v3, v2) = % 95.22/13.52 v1) | ~ (image$ag(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod_set$] : ! % 95.22/13.52 [v1: ZF_set_ZF_set_prod_set$] : ! [v2: Nat_ZF_prod_set$] : ! [v3: % 95.22/13.52 Nat_ZF_prod_ZF_set_ZF_set_prod_fun$] : (v1 = v0 | ~ (image$af(v3, v2) = v1) % 95.22/13.52 | ~ (image$af(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_nat_prod_set$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_nat_prod_set$] : ! [v2: ZF_ZF_prod_nat_set_fun$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_set$] : (v1 = v0 | ~ (sigma$i(v3, v2) = v1) | ~ (sigma$i(v3, % 95.22/13.52 v2) = v0)) & ! [v0: ZF_ZF_set_prod_set$] : ! [v1: ZF_ZF_set_prod_set$] % 95.22/13.52 : ! [v2: ZF_ZF_prod_nat_prod_set$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$] : (v1 = v0 | ~ (image$ae(v3, v2) = % 95.22/13.52 v1) | ~ (image$ae(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_prod_set$] : ! % 95.22/13.52 [v1: ZF_ZF_prod_ZF_prod_set$] : ! [v2: ZF_ZF_prod_ZF_set_fun$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_set$] : (v1 = v0 | ~ (sigma$g(v3, v2) = v1) | ~ (sigma$g(v3, % 95.22/13.52 v2) = v0)) & ! [v0: ZF_ZF_set_prod_set$] : ! [v1: ZF_ZF_set_prod_set$] % 95.22/13.52 : ! [v2: ZF_ZF_prod_ZF_prod_set$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$] : (v1 = v0 | ~ (image$ad(v3, v2) = % 95.22/13.52 v1) | ~ (image$ad(v3, v2) = v0)) & ! [v0: ZF_ZF_set_prod_set$] : ! [v1: % 95.22/13.52 ZF_ZF_set_prod_set$] : ! [v2: ZF_ZF_set_set_fun$] : ! [v3: ZF_set$] : (v1 % 95.22/13.52 = v0 | ~ (sigma$h(v3, v2) = v1) | ~ (sigma$h(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_ZF_set_prod_set$] : ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: % 95.22/13.52 ZF_nat_prod_set$] : ! [v3: ZF_nat_prod_ZF_set_ZF_set_prod_fun$] : (v1 = v0 % 95.22/13.52 | ~ (image$ac(v3, v2) = v1) | ~ (image$ac(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_ZF_prod_prod_set$] : ! [v1: ZF_ZF_ZF_prod_prod_set$] : ! [v2: % 95.22/13.52 ZF_ZF_ZF_prod_set_fun$] : ! [v3: ZF_set$] : (v1 = v0 | ~ (sigma$e(v3, v2) % 95.22/13.52 = v1) | ~ (sigma$e(v3, v2) = v0)) & ! [v0: ZF_set_ZF_prod_set$] : ! % 95.22/13.52 [v1: ZF_set_ZF_prod_set$] : ! [v2: ZF_ZF_ZF_prod_prod_set$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$] : (v1 = v0 | ~ (image$ab(v3, v2) = % 95.22/13.52 v1) | ~ (image$ab(v3, v2) = v0)) & ! [v0: ZF_set_ZF_prod_set$] : ! [v1: % 95.22/13.52 ZF_set_ZF_prod_set$] : ! [v2: ZF_set_ZF_set_fun$] : ! [v3: ZF_set_set$] : % 95.22/13.52 (v1 = v0 | ~ (sigma$f(v3, v2) = v1) | ~ (sigma$f(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set$] : ! % 95.22/13.52 [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (relcomp$(v3, v2) = v1) | ~ % 95.22/13.52 (relcomp$(v3, v2) = v0)) & ! [v0: Nat_nat_prod_set$] : ! [v1: % 95.22/13.52 Nat_nat_prod_set$] : ! [v2: Nat_nat_set_fun$] : ! [v3: Nat_set$] : (v1 = % 95.22/13.52 v0 | ~ (sigma$d(v3, v2) = v1) | ~ (sigma$d(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_prod_set$] : ! [v1: Nat_ZF_prod_set$] : ! [v2: Nat_ZF_set_fun$] : % 95.22/13.52 ! [v3: Nat_set$] : (v1 = v0 | ~ (sigma$c(v3, v2) = v1) | ~ (sigma$c(v3, v2) % 95.22/13.52 = v0)) & ! [v0: ZF_nat_prod_set$] : ! [v1: ZF_nat_prod_set$] : ! [v2: % 95.22/13.52 ZF_nat_set_fun$] : ! [v3: ZF_set$] : (v1 = v0 | ~ (sigma$b(v3, v2) = v1) | % 95.22/13.52 ~ (sigma$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.52 MultipleValueBool] : ! [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_set$] : % 95.22/13.52 (v1 = v0 | ~ (less_eq$e(v3, v2) = v1) | ~ (less_eq$e(v3, v2) = v0)) & ! % 95.22/13.52 [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_ZF_fun$] % 95.22/13.52 : ! [v3: ZF_ZF_prod_ZF_ZF_prod_prod_set$] : (v1 = v0 | ~ (relImage$b(v3, v2) % 95.22/13.52 = v1) | ~ (relImage$b(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod_set$] : % 95.22/13.52 ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: % 95.22/13.52 Nat_nat_prod_set$] : (v1 = v0 | ~ (relImage$a(v3, v2) = v1) | ~ % 95.22/13.52 (relImage$a(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod_set$] : ! [v1: % 95.22/13.52 ZF_set_ZF_set_prod_set$] : ! [v2: ZF_set_ZF_set_set_fun$] : ! [v3: % 95.22/13.52 ZF_set_set$] : (v1 = v0 | ~ (sigma$a(v3, v2) = v1) | ~ (sigma$a(v3, v2) = % 95.22/13.52 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.52 ZF_set_ZF_set_prod_set$] : ! [v3: ZF_set_ZF_set_prod_set$] : (v1 = v0 | ~ % 95.22/13.52 (less_eq$d(v3, v2) = v1) | ~ (less_eq$d(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_ZF_set_prod_set$] : ! [v1: ZF_set_ZF_set_prod_set$] : ! [v2: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v3: ZF_ZF_prod_set$] : (v1 = v0 | ~ (relImage$(v3, % 95.22/13.52 v2) = v1) | ~ (relImage$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! % 95.22/13.52 [v1: ZF_ZF_prod_set$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_ZF_prod_fun$] : (v1 % 95.22/13.52 = v0 | ~ (image$aa(v3, v2) = v1) | ~ (image$aa(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (image$z(v3, v2) = v1) | ~ (image$z(v3, % 95.22/13.52 v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: Nat_set$] : ! % 95.22/13.52 [v3: Nat_b_fun$] : (v1 = v0 | ~ (image$y(v3, v2) = v1) | ~ (image$y(v3, v2) % 95.22/13.52 = v0)) & ! [v0: B$] : ! [v1: B$] : ! [v2: Nat$] : ! [v3: Nat_b_fun$] : % 95.22/13.52 (v1 = v0 | ~ (fun_app$cq(v3, v2) = v1) | ~ (fun_app$cq(v3, v2) = v0)) & ! % 95.22/13.52 [v0: A_set$] : ! [v1: A_set$] : ! [v2: Nat_set$] : ! [v3: Nat_a_fun$] : (v1 % 95.22/13.52 = v0 | ~ (image$x(v3, v2) = v1) | ~ (image$x(v3, v2) = v0)) & ! [v0: A$] % 95.22/13.52 : ! [v1: A$] : ! [v2: Nat$] : ! [v3: Nat_a_fun$] : (v1 = v0 | ~ % 95.22/13.52 (fun_app$cp(v3, v2) = v1) | ~ (fun_app$cp(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_ZF_set_fun$] : ! [v1: A_ZF_set_fun$] : ! [v2: A$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (hOMCollection$(v3, % 95.22/13.52 v2) = v1) | ~ (hOMCollection$(v3, v2) = v0)) & ! [v0: ZF_set$] : ! % 95.22/13.52 [v1: ZF_set$] : ! [v2: A$] : ! [v3: A_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (fun_app$co(v3, v2) = v1) | ~ (fun_app$co(v3, v2) = v0)) & ! [v0: ZF_set$] % 95.22/13.52 : ! [v1: ZF_set$] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_ZF_fun$] : (v1 = v0 % 95.22/13.52 | ~ (image$w(v3, v2) = v1) | ~ (image$w(v3, v2) = v0)) & ! [v0: Nat_set$] % 95.22/13.52 : ! [v1: Nat_set$] : ! [v2: Nat_set$] : ! [v3: Nat_nat_fun$] : (v1 = v0 | % 95.22/13.52 ~ (image$v(v3, v2) = v1) | ~ (image$v(v3, v2) = v0)) & ! [v0: Nat_set$] : % 95.22/13.52 ! [v1: Nat_set$] : ! [v2: ZF_set$] : ! [v3: ZF_nat_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$u(v3, v2) = v1) | ~ (image$u(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set$] : ! % 95.22/13.52 [v3: ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (image$t(v3, v2) = v1) | ~ % 95.22/13.52 (image$t(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! % 95.22/13.52 [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$s(v3, v2) = v1) | ~ (image$s(v3, v2) = v0)) & ! [v0: ZF_set$] : ! % 95.22/13.52 [v1: ZF_set$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (image$r(v3, v2) = v1) | ~ (image$r(v3, v2) = v0)) & ! [v0: ZF_set_set$] : % 95.22/13.52 ! [v1: ZF_set_set$] : ! [v2: ZF_set_set$] : ! [v3: % 95.22/13.52 ZF_set_set_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$cn(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$cn(v3, v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: % 95.22/13.52 ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : ! [v3: % 95.22/13.52 ZF_ZF_fun_ZF_ZF_fun_fun$] : (v1 = v0 | ~ (id_update$(v3, v2) = v1) | ~ % 95.22/13.52 (id_update$(v3, v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: % 95.22/13.52 ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : ! [v3: % 95.22/13.52 ZF_ZF_fun_ZF_ZF_fun_fun$] : (v1 = v0 | ~ (cod_update$(v3, v2) = v1) | ~ % 95.22/13.52 (cod_update$(v3, v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: % 95.22/13.52 ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$] : (v1 = v0 | ~ (comp_update$(v3, % 95.22/13.52 v2) = v1) | ~ (comp_update$(v3, v2) = v0)) & ! [v0: MultipleValueBool] % 95.22/13.52 : ! [v1: MultipleValueBool] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_set$] : % 95.22/13.52 (v1 = v0 | ~ (less_eq$b(v3, v2) = v1) | ~ (less_eq$b(v3, v2) = v0)) & ! % 95.22/13.52 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: B_set$] : ! % 95.22/13.52 [v3: B_set$] : (v1 = v0 | ~ (less_eq$a(v3, v2) = v1) | ~ (less_eq$a(v3, v2) % 95.22/13.52 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.52 A_set$] : ! [v3: A_set$] : (v1 = v0 | ~ (less_eq$(v3, v2) = v1) | ~ % 95.22/13.52 (less_eq$(v3, v2) = v0)) & ! [v0: A_b_b_c_LSCategory_ext_Category_ext$] : % 95.22/13.52 ! [v1: A_b_b_c_LSCategory_ext_Category_ext$] : ! [v2: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v3: B_set_b_set_fun$] : (v1 = v0 % 95.22/13.52 | ~ (mor_update$a(v3, v2) = v1) | ~ (mor_update$a(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_unit_Category_ext$] : ! [v1: ZF_ZF_unit_Category_ext$] : ! [v2: % 95.22/13.52 ZF_ZF_unit_Category_ext$] : ! [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (mor_update$(v3, v2) = v1) | ~ (mor_update$(v3, v2) = v0)) & ! [v0: ZF$] : % 95.22/13.52 ! [v1: ZF$] : ! [v2: Unit$] : ! [v3: ZF$] : (v1 = v0 | ~ (rec_unit$(v3, % 95.22/13.52 v2) = v1) | ~ (rec_unit$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! % 95.22/13.52 [v1: ZF_bool_fun$] : ! [v2: Unit$] : ! [v3: ZF$] : (v1 = v0 | ~ % 95.22/13.52 (rec_set_unit$(v3, v2) = v1) | ~ (rec_set_unit$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_ZF_fun$] : ! [v1: A_ZF_fun$] : ! [v2: A$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (homSet$(v3, v2) = v1) % 95.22/13.52 | ~ (homSet$(v3, v2) = v0)) & ! [v0: B_c_LSCategory_ext$] : ! [v1: % 95.22/13.52 B_c_LSCategory_ext$] : ! [v2: C$] : ! [v3: B_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (lSCategory_ext$(v3, v2) = v1) | ~ (lSCategory_ext$(v3, v2) = v0)) & ! % 95.22/13.52 [v0: B_ZF_fun$] : ! [v1: B_ZF_fun$] : ! [v2: A$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (homFtorMap$(v3, v2) = % 95.22/13.52 v1) | ~ (homFtorMap$(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (restrict$d(v3, v2) = v1) | ~ (restrict$d(v3, v2) = v0)) & ! [v0: % 95.22/13.52 B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: B_set$] : ! [v3: B_a_fun$] : (v1 = % 95.22/13.52 v0 | ~ (restrict$b(v3, v2) = v1) | ~ (restrict$b(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_b_fun$] : ! [v1: A_b_fun$] : ! [v2: A_set$] : ! [v3: A_b_fun$] : (v1 = % 95.22/13.52 v0 | ~ (restrict$c(v3, v2) = v1) | ~ (restrict$c(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_ZF_fun$] : ! [v1: A_ZF_fun$] : ! [v2: B$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (homFtorMapContra$(v3, % 95.22/13.52 v2) = v1) | ~ (homFtorMapContra$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.52 ZF_ZF_prod_ZF_fun_set$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (member$l(v3, v2) = v1) | ~ (member$l(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.52 B_b_prod_b_fun_set$] : ! [v3: B_b_prod_b_fun$] : (v1 = v0 | ~ % 95.22/13.52 (member$k(v3, v2) = v1) | ~ (member$k(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v2: A$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (homFtorContra$a(v3, % 95.22/13.52 v2) = v1) | ~ (homFtorContra$a(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v2: A$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (homFtor$a(v3, v2) = % 95.22/13.52 v1) | ~ (homFtor$a(v3, v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : % 95.22/13.52 ! [v1: ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : ! [v3: % 95.22/13.52 Unit_unit_fun$] : (v1 = v0 | ~ (more_update$(v3, v2) = v1) | ~ % 95.22/13.52 (more_update$(v3, v2) = v0)) & ! [v0: Unit$] : ! [v1: Unit$] : ! [v2: % 95.22/13.52 Unit$] : ! [v3: Unit_unit_fun$] : (v1 = v0 | ~ (fun_app$cm(v3, v2) = v1) | % 95.22/13.52 ~ (fun_app$cm(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.52 MultipleValueBool] : ! [v2: B_b_prod_set$] : ! [v3: B_b_prod$] : (v1 = v0 % 95.22/13.52 | ~ (member$j(v3, v2) = v1) | ~ (member$j(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_b_fun_set$] : ! % 95.22/13.52 [v3: A_b_fun$] : (v1 = v0 | ~ (member$i(v3, v2) = v1) | ~ (member$i(v3, v2) % 95.22/13.52 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.52 A_b_fun$] : ! [v3: A_b_fun_bool_fun$] : (v1 = v0 | ~ (fun_app$cl(v3, v2) = % 95.22/13.52 v1) | ~ (fun_app$cl(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.52 MultipleValueBool] : ! [v2: B_a_fun_set$] : ! [v3: B_a_fun$] : (v1 = v0 | % 95.22/13.52 ~ (member$h(v3, v2) = v1) | ~ (member$h(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: B_a_fun$] : ! % 95.22/13.52 [v3: B_a_fun_bool_fun$] : (v1 = v0 | ~ (fun_app$ck(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$ck(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.52 MultipleValueBool] : ! [v2: B_ZF_fun_set$] : ! [v3: B_ZF_fun$] : (v1 = v0 % 95.22/13.52 | ~ (member$g(v3, v2) = v1) | ~ (member$g(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: B_ZF_fun$] : ! % 95.22/13.52 [v3: B_ZF_fun_bool_fun$] : (v1 = v0 | ~ (fun_app$cj(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$cj(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.52 MultipleValueBool] : ! [v2: ZF_ZF_fun_set$] : ! [v3: ZF_ZF_fun$] : (v1 = % 95.22/13.52 v0 | ~ (member$f(v3, v2) = v1) | ~ (member$f(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF_ZF_fun$] : ! % 95.22/13.52 [v3: ZF_ZF_fun_bool_fun$] : (v1 = v0 | ~ (fun_app$ci(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$ci(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_bool_fun_fun$] : ! [v2: ZF$] : ! [v3: ZF_ZF_unit_Category_ext$] : % 95.22/13.52 (v1 = v0 | ~ (mapsTo$a(v3, v2) = v1) | ~ (mapsTo$a(v3, v2) = v0)) & ! [v0: % 95.22/13.52 B_bool_fun$] : ! [v1: B_bool_fun$] : ! [v2: B$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (inverse_rel$(v3, v2) % 95.22/13.52 = v1) | ~ (inverse_rel$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v2: A$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (homFtorContra$(v3, % 95.22/13.52 v2) = v1) | ~ (homFtorContra$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.52 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : ! [v2: A$] : ! [v3: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (homFtor$(v3, v2) = % 95.22/13.52 v1) | ~ (homFtor$(v3, v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! % 95.22/13.52 [v1: ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : ! [v3: % 95.22/13.52 ZF_set_ZF_set_fun$] : (v1 = v0 | ~ (obj_update$a(v3, v2) = v1) | ~ % 95.22/13.52 (obj_update$a(v3, v2) = v0)) & ! [v0: A_b_b_c_LSCategory_ext_Category_ext$] % 95.22/13.52 : ! [v1: A_b_b_c_LSCategory_ext_Category_ext$] : ! [v2: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v3: A_set_a_set_fun$] : (v1 = v0 % 95.22/13.52 | ~ (obj_update$(v3, v2) = v1) | ~ (obj_update$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_unit_Category_ext$] : ! [v1: ZF_ZF_unit_Category_ext$] : ! [v2: % 95.22/13.52 ZF_ZF_unit_Category_ext$] : ! [v3: ZF_ZF_fun_ZF_ZF_fun_fun$] : (v1 = v0 | % 95.22/13.52 ~ (dom_update$a(v3, v2) = v1) | ~ (dom_update$a(v3, v2) = v0)) & ! [v0: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v1: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v2: % 95.22/13.52 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v3: B_a_fun_b_a_fun_fun$] : (v1 % 95.22/13.52 = v0 | ~ (dom_update$(v3, v2) = v1) | ~ (dom_update$(v3, v2) = v0)) & ! % 95.22/13.52 [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: B_a_fun$] : ! [v3: % 95.22/13.52 B_a_fun_b_a_fun_fun$] : (v1 = v0 | ~ (fun_app$ch(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$ch(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 95.22/13.52 ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_nat_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (fun_app$cg(v3, v2) = v1) | ~ (fun_app$cg(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$cf(v3, v2) = v1) | % 95.22/13.52 ~ (fun_app$cf(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_bool_fun_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: ZF_bool_fun$] : (v1 = % 95.22/13.52 v0 | ~ (uxg$(v3, v2) = v1) | ~ (uxg$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_nat_ZF_set_ZF_set_prod_fun_fun$] : ! [v1: % 95.22/13.52 Nat_nat_ZF_set_ZF_set_prod_fun_fun$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: % 95.22/13.52 Nat_ZF_set_fun$] : (v1 = v0 | ~ (uyb$(v3, v2) = v1) | ~ (uyb$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: Nat_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_set_ZF_set_prod_fun$] : ! [v2: Nat$] : ! [v3: % 95.22/13.52 Nat_nat_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$ce(v3, v2) = % 95.22/13.52 v1) | ~ (fun_app$ce(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_ZF_set_ZF_set_prod_fun_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_ZF_set_ZF_set_prod_fun_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: % 95.22/13.52 Nat_ZF_set_fun$] : (v1 = v0 | ~ (uxx$(v3, v2) = v1) | ~ (uxx$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_set_ZF_set_prod_fun$] : ! [v2: Nat$] : ! [v3: % 95.22/13.52 Nat_ZF_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$cd(v3, v2) = % 95.22/13.52 v1) | ~ (fun_app$cd(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : ! % 95.22/13.52 [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uxz$(v3, v2) = v1) | ~ (uxz$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_prod_ZF_set_ZF_prod_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_ZF_set_ZF_prod_fun$] : ! [v2: Nat$] : ! [v3: % 95.22/13.52 Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$cc(v3, v2) % 95.22/13.52 = v1) | ~ (fun_app$cc(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_nat_ZF_set_ZF_set_prod_fun_fun$] : ! [v1: % 95.22/13.52 ZF_nat_ZF_set_ZF_set_prod_fun_fun$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: % 95.22/13.52 ZF_ZF_set_fun$] : (v1 = v0 | ~ (uxp$(v3, v2) = v1) | ~ (uxp$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: Nat_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_set_ZF_set_prod_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.52 ZF_nat_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$cb(v3, v2) = % 95.22/13.52 v1) | ~ (fun_app$cb(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod$] : ! % 95.22/13.52 [v1: ZF_set_ZF_set_prod$] : ! [v2: Nat$] : ! [v3: % 95.22/13.52 Nat_ZF_set_ZF_set_prod_fun$] : (v1 = v0 | ~ (fun_app$ca(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$ca(v3, v2) = v0)) & ! [v0: ZF_ZF_ZF_set_ZF_set_prod_fun_fun$] : ! % 95.22/13.52 [v1: ZF_ZF_ZF_set_ZF_set_prod_fun_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: % 95.22/13.52 ZF_ZF_set_fun$] : (v1 = v0 | ~ (uyf$(v3, v2) = v1) | ~ (uyf$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_set_ZF_set_prod_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$bz(v3, v2) = v1) % 95.22/13.52 | ~ (fun_app$bz(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_prod$] : ! [v1: % 95.22/13.52 ZF_set_ZF_set_prod$] : ! [v2: ZF$] : ! [v3: ZF_ZF_set_ZF_set_prod_fun$] : % 95.22/13.52 (v1 = v0 | ~ (fun_app$by(v3, v2) = v1) | ~ (fun_app$by(v3, v2) = v0)) & ! % 95.22/13.52 [v0: ZF_set_ZF_set_prod$] : ! [v1: ZF_set_ZF_set_prod$] : ! [v2: ZF_set$] : % 95.22/13.52 ! [v3: ZF_set$] : (v1 = v0 | ~ (pair$d(v3, v2) = v1) | ~ (pair$d(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : ! % 95.22/13.52 [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uxm$(v3, v2) = v1) | ~ (uxm$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_prod_ZF_set_ZF_prod_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_ZF_set_ZF_prod_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$bx(v3, v2) = % 95.22/13.52 v1) | ~ (fun_app$bx(v3, v2) = v0)) & ! [v0: ZF_set_ZF_prod$] : ! [v1: % 95.22/13.52 ZF_set_ZF_prod$] : ! [v2: ZF_ZF_prod$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_set_ZF_prod_fun$] : (v1 = v0 | ~ (fun_app$bw(v3, v2) = v1) | % 95.22/13.52 ~ (fun_app$bw(v3, v2) = v0)) & ! [v0: ZF_set_ZF_prod$] : ! [v1: % 95.22/13.52 ZF_set_ZF_prod$] : ! [v2: ZF$] : ! [v3: ZF_set$] : (v1 = v0 | ~ % 95.22/13.52 (pair$c(v3, v2) = v1) | ~ (pair$c(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_ZF_ZF_prod_fun_fun$] : ! [v1: ZF_ZF_ZF_ZF_prod_fun_fun$] : ! [v2: % 95.22/13.52 ZF_ZF_fun$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (uyg$(v3, v2) = v1) | ~ % 95.22/13.52 (uyg$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$] : ! % 95.22/13.52 [v1: ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$] : ! [v2: Nat_ZF_set_fun$] : ! % 95.22/13.52 [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uxu$(v3, v2) = v1) | ~ (uxu$(v3, % 95.22/13.52 v2) = v0)) & ! [v0: Nat_ZF_ZF_set_prod_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_ZF_set_prod_fun$] : ! [v2: ZF_ZF_prod$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$bv(v3, v2) % 95.22/13.52 = v1) | ~ (fun_app$bv(v3, v2) = v0)) & ! [v0: ZF_ZF_set_prod$] : ! [v1: % 95.22/13.52 ZF_ZF_set_prod$] : ! [v2: Nat$] : ! [v3: Nat_ZF_ZF_set_prod_fun$] : (v1 = % 95.22/13.52 v0 | ~ (fun_app$bu(v3, v2) = v1) | ~ (fun_app$bu(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uxr$(v3, v2) = v1) | ~ (uxr$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_ZF_set_prod_fun$] : ! [v1: ZF_ZF_ZF_set_prod_fun$] : % 95.22/13.52 ! [v2: ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$] : (v1 = % 95.22/13.52 v0 | ~ (fun_app$bt(v3, v2) = v1) | ~ (fun_app$bt(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_set_prod$] : ! [v1: ZF_ZF_set_prod$] : ! [v2: ZF$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_set_prod_fun$] : (v1 = v0 | ~ (fun_app$bs(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$bs(v3, v2) = v0)) & ! [v0: ZF_ZF_set_prod$] : ! [v1: % 95.22/13.52 ZF_ZF_set_prod$] : ! [v2: ZF_set$] : ! [v3: ZF$] : (v1 = v0 | ~ % 95.22/13.52 (pair$b(v3, v2) = v1) | ~ (pair$b(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : % 95.22/13.52 ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uyd$(v3, v2) = v1) | ~ (uyd$(v3, % 95.22/13.52 v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v2: ZF_ZF_prod$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$] : (v1 = v0 | ~ (fun_app$br(v3, % 95.22/13.52 v2) = v1) | ~ (fun_app$br(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_nat_ZF_ZF_prod_set_fun_fun$] : ! [v1: Nat_nat_ZF_ZF_prod_set_fun_fun$] % 95.22/13.52 : ! [v2: Nat_ZF_set_fun$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uzt$(v3, v2) = v1) | ~ (uzt$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_ZF_prod_set_fun$] : ! [v1: Nat_ZF_ZF_prod_set_fun$] : ! [v2: Nat$] % 95.22/13.52 : ! [v3: Nat_nat_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (fun_app$bq(v3, v2) % 95.22/13.52 = v1) | ~ (fun_app$bq(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_nat_ZF_ZF_prod_set_fun_fun$] : ! [v1: ZF_nat_ZF_ZF_prod_set_fun_fun$] : % 95.22/13.52 ! [v2: Nat_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uzo$(v3, % 95.22/13.52 v2) = v1) | ~ (uzo$(v3, v2) = v0)) & ! [v0: Nat_ZF_ZF_prod_set_fun$] : % 95.22/13.52 ! [v1: Nat_ZF_ZF_prod_set_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.52 ZF_nat_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (fun_app$bp(v3, v2) = v1) | % 95.22/13.52 ~ (fun_app$bp(v3, v2) = v0)) & ! [v0: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : ! % 95.22/13.52 [v1: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: % 95.22/13.52 Nat_ZF_set_fun$] : (v1 = v0 | ~ (uzr$(v3, v2) = v1) | ~ (uzr$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_ZF_prod_set_fun$] : % 95.22/13.52 ! [v2: Nat$] : ! [v3: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.52 (fun_app$bo(v3, v2) = v1) | ~ (fun_app$bo(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_ZF_ZF_prod_set_fun_fun$] : ! [v1: ZF_ZF_ZF_ZF_prod_set_fun_fun$] : ! % 95.22/13.52 [v2: ZF_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uzu$(v3, v2) = % 95.22/13.52 v1) | ~ (uzu$(v3, v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_set_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_ZF_prod_set_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (fun_app$bn(v3, v2) = v1) | % 95.22/13.52 ~ (fun_app$bn(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_bool_fun_fun$] : ! [v3: ZF_bool_fun$] % 95.22/13.52 : (v1 = v0 | ~ (uxk$(v3, v2) = v1) | ~ (uxk$(v3, v2) = v0)) & ! [v0: A$] : % 95.22/13.52 ! [v1: A$] : ! [v2: A$] : ! [v3: A_a_fun$] : (v1 = v0 | ~ (fun_app$bm(v3, % 95.22/13.52 v2) = v1) | ~ (fun_app$bm(v3, v2) = v0)) & ! [v0: B$] : ! [v1: B$] : % 95.22/13.52 ! [v2: A$] : ! [v3: A_b_fun$] : (v1 = v0 | ~ (fun_app$bl(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$bl(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: B$] : ! % 95.22/13.52 [v3: B_a_fun$] : (v1 = v0 | ~ (fun_app$bk(v3, v2) = v1) | ~ (fun_app$bk(v3, % 95.22/13.52 v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.52 ZF_set_a_fun$] : (v1 = v0 | ~ (fun_app$bj(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$bj(v3, v2) = v0)) & ! [v0: A$] : ! [v1: A$] : ! [v2: ZF$] : ! % 95.22/13.52 [v3: ZF_a_fun$] : (v1 = v0 | ~ (fun_app$bi(v3, v2) = v1) | ~ (fun_app$bi(v3, % 95.22/13.52 v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: A_set$] : ! % 95.22/13.52 [v3: A_set_a_set_fun$] : (v1 = v0 | ~ (fun_app$bh(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$bh(v3, v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.52 A_set$] : ! [v3: A_b_fun$] : (v1 = v0 | ~ (image$o(v3, v2) = v1) | ~ % 95.22/13.52 (image$o(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 95.22/13.52 A_set$] : ! [v3: A_ZF_fun$] : (v1 = v0 | ~ (image$n(v3, v2) = v1) | ~ % 95.22/13.52 (image$n(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 95.22/13.52 B_set$] : ! [v3: B_a_fun$] : (v1 = v0 | ~ (image$m(v3, v2) = v1) | ~ % 95.22/13.52 (image$m(v3, v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.52 B_set$] : ! [v3: B_set_b_set_fun$] : (v1 = v0 | ~ (fun_app$bg(v3, v2) = % 95.22/13.52 v1) | ~ (fun_app$bg(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] % 95.22/13.52 : ! [v2: B_set$] : ! [v3: B_ZF_fun$] : (v1 = v0 | ~ (image$k(v3, v2) = v1) % 95.22/13.52 | ~ (image$k(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 95.22/13.52 ZF_set_set$] : ! [v3: ZF_set_a_fun$] : (v1 = v0 | ~ (image$j(v3, v2) = v1) % 95.22/13.52 | ~ (image$j(v3, v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 95.22/13.52 ZF_set$] : ! [v3: ZF_a_fun$] : (v1 = v0 | ~ (image$i(v3, v2) = v1) | ~ % 95.22/13.52 (image$i(v3, v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.52 ZF_set$] : ! [v3: ZF_b_fun$] : (v1 = v0 | ~ (image$h(v3, v2) = v1) | ~ % 95.22/13.52 (image$h(v3, v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_bool_fun_fun$] : ! [v2: ZF$] : ! [v3: tlbool] : (v1 = v0 | ~ % 95.22/13.52 (uuh$(v3, v2) = v1) | ~ (uuh$(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : % 95.22/13.52 ! [v1: ZF_set_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: Nat_ZF_set_fun$] : % 95.22/13.52 (v1 = v0 | ~ (uwf$(v3, v2) = v1) | ~ (uwf$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: ZF_bool_fun$] : ! % 95.22/13.52 [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uwg$(v3, v2) = v1) | ~ (uwg$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 95.22/13.52 ZF_bool_fun$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (uwi$(v3, v2) = v1) | ~ % 95.22/13.52 (uwi$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! % 95.22/13.52 [v2: ZF_ZF_prod_bool_fun$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uwh$(v3, v2) = v1) | ~ (uwh$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! % 95.22/13.52 [v1: ZF_bool_fun$] : ! [v2: A_set$] : ! [v3: A_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uwm$(v3, v2) = v1) | ~ (uwm$(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] % 95.22/13.52 : ! [v2: A$] : ! [v3: A_ZF_fun$] : (v1 = v0 | ~ (fun_app$bf(v3, v2) = v1) | % 95.22/13.52 ~ (fun_app$bf(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: % 95.22/13.52 ZF_bool_fun$] : ! [v2: B_set$] : ! [v3: B_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uwn$(v3, v2) = v1) | ~ (uwn$(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : % 95.22/13.52 ! [v1: ZF_set_bool_fun$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_set_fun$] : (v1 % 95.22/13.52 = v0 | ~ (uwj$(v3, v2) = v1) | ~ (uwj$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat_set$] : ! % 95.22/13.52 [v3: Nat$] : (v1 = v0 | ~ (member$e(v3, v2) = v1) | ~ (member$e(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 95.22/13.52 ZF_set_set$] : ! [v3: ZF_set_ZF_fun$] : (v1 = v0 | ~ (uwp$(v3, v2) = v1) | % 95.22/13.52 ~ (uwp$(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: ZF_set$] : % 95.22/13.52 ! [v3: ZF_set_ZF_fun$] : (v1 = v0 | ~ (fun_app$be(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$be(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 95.22/13.52 ZF_set_bool_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | % 95.22/13.52 ~ (uwk$(v3, v2) = v1) | ~ (uwk$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! % 95.22/13.52 [v1: ZF_bool_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uwo$(v3, v2) = v1) | ~ (uwo$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! % 95.22/13.52 [v1: ZF_bool_fun$] : ! [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_fun$] : % 95.22/13.52 (v1 = v0 | ~ (uwl$(v3, v2) = v1) | ~ (uwl$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF_ZF_prod_set$] : % 95.22/13.52 ! [v3: ZF_ZF_prod$] : (v1 = v0 | ~ (member$d(v3, v2) = v1) | ~ % 95.22/13.52 (member$d(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] % 95.22/13.52 : ! [v2: Nat_set$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uzp$(v3, v2) = % 95.22/13.52 v1) | ~ (uzp$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uzs$(v3, v2) = v1) | ~ (uzs$(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: % 95.22/13.52 Nat_set$] : ! [v2: Nat$] : ! [v3: Nat_nat_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (fun_app$bd(v3, v2) = v1) | ~ (fun_app$bd(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_nat_set_fun$] : ! % 95.22/13.52 [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uyq$(v3, v2) = v1) | ~ (uyq$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: ZF$] : ! [v3: % 95.22/13.52 ZF_nat_set_fun$] : (v1 = v0 | ~ (fun_app$bc(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$bc(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v2: ZF_nat_set_fun$] : ! [v3: Nat_ZF_set_fun$] : (v1 % 95.22/13.52 = v0 | ~ (uyp$(v3, v2) = v1) | ~ (uyp$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_ZF_set_fun$] : ! % 95.22/13.52 [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uys$(v3, v2) = v1) | ~ (uys$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uyr$(v3, v2) = % 95.22/13.52 v1) | ~ (uyr$(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v2: Nat_set$] : ! [v3: Nat_nat_ZF_set_fun_fun$] : % 95.22/13.52 (v1 = v0 | ~ (uze$(v3, v2) = v1) | ~ (uze$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.52 Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (uzb$(v3, v2) = v1) | ~ (uzb$(v3, % 95.22/13.52 v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 95.22/13.52 Nat_set$] : ! [v3: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (uyy$(v3, v2) = % 95.22/13.52 v1) | ~ (uyy$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_ZF_set_fun_fun$] : (v1 = % 95.22/13.52 v0 | ~ (uyv$(v3, v2) = v1) | ~ (uyv$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.52 ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (uyx$(v3, v2) = v1) | ~ (uyx$(v3, % 95.22/13.52 v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! % 95.22/13.52 [v2: ZF_set$] : ! [v3: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (uza$(v3, v2) % 95.22/13.52 = v1) | ~ (uza$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_ZF_set_fun_fun$] : (v1 % 95.22/13.52 = v0 | ~ (uzd$(v3, v2) = v1) | ~ (uzd$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_set$] : ! [v3: % 95.22/13.52 Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (uzg$(v3, v2) = v1) | ~ (uzg$(v3, % 95.22/13.52 v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! % 95.22/13.52 [v2: Nat_nat_fun$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uvk$(v3, v2) = % 95.22/13.52 v1) | ~ (uvk$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v2: ZF_nat_fun$] : ! [v3: Nat_ZF_set_fun$] : (v1 = v0 % 95.22/13.52 | ~ (uvj$(v3, v2) = v1) | ~ (uvj$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_ZF_set_fun$] : ! % 95.22/13.52 [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ (uve$(v3, v2) = v1) | ~ (uve$(v3, % 95.22/13.52 v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 95.22/13.52 ZF_ZF_set_fun$] : ! [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ (uvc$(v3, v2) % 95.22/13.52 = v1) | ~ (uvc$(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_set_fun$] : ! [v2: Nat_ZF_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 % 95.22/13.52 | ~ (uvg$(v3, v2) = v1) | ~ (uvg$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] % 95.22/13.52 : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF_ZF_set_fun$] : % 95.22/13.52 (v1 = v0 | ~ (uvf$(v3, v2) = v1) | ~ (uvf$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_ZF_set_fun$] : ! [v1: ZF_ZF_prod_ZF_set_fun$] : ! [v2: % 95.22/13.52 ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uvh$(v3, v2) % 95.22/13.52 = v1) | ~ (uvh$(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! % 95.22/13.52 [v2: ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.52 (fun_app$bb(v3, v2) = v1) | ~ (fun_app$bb(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod_ZF_fun$] : ! [v1: ZF_ZF_prod_ZF_fun$] : ! [v2: % 95.22/13.52 ZF_ZF_prod_ZF_fun$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (uvd$(v3, v2) = % 95.22/13.52 v1) | ~ (uvd$(v3, v2) = v0)) & ! [v0: Nat_ZF_fun$] : ! [v1: % 95.22/13.52 Nat_ZF_fun$] : ! [v2: Nat_ZF_ZF_prod_fun$] : ! [v3: ZF_ZF_prod_ZF_fun$] : % 95.22/13.52 (v1 = v0 | ~ (uwr$(v3, v2) = v1) | ~ (uwr$(v3, v2) = v0)) & ! [v0: % 95.22/13.52 ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : ! [v2: Nat$] : ! [v3: % 95.22/13.52 Nat_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (fun_app$ba(v3, v2) = v1) | ~ % 95.22/13.52 (fun_app$ba(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! % 95.22/13.52 [v2: ZF_ZF_ZF_prod_fun$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.52 (uwq$(v3, v2) = v1) | ~ (uwq$(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_fun$] % 95.22/13.52 : ! [v1: ZF_ZF_prod_ZF_fun$] : ! [v2: ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v3: % 95.22/13.52 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uvi$(v3, v2) = v1) | ~ (uvi$(v3, v2) = % 95.22/13.52 v0)) & ! [v0: ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : ! [v2: ZF_ZF_prod$] % 95.22/13.52 : ! [v3: ZF_ZF_prod_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (fun_app$az(v3, v2) = % 95.22/13.53 v1) | ~ (fun_app$az(v3, v2) = v0)) & ! [v0: ZF_set_ZF_set_set_fun$] : ! % 95.22/13.53 [v1: ZF_set_ZF_set_set_fun$] : ! [v2: Nat_set$] : ! [v3: Nat_ZF_set_fun$] : % 95.22/13.53 (v1 = v0 | ~ (uxa$(v3, v2) = v1) | ~ (uxa$(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_set_set_fun$] : ! [v1: ZF_ZF_set_set_fun$] : ! [v2: Nat_set$] : ! % 95.22/13.53 [v3: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uxw$(v3, v2) = v1) | ~ (uxw$(v3, v2) = % 95.22/13.53 v0)) & ! [v0: ZF_set_ZF_set_set_fun$] : ! [v1: ZF_set_ZF_set_set_fun$] : % 95.22/13.53 ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uwz$(v3, v2) = v1) % 95.22/13.53 | ~ (uwz$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_set_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_set_fun$] : (v1 = v0 % 95.22/13.53 | ~ (uxt$(v3, v2) = v1) | ~ (uxt$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] % 95.22/13.53 : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_set$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 % 95.22/13.53 | ~ (uyh$(v3, v2) = v1) | ~ (uyh$(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set_ZF_set_fun$] : ! [v1: ZF_set_ZF_set_fun$] : ! [v2: ZF_ZF_prod_set$] % 95.22/13.53 : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uxo$(v3, v2) = v1) | ~ % 95.22/13.53 (uxo$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : % 95.22/13.53 ! [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.53 (uxb$(v3, v2) = v1) | ~ (uxb$(v3, v2) = v0)) & ! [v0: Nat_ZF_set_set_fun$] % 95.22/13.53 : ! [v1: Nat_ZF_set_set_fun$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: % 95.22/13.53 ZF_ZF_set_fun$] : (v1 = v0 | ~ (uzk$(v3, v2) = v1) | ~ (uzk$(v3, v2) = % 95.22/13.53 v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: Nat$] : ! % 95.22/13.53 [v3: Nat_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$ay(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$ay(v3, v2) = v0)) & ! [v0: ZF_ZF_set_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_set_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_ZF_set_fun$] : % 95.22/13.53 (v1 = v0 | ~ (uzj$(v3, v2) = v1) | ~ (uzj$(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: ZF$] : ! [v3: % 95.22/13.53 ZF_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$ax(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$ax(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v2: Nat_ZF_set_fun$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 % 95.22/13.53 | ~ (uzm$(v3, v2) = v1) | ~ (uzm$(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] % 95.22/13.53 : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_ZF_set_fun$] : ! [v3: ZF_ZF_fun$] : % 95.22/13.53 (v1 = v0 | ~ (uzl$(v3, v2) = v1) | ~ (uzl$(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: Nat$] : ! [v3: % 95.22/13.53 Nat_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$aw(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$aw(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v2: Nat_ZF_ZF_prod_set_fun$] : ! [v3: % 95.22/13.53 ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uzi$(v3, v2) = v1) | ~ (uzi$(v3, v2) = % 95.22/13.53 v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF$] % 95.22/13.53 : ! [v3: ZF_ZF_ZF_prod_set_fun$] : (v1 = v0 | ~ (fun_app$av(v3, v2) = v1) | % 95.22/13.53 ~ (fun_app$av(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 95.22/13.53 ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_set_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.53 (fun_app$au(v3, v2) = v1) | ~ (fun_app$au(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_ZF_ZF_prod_set_fun$] % 95.22/13.53 : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uzh$(v3, v2) = v1) | ~ % 95.22/13.53 (uzh$(v3, v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! % 95.22/13.53 [v2: Nat$] : ! [v3: Nat_ZF_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$at(v3, v2) % 95.22/13.53 = v1) | ~ (fun_app$at(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_fun$] : ! [v2: B$] : ! [v3: A_b_b_c_LSCategory_ext_Category_ext$] : % 95.22/13.53 (v1 = v0 | ~ (uup$(v3, v2) = v1) | ~ (uup$(v3, v2) = v0)) & ! [v0: B$] : ! % 95.22/13.53 [v1: B$] : ! [v2: ZF$] : ! [v3: ZF_b_fun$] : (v1 = v0 | ~ (fun_app$as(v3, % 95.22/13.53 v2) = v1) | ~ (fun_app$as(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_fun$] : ! [v2: B$] : ! [v3: A_b_b_c_LSCategory_ext_Category_ext$] % 95.22/13.53 : (v1 = v0 | ~ (uuq$(v3, v2) = v1) | ~ (uuq$(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun$] : ! [v3: % 95.22/13.53 ZF_bool_fun$] : (v1 = v0 | ~ (uvb$(v3, v2) = v1) | ~ (uvb$(v3, v2) = v0)) % 95.22/13.53 & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: A_bool_fun$] : ! [v3: % 95.22/13.53 A_set$] : (v1 = v0 | ~ (uux$(v3, v2) = v1) | ~ (uux$(v3, v2) = v0)) & ! % 95.22/13.53 [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! [v2: B_bool_fun$] : ! [v3: % 95.22/13.53 B_set$] : (v1 = v0 | ~ (uuy$(v3, v2) = v1) | ~ (uuy$(v3, v2) = v0)) & ! % 95.22/13.53 [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun$] % 95.22/13.53 : ! [v3: ZF_set_set$] : (v1 = v0 | ~ (uuz$(v3, v2) = v1) | ~ (uuz$(v3, v2) % 95.22/13.53 = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 95.22/13.53 ZF_bool_fun$] : ! [v3: ZF_set$] : (v1 = v0 | ~ (uva$(v3, v2) = v1) | ~ % 95.22/13.53 (uva$(v3, v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! [v2: % 95.22/13.53 ZF$] : ! [v3: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (uuo$(v3, v2) = v1) | ~ (uuo$(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] % 95.22/13.53 : ! [v2: B$] : ! [v3: B_ZF_fun$] : (v1 = v0 | ~ (fun_app$ar(v3, v2) = v1) | % 95.22/13.53 ~ (fun_app$ar(v3, v2) = v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_fun_fun$] : ! [v2: ZF_ZF_ZF_fun_fun$] : ! [v3: % 95.22/13.53 ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$] : (v1 = v0 | ~ (fun_app$aq(v3, v2) % 95.22/13.53 = v1) | ~ (fun_app$aq(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! % 95.22/13.53 [v2: Nat$] : ! [v3: Nat_nat_fun$] : (v1 = v0 | ~ (fun_app$ap(v3, v2) = v1) | % 95.22/13.53 ~ (fun_app$ap(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: ZF$] % 95.22/13.53 : ! [v3: ZF_nat_fun$] : (v1 = v0 | ~ (fun_app$ao(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$ao(v3, v2) = v0)) & ! [v0: B_b_fun$] : ! [v1: B_b_fun$] : ! [v2: % 95.22/13.53 B$] : ! [v3: B_b_b_fun_fun$] : (v1 = v0 | ~ (fun_app$an(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$an(v3, v2) = v0)) & ! [v0: B$] : ! [v1: B$] : ! [v2: B$] : ! % 95.22/13.53 [v3: B_b_fun$] : (v1 = v0 | ~ (fun_app$am(v3, v2) = v1) | ~ (fun_app$am(v3, % 95.22/13.53 v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_fun$] : ! [v1: ZF_ZF_prod_ZF_fun$] : % 95.22/13.53 ! [v2: ZF_ZF_prod_set$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.53 (restrict$(v3, v2) = v1) | ~ (restrict$(v3, v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: B_b_prod$] : ! % 95.22/13.53 [v3: B_b_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$al(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$al(v3, v2) = v0)) & ! [v0: B_b_prod$] : ! [v1: B_b_prod$] : ! % 95.22/13.53 [v2: B$] : ! [v3: B$] : (v1 = v0 | ~ (pair$a(v3, v2) = v1) | ~ (pair$a(v3, % 95.22/13.53 v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! [v2: B$] : % 95.22/13.53 ! [v3: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (compDefined$a(v3, v2) = v1) | ~ (compDefined$a(v3, v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF_ZF_prod$] : ! % 95.22/13.53 [v3: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ (fun_app$ak(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$ak(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: Nat$] : % 95.22/13.53 ! [v3: Nat_ZF_fun$] : (v1 = v0 | ~ (fun_app$aj(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$aj(v3, v2) = v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: % 95.22/13.53 ZF_ZF_prod$] : ! [v3: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (fun_app$ai(v3, % 95.22/13.53 v2) = v1) | ~ (fun_app$ai(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! % 95.22/13.53 [v1: Nat_bool_fun$] : ! [v2: ZF$] : ! [v3: ZF_nat_bool_fun_fun$] : (v1 = v0 % 95.22/13.53 | ~ (fun_app$ah(v3, v2) = v1) | ~ (fun_app$ah(v3, v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat$] : ! [v3: % 95.22/13.53 Nat_bool_fun$] : (v1 = v0 | ~ (fun_app$ag(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$ag(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 95.22/13.53 Nat_set$] : ! [v3: Nat_set_ZF_set_fun$] : (v1 = v0 | ~ (fun_app$af(v3, v2) % 95.22/13.53 = v1) | ~ (fun_app$af(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: % 95.22/13.53 ZF_set$] : ! [v2: ZF_set$] : ! [v3: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.53 (fun_app$ae(v3, v2) = v1) | ~ (fun_app$ae(v3, v2) = v0)) & ! [v0: % 95.22/13.53 Bool_set$] : ! [v1: Bool_set$] : ! [v2: A_set_set$] : ! [v3: % 95.22/13.53 A_set_bool_fun$] : (v1 = v0 | ~ (image$e(v3, v2) = v1) | ~ (image$e(v3, % 95.22/13.53 v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] : ! [v2: % 95.22/13.53 B_set_set$] : ! [v3: B_set_bool_fun$] : (v1 = v0 | ~ (image$d(v3, v2) = % 95.22/13.53 v1) | ~ (image$d(v3, v2) = v0)) & ! [v0: Bool_set$] : ! [v1: Bool_set$] % 95.22/13.53 : ! [v2: ZF_set_set_set$] : ! [v3: ZF_set_set_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (image$c(v3, v2) = v1) | ~ (image$c(v3, v2) = v0)) & ! [v0: Bool_set$] : % 95.22/13.53 ! [v1: Bool_set$] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_bool_fun$] : (v1 = % 95.22/13.53 v0 | ~ (image$b(v3, v2) = v1) | ~ (image$b(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.53 ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (fun_app$ad(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$ad(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v2: Nat$] : ! [v3: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 % 95.22/13.53 | ~ (fun_app$ac(v3, v2) = v1) | ~ (fun_app$ac(v3, v2) = v0)) & ! [v0: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.53 ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (fun_app$ab(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$ab(v3, v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v2: Nat$] : ! [v3: Nat_nat_ZF_set_fun_fun$] : (v1 = % 95.22/13.53 v0 | ~ (fun_app$aa(v3, v2) = v1) | ~ (fun_app$aa(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set$] : ! [v1: ZF_set$] : ! [v2: ZF_ZF_fun$] : ! [v3: % 95.22/13.53 ZF_ZF_fun_ZF_set_fun$] : (v1 = v0 | ~ (fun_app$z(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$z(v3, v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF_ZF_ZF_set_fun_fun$] : (v1 % 95.22/13.53 = v0 | ~ (vaj$(v3, v2) = v1) | ~ (vaj$(v3, v2) = v0)) & ! [v0: ZF_set$] : % 95.22/13.53 ! [v1: ZF_set$] : ! [v2: Nat_ZF_fun$] : ! [v3: Nat_ZF_fun_ZF_set_fun$] : % 95.22/13.53 (v1 = v0 | ~ (fun_app$y(v3, v2) = v1) | ~ (fun_app$y(v3, v2) = v0)) & ! % 95.22/13.53 [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_ZF_fun$] : ! % 95.22/13.53 [v3: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (vam$(v3, v2) = v1) | ~ % 95.22/13.53 (vam$(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 95.22/13.53 ZF_nat_fun$] : ! [v3: ZF_nat_fun_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.53 (fun_app$w(v3, v2) = v1) | ~ (fun_app$w(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_nat_fun$] : ! [v3: % 95.22/13.53 Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vap$(v3, v2) = v1) | ~ (vap$(v3, % 95.22/13.53 v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: % 95.22/13.53 ZF_set$] : ! [v3: ZF_set_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$x(v3, % 95.22/13.53 v2) = v1) | ~ (fun_app$x(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: % 95.22/13.53 ZF_set$] : ! [v2: Nat_nat_fun$] : ! [v3: Nat_nat_fun_ZF_set_fun$] : (v1 = % 95.22/13.53 v0 | ~ (fun_app$t(v3, v2) = v1) | ~ (fun_app$t(v3, v2) = v0)) & ! [v0: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: Nat_nat_fun$] : ! % 95.22/13.53 [v3: Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (vas$(v3, v2) = v1) | ~ % 95.22/13.53 (vas$(v3, v2) = v0)) & ! [v0: ZF_set_set$] : ! [v1: ZF_set_set$] : ! [v2: % 95.22/13.53 Nat_set$] : ! [v3: Nat_set_ZF_set_set_fun$] : (v1 = v0 | ~ (fun_app$v(v3, % 95.22/13.53 v2) = v1) | ~ (fun_app$v(v3, v2) = v0)) & ! [v0: ZF_set$] : ! [v1: % 95.22/13.53 ZF_set$] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_set_ZF_set_fun$] : (v1 = v0 % 95.22/13.53 | ~ (fun_app$u(v3, v2) = v1) | ~ (fun_app$u(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set$] : ! [v1: ZF_set$] : ! [v2: ZF$] : ! [v3: ZF_ZF_set_fun$] : (v1 = % 95.22/13.53 v0 | ~ (fun_app$s(v3, v2) = v1) | ~ (fun_app$s(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set$] : ! [v1: ZF_set$] : ! [v2: Nat$] : ! [v3: Nat_ZF_set_fun$] : (v1 % 95.22/13.53 = v0 | ~ (fun_app$r(v3, v2) = v1) | ~ (fun_app$r(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: Nat$] : ! [v3: % 95.22/13.53 ZF_nat_bool_fun_fun$] : (v1 = v0 | ~ (uzz$(v3, v2) = v1) | ~ (uzz$(v3, v2) % 95.22/13.53 = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF$] : ! % 95.22/13.53 [v3: ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$q(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$q(v3, v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! % 95.22/13.53 [v2: A_set$] : ! [v3: A_set_a_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$o(v3, % 95.22/13.53 v2) = v1) | ~ (fun_app$o(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 95.22/13.53 ! [v1: MultipleValueBool] : ! [v2: A$] : ! [v3: A_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (fun_app$n(v3, v2) = v1) | ~ (fun_app$n(v3, v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_set$] : ! [v3: % 95.22/13.53 A_set_bool_fun$] : (v1 = v0 | ~ (fun_app$p(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$p(v3, v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! % 95.22/13.53 [v2: B_set$] : ! [v3: B_set_b_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$l(v3, % 95.22/13.53 v2) = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 95.22/13.53 ! [v1: MultipleValueBool] : ! [v2: B$] : ! [v3: B_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (fun_app$k(v3, v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: B_set$] : ! [v3: % 95.22/13.53 B_set_bool_fun$] : (v1 = v0 | ~ (fun_app$m(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$m(v3, v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: % 95.22/13.53 ZF_set_bool_fun$] : ! [v2: ZF_set_set$] : ! [v3: % 95.22/13.53 ZF_set_set_ZF_set_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$i(v3, v2) = v1) | % 95.22/13.53 ~ (fun_app$i(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.53 MultipleValueBool] : ! [v2: ZF_set_set$] : ! [v3: ZF_set_set_bool_fun$] : % 95.22/13.53 (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) & ! % 95.22/13.53 [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.53 ZF_set_ZF_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$g(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$g(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.53 MultipleValueBool] : ! [v2: ZF$] : ! [v3: ZF_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (fun_app$f(v3, v2) = v1) | ~ (fun_app$f(v3, v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: ZF_set$] : ! [v3: % 95.22/13.53 ZF_set_bool_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$h(v3, v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_prod_fun$] : ! [v2: ZF$] : ! [v3: ZF_ZF_ZF_ZF_prod_fun_fun$] : % 95.22/13.53 (v1 = v0 | ~ (fun_app$e(v3, v2) = v1) | ~ (fun_app$e(v3, v2) = v0)) & ! % 95.22/13.53 [v0: ZF_ZF_prod$] : ! [v1: ZF_ZF_prod$] : ! [v2: ZF$] : ! [v3: % 95.22/13.53 ZF_ZF_ZF_prod_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$d(v3, v2) = v0)) & ! [v0: ZF_ZF_prod_set$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_set$] : ! [v2: ZF_set$] : ! [v3: ZF_set_ZF_ZF_prod_set_fun$] : % 95.22/13.53 (v1 = v0 | ~ (fun_app$c(v3, v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! % 95.22/13.53 [v0: ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_set_fun$] : % 95.22/13.53 ! [v3: ZF_set$] : (v1 = v0 | ~ (sigma$(v3, v2) = v1) | ~ (sigma$(v3, v2) = % 95.22/13.53 v0)) & ! [v0: ZF$] : ! [v1: ZF$] : ! [v2: ZF_ZF_fun$] : ! [v3: ZF$] : % 95.22/13.53 (v1 = v0 | ~ (repl$(v3, v2) = v1) | ~ (repl$(v3, v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: ZF$] : ! [v3: % 95.22/13.53 ZF_ZF_ZF_fun_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = v1) | ~ % 95.22/13.53 (fun_app$b(v3, v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! % 95.22/13.53 [v2: ZF_ZF_fun$] : ! [v3: ZF_ZF_fun_ZF_ZF_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (fun_app$a(v3, v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) & ! [v0: ZF$] : ! % 95.22/13.53 [v1: ZF$] : ! [v2: ZF$] : ! [v3: ZF_ZF_fun$] : (v1 = v0 | ~ (fun_app$(v3, % 95.22/13.53 v2) = v1) | ~ (fun_app$(v3, v2) = v0)) & ! [v0: B_set$] : ! [v1: % 95.22/13.53 B_set$] : ! [v2: B_set_set$] : (v1 = v0 | ~ (inf$b(v2) = v1) | ~ % 95.22/13.53 (inf$b(v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: A_set_set$] % 95.22/13.53 : (v1 = v0 | ~ (inf$a(v2) = v1) | ~ (inf$a(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_bool_fun_set$] : (v1 = v0 % 95.22/13.53 | ~ (sup$j(v2) = v1) | ~ (sup$j(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : % 95.22/13.53 ! [v1: ZF_set_bool_fun$] : ! [v2: ZF_set_bool_fun_set$] : (v1 = v0 | ~ % 95.22/13.53 (sup$i(v2) = v1) | ~ (sup$i(v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: % 95.22/13.53 B_bool_fun$] : ! [v2: B_bool_fun_set$] : (v1 = v0 | ~ (sup$h(v2) = v1) | % 95.22/13.53 ~ (sup$h(v2) = v0)) & ! [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: % 95.22/13.53 A_bool_fun_set$] : (v1 = v0 | ~ (sup$g(v2) = v1) | ~ (sup$g(v2) = v0)) & % 95.22/13.53 ! [v0: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v2: ZF_ZF_ZF_ZF_prod_set_fun_fun$] : % 95.22/13.53 (v1 = v0 | ~ (case_prod$p(v2) = v1) | ~ (case_prod$p(v2) = v0)) & ! [v0: % 95.22/13.53 Nat_nat_prod_ZF_ZF_prod_set_fun$] : ! [v1: % 95.22/13.53 Nat_nat_prod_ZF_ZF_prod_set_fun$] : ! [v2: Nat_nat_ZF_ZF_prod_set_fun_fun$] % 95.22/13.53 : (v1 = v0 | ~ (case_prod$o(v2) = v1) | ~ (case_prod$o(v2) = v0)) & ! [v0: % 95.22/13.53 Nat_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: Nat_ZF_prod_ZF_ZF_prod_set_fun$] % 95.22/13.53 : ! [v2: Nat_ZF_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (case_prod$n(v2) = % 95.22/13.53 v1) | ~ (case_prod$n(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_nat_prod_ZF_ZF_prod_set_fun$] : ! [v1: ZF_nat_prod_ZF_ZF_prod_set_fun$] % 95.22/13.53 : ! [v2: ZF_nat_ZF_ZF_prod_set_fun_fun$] : (v1 = v0 | ~ (case_prod$m(v2) = % 95.22/13.53 v1) | ~ (case_prod$m(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_set_set_ZF_set_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_set_set_ZF_set_set_fun$] : ! [v2: ZF_ZF_prod_set_ZF_set_fun$] : % 95.22/13.53 (v1 = v0 | ~ (image$av(v2) = v1) | ~ (image$av(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set_set_ZF_set_set_set_fun$] : ! [v1: ZF_set_set_ZF_set_set_set_fun$] : % 95.22/13.53 ! [v2: ZF_set_ZF_set_set_fun$] : (v1 = v0 | ~ (image$au(v2) = v1) | ~ % 95.22/13.53 (image$au(v2) = v0)) & ! [v0: Nat_set_set_ZF_set_set_set_fun$] : ! [v1: % 95.22/13.53 Nat_set_set_ZF_set_set_set_fun$] : ! [v2: Nat_set_ZF_set_set_fun$] : (v1 = % 95.22/13.53 v0 | ~ (image$at(v2) = v1) | ~ (image$at(v2) = v0)) & ! [v0: B_set$] : ! % 95.22/13.53 [v1: B_set$] : ! [v2: B_set_set$] : (v1 = v0 | ~ (sup$c(v2) = v1) | ~ % 95.22/13.53 (sup$c(v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: A_set_set$] % 95.22/13.53 : (v1 = v0 | ~ (sup$b(v2) = v1) | ~ (sup$b(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_set$] : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_set$] : (v1 % 95.22/13.53 = v0 | ~ (converse$(v2) = v1) | ~ (converse$(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_ZF_set_ZF_set_prod_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$l(v2) = v1) | % 95.22/13.53 ~ (case_prod$l(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$k(v2) % 95.22/13.53 = v1) | ~ (case_prod$k(v2) = v0)) & ! [v0: % 95.22/13.53 Nat_nat_prod_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.53 Nat_nat_prod_ZF_set_ZF_set_prod_fun$] : ! [v2: % 95.22/13.53 Nat_nat_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$j(v2) = v1) % 95.22/13.53 | ~ (case_prod$j(v2) = v0)) & ! [v0: % 95.22/13.53 Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$] : ! [v2: % 95.22/13.53 Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$i(v2) = % 95.22/13.53 v1) | ~ (case_prod$i(v2) = v0)) & ! [v0: % 95.22/13.53 Nat_ZF_prod_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_prod_ZF_set_ZF_set_prod_fun$] : ! [v2: % 95.22/13.53 Nat_ZF_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$h(v2) = v1) | % 95.22/13.53 ~ (case_prod$h(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$g(v2) = % 95.22/13.53 v1) | ~ (case_prod$g(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$f(v2) = % 95.22/13.53 v1) | ~ (case_prod$f(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_nat_prod_ZF_set_ZF_set_prod_fun$] : ! [v1: % 95.22/13.53 ZF_nat_prod_ZF_set_ZF_set_prod_fun$] : ! [v2: % 95.22/13.53 ZF_nat_ZF_set_ZF_set_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$e(v2) = v1) | % 95.22/13.53 ~ (case_prod$e(v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$] % 95.22/13.53 : ! [v1: ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$] : (v1 = v0 | ~ (case_prod$d(v2) = % 95.22/13.53 v1) | ~ (case_prod$d(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_ZF_prod_fun$] : % 95.22/13.53 ! [v1: ZF_ZF_prod_ZF_ZF_prod_fun$] : ! [v2: ZF_ZF_ZF_ZF_prod_fun_fun$] : (v1 % 95.22/13.53 = v0 | ~ (case_prod$c(v2) = v1) | ~ (case_prod$c(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_bool_fun$] : ! [v1: ZF_ZF_prod_bool_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (case_prod$b(v2) = v1) | ~ % 95.22/13.53 (case_prod$b(v2) = v0)) & ! [v0: ZF_set_set_ZF_set_set_fun$] : ! [v1: % 95.22/13.53 ZF_set_set_ZF_set_set_fun$] : ! [v2: ZF_set_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.53 (image$q(v2) = v1) | ~ (image$q(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! % 95.22/13.53 [v1: ZF_set_bool_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (less_eq$c(v2) = v1) % 95.22/13.53 | ~ (less_eq$c(v2) = v0)) & ! [v0: ZF_ZF_fun_ZF_ZF_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_fun_ZF_ZF_fun_fun$] : ! [v2: ZF_ZF_fun$] : (v1 = v0 | ~ (comp$b(v2) % 95.22/13.53 = v1) | ~ (comp$b(v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! % 95.22/13.53 [v1: ZF_ZF_unit_Category_ext$] : ! [v2: % 95.22/13.53 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : (v1 = v0 | ~ (catDom$a(v2) = v1) % 95.22/13.53 | ~ (catDom$a(v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! % 95.22/13.53 [v2: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : (v1 = v0 | ~ (mapO$b(v2) = % 95.22/13.53 v1) | ~ (mapO$b(v2) = v0)) & ! [v0: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v1: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v2: % 95.22/13.53 A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$] : (v1 = v0 % 95.22/13.53 | ~ (catDom$(v2) = v1) | ~ (catDom$(v2) = v0)) & ! [v0: A_a_fun$] : ! % 95.22/13.53 [v1: A_a_fun$] : ! [v2: % 95.22/13.53 A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$] : (v1 = v0 % 95.22/13.53 | ~ (mapO$a(v2) = v1) | ~ (mapO$a(v2) = v0)) & ! [v0: B_ZF_fun$] : ! % 95.22/13.53 [v1: B_ZF_fun$] : ! [v2: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] % 95.22/13.53 : (v1 = v0 | ~ (mapM$(v2) = v1) | ~ (mapM$(v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.53 (preFunctor$b(v2) = v1) | ~ (preFunctor$b(v2) = v0)) & ! [v0: A_ZF_fun$] : % 95.22/13.53 ! [v1: A_ZF_fun$] : ! [v2: % 95.22/13.53 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.53 (mapO$(v2) = v1) | ~ (mapO$(v2) = v0)) & ! [v0: B$] : ! [v1: B$] : ! % 95.22/13.53 [v2: B_bool_fun$] : (v1 = v0 | ~ (the$a(v2) = v1) | ~ (the$a(v2) = v0)) & ! % 95.22/13.53 [v0: C$] : ! [v1: C$] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = % 95.22/13.53 v0 | ~ (more$b(v2) = v1) | ~ (more$b(v2) = v0)) & ! [v0: B_ZF_fun_set$] : % 95.22/13.53 ! [v1: B_ZF_fun_set$] : ! [v2: B_set$] : (v1 = v0 | ~ (extensional$e(v2) = % 95.22/13.53 v1) | ~ (extensional$e(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_fun_set$] : ! % 95.22/13.53 [v1: ZF_ZF_prod_ZF_fun_set$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 95.22/13.53 (extensional$d(v2) = v1) | ~ (extensional$d(v2) = v0)) & ! [v0: % 95.22/13.53 B_b_prod_b_fun_set$] : ! [v1: B_b_prod_b_fun_set$] : ! [v2: B_b_prod_set$] % 95.22/13.53 : (v1 = v0 | ~ (extensional$c(v2) = v1) | ~ (extensional$c(v2) = v0)) & ! % 95.22/13.53 [v0: ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.53 ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$] : ! [v2: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (unitFunctor$(v2) = v1) | ~ % 95.22/13.53 (unitFunctor$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.53 MultipleValueBool] : ! [v2: ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$] : % 95.22/13.53 (v1 = v0 | ~ (functor$c(v2) = v1) | ~ (functor$c(v2) = v0)) & ! [v0: ZF$] : % 95.22/13.53 ! [v1: ZF$] : ! [v2: ZF_bool_fun$] : (v1 = v0 | ~ (the$(v2) = v1) | ~ % 95.22/13.53 (the$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 95.22/13.53 ! [v2: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.53 (functor$b(v2) = v1) | ~ (functor$b(v2) = v0)) & ! [v0: MultipleValueBool] % 95.22/13.53 : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.53 (functor$a(v2) = v1) | ~ (functor$a(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] % 95.22/13.53 : (v1 = v0 | ~ (identityFunctor$b(v2) = v1) | ~ (identityFunctor$b(v2) = % 95.22/13.53 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : (v1 = v0 | ~ (functor$(v2) = v1) % 95.22/13.53 | ~ (functor$(v2) = v0)) & ! [v0: A_b_fun_set$] : ! [v1: A_b_fun_set$] : % 95.22/13.53 ! [v2: A_set$] : (v1 = v0 | ~ (extensional$b(v2) = v1) | ~ % 95.22/13.53 (extensional$b(v2) = v0)) & ! [v0: ZF_ZF_fun_set$] : ! [v1: % 95.22/13.53 ZF_ZF_fun_set$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (extensional$a(v2) = v1) % 95.22/13.53 | ~ (extensional$a(v2) = v0)) & ! [v0: B_a_fun_set$] : ! [v1: % 95.22/13.53 B_a_fun_set$] : ! [v2: B_set$] : (v1 = v0 | ~ (extensional$(v2) = v1) | ~ % 95.22/13.53 (extensional$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.53 MultipleValueBool] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = % 95.22/13.53 v0 | ~ (extCategory$a(v2) = v1) | ~ (extCategory$a(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_bool_fun_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (objIso$(v2) = v1) | ~ % 95.22/13.53 (objIso$(v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (inverse$a(v2) = v1) | ~ % 95.22/13.53 (inverse$a(v2) = v0)) & ! [v0: B_b_fun$] : ! [v1: B_b_fun$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (inverse$(v2) = v1) | % 95.22/13.53 ~ (inverse$(v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: B_bool_fun$] : ! % 95.22/13.53 [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (isomorphism$a(v2) % 95.22/13.53 = v1) | ~ (isomorphism$a(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 95.22/13.53 [v1: MultipleValueBool] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (extCategory$(v2) = v1) | ~ (extCategory$(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : % 95.22/13.53 (v1 = v0 | ~ (isomorphism$(v2) = v1) | ~ (isomorphism$(v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : (v1 = v0 | ~ (preFunctor$a(v2) = % 95.22/13.53 v1) | ~ (preFunctor$a(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.53 MultipleValueBool] : ! [v2: % 95.22/13.53 ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.53 (preFunctor$(v2) = v1) | ~ (preFunctor$(v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (lSCategory_axioms$(v2) = v1) | ~ (lSCategory_axioms$(v2) = v0)) & ! [v0: % 95.22/13.53 Unit$] : ! [v1: Unit$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (more$a(v2) = v1) | ~ (more$a(v2) = v0)) & ! [v0: B_c_LSCategory_ext$] : % 95.22/13.53 ! [v1: B_c_LSCategory_ext$] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : % 95.22/13.53 (v1 = v0 | ~ (more$(v2) = v1) | ~ (more$(v2) = v0)) & ! [v0: ZF_set_set$] : % 95.22/13.53 ! [v1: ZF_set_set$] : ! [v2: ZF_set_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (collect$j(v2) = v1) | ~ (collect$j(v2) = v0)) & ! [v0: B_set$] : ! [v1: % 95.22/13.53 B_set$] : ! [v2: B_bool_fun$] : (v1 = v0 | ~ (collect$i(v2) = v1) | ~ % 95.22/13.53 (collect$i(v2) = v0)) & ! [v0: A_set$] : ! [v1: A_set$] : ! [v2: % 95.22/13.53 A_bool_fun$] : (v1 = v0 | ~ (collect$h(v2) = v1) | ~ (collect$h(v2) = v0)) % 95.22/13.53 & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | % 95.22/13.53 ~ (collect$g(v2) = v1) | ~ (collect$g(v2) = v0)) & ! [v0: A_b_fun_set$] : % 95.22/13.53 ! [v1: A_b_fun_set$] : ! [v2: A_b_fun_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (collect$f(v2) = v1) | ~ (collect$f(v2) = v0)) & ! [v0: B_a_fun_set$] : ! % 95.22/13.53 [v1: B_a_fun_set$] : ! [v2: B_a_fun_bool_fun$] : (v1 = v0 | ~ (collect$e(v2) % 95.22/13.53 = v1) | ~ (collect$e(v2) = v0)) & ! [v0: B_ZF_fun_set$] : ! [v1: % 95.22/13.53 B_ZF_fun_set$] : ! [v2: B_ZF_fun_bool_fun$] : (v1 = v0 | ~ (collect$d(v2) % 95.22/13.53 = v1) | ~ (collect$d(v2) = v0)) & ! [v0: ZF_ZF_fun_set$] : ! [v1: % 95.22/13.53 ZF_ZF_fun_set$] : ! [v2: ZF_ZF_fun_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (collect$c(v2) = v1) | ~ (collect$c(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] % 95.22/13.53 : (v1 = v0 | ~ (identityFunctor$a(v2) = v1) | ~ (identityFunctor$a(v2) = % 95.22/13.53 v0)) & ! [v0: % 95.22/13.53 A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v1: % 95.22/13.53 A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (identityFunctor$(v2) % 95.22/13.53 = v1) | ~ (identityFunctor$(v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (cod$a(v2) = % 95.22/13.53 v1) | ~ (cod$a(v2) = v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! % 95.22/13.53 [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (cod$(v2) = v1) | % 95.22/13.53 ~ (cod$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 95.22/13.53 : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (category_axioms$a(v2) = % 95.22/13.53 v1) | ~ (category_axioms$a(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 95.22/13.53 [v1: MultipleValueBool] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 % 95.22/13.53 = v0 | ~ (category_axioms$(v2) = v1) | ~ (category_axioms$(v2) = v0)) & ! % 95.22/13.53 [v0: ZF_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_bool_fun_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (inverse_rel$a(v2) = v1) | ~ % 95.22/13.53 (inverse_rel$a(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.53 MultipleValueBool] : ! [v2: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$] : (v1 % 95.22/13.53 = v0 | ~ (functorM$c(v2) = v1) | ~ (functorM$c(v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.53 (functorM$b(v2) = v1) | ~ (functorM$b(v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$] : (v1 = v0 % 95.22/13.53 | ~ (functorM$a(v2) = v1) | ~ (functorM$a(v2) = v0)) & ! [v0: % 95.22/13.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$] : (v1 = v0 | ~ % 95.22/13.53 (functorM$(v2) = v1) | ~ (functorM$(v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (id$a(v2) % 95.22/13.53 = v1) | ~ (id$a(v2) = v0)) & ! [v0: A_b_fun$] : ! [v1: A_b_fun$] : ! % 95.22/13.53 [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (id$(v2) = v1) | ~ % 95.22/13.53 (id$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 95.22/13.53 ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (category$a(v2) = v1) | ~ % 95.22/13.53 (category$a(v2) = v0)) & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (mor$a(v2) = v1) | ~ (mor$a(v2) = % 95.22/13.53 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (category$(v2) = v1) | % 95.22/13.53 ~ (category$(v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | % 95.22/13.53 ~ (makeCat$a(v2) = v1) | ~ (makeCat$a(v2) = v0)) & ! [v0: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v1: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (makeCat$(v2) = v1) | % 95.22/13.53 ~ (makeCat$(v2) = v0)) & ! [v0: ZF_ZF_fun$] : ! [v1: ZF_ZF_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ (dom$a(v2) = v1) | ~ (dom$a(v2) = % 95.22/13.53 v0)) & ! [v0: B_a_fun$] : ! [v1: B_a_fun$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (dom$(v2) = v1) | ~ % 95.22/13.53 (dom$(v2) = v0)) & ! [v0: ZF_ZF_unit_Category_ext$] : ! [v1: % 95.22/13.53 ZF_ZF_unit_Category_ext$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | % 95.22/13.53 ~ (oppositeCategory$a(v2) = v1) | ~ (oppositeCategory$a(v2) = v0)) & ! % 95.22/13.53 [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = % 95.22/13.53 v0 | ~ (obj$a(v2) = v1) | ~ (obj$a(v2) = v0)) & ! [v0: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v1: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (oppositeCategory$(v2) % 95.22/13.53 = v1) | ~ (oppositeCategory$(v2) = v0)) & ! [v0: A_set$] : ! [v1: % 95.22/13.53 A_set$] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (obj$(v2) = v1) | ~ (obj$(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 95.22/13.53 MultipleValueBool] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = % 95.22/13.53 v0 | ~ (lSCategory$(v2) = v1) | ~ (lSCategory$(v2) = v0)) & ! [v0: % 95.22/13.53 Nat_nat_set_fun$] : ! [v1: Nat_nat_set_fun$] : ! [v2: Nat_set$] : (v1 = v0 % 95.22/13.53 | ~ (uyc$(v2) = v1) | ~ (uyc$(v2) = v0)) & ! [v0: ZF_nat_set_fun$] : ! % 95.22/13.53 [v1: ZF_nat_set_fun$] : ! [v2: Nat_set$] : (v1 = v0 | ~ (uxq$(v2) = v1) | ~ % 95.22/13.53 (uxq$(v2) = v0)) & ! [v0: ZF_ZF_prod_nat_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_nat_set_fun$] : ! [v2: Nat_set$] : (v1 = v0 | ~ (uxv$(v2) = v1) % 95.22/13.53 | ~ (uxv$(v2) = v0)) & ! [v0: Nat_ZF_set_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_set_fun$] : ! [v2: ZF_set_set$] : (v1 = v0 | ~ (uyj$(v2) = v1) % 95.22/13.53 | ~ (uyj$(v2) = v0)) & ! [v0: ZF_ZF_set_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_set_fun$] : ! [v2: ZF_set_set$] : (v1 = v0 | ~ (uyi$(v2) = v1) | % 95.22/13.53 ~ (uyi$(v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : % 95.22/13.53 ! [v2: ZF_set$] : (v1 = v0 | ~ (uxy$(v2) = v1) | ~ (uxy$(v2) = v0)) & ! % 95.22/13.53 [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: ZF_set$] : (v1 = v0 | % 95.22/13.53 ~ (uxi$(v2) = v1) | ~ (uxi$(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_set_fun$] : % 95.22/13.53 ! [v1: ZF_ZF_prod_ZF_set_fun$] : ! [v2: ZF_set$] : (v1 = v0 | ~ (uxs$(v2) = % 95.22/13.53 v1) | ~ (uxs$(v2) = v0)) & ! [v0: Nat_ZF_ZF_prod_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_ZF_prod_set_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 95.22/13.53 (uya$(v2) = v1) | ~ (uya$(v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_set_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_ZF_prod_set_fun$] : ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ % 95.22/13.53 (uxn$(v2) = v1) | ~ (uxn$(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_ZF_prod_ZF_ZF_prod_set_fun$] : ! [v1: ZF_ZF_prod_ZF_ZF_prod_set_fun$] : % 95.22/13.53 ! [v2: ZF_ZF_prod_set$] : (v1 = v0 | ~ (uye$(v2) = v1) | ~ (uye$(v2) = v0)) % 95.22/13.53 & ! [v0: ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$] : ! [v2: ZF_ZF_fun$] : (v1 = v0 | % 95.22/13.53 ~ (uuk$(v2) = v1) | ~ (uuk$(v2) = v0)) & ! [v0: A_set_a_set_fun$] : ! % 95.22/13.53 [v1: A_set_a_set_fun$] : ! [v2: A_a_fun$] : (v1 = v0 | ~ (image$p(v2) = v1) % 95.22/13.53 | ~ (image$p(v2) = v0)) & ! [v0: B_set_b_set_fun$] : ! [v1: % 95.22/13.53 B_set_b_set_fun$] : ! [v2: B_b_fun$] : (v1 = v0 | ~ (image$l(v2) = v1) | % 95.22/13.53 ~ (image$l(v2) = v0)) & ! [v0: Nat_ZF_ZF_set_fun_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_ZF_set_fun_fun$] : ! [v2: Nat_ZF_set_fun$] : (v1 = v0 | ~ (uzn$(v2) % 95.22/13.53 = v1) | ~ (uzn$(v2) = v0)) & ! [v0: ZF_ZF_ZF_set_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_set_fun_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uzq$(v2) = % 95.22/13.53 v1) | ~ (uzq$(v2) = v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_fun_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uul$(v2) = % 95.22/13.53 v1) | ~ (uul$(v2) = v0)) & ! [v0: ZF_set_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_set_ZF_set_fun$] : ! [v2: ZF_ZF_fun$] : (v1 = v0 | ~ (image$g(v2) = v1) % 95.22/13.53 | ~ (image$g(v2) = v0)) & ! [v0: ZF_ZF_prod_set_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_set_ZF_set_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ % 95.22/13.53 (image$f(v2) = v1) | ~ (image$f(v2) = v0)) & ! [v0: Nat_ZF_bool_fun_fun$] % 95.22/13.53 : ! [v1: Nat_ZF_bool_fun_fun$] : ! [v2: Nat_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.53 (vac$(v2) = v1) | ~ (vac$(v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ (vab$(v2) % 95.22/13.53 = v1) | ~ (vab$(v2) = v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_fun_fun$] : ! [v2: ZF$] : (v1 = v0 | ~ (uus$(v2) = v1) | ~ % 95.22/13.53 (uus$(v2) = v0)) & ! [v0: ZF_b_fun$] : ! [v1: ZF_b_fun$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (zF2mor$(v2) = v1) | % 95.22/13.53 ~ (zF2mor$(v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_bool_fun_fun$] : ! [v2: ZF$] : (v1 = v0 | ~ (uyl$(v2) = v1) | ~ % 95.22/13.53 (uyl$(v2) = v0)) & ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (mor$(v2) = v1) | ~ % 95.22/13.53 (mor$(v2) = v0)) & ! [v0: B_ZF_fun$] : ! [v1: B_ZF_fun$] : ! [v2: % 95.22/13.53 A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (mor2ZF$(v2) = v1) | % 95.22/13.53 ~ (mor2ZF$(v2) = v0)) & ! [v0: B_b_b_fun_fun$] : ! [v1: B_b_b_fun_fun$] : % 95.22/13.53 ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (uud$(v2) = v1) | % 95.22/13.53 ~ (uud$(v2) = v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_fun_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (uue$(v2) = v1) | ~ (uue$(v2) = v0)) & ! [v0: B_b_b_fun_fun$] : ! [v1: % 95.22/13.53 B_b_b_fun_fun$] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | % 95.22/13.53 ~ (comp$a(v2) = v1) | ~ (comp$a(v2) = v0)) & ! [v0: B_b_prod_b_fun$] : ! % 95.22/13.53 [v1: B_b_prod_b_fun$] : ! [v2: B_b_b_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (case_prod$a(v2) = v1) | ~ (case_prod$a(v2) = v0)) & ! [v0: B_b_prod_set$] % 95.22/13.53 : ! [v1: B_b_prod_set$] : ! [v2: B_b_prod_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (collect$b(v2) = v1) | ~ (collect$b(v2) = v0)) & ! [v0: B_b_b_fun_fun$] : % 95.22/13.53 ! [v1: B_b_b_fun_fun$] : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = % 95.22/13.53 v0 | ~ (uum$(v2) = v1) | ~ (uum$(v2) = v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] : % 95.22/13.53 ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (comp$(v2) = v1) | ~ (comp$(v2) = v0)) & ! [v0: ZF_ZF_prod_ZF_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_prod_ZF_fun$] : ! [v2: ZF_ZF_ZF_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (case_prod$(v2) = v1) | ~ (case_prod$(v2) = v0)) & ! [v0: ZF_ZF_prod_set$] % 95.22/13.53 : ! [v1: ZF_ZF_prod_set$] : ! [v2: ZF_ZF_prod_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (collect$a(v2) = v1) | ~ (collect$a(v2) = v0)) & ! [v0: ZF_ZF_ZF_fun_fun$] % 95.22/13.53 : ! [v1: ZF_ZF_ZF_fun_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | % 95.22/13.53 ~ (uun$(v2) = v1) | ~ (uun$(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v2: ZF_bool_fun$] : (v1 = v0 | ~ (uxh$(v2) = v1) | ~ % 95.22/13.53 (uxh$(v2) = v0)) & ! [v0: B_b_prod_bool_fun$] : ! [v1: B_b_prod_bool_fun$] % 95.22/13.53 : ! [v2: A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (uui$(v2) = % 95.22/13.53 v1) | ~ (uui$(v2) = v0)) & ! [v0: ZF_ZF_prod_bool_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_prod_bool_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (uuj$(v2) = v1) | ~ (uuj$(v2) = v0)) & ! [v0: ZF_ZF_bool_fun_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_bool_fun_fun$] : ! [v2: ZF_ZF_unit_Category_ext$] : (v1 = v0 | ~ % 95.22/13.53 (compDefined$(v2) = v1) | ~ (compDefined$(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: Nat_ZF_set_fun$] : % 95.22/13.53 (v1 = v0 | ~ (uww$(v2) = v1) | ~ (uww$(v2) = v0)) & ! [v0: ZF_bool_fun$] : % 95.22/13.53 ! [v1: ZF_bool_fun$] : ! [v2: Nat_ZF_fun$] : (v1 = v0 | ~ (uwx$(v2) = v1) | % 95.22/13.53 ~ (uwx$(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : % 95.22/13.53 ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ (uwu$(v2) = v1) | ~ (uwu$(v2) = v0)) % 95.22/13.53 & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_ZF_fun$] : (v1 = % 95.22/13.53 v0 | ~ (uwv$(v2) = v1) | ~ (uwv$(v2) = v0)) & ! [v0: ZF_bool_fun$] : ! % 95.22/13.53 [v1: ZF_bool_fun$] : ! [v2: ZF_ZF_prod_ZF_fun$] : (v1 = v0 | ~ (uwt$(v2) = % 95.22/13.53 v1) | ~ (uwt$(v2) = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] % 95.22/13.53 : ! [v2: ZF_nat_bool_fun_fun$] : (v1 = v0 | ~ (uzy$(v2) = v1) | ~ (uzy$(v2) % 95.22/13.53 = v0)) & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (uzv$(v2) = v1) | ~ (uzv$(v2) = v0)) & % 95.22/13.53 ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (uxl$(v2) = v1) | ~ (uxl$(v2) = v0)) & % 95.22/13.53 ! [v0: Nat_set_ZF_set_fun$] : ! [v1: Nat_set_ZF_set_fun$] : ! [v2: % 95.22/13.53 Nat_ZF_set_fun$] : (v1 = v0 | ~ (uyt$(v2) = v1) | ~ (uyt$(v2) = v0)) & ! % 95.22/13.53 [v0: ZF_set_ZF_set_fun$] : ! [v1: ZF_set_ZF_set_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_set_fun$] : (v1 = v0 | ~ (uyu$(v2) = v1) | ~ (uyu$(v2) = v0)) & ! % 95.22/13.53 [v0: A_bool_fun$] : ! [v1: A_bool_fun$] : ! [v2: A_set_set$] : (v1 = v0 | ~ % 95.22/13.53 (vad$(v2) = v1) | ~ (vad$(v2) = v0)) & ! [v0: B_bool_fun$] : ! [v1: % 95.22/13.53 B_bool_fun$] : ! [v2: B_set_set$] : (v1 = v0 | ~ (vae$(v2) = v1) | ~ % 95.22/13.53 (vae$(v2) = v0)) & ! [v0: ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : % 95.22/13.53 ! [v2: ZF_set_set_set$] : (v1 = v0 | ~ (vaf$(v2) = v1) | ~ (vaf$(v2) = v0)) % 95.22/13.53 & ! [v0: ZF_bool_fun$] : ! [v1: ZF_bool_fun$] : ! [v2: ZF_set_set$] : (v1 = % 95.22/13.53 v0 | ~ (vag$(v2) = v1) | ~ (vag$(v2) = v0)) & ! [v0: MultipleValueBool] : % 95.22/13.53 ! [v1: MultipleValueBool] : ! [v2: Bool_set$] : (v1 = v0 | ~ (sup$a(v2) = % 95.22/13.53 v1) | ~ (sup$a(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v2: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vai$(v2) = % 95.22/13.53 v1) | ~ (vai$(v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v2: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (val$(v2) % 95.22/13.53 = v1) | ~ (val$(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v2: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vao$(v2) % 95.22/13.53 = v1) | ~ (vao$(v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v2: Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (var$(v2) = v1) | ~ (var$(v2) = v0)) & ! [v0: ZF_ZF_fun_ZF_set_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_fun_ZF_set_fun$] : ! [v2: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (vav$(v2) = v1) | ~ (vav$(v2) = v0)) & ! [v0: Nat_ZF_fun_ZF_set_fun$] : ! % 95.22/13.53 [v1: Nat_ZF_fun_ZF_set_fun$] : ! [v2: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (vax$(v2) = v1) | ~ (vax$(v2) = v0)) & ! [v0: ZF_nat_fun_ZF_set_fun$] : ! % 95.22/13.53 [v1: ZF_nat_fun_ZF_set_fun$] : ! [v2: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (vaz$(v2) = v1) | ~ (vaz$(v2) = v0)) & ! [v0: Nat_nat_fun_ZF_set_fun$] : % 95.22/13.53 ! [v1: Nat_nat_fun_ZF_set_fun$] : ! [v2: Nat_nat_ZF_set_fun_fun$] : (v1 = v0 % 95.22/13.53 | ~ (vbb$(v2) = v1) | ~ (vbb$(v2) = v0)) & ! [v0: ZF_set$] : ! [v1: % 95.22/13.53 ZF_set$] : ! [v2: ZF_set_set$] : (v1 = v0 | ~ (inf$(v2) = v1) | ~ % 95.22/13.53 (inf$(v2) = v0)) & ! [v0: ZF_ZF_ZF_set_fun_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_ZF_set_fun_fun$] : ! [v2: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (uyw$(v2) = v1) | ~ (uyw$(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v2: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vau$(v2) = % 95.22/13.53 v1) | ~ (vau$(v2) = v0)) & ! [v0: Nat_ZF_ZF_set_fun_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_ZF_set_fun_fun$] : ! [v2: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (uyz$(v2) = v1) | ~ (uyz$(v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v2: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (vaw$(v2) % 95.22/13.53 = v1) | ~ (vaw$(v2) = v0)) & ! [v0: ZF_nat_ZF_set_fun_fun$] : ! [v1: % 95.22/13.53 ZF_nat_ZF_set_fun_fun$] : ! [v2: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (uzc$(v2) = v1) | ~ (uzc$(v2) = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: % 95.22/13.53 ZF_ZF_set_fun$] : ! [v2: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ (vay$(v2) % 95.22/13.53 = v1) | ~ (vay$(v2) = v0)) & ! [v0: Nat_nat_ZF_set_fun_fun$] : ! [v1: % 95.22/13.53 Nat_nat_ZF_set_fun_fun$] : ! [v2: Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (uzf$(v2) = v1) | ~ (uzf$(v2) = v0)) & ! [v0: Nat_ZF_set_fun$] : ! [v1: % 95.22/13.53 Nat_ZF_set_fun$] : ! [v2: Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (vba$(v2) = v1) | ~ (vba$(v2) = v0)) & ! [v0: ZF_ZF_fun_ZF_set_fun$] : ! % 95.22/13.53 [v1: ZF_ZF_fun_ZF_set_fun$] : ! [v2: ZF_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (vak$(v2) = v1) | ~ (vak$(v2) = v0)) & ! [v0: Nat_ZF_fun_ZF_set_fun$] : ! % 95.22/13.53 [v1: Nat_ZF_fun_ZF_set_fun$] : ! [v2: ZF_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (van$(v2) = v1) | ~ (van$(v2) = v0)) & ! [v0: ZF_nat_fun_ZF_set_fun$] : ! % 95.22/13.53 [v1: ZF_nat_fun_ZF_set_fun$] : ! [v2: Nat_ZF_ZF_set_fun_fun$] : (v1 = v0 | ~ % 95.22/13.53 (vaq$(v2) = v1) | ~ (vaq$(v2) = v0)) & ! [v0: ZF_set_ZF_set_set_fun$] : ! % 95.22/13.53 [v1: ZF_set_ZF_set_set_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.53 (image$a(v2) = v1) | ~ (image$a(v2) = v0)) & ! [v0: % 95.22/13.53 Nat_nat_fun_ZF_set_fun$] : ! [v1: Nat_nat_fun_ZF_set_fun$] : ! [v2: % 95.22/13.53 Nat_nat_ZF_set_fun_fun$] : (v1 = v0 | ~ (vat$(v2) = v1) | ~ (vat$(v2) = % 95.22/13.53 v0)) & ! [v0: Nat_set_ZF_set_set_fun$] : ! [v1: Nat_set_ZF_set_set_fun$] % 95.22/13.53 : ! [v2: Nat_ZF_set_fun$] : (v1 = v0 | ~ (image$(v2) = v1) | ~ (image$(v2) % 95.22/13.53 = v0)) & ! [v0: ZF_ZF_set_fun$] : ! [v1: ZF_ZF_set_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (uzx$(v2) = v1) | ~ (uzx$(v2) = v0)) & % 95.22/13.53 ! [v0: ZF_ZF_bool_fun_fun$] : ! [v1: ZF_ZF_bool_fun_fun$] : ! [v2: % 95.22/13.53 ZF_ZF_bool_fun_fun$] : (v1 = v0 | ~ (uzw$(v2) = v1) | ~ (uzw$(v2) = v0)) & % 95.22/13.53 ! [v0: Nat_ZF_set_fun$] : ! [v1: Nat_ZF_set_fun$] : ! [v2: % 95.22/13.53 ZF_nat_bool_fun_fun$] : (v1 = v0 | ~ (vaa$(v2) = v1) | ~ (vaa$(v2) = v0)) % 95.22/13.53 & ! [v0: ZF_set$] : ! [v1: ZF_set$] : ! [v2: ZF_bool_fun$] : (v1 = v0 | ~ % 95.22/13.53 (collect$(v2) = v1) | ~ (collect$(v2) = v0)) & ! [v0: A_set_bool_fun$] : % 95.22/13.53 ! [v1: A_set_bool_fun$] : ! [v2: A$] : (v1 = v0 | ~ (member$c(v2) = v1) | ~ % 95.22/13.53 (member$c(v2) = v0)) & ! [v0: B_set_bool_fun$] : ! [v1: B_set_bool_fun$] : % 95.22/13.53 ! [v2: B$] : (v1 = v0 | ~ (member$b(v2) = v1) | ~ (member$b(v2) = v0)) & ! % 95.22/13.53 [v0: ZF_set_set_bool_fun$] : ! [v1: ZF_set_set_bool_fun$] : ! [v2: ZF_set$] % 95.22/13.53 : (v1 = v0 | ~ (member$a(v2) = v1) | ~ (member$a(v2) = v0)) & ! [v0: % 95.22/13.53 ZF_set_bool_fun$] : ! [v1: ZF_set_bool_fun$] : ! [v2: ZF$] : (v1 = v0 | ~ % 95.22/13.53 (member$(v2) = v1) | ~ (member$(v2) = v0)) & ! [v0: ZF_ZF_ZF_prod_fun$] : % 95.22/13.53 ! [v1: ZF_ZF_ZF_prod_fun$] : ! [v2: ZF$] : (v1 = v0 | ~ (pair$(v2) = v1) | % 95.22/13.53 ~ (pair$(v2) = v0)) & ! [v0: ZF_set_ZF_ZF_prod_set_fun$] : ! [v1: % 95.22/13.53 ZF_set_ZF_ZF_prod_set_fun$] : ! [v2: ZF_ZF_set_fun$] : (v1 = v0 | ~ % 95.22/13.53 (uyo$(v2) = v1) | ~ (uyo$(v2) = v0)) % 95.22/13.53 % 95.22/13.53 Further assumptions not needed in the proof: % 95.22/13.53 -------------------------------------------- % 95.22/13.53 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 95.22/13.53 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 95.22/13.53 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, % 95.22/13.53 axiom12, axiom120, axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, % 95.22/13.53 axiom127, axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, % 95.22/13.53 axiom134, axiom135, axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, % 95.22/13.53 axiom141, axiom142, axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, % 95.22/13.53 axiom149, axiom15, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, % 95.22/13.53 axiom156, axiom157, axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, % 95.22/13.53 axiom163, axiom164, axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, % 95.22/13.53 axiom170, axiom171, axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, % 95.22/13.53 axiom178, axiom179, axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, % 95.22/13.53 axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, axiom194, axiom195, % 95.22/13.53 axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, axiom200, axiom201, % 95.22/13.53 axiom202, axiom204, axiom205, axiom206, axiom207, axiom208, axiom209, axiom21, % 95.22/13.53 axiom210, axiom211, axiom213, axiom214, axiom215, axiom216, axiom217, axiom218, % 95.22/13.53 axiom219, axiom22, axiom220, axiom221, axiom222, axiom223, axiom224, axiom225, % 95.22/13.53 axiom226, axiom227, axiom228, axiom229, axiom23, axiom230, axiom231, axiom232, % 95.22/13.53 axiom233, axiom234, axiom235, axiom236, axiom237, axiom238, axiom239, axiom24, % 95.22/13.53 axiom240, axiom241, axiom242, axiom243, axiom244, axiom245, axiom246, axiom247, % 95.22/13.53 axiom248, axiom249, axiom25, axiom250, axiom251, axiom252, axiom253, axiom254, % 95.22/13.53 axiom255, axiom256, axiom257, axiom258, axiom259, axiom26, axiom260, axiom261, % 95.22/13.53 axiom262, axiom263, axiom264, axiom265, axiom266, axiom267, axiom268, axiom269, % 95.22/13.53 axiom27, axiom270, axiom271, axiom272, axiom273, axiom274, axiom275, axiom276, % 95.22/13.53 axiom277, axiom278, axiom279, axiom28, axiom280, axiom281, axiom282, axiom283, % 95.22/13.53 axiom284, axiom285, axiom286, axiom287, axiom288, axiom289, axiom29, axiom290, % 95.22/13.53 axiom291, axiom292, axiom293, axiom294, axiom295, axiom296, axiom297, axiom298, % 95.22/13.53 axiom299, axiom3, axiom30, axiom300, axiom301, axiom302, axiom303, axiom304, % 95.22/13.53 axiom305, axiom306, axiom307, axiom308, axiom309, axiom31, axiom310, axiom311, % 95.22/13.53 axiom312, axiom313, axiom314, axiom315, axiom316, axiom317, axiom318, axiom319, % 95.22/13.53 axiom32, axiom320, axiom321, axiom322, axiom323, axiom324, axiom325, axiom326, % 95.22/13.53 axiom327, axiom328, axiom329, axiom33, axiom330, axiom331, axiom332, axiom333, % 95.22/13.53 axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, axiom34, axiom340, % 95.22/13.53 axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, axiom347, axiom348, % 95.22/13.53 axiom349, axiom35, axiom350, axiom351, axiom352, axiom353, axiom354, axiom355, % 95.22/13.53 axiom356, axiom357, axiom358, axiom359, axiom36, axiom360, axiom361, axiom362, % 95.22/13.53 axiom363, axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, axiom37, % 95.22/13.53 axiom370, axiom371, axiom372, axiom373, axiom374, axiom375, axiom376, axiom377, % 95.22/13.53 axiom378, axiom379, axiom38, axiom380, axiom381, axiom382, axiom383, axiom384, % 95.22/13.53 axiom385, axiom386, axiom387, axiom388, axiom389, axiom39, axiom390, axiom391, % 95.22/13.53 axiom392, axiom393, axiom394, axiom395, axiom396, axiom397, axiom398, axiom399, % 95.22/13.53 axiom4, axiom40, axiom400, axiom401, axiom402, axiom403, axiom404, axiom405, % 95.22/13.53 axiom406, axiom407, axiom408, axiom409, axiom41, axiom410, axiom411, axiom412, % 95.22/13.53 axiom413, axiom414, axiom415, axiom416, axiom417, axiom418, axiom419, axiom42, % 95.22/13.53 axiom420, axiom421, axiom422, axiom423, axiom424, axiom425, axiom426, axiom427, % 95.22/13.53 axiom428, axiom429, axiom43, axiom430, axiom431, axiom432, axiom433, axiom434, % 95.22/13.53 axiom435, axiom436, axiom437, axiom438, axiom439, axiom44, axiom440, axiom441, % 95.22/13.53 axiom442, axiom443, axiom444, axiom445, axiom446, axiom447, axiom448, axiom449, % 95.22/13.53 axiom45, axiom450, axiom451, axiom452, axiom453, axiom454, axiom455, axiom456, % 95.22/13.53 axiom457, axiom458, axiom459, axiom46, axiom460, axiom461, axiom462, axiom463, % 95.22/13.53 axiom464, axiom465, axiom466, axiom467, axiom468, axiom469, axiom47, axiom470, % 95.22/13.53 axiom471, axiom472, axiom473, axiom474, axiom475, axiom476, axiom477, axiom478, % 95.22/13.53 axiom479, axiom48, axiom480, axiom481, axiom482, axiom483, axiom484, axiom485, % 95.22/13.53 axiom486, axiom487, axiom488, axiom489, axiom49, axiom490, axiom491, axiom492, % 95.22/13.53 axiom493, axiom494, axiom495, axiom496, axiom497, axiom498, axiom499, axiom5, % 95.22/13.53 axiom50, axiom500, axiom501, axiom502, axiom503, axiom504, axiom505, axiom506, % 95.22/13.53 axiom507, axiom508, axiom509, axiom51, axiom510, axiom511, axiom512, axiom513, % 95.22/13.53 axiom514, axiom515, axiom516, axiom517, axiom518, axiom519, axiom52, axiom520, % 95.22/13.53 axiom521, axiom522, axiom523, axiom524, axiom525, axiom526, axiom527, axiom528, % 95.22/13.53 axiom529, axiom53, axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, % 95.22/13.53 axiom536, axiom537, axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, % 95.22/13.53 axiom543, axiom544, axiom545, axiom546, axiom547, axiom548, axiom549, axiom55, % 95.22/13.53 axiom550, axiom551, axiom552, axiom553, axiom554, axiom555, axiom556, axiom557, % 95.22/13.53 axiom558, axiom559, axiom56, axiom560, axiom561, axiom562, axiom563, axiom564, % 95.22/13.53 axiom565, axiom566, axiom567, axiom568, axiom569, axiom57, axiom570, axiom571, % 95.22/13.53 axiom572, axiom573, axiom574, axiom575, axiom576, axiom577, axiom578, axiom579, % 95.22/13.53 axiom58, axiom580, axiom581, axiom582, axiom583, axiom584, axiom585, axiom586, % 95.22/13.53 axiom587, axiom588, axiom589, axiom59, axiom590, axiom591, axiom592, axiom593, % 95.22/13.53 axiom594, axiom595, axiom596, axiom597, axiom598, axiom599, axiom6, axiom60, % 95.22/13.53 axiom600, axiom601, axiom602, axiom603, axiom604, axiom605, axiom606, axiom607, % 95.22/13.53 axiom608, axiom609, axiom61, axiom610, axiom611, axiom612, axiom613, axiom614, % 95.22/13.53 axiom615, axiom616, axiom617, axiom618, axiom619, axiom62, axiom620, axiom621, % 95.22/13.53 axiom622, axiom623, axiom624, axiom625, axiom626, axiom627, axiom628, axiom629, % 95.22/13.53 axiom63, axiom630, axiom631, axiom632, axiom633, axiom634, axiom635, axiom636, % 95.22/13.53 axiom637, axiom638, axiom639, axiom64, axiom640, axiom641, axiom642, axiom643, % 95.22/13.53 axiom644, axiom645, axiom646, axiom647, axiom648, axiom649, axiom65, axiom650, % 95.22/13.53 axiom651, axiom652, axiom653, axiom654, axiom655, axiom656, axiom657, axiom658, % 95.22/13.53 axiom659, axiom66, axiom660, axiom661, axiom662, axiom663, axiom664, axiom665, % 95.22/13.53 axiom666, axiom667, axiom668, axiom669, axiom67, axiom670, axiom671, axiom672, % 95.22/13.53 axiom673, axiom674, axiom675, axiom676, axiom677, axiom678, axiom679, axiom68, % 95.22/13.53 axiom680, axiom681, axiom682, axiom683, axiom684, axiom685, axiom686, axiom687, % 95.22/13.53 axiom688, axiom689, axiom69, axiom690, axiom691, axiom692, axiom693, axiom694, % 95.22/13.53 axiom695, axiom696, axiom697, axiom698, axiom699, axiom7, axiom70, axiom700, % 95.22/13.53 axiom701, axiom702, axiom703, axiom704, axiom705, axiom706, axiom707, axiom708, % 95.22/13.53 axiom709, axiom71, axiom710, axiom711, axiom712, axiom713, axiom714, axiom715, % 95.22/13.53 axiom716, axiom717, axiom718, axiom719, axiom72, axiom720, axiom721, axiom722, % 95.22/13.53 axiom723, axiom724, axiom725, axiom726, axiom727, axiom728, axiom729, axiom73, % 95.22/13.53 axiom730, axiom731, axiom732, axiom733, axiom734, axiom735, axiom736, axiom737, % 95.22/13.53 axiom738, axiom739, axiom74, axiom740, axiom741, axiom742, axiom743, axiom744, % 95.22/13.53 axiom745, axiom746, axiom747, axiom748, axiom749, axiom75, axiom750, axiom751, % 95.22/13.53 axiom752, axiom753, axiom754, axiom755, axiom756, axiom757, axiom758, axiom759, % 95.22/13.53 axiom76, axiom760, axiom761, axiom762, axiom763, axiom764, axiom765, axiom766, % 95.22/13.53 axiom767, axiom768, axiom769, axiom77, axiom770, axiom771, axiom772, axiom773, % 95.22/13.53 axiom774, axiom775, axiom776, axiom777, axiom778, axiom779, axiom78, axiom780, % 95.22/13.53 axiom781, axiom782, axiom783, axiom784, axiom785, axiom786, axiom787, axiom788, % 95.22/13.53 axiom789, axiom79, axiom790, axiom791, axiom792, axiom793, axiom794, axiom795, % 95.22/13.53 axiom796, axiom797, axiom798, axiom799, axiom8, axiom80, axiom800, axiom801, % 95.22/13.53 axiom802, axiom803, axiom804, axiom805, axiom806, axiom807, axiom808, axiom809, % 95.22/13.53 axiom81, axiom810, axiom811, axiom812, axiom813, axiom814, axiom815, axiom816, % 95.22/13.53 axiom817, axiom818, axiom819, axiom82, axiom820, axiom821, axiom83, axiom84, % 95.22/13.53 axiom85, axiom86, axiom87, axiom88, axiom89, axiom9, axiom90, axiom91, axiom92, % 95.22/13.53 axiom93, axiom94, axiom95, axiom96, axiom97, axiom98, axiom99, formula_823, % 95.22/13.53 formula_824 % 95.22/13.53 % 95.22/13.53 Those formulas are unsatisfiable: % 95.22/13.53 --------------------------------- % 95.22/13.53 % 95.22/13.53 Begin of proof % 95.22/13.54 | % 95.22/13.54 | ALPHA: (axiom186) implies: % 95.22/13.54 | (1) lSCategory$(c$) = 0 % 95.22/13.54 | % 95.22/13.54 | ALPHA: (axiom187) implies: % 95.22/13.54 | (2) ? [v0: B_set_bool_fun$] : ? [v1: B_set$] : (mor$(c$) = v1 & % 95.22/13.54 | member$b(f$) = v0 & fun_app$m(v0, v1) = 0 & B_set_bool_fun$(v0) & % 95.22/13.54 | B_set$(v1)) % 95.22/13.54 | % 95.22/13.54 | ALPHA: (axiom188) implies: % 95.22/13.54 | (3) ? [v0: B_set_bool_fun$] : ? [v1: B_set$] : (mor$(c$) = v1 & % 95.22/13.54 | member$b(g$) = v0 & fun_app$m(v0, v1) = 0 & B_set_bool_fun$(v0) & % 95.22/13.54 | B_set$(v1)) % 95.22/13.54 | % 95.22/13.54 | ALPHA: (conjecture185) implies: % 95.22/13.54 | (4) A_b_b_c_LSCategory_ext_Category_ext$(c$) % 95.22/13.54 | (5) B$(f$) % 95.22/13.54 | (6) ? [v0: B_a_fun$] : ? [v1: A$] : ? [v2: A_set_bool_fun$] : ? [v3: % 95.22/13.54 | A_set$] : ? [v4: int] : ( ~ (v4 = 0) & dom$(c$) = v0 & obj$(c$) = v3 % 95.22/13.54 | & fun_app$bk(v0, f$) = v1 & member$c(v1) = v2 & fun_app$p(v2, v3) = % 95.22/13.54 | v4 & A_set_bool_fun$(v2) & A$(v1) & A_set$(v3) & B_a_fun$(v0)) % 95.22/13.54 | % 95.22/13.54 | ALPHA: (function-axioms) implies: % 95.22/13.54 | (7) ! [v0: B_set_bool_fun$] : ! [v1: B_set_bool_fun$] : ! [v2: B$] : (v1 % 95.22/13.54 | = v0 | ~ (member$b(v2) = v1) | ~ (member$b(v2) = v0)) % 95.22/13.54 | (8) ! [v0: B_set$] : ! [v1: B_set$] : ! [v2: % 95.22/13.54 | A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (mor$(v2) = v1) % 95.22/13.54 | | ~ (mor$(v2) = v0)) % 95.22/13.54 | (9) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.54 | A_b_b_c_LSCategory_ext_Category_ext$] : (v1 = v0 | ~ (category$(v2) % 95.22/13.54 | = v1) | ~ (category$(v2) = v0)) % 95.22/13.54 | (10) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 95.22/13.54 | B_set$] : ! [v3: B_set_bool_fun$] : (v1 = v0 | ~ (fun_app$m(v3, % 95.22/13.54 | v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) % 95.22/13.54 | % 95.22/13.54 | DELTA: instantiating (2) with fresh symbols all_1121_0, all_1121_1 gives: % 95.22/13.54 | (11) mor$(c$) = all_1121_0 & member$b(f$) = all_1121_1 & % 95.22/13.54 | fun_app$m(all_1121_1, all_1121_0) = 0 & B_set_bool_fun$(all_1121_1) & % 95.22/13.54 | B_set$(all_1121_0) % 95.22/13.54 | % 95.22/13.54 | ALPHA: (11) implies: % 95.22/13.54 | (12) fun_app$m(all_1121_1, all_1121_0) = 0 % 95.22/13.54 | (13) member$b(f$) = all_1121_1 % 95.22/13.54 | (14) mor$(c$) = all_1121_0 % 95.22/13.54 | % 95.22/13.54 | DELTA: instantiating (3) with fresh symbols all_1123_0, all_1123_1 gives: % 95.22/13.55 | (15) mor$(c$) = all_1123_0 & member$b(g$) = all_1123_1 & % 95.22/13.55 | fun_app$m(all_1123_1, all_1123_0) = 0 & B_set_bool_fun$(all_1123_1) & % 95.22/13.55 | B_set$(all_1123_0) % 95.22/13.55 | % 95.22/13.55 | ALPHA: (15) implies: % 95.22/13.55 | (16) mor$(c$) = all_1123_0 % 95.22/13.55 | % 95.22/13.55 | DELTA: instantiating (6) with fresh symbols all_1139_0, all_1139_1, % 95.22/13.55 | all_1139_2, all_1139_3, all_1139_4 gives: % 95.22/13.55 | (17) ~ (all_1139_0 = 0) & dom$(c$) = all_1139_4 & obj$(c$) = all_1139_1 & % 95.22/13.55 | fun_app$bk(all_1139_4, f$) = all_1139_3 & member$c(all_1139_3) = % 95.22/13.55 | all_1139_2 & fun_app$p(all_1139_2, all_1139_1) = all_1139_0 & % 95.22/13.55 | A_set_bool_fun$(all_1139_2) & A$(all_1139_3) & A_set$(all_1139_1) & % 95.22/13.55 | B_a_fun$(all_1139_4) % 95.22/13.55 | % 95.22/13.55 | ALPHA: (17) implies: % 95.22/13.55 | (18) ~ (all_1139_0 = 0) % 95.22/13.55 | (19) fun_app$p(all_1139_2, all_1139_1) = all_1139_0 % 95.22/13.55 | (20) member$c(all_1139_3) = all_1139_2 % 95.22/13.55 | (21) fun_app$bk(all_1139_4, f$) = all_1139_3 % 95.22/13.55 | (22) obj$(c$) = all_1139_1 % 95.22/13.55 | (23) dom$(c$) = all_1139_4 % 95.22/13.55 | % 95.22/13.55 | GROUND_INST: instantiating (8) with all_1121_0, all_1123_0, c$, simplifying % 95.22/13.55 | with (14), (16) gives: % 95.22/13.55 | (24) all_1123_0 = all_1121_0 % 95.22/13.55 | % 95.22/13.55 | GROUND_INST: instantiating (axiom212) with c$, simplifying with (1), (4) % 95.22/13.55 | gives: % 95.22/13.55 | (25) category$(c$) = 0 % 95.22/13.55 | % 95.22/13.55 | GROUND_INST: instantiating (axiom203) with c$, f$, all_1139_4, all_1139_3, % 95.22/13.55 | all_1139_2, all_1139_1, all_1139_0, simplifying with (4), (5), % 95.22/13.55 | (19), (20), (21), (22), (23) gives: % 95.22/13.55 | (26) all_1139_0 = 0 | ? [v0: any] : ? [v1: B_set_bool_fun$] : ? [v2: % 95.22/13.55 | B_set$] : ? [v3: any] : (category$(c$) = v0 & mor$(c$) = v2 & % 95.22/13.55 | member$b(f$) = v1 & fun_app$m(v1, v2) = v3 & B_set_bool_fun$(v1) & % 95.22/13.55 | B_set$(v2) & ( ~ (v3 = 0) | ~ (v0 = 0))) % 95.22/13.55 | % 95.22/13.55 | BETA: splitting (26) gives: % 95.22/13.55 | % 95.22/13.55 | Case 1: % 95.22/13.55 | | % 95.22/13.55 | | (27) all_1139_0 = 0 % 95.22/13.55 | | % 95.22/13.55 | | REDUCE: (18), (27) imply: % 95.22/13.55 | | (28) $false % 95.22/13.55 | | % 95.22/13.55 | | CLOSE: (28) is inconsistent. % 95.22/13.55 | | % 95.22/13.55 | Case 2: % 95.22/13.55 | | % 95.22/13.55 | | (29) ? [v0: any] : ? [v1: B_set_bool_fun$] : ? [v2: B_set$] : ? [v3: % 95.22/13.55 | | any] : (category$(c$) = v0 & mor$(c$) = v2 & member$b(f$) = v1 & % 95.22/13.55 | | fun_app$m(v1, v2) = v3 & B_set_bool_fun$(v1) & B_set$(v2) & ( ~ % 95.22/13.55 | | (v3 = 0) | ~ (v0 = 0))) % 95.22/13.55 | | % 95.22/13.55 | | DELTA: instantiating (29) with fresh symbols all_1316_0, all_1316_1, % 95.22/13.55 | | all_1316_2, all_1316_3 gives: % 95.22/13.55 | | (30) category$(c$) = all_1316_3 & mor$(c$) = all_1316_1 & member$b(f$) = % 95.22/13.55 | | all_1316_2 & fun_app$m(all_1316_2, all_1316_1) = all_1316_0 & % 95.22/13.55 | | B_set_bool_fun$(all_1316_2) & B_set$(all_1316_1) & ( ~ (all_1316_0 = % 95.22/13.55 | | 0) | ~ (all_1316_3 = 0)) % 95.22/13.55 | | % 95.22/13.55 | | ALPHA: (30) implies: % 95.22/13.55 | | (31) fun_app$m(all_1316_2, all_1316_1) = all_1316_0 % 95.22/13.55 | | (32) member$b(f$) = all_1316_2 % 95.22/13.55 | | (33) mor$(c$) = all_1316_1 % 95.22/13.55 | | (34) category$(c$) = all_1316_3 % 95.22/13.55 | | (35) ~ (all_1316_0 = 0) | ~ (all_1316_3 = 0) % 95.22/13.55 | | % 95.22/13.55 | | GROUND_INST: instantiating (7) with all_1121_1, all_1316_2, f$, simplifying % 95.22/13.55 | | with (13), (32) gives: % 95.22/13.55 | | (36) all_1316_2 = all_1121_1 % 95.22/13.55 | | % 95.22/13.55 | | GROUND_INST: instantiating (8) with all_1121_0, all_1316_1, c$, simplifying % 95.22/13.55 | | with (14), (33) gives: % 95.22/13.55 | | (37) all_1316_1 = all_1121_0 % 95.22/13.55 | | % 95.22/13.55 | | GROUND_INST: instantiating (9) with 0, all_1316_3, c$, simplifying with % 95.22/13.55 | | (25), (34) gives: % 95.22/13.55 | | (38) all_1316_3 = 0 % 95.22/13.55 | | % 95.22/13.55 | | REDUCE: (31), (36), (37) imply: % 95.22/13.55 | | (39) fun_app$m(all_1121_1, all_1121_0) = all_1316_0 % 95.22/13.55 | | % 95.22/13.55 | | BETA: splitting (35) gives: % 95.22/13.55 | | % 95.22/13.55 | | Case 1: % 95.22/13.55 | | | % 95.22/13.55 | | | (40) ~ (all_1316_0 = 0) % 95.22/13.55 | | | % 95.22/13.55 | | | GROUND_INST: instantiating (10) with 0, all_1316_0, all_1121_0, % 95.22/13.55 | | | all_1121_1, simplifying with (12), (39) gives: % 95.22/13.55 | | | (41) all_1316_0 = 0 % 95.22/13.55 | | | % 95.22/13.55 | | | REDUCE: (40), (41) imply: % 95.22/13.55 | | | (42) $false % 95.22/13.55 | | | % 95.22/13.55 | | | CLOSE: (42) is inconsistent. % 95.22/13.55 | | | % 95.22/13.55 | | Case 2: % 95.22/13.55 | | | % 95.22/13.55 | | | (43) ~ (all_1316_3 = 0) % 95.22/13.55 | | | % 95.22/13.55 | | | REDUCE: (38), (43) imply: % 95.22/13.55 | | | (44) $false % 95.22/13.55 | | | % 95.22/13.55 | | | CLOSE: (44) is inconsistent. % 95.22/13.55 | | | % 95.22/13.55 | | End of split % 95.22/13.55 | | % 95.22/13.55 | End of split % 95.22/13.55 | % 95.22/13.55 End of proof % 95.22/13.55 % SZS output end Proof for theBenchmark % 95.22/13.56 % 95.22/13.56 12931ms %------------------------------------------------------------------------------