%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SEV646+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n022.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 : Tue May 5 06:56:07 PM UTC 2026 % Result : Theorem 43.66s 43.96s % Output : Proof 43.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV646+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_zenon %s %d % 0.15/0.34 % Computer : n022.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue May 5 07:08:50 EDT 2026 % 0.15/0.34 % CPUTime : % 0.47/0.68 Zenon warning: unused variable (Vvar__1___24Anonymous__107527 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.47/0.68 Zenon warning: unused variable (Vvar__1___24Anonymous__107529 : zenon_U) in $_discrim_Coq.Bool.Bool.ReflectT$Coq.Bool.Bool.ReflectF % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107602 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107606 : zenon_U) in $_discrim_Coq.Init.Datatypes.CompEqT$Coq.Init.Datatypes.CompLtT % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__2035 : zenon_U) in $_discrim_Coq.Init.Specif.inleft$Coq.Init.Specif.inright % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__264 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__267 : zenon_U) in $_discrim_Coq.Init.Specif.left$Coq.Init.Specif.right % 0.47/0.68 Zenon warning: unused variable (Vvar__1___24Anonymous__110483 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__110486 : zenon_U) in $_discrim_Coq.Reals.Rfunctions.ZintNull$Coq.Reals.Rfunctions.ZintPos % 0.47/0.68 Zenon warning: unused variable (Vvar__5___24Anonymous__109588 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.47/0.68 Zenon warning: unused variable (Vvar__5___24Anonymous__109594 : zenon_U) in $_discrim_Coq.Structures.OrderedType.LT$Coq.Structures.OrderedType.EQ % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__112665 : zenon_U) in $_discrim_Coq.setoid_ring.Ring_theory.Abstract$Coq.setoid_ring.Ring_theory.Computational % 0.47/0.68 Zenon warning: unused variable (Vvar__1___24Anonymous__107536 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.47/0.68 Zenon warning: unused variable (Vvar__1___24Anonymous__107537 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectF % 0.47/0.68 Zenon warning: unused variable (Vvar__1___24Anonymous__107532 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.47/0.68 Zenon warning: unused variable (Vvar__1___24Anonymous__107533 : zenon_U) in $_inj_Coq.Bool.Bool.ReflectT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107613 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107614 : zenon_U) in $_inj_Coq.Init.Datatypes.CompEqT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107629 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107630 : zenon_U) in $_inj_Coq.Init.Datatypes.CompGtT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107621 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__107622 : zenon_U) in $_inj_Coq.Init.Datatypes.CompLtT % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__2008 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.47/0.68 Zenon warning: unused variable (Vvar__3___24Anonymous__2009 : zenon_U) in $_inj_Coq.Init.Specif.exist % 0.47/0.68 Zenon warning: unused variable (Vvar__4___24Anonymous__113084 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.47/0.68 Zenon warning: unused variable (Vvar__4___24Anonymous__113085 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.47/0.68 Zenon warning: unused variable (Vvar__5___24Anonymous__113086 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.47/0.68 Zenon warning: unused variable (Vvar__5___24Anonymous__113087 : zenon_U) in $_inj_Coq.Init.Specif.exist2 % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__2046 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__2047 : zenon_U) in $_inj_Coq.Init.Specif.inright % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__272 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__273 : zenon_U) in $_inj_Coq.Init.Specif.left % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__278 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.47/0.68 Zenon warning: unused variable (Vvar__2___24Anonymous__279 : zenon_U) in $_inj_Coq.Init.Specif.right % 0.47/0.68 Zenon warning: unused variable (Vvar__1__cond__neg__109669 : zenon_U) in $_inj_Coq.Reals.RIneq.mknegreal % 0.47/0.68 Zenon warning: unused variable (Vvar__1__cond__neg__109670 : zenon_U) in $_inj_Coq.Reals.RIneq.mknegreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__nonneg__109648 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonnegreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__nonneg__109649 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonnegreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__nonpos__109662 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonposreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__nonpos__109663 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonposreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__nonzero__109676 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__nonzero__109677 : zenon_U) in $_inj_Coq.Reals.RIneq.mknonzeroreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__pos__109655 : zenon_U) in $_inj_Coq.Reals.RIneq.mkposreal % 43.66/43.96 Zenon warning: unused variable (Vvar__1__cond__pos__109656 : zenon_U) in $_inj_Coq.Reals.RIneq.mkposreal % 43.66/43.96 Zenon warning: unused variable (Vvar__2___24Anonymous__110501 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 43.66/43.96 Zenon warning: unused variable (Vvar__2___24Anonymous__110502 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNeg % 43.66/43.96 Zenon warning: unused variable (Vvar__1___24Anonymous__110489 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 43.66/43.96 Zenon warning: unused variable (Vvar__1___24Anonymous__110490 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintNull % 43.66/43.96 Zenon warning: unused variable (Vvar__2___24Anonymous__110495 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 43.66/43.96 Zenon warning: unused variable (Vvar__2___24Anonymous__110496 : zenon_U) in $_inj_Coq.Reals.Rfunctions.ZintPos % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__109617 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__109618 : zenon_U) in $_inj_Coq.Structures.OrderedType.EQ % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__109629 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__109630 : zenon_U) in $_inj_Coq.Structures.OrderedType.GT % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__109605 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__109606 : zenon_U) in $_inj_Coq.Structures.OrderedType.LT % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__113420 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__113421 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 43.66/43.96 Zenon warning: unused variable (Vvar__6___24Anonymous__113422 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 43.66/43.96 Zenon warning: unused variable (Vvar__6___24Anonymous__113423 : zenon_U) in $_inj_Coq.ZArith.Znumtheory.Euclid_intro % 43.66/43.96 Zenon warning: unused variable (Vvar__4___24Anonymous__113479 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 43.66/43.96 Zenon warning: unused variable (Vvar__4___24Anonymous__113480 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__113481 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 43.66/43.96 Zenon warning: unused variable (Vvar__5___24Anonymous__113482 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 43.66/43.96 Zenon warning: unused variable (Vvar__6___24Anonymous__113483 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 43.66/43.96 Zenon warning: unused variable (Vvar__6___24Anonymous__113484 : zenon_U) in $_inj_Coq.ZArith.Zpower.Zdiv_rest_proof % 43.66/43.96 Zenon warning: unused variable (Vvar__3___24Anonymous__112672 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 43.66/43.96 Zenon warning: unused variable (Vvar__3___24Anonymous__112673 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Computational % 43.66/43.96 Zenon warning: unused variable (Vvar__17___24Anonymous__112708 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 43.66/43.96 Zenon warning: unused variable (Vvar__17___24Anonymous__112709 : zenon_U) in $_inj_Coq.setoid_ring.Ring_theory.Morphism % 43.66/43.96 (* PROOF-FOUND *) % 43.66/43.96 % SZS status Theorem % 43.66/43.96 (* BEGIN-PROOF *) % 43.66/43.96 % SZS output start Proof % 43.66/43.96 Theorem _HAMMER_GOAL : (forall V0__s : zenon_U, ((cIntMap_2eFset_2eFSet___24t V0__s)->(forall V1__s_27 : zenon_U, ((cIntMap_2eFset_2eFSet___24t V1__s_27)->(forall V2__s_27_27 : zenon_U, ((cIntMap_2eFset_2eFSet___24t V2__s_27_27)->(cMapaxioms_2eeqmap___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 V0__s V1__s_27) V2__s_27_27) (cIntMap_2eFset_2eFSetUnion___24a2 V0__s (cIntMap_2eFset_2eFSetUnion___24a2 V1__s_27 V2__s_27_27))))))))). % 43.66/43.96 Proof. % 43.66/43.96 assert (zenon_L1_ : (~((cCoq_2eInit_2eDatatypes_2eunit) = (cCoq_2eInit_2eDatatypes_2eunit))) -> False). % 43.66/43.96 do 0 intro. intros zenon_Hbe9. % 43.66/43.96 apply zenon_Hbe9. apply refl_equal. % 43.66/43.96 (* end of lemma zenon_L1_ *) % 43.66/43.96 assert (zenon_L2_ : forall (zenon_TV2__s_27_27_enj : zenon_U) (zenon_TV1__s_27_enk : zenon_U), (~((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj) = (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj))) -> False). % 43.66/43.96 do 2 intro. intros zenon_Hbea. % 43.66/43.96 generalize ($_def_IntMap.Fset.FSetUnion zenon_TV1__s_27_enk). zenon_intro zenon_Hbed. % 43.66/43.96 generalize (zenon_Hbed zenon_TV2__s_27_27_enj). zenon_intro zenon_Hbee. % 43.66/43.96 apply (zenon_congruence_lr_s _ (fun zenon_Vw : _ => (~((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj) = zenon_Vw))) _ _ zenon_Hbea zenon_Hbee). zenon_intro zenon_Hbef. % 43.66/43.96 apply zenon_Hbef. apply refl_equal. % 43.66/43.96 (* end of lemma zenon_L2_ *) % 43.66/43.96 apply NNPP. intro zenon_G. % 43.66/43.96 generalize ($tdef_Type (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hbf0. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hbf0); [ zenon_intro zenon_Hbf3; zenon_intro zenon_Hbf2 | zenon_intro $_typeof_Coq.Init.Datatypes.unit; zenon_intro zenon_Hbf1 ]. % 43.66/43.96 exact (zenon_Hbf3 $_typeof_Coq.Init.Datatypes.unit). % 43.66/43.96 apply (zenon_notallex_s (fun V0__s : zenon_U => ((cIntMap_2eFset_2eFSet___24t V0__s)->(forall V1__s_27 : zenon_U, ((cIntMap_2eFset_2eFSet___24t V1__s_27)->(forall V2__s_27_27 : zenon_U, ((cIntMap_2eFset_2eFSet___24t V2__s_27_27)->(cMapaxioms_2eeqmap___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 V0__s V1__s_27) V2__s_27_27) (cIntMap_2eFset_2eFSetUnion___24a2 V0__s (cIntMap_2eFset_2eFSetUnion___24a2 V1__s_27 V2__s_27_27))))))))) zenon_G); [ zenon_intro zenon_Hbf4; idtac ]. % 43.66/43.96 elim zenon_Hbf4. zenon_intro zenon_TV0__s_ent. zenon_intro zenon_Hbf6. % 43.66/43.96 apply (zenon_notimply_s _ _ zenon_Hbf6). zenon_intro zenon_Hbf8. zenon_intro zenon_Hbf7. % 43.66/43.96 apply (zenon_notallex_s (fun V1__s_27 : zenon_U => ((cIntMap_2eFset_2eFSet___24t V1__s_27)->(forall V2__s_27_27 : zenon_U, ((cIntMap_2eFset_2eFSet___24t V2__s_27_27)->(cMapaxioms_2eeqmap___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent V1__s_27) V2__s_27_27) (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent (cIntMap_2eFset_2eFSetUnion___24a2 V1__s_27 V2__s_27_27))))))) zenon_Hbf7); [ zenon_intro zenon_Hbf9; idtac ]. % 43.66/43.96 elim zenon_Hbf9. zenon_intro zenon_TV1__s_27_enk. zenon_intro zenon_Hbfa. % 43.66/43.96 apply (zenon_notimply_s _ _ zenon_Hbfa). zenon_intro zenon_Hbfc. zenon_intro zenon_Hbfb. % 43.66/43.96 apply (zenon_notallex_s (fun V2__s_27_27 : zenon_U => ((cIntMap_2eFset_2eFSet___24t V2__s_27_27)->(cMapaxioms_2eeqmap___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent zenon_TV1__s_27_enk) V2__s_27_27) (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk V2__s_27_27))))) zenon_Hbfb); [ zenon_intro zenon_Hbfd; idtac ]. % 43.66/43.96 elim zenon_Hbfd. zenon_intro zenon_TV2__s_27_27_enj. zenon_intro zenon_Hbfe. % 43.66/43.96 apply (zenon_notimply_s _ _ zenon_Hbfe). zenon_intro zenon_Hc00. zenon_intro zenon_Hbff. % 43.66/43.96 generalize ($_def_Mapaxioms.eqmap (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc01. % 43.66/43.96 generalize (zenon_Hc01 (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj)). zenon_intro zenon_Hc02. % 43.66/43.96 generalize (zenon_Hc02 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj))). zenon_intro zenon_Hc03. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc03); [ zenon_intro zenon_Hbff; zenon_intro zenon_Hc06 | zenon_intro zenon_Hc05; zenon_intro zenon_Hc04 ]. % 43.66/43.96 generalize (Mapaxioms.MapMerge_assoc (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc07. % 43.66/43.96 apply (zenon_imply_s _ _ zenon_Hc07); [ zenon_intro zenon_Hbf3 | zenon_intro zenon_Hc08 ]. % 43.66/43.96 generalize ($tdef_Type (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hbf0. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hbf0); [ zenon_intro zenon_Hbf3; zenon_intro zenon_Hbf2 | zenon_intro $_typeof_Coq.Init.Datatypes.unit; zenon_intro zenon_Hbf1 ]. % 43.66/43.96 exact (zenon_Hbf2 zenon_Hbf1). % 43.66/43.96 exact (zenon_Hbf3 $_typeof_Coq.Init.Datatypes.unit). % 43.66/43.96 generalize (zenon_Hc08 zenon_TV0__s_ent). zenon_intro zenon_Hc09. % 43.66/43.96 apply (zenon_imply_s _ _ zenon_Hc09); [ zenon_intro zenon_Hc0b | zenon_intro zenon_Hc0a ]. % 43.66/43.96 generalize ($tdef_IntMap.Map.Map (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc0c. % 43.66/43.96 generalize (zenon_Hc0c zenon_TV0__s_ent). zenon_intro zenon_Hc0d. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc0d); [ zenon_intro zenon_Hc0b; zenon_intro zenon_Hc10 | zenon_intro zenon_Hc0f; zenon_intro zenon_Hc0e ]. % 43.66/43.96 generalize ($_def_IntMap.Fset.FSet zenon_TV0__s_ent). zenon_intro zenon_Hc11. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc11); [ zenon_intro zenon_Hc12; zenon_intro zenon_Hc0b | zenon_intro zenon_Hbf8; zenon_intro zenon_Hc0f ]. % 43.66/43.96 exact (zenon_Hc12 zenon_Hbf8). % 43.66/43.96 generalize ($tdef_IntMap.Map.Map (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc0c. % 43.66/43.96 generalize (zenon_Hc0c zenon_TV0__s_ent). zenon_intro zenon_Hc0d. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc0d); [ zenon_intro zenon_Hc0b; zenon_intro zenon_Hc10 | zenon_intro zenon_Hc0f; zenon_intro zenon_Hc0e ]. % 43.66/43.96 exact (zenon_Hc0b zenon_Hc0f). % 43.66/43.96 exact (zenon_Hc10 zenon_Hc0e). % 43.66/43.96 exact (zenon_Hc0b zenon_Hc0f). % 43.66/43.96 generalize (zenon_Hc0a zenon_TV1__s_27_enk). zenon_intro zenon_Hc13. % 43.66/43.96 apply (zenon_imply_s _ _ zenon_Hc13); [ zenon_intro zenon_Hc15 | zenon_intro zenon_Hc14 ]. % 43.66/43.96 generalize ($tdef_IntMap.Map.Map (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc0c. % 43.66/43.96 generalize (zenon_Hc0c zenon_TV1__s_27_enk). zenon_intro zenon_Hc16. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc16); [ zenon_intro zenon_Hc15; zenon_intro zenon_Hc19 | zenon_intro zenon_Hc18; zenon_intro zenon_Hc17 ]. % 43.66/43.96 generalize ($_def_IntMap.Fset.FSet zenon_TV1__s_27_enk). zenon_intro zenon_Hc1a. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc1a); [ zenon_intro zenon_Hc1b; zenon_intro zenon_Hc15 | zenon_intro zenon_Hbfc; zenon_intro zenon_Hc18 ]. % 43.66/43.96 exact (zenon_Hc1b zenon_Hbfc). % 43.66/43.96 generalize ($tdef_IntMap.Map.Map (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc0c. % 43.66/43.96 generalize (zenon_Hc0c zenon_TV1__s_27_enk). zenon_intro zenon_Hc16. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc16); [ zenon_intro zenon_Hc15; zenon_intro zenon_Hc19 | zenon_intro zenon_Hc18; zenon_intro zenon_Hc17 ]. % 43.66/43.96 exact (zenon_Hc15 zenon_Hc18). % 43.66/43.96 exact (zenon_Hc19 zenon_Hc17). % 43.66/43.96 exact (zenon_Hc15 zenon_Hc18). % 43.66/43.96 generalize (zenon_Hc14 zenon_TV2__s_27_27_enj). zenon_intro zenon_Hc1c. % 43.66/43.96 apply (zenon_imply_s _ _ zenon_Hc1c); [ zenon_intro zenon_Hc1e | zenon_intro zenon_Hc1d ]. % 43.66/43.96 generalize ($tdef_IntMap.Map.Map (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc0c. % 43.66/43.96 generalize (zenon_Hc0c zenon_TV2__s_27_27_enj). zenon_intro zenon_Hc1f. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc1f); [ zenon_intro zenon_Hc1e; zenon_intro zenon_Hc22 | zenon_intro zenon_Hc21; zenon_intro zenon_Hc20 ]. % 43.66/43.96 generalize ($_def_IntMap.Fset.FSet zenon_TV2__s_27_27_enj). zenon_intro zenon_Hc23. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc23); [ zenon_intro zenon_Hc24; zenon_intro zenon_Hc1e | zenon_intro zenon_Hc00; zenon_intro zenon_Hc21 ]. % 43.66/43.96 exact (zenon_Hc24 zenon_Hc00). % 43.66/43.96 generalize ($tdef_IntMap.Map.Map (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc0c. % 43.66/43.96 generalize (zenon_Hc0c zenon_TV2__s_27_27_enj). zenon_intro zenon_Hc1f. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc1f); [ zenon_intro zenon_Hc1e; zenon_intro zenon_Hc22 | zenon_intro zenon_Hc21; zenon_intro zenon_Hc20 ]. % 43.66/43.96 exact (zenon_Hc1e zenon_Hc21). % 43.66/43.96 exact (zenon_Hc22 zenon_Hc20). % 43.66/43.96 exact (zenon_Hc1e zenon_Hc21). % 43.66/43.96 generalize ($_def_Mapaxioms.eqmap (cCoq_2eInit_2eDatatypes_2eunit)). zenon_intro zenon_Hc01. % 43.66/43.96 generalize (zenon_Hc01 (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj)). zenon_intro zenon_Hc25. % 43.66/43.96 generalize (zenon_Hc25 (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj))). zenon_intro zenon_Hc26. % 43.66/43.96 apply (zenon_equiv_s _ _ zenon_Hc26); [ zenon_intro zenon_Hc29; zenon_intro zenon_Hc28 | zenon_intro zenon_Hc1d; zenon_intro zenon_Hc27 ]. % 43.66/43.96 exact (zenon_Hc29 zenon_Hc1d). % 43.66/43.96 cut ((cIntMap_2eMap_2eeqm___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj)) (cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj)))) = (cIntMap_2eMap_2eeqm___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj)) (cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj))))). % 43.66/43.96 intro zenon_D_pnotp. % 43.66/43.96 apply zenon_Hc06. % 43.66/43.96 rewrite <- zenon_D_pnotp. % 43.66/43.96 exact zenon_Hc27. % 43.66/43.96 cut (((cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj))) = (cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj))))); [idtac | apply NNPP; zenon_intro zenon_Hc2a]. % 43.66/43.96 cut (((cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj)) = (cIntMap_2eMap_2eMapGet___24a2 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj)))); [idtac | apply NNPP; zenon_intro zenon_Hc2b]. % 43.66/43.96 cut (((cCoq_2eInit_2eDatatypes_2eunit) = (cCoq_2eInit_2eDatatypes_2eunit))); [idtac | apply NNPP; zenon_intro zenon_Hbe9]. % 43.66/43.96 congruence. % 43.66/43.96 apply zenon_Hbe9. apply refl_equal. % 43.66/43.96 cut (((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj) = (cIntMap_2eFset_2eFSetUnion___24a2 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj))); [idtac | apply NNPP; zenon_intro zenon_Hc2c]. % 43.66/43.96 cut (((cCoq_2eInit_2eDatatypes_2eunit) = (cCoq_2eInit_2eDatatypes_2eunit))); [idtac | apply NNPP; zenon_intro zenon_Hbe9]. % 43.66/43.96 congruence. % 43.66/43.96 apply zenon_Hbe9. apply refl_equal. % 43.66/43.96 generalize ($_def_IntMap.Fset.FSetUnion (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent zenon_TV1__s_27_enk)). zenon_intro zenon_Hc2d. % 43.66/43.96 generalize (zenon_Hc2d zenon_TV2__s_27_27_enj). zenon_intro zenon_Hc2e. % 43.66/43.96 apply (zenon_congruence_lr_s _ (fun zenon_Vq : _ => (~((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent zenon_TV1__s_27_enk) zenon_TV2__s_27_27_enj) = zenon_Vq))) _ _ zenon_Hc2c zenon_Hc2e). zenon_intro zenon_Hc2f. % 43.66/44.03 cut ((zenon_TV2__s_27_27_enj = zenon_TV2__s_27_27_enj)); [idtac | apply NNPP; zenon_intro zenon_Hc30]. % 43.66/44.03 cut (((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent zenon_TV1__s_27_enk) = (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent zenon_TV1__s_27_enk))); [idtac | apply NNPP; zenon_intro zenon_Hc31]. % 43.66/44.03 cut (((cCoq_2eInit_2eDatatypes_2eunit) = (cCoq_2eInit_2eDatatypes_2eunit))); [idtac | apply NNPP; zenon_intro zenon_Hbe9]. % 43.66/44.03 congruence. % 43.66/44.03 apply zenon_Hbe9. apply refl_equal. % 43.66/44.03 generalize ($_def_IntMap.Fset.FSetUnion zenon_TV0__s_ent). zenon_intro zenon_Hc32. % 43.66/44.03 generalize (zenon_Hc32 zenon_TV1__s_27_enk). zenon_intro zenon_Hc33. % 43.66/44.03 apply (zenon_congruence_lr_s _ (fun zenon_Vs : _ => (~((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent zenon_TV1__s_27_enk) = zenon_Vs))) _ _ zenon_Hc31 zenon_Hc33). zenon_intro zenon_Hc34. % 43.66/44.03 apply zenon_Hc34. apply refl_equal. % 43.66/44.03 apply zenon_Hc30. apply refl_equal. % 43.66/44.03 cut (((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj)) = (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV0__s_ent (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj)))); [idtac | apply NNPP; zenon_intro zenon_Hc35]. % 43.66/44.03 cut (((cCoq_2eInit_2eDatatypes_2eunit) = (cCoq_2eInit_2eDatatypes_2eunit))); [idtac | apply NNPP; zenon_intro zenon_Hbe9]. % 43.66/44.03 congruence. % 43.66/44.03 apply zenon_Hbe9. apply refl_equal. % 43.66/44.03 generalize ($_def_IntMap.Fset.FSetUnion zenon_TV0__s_ent). zenon_intro zenon_Hc32. % 43.66/44.03 generalize (zenon_Hc32 (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj)). zenon_intro zenon_Hc36. % 43.66/44.03 apply (zenon_congruence_lr_s _ (fun zenon_Vu : _ => (~((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV0__s_ent (cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj)) = zenon_Vu))) _ _ zenon_Hc35 zenon_Hc36). zenon_intro zenon_Hc37. % 43.66/44.03 cut (((cIntMap_2eMap_2eMapMerge___24a3 (cCoq_2eInit_2eDatatypes_2eunit) zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj) = (cIntMap_2eFset_2eFSetUnion___24a2 zenon_TV1__s_27_enk zenon_TV2__s_27_27_enj))); [idtac | apply NNPP; zenon_intro zenon_Hbea]. % 43.66/44.03 cut ((zenon_TV0__s_ent = zenon_TV0__s_ent)); [idtac | apply NNPP; zenon_intro zenon_Hc38]. % 43.66/44.03 cut (((cCoq_2eInit_2eDatatypes_2eunit) = (cCoq_2eInit_2eDatatypes_2eunit))); [idtac | apply NNPP; zenon_intro zenon_Hbe9]. % 43.66/44.03 congruence. % 43.66/44.03 apply zenon_Hbe9. apply refl_equal. % 43.66/44.03 apply zenon_Hc38. apply refl_equal. % 43.66/44.03 apply (zenon_L2_ zenon_TV2__s_27_27_enj zenon_TV1__s_27_enk); trivial. % 43.66/44.03 exact (zenon_Hbff zenon_Hc05). % 43.66/44.03 Qed. % 43.66/44.03 % SZS output end Proof % 43.66/44.03 (* END-PROOF *) % 43.66/44.03 nodes searched: 162613 % 43.66/44.03 max branch formulas: 90134 % 43.66/44.03 proof nodes created: 92 % 43.66/44.03 formulas created: 3857579 % 43.66/44.03 %------------------------------------------------------------------------------