%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW323+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 12 07:16:44 PM UTC 2026 % Result : Theorem 72.02s 69.91s % Output : Proof 72.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW323+1 : TPTP v9.2.1. Released v5.2.0. % 0.00/0.13 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.16/0.34 % Computer : n001.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 11 14:32:19 EDT 2026 % 0.16/0.34 % CPUTime : % 72.02/69.91 % SZS status Theorem % 72.02/69.91 % SZS output start Proof % 72.02/69.92 % 72.02/69.92 =============================================================== % 72.02/69.92 TPTP Problem: conj_5 (conjecture with 5232 axiom(s)) % 72.02/69.92 Axioms: [fact_ext,fact_empty,fact_hoare__derivs_Oequations_I1_J,fact_triple_Oinject,fact_cut,fact_hoare__derivs_Oinsert,fact_derivs__insertD,fact_finite__imageI,fact_finite_OinsertI,fact_finite_OemptyI,fact_image__eqI,fact_insertE,fact_insertCI,fact_emptyE,fact_image__constant,fact_image__constant__conv,fact_insert__image,fact_singleton__iff,fact_singletonE,fact_equalityCE,fact_eq__mem__trans,fact_eqelem__imp__iff,fact_eqset__imp__iff,fact_mem__def,fact_finite__code,fact_finite,fact_insert__code,fact_insert__commute,fact_insert__absorb2,fact_image__image,fact_equals0D,fact_empty__iff,fact_ex__in__conv,fact_all__not__in__conv,fact_insert__absorb,fact_insertI2,fact_insert__ident,fact_insert__iff,fact_insertI1,fact_rev__image__eqI,fact_imageI,fact_image__iff,fact_finite_Oequations_I1_J,fact_singleton__inject,fact_doubleton__eq__iff,fact_insert__not__empty,fact_empty__not__insert,fact_finite__insert,fact_image__is__empty,fact_image__empty,fact_empty__is__image,fact_image__insert,fact_the__elem__eq,fact_bot__fun__def,fact_bot__empty__eq,fact_triple_Osimps_I2_J,fact_triple_Orecs,fact_folding__one_Oinsert,fact_bot__apply,fact_escape,fact_folding__one__idem_Oinsert__idem,fact_hoare__derivs_Oequations_I7_J,fact_hoare__derivs_OSkip,fact_conseq1,fact_folding__one__idem_Oidem,fact_eq__mem,fact_folding__one_Osingleton,fact_folding__one__idem_Oin__idem,fact_pred__equals__eq,fact_folding__one_Oclosed,fact_conseq2,fact_Comp,fact_the__elem__def,fact_LoopF,fact_folding__one__idem_Ohom__commute,fact_folding__image__simple_Oinsert,fact_folding__one_Oremove,fact_folding__image__simple__idem_Oinsert__idem,fact_finite__induct,fact_folding__image__simple__idem_Oin__idem,fact_image__ident,fact_DiffE,fact_DiffI,fact_finite__Diff,fact_Diff__idemp,fact_folding__image__simple__idem_Oidem,fact_DiffD2,fact_DiffD1,fact_Diff__iff,fact_Diff__cancel,fact_Diff__empty,fact_empty__Diff,fact_finite__Diff2,fact_folding__image__simple_Oinsert__remove,fact_insert__Diff1,fact_insert__Diff__if,fact_insert__Diff__single,fact_Diff__insert2,fact_Diff__insert,fact_finite__Diff__insert,fact_folding__image__simple_Oempty,fact_folding__image__simple_Oremove,fact_insert__Diff,fact_Diff__insert__absorb,fact_folding__one_Oinsert__remove,fact_fun__diff__def,fact_com_Osimps_I12_J,fact_com_Osimps_I13_J,fact_com_Osimps_I16_J,fact_com_Osimps_I17_J,fact_com_Osimps_I46_J,fact_com_Osimps_I47_J,fact_minus__apply,fact_fun__upd__image,fact_finite__empty__induct,fact_fun__left__comm__idem__remove,fact_the__sym__eq__trivial,fact_fun__upd__triv,fact_fun__upd__idem__iff,fact_fun__upd__upd,fact_fun__upd__same,fact_fun__upd__apply,fact_fun__upd__twist,fact_fun__upd__other,fact_fun__upd__idem,fact_fun__left__comm__idem_Ofun__left__idem,fact_fun__upd__def,fact_fun__left__comm__idem_Ofun__left__comm__idem__apply,fact_fun__left__comm__idem__insert,fact_com_Osimps_I5_J,fact_com_Osimps_I3_J,fact_the__eq__trivial,fact_fold__graph_H_Ointros_I2_J,fact_Diff1__fold__graph,fact_inj__on__insert,fact_folding__one_Oeq__fold_H,fact_minus__fold__remove,fact_the__inv__into__def,fact_subset__insert__iff,fact_diff__single__insert,fact_setsum__diff1,fact_setsum__diff1__ring,fact_override__on__def,fact_order__refl,fact_equalityI,fact_subsetD,fact_empty__subsetI,fact_inj__on__empty,fact_linorder__le__cases,fact_le__funE,fact_xt1_I6_J,fact_xt1_I5_J,fact_order__trans,fact_order__antisym,fact_xt1_I4_J,fact_ord__le__eq__trans,fact_xt1_I3_J,fact_ord__eq__le__trans,fact_predicate1D,fact_order__antisym__conv,fact_le__funD,fact_order__eq__refl,fact_rev__predicate1D,fact_order__eq__iff,fact_linorder__linear,fact_le__fun__def,fact_setsum__commute,fact_equalityE,fact_subset__trans,fact_equalityD2,fact_equalityD1,fact_set__eq__subset,fact_subset__refl,fact_subset__inj__on,fact_inj__on__def,fact_inj__on__id2,fact_the__inv__into__f__eq,fact_the__inv__into__f__f,fact_the__inv__into__onto,fact_inj__on__the__inv__into,fact_the__inv__into__into,fact_setsum__diff__nat,fact_setsum__subtractf,fact_fold__def,fact_endo__inj__surj,fact_finite__surj__inj,fact_inj__on__image__set__diff,fact_inj__onD,fact_inj__on__iff,fact_inj__on__contraD,fact_inj__on__diff,fact_setsum__diff,fact_fold__graph_H_Ointros_I1_J,fact_fold__graph_H_Oequations_I1_J,fact_fold__empty,fact_f__the__inv__into__f,fact_set__mp,fact_set__rev__mp,fact_in__mono,fact_bot__least,fact_subset__empty,fact_finite__subset,fact_rev__finite__subset,fact_insert__mono,fact_subset__insertI2,fact_subset__insertI,fact_image__mono,fact_subset__image__iff,fact_double__diff,fact_Diff__mono,fact_Diff__subset,fact_thin,fact_weaken,fact_asm,fact_empty__fold__graphE,fact_fold__graph_OemptyI,fact_fold__graph_Oequations_I1_J,fact_fold__graph__imp__finite,fact_pred__subset__eq,fact_finite__imageD,fact_subset__insert,fact_insert__subset,fact_subset__singletonD,fact_finite__surj,fact_image__diff__subset,fact_fold__graph_OinsertI,fact_setsum__diff1__nat,fact_folding__image__simple__idem_Osubset__idem,fact_inj__on__fun__updI,fact_override__on__apply__in,fact_override__on__apply__notin,fact_override__on__emptyset,fact_fun__left__comm__idem_Ofold__insert__idem2,fact_fun__left__comm__idem_Ofold__insert__idem,fact_folding__one__idem_Oeq__fold__idem_H,fact_folding__one__idem_Osubset__idem,fact_inj__on__iff__surj,fact_fun__left__comm_Ofold__rec,fact_fold1Set_Ointros,fact_flat__lub__def,fact_fun__left__comm_Ofold__insert__remove,fact_fold__graph_H_Oequations_I2_J,fact_diff__eq__diff__less__eq,fact_fun__left__comm_Ofold__insert2,fact_fun__left__comm_Ofold__insert,fact_finite__subset__induct,fact_setsum_Oremove,fact_fun__left__comm_Ofun__left__comm,fact_add__right__imp__eq,fact_add__imp__eq,fact_add__left__imp__eq,fact_add__right__cancel,fact_add__left__cancel,fact_ab__semigroup__add__class_Oadd__ac_I1_J,fact_add__le__imp__le__left,fact_add__le__imp__le__right,fact_add__mono,fact_add__left__mono,fact_add__right__mono,fact_add__le__cancel__left,fact_add__le__cancel__right,fact_add__diff__cancel,fact_diff__add__cancel,fact_fun__left__comm_Ofun__left__comm__apply,fact_setsum__addf,fact_fun__left__comm_Ofold__graph__determ,fact_empty__fold1SetE,fact_fold1Set__nonempty,fact_setsum_Odistrib,fact_diff__eq__diff__eq,fact_fun__left__comm_Ofold__fun__comm,fact_fun__left__comm_Ofold__equality,fact_fold1Set__sing,fact_setsum_Oinsert,fact_setsum__insert,fact_setsum_Oinsert__remove,fact_fun__left__comm_Ofold__graph__fold,fact_setsum__diff1_H,fact_fun__left__comm_Ofold__graph__insertE__aux,fact_fold1Set_Oequations,fact_insert__fold1SetE,fact_fun__left__comm_Ofold__graph__insertE,fact_fold__graph__permute__diff,fact_setsum__reindex__cong,fact_psubset__insert__iff,fact_comm__monoid__big_Oinfinite,fact_Max__mono,fact_Min__antimono,fact_finite__nonempty__imp__fold1Set,fact_ab__semigroup__mult__class_Omult__ac_I1_J,fact_mult__left__idem,fact_mult__idem,fact_times_Oidem,fact_linorder__cases,fact_order__less__asym,fact_xt1_I10_J,fact_order__less__trans,fact_xt1_I2_J,fact_ord__less__eq__trans,fact_xt1_I1_J,fact_ord__eq__less__trans,fact_xt1_I9_J,fact_order__less__asym_H,fact_order__less__imp__not__eq2,fact_order__less__imp__not__eq,fact_order__less__imp__not__less,fact_order__less__not__sym,fact_less__imp__neq,fact_linorder__neqE,fact_linorder__antisym__conv3,fact_linorder__less__linear,fact_not__less__iff__gr__or__eq,fact_linorder__neq__iff,fact_order__less__irrefl,fact_psubset__trans,fact_less__fun__def,fact_xt1_I8_J,fact_order__le__less__trans,fact_xt1_I7_J,fact_order__less__le__trans,fact_xt1_I11_J,fact_order__le__neq__trans,fact_order__le__imp__less__or__eq,fact_linorder__antisym__conv2,fact_order__less__imp__le,fact_leD,fact_xt1_I12_J,fact_order__neq__le__trans,fact_linorder__antisym__conv1,fact_not__leE,fact_leI,fact_order__le__less,fact_less__le__not__le,fact_order__less__le,fact_linorder__le__less__linear,fact_linorder__not__le,fact_linorder__not__less,fact_psubsetD,fact_add__less__cancel__right,fact_add__less__cancel__left,fact_add__strict__right__mono,fact_add__strict__left__mono,fact_add__strict__mono,fact_add__less__imp__less__right,fact_add__less__imp__less__left,fact_not__psubset__empty,fact_diff__eq__diff__less,fact_subset__psubset__trans,fact_psubset__subset__trans,fact_psubset__imp__subset,fact_subset__iff__psubset__eq,fact_psubset__eq,fact_fun__left__comm,fact_fun__left__comm__idem,fact_setsum__right__distrib,fact_setsum__left__distrib,fact_setsum__product,fact_add__le__less__mono,fact_add__less__le__mono,fact_inj__on__strict__subset,fact_Min_Osingleton,fact_Max_Osingleton,fact_fold__graph__insert__swap,fact_Min__le,fact_Max__ge,fact_Min__in,fact_Max__in,fact_less__add__iff2,fact_less__add__iff1,fact_le__add__iff2,fact_le__add__iff1,fact_eq__add__iff2,fact_eq__add__iff1,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J,fact_crossproduct__noteq,fact_comm__semiring__class_Odistrib,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I8_J,fact_linorder__neqE__linordered__idom,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,fact_crossproduct__eq,fact_combine__common__factor,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J,fact_setsum__strict__mono,fact_Min_Oremove,fact_Max_Oremove,fact_fold1__eq__fold,fact_fold1__insert,fact_setprod_Oremove,fact_Min__eqI,fact_Max__eqI,fact_minus__Max__eq__Min,fact_minus__Min__eq__Max,fact_ComplI,fact_inj__uminus,fact_neg__equal__iff__equal,fact_minus__equation__iff,fact_equation__minus__iff,fact_minus__min__eq__max,fact_minus__max__eq__min,fact_minus__minus,fact_min__max_Odistrib__sup__le,fact_min__max_Odistrib__inf__le,fact_min__max_Oinf__sup__distrib2,fact_min__max_Osup__inf__distrib2,fact_min__max_Oinf__assoc,fact_min__max_Oinf_Oassoc,fact_min__max_Osup__assoc,fact_min__max_Osup_Oassoc,fact_compl__eq__compl__iff,fact_min__max_Oinf__sup__distrib1,fact_min__max_Osup__inf__distrib1,fact_min__max_Oinf__left__commute,fact_min__max_Oinf_Oleft__commute,fact_min__max_Osup__left__commute,fact_min__max_Osup_Oleft__commute,fact_min__max_Oinf__left__idem,fact_min__max_Oinf_Oleft__idem,fact_min__max_Osup__left__idem,fact_min__max_Osup_Oleft__idem,fact_min__max_Oinf__sup__absorb,fact_min__max_Osup__inf__absorb,fact_min__max_Oinf__commute,fact_min__max_Oinf_Ocommute,fact_min__max_Osup__commute,fact_min__max_Osup_Ocommute,fact_uminus__apply,fact_min__max_Oinf_Oidem,fact_min__max_Osup_Oidem,fact_double__compl,fact_fun__Compl__def,fact_Min_Oidem,fact_Max_Oidem,fact_min__max_Ole__supE,fact_min__max_Osup__mono,fact_min__max_Osup__least,fact_min__max_Ole__supI,fact_min__max_Osup__absorb1,fact_min__max_Osup__absorb2,fact_min__max_Ole__supI2,fact_min__max_Ole__supI1,fact_min__max_Ole__sup__iff,fact_min__max_Ole__iff__sup,fact_le__maxI2,fact_le__maxI1,fact_le__max__iff__disj,fact_compl__mono,fact_compl__le__compl__iff,fact_le__minus__iff,fact_minus__le__iff,fact_neg__le__iff__le,fact_le__imp__neg__le,fact_min__max_Ole__infE,fact_min__max_Oinf__mono,fact_min__max_Oinf__greatest,fact_min__max_Ole__infI,fact_min__max_Oinf__absorb2,fact_min__max_Oinf__absorb1,fact_min__max_Ole__infI2,fact_min__max_Ole__infI1,fact_min__max_Ole__inf__iff,fact_min__max_Ole__iff__inf,fact_min__max_Oinf__le2,fact_min__max_Oinf__le1,fact_min__le__iff__disj,fact_min__max_Oless__supI2,fact_min__max_Oless__supI1,fact_max__less__iff__conj,fact_less__max__iff__disj,fact_neg__less__iff__less,fact_minus__less__iff,fact_less__minus__iff,fact_min__max_Oless__infI2,fact_min__max_Oless__infI1,fact_min__less__iff__disj,fact_min__less__iff__conj,fact_max__add__distrib__left,fact_minus__add__distrib,fact_minus__add,fact_add__minus__cancel,fact_minus__add__cancel,fact_minus__mult__right,fact_minus__mult__left,fact_minus__mult__commute,fact_minus__mult__minus,fact_square__eq__iff,fact_min__add__distrib__left,fact_ComplE,fact_ComplD,fact_Compl__iff,fact_Max_OF__eq,fact_Min_OF__eq,fact_max__diff__distrib__left,fact_minus__diff__eq,fact_min__diff__distrib__left,fact_Compl__anti__mono,fact_Compl__subset__Compl__iff,fact_setprod__timesf,fact_min__max_Ofun__left__comm__idem__sup,fact_min__max_Ofun__left__comm__idem__inf,fact_min__max_Ofold1__belowI,fact_fold1__below__iff,fact_min__max_Obelow__fold1__iff,fact_setsum__negf,fact_fold1__strict__below__iff,fact_strict__below__fold1__iff,fact_fold1__antimono,fact_diff__def,fact_ab__diff__minus,fact_diff__minus__eq__add,fact_comm__ring__1__class_Onormalizing__ring__rules_I2_J,fact_subset__Compl__self__eq,fact_setprod_Odistrib,fact_fold1__singleton__def,fact_fold1__singleton,fact_folding__one_Oeq__fold,fact_min__max_Ofold__sup__insert,fact_Max_Oin__idem,fact_min__max_Ofold__inf__insert,fact_Min_Oin__idem,fact_fold1__def,fact_setprod_Oinsert,fact_setprod__insert,fact_min__max_Osup__le__fold__sup,fact_min__max_Ofold__inf__le__inf,fact_Max__insert,fact_Min__insert,fact_Max_Osubset__idem,fact_Min_Osubset__idem,fact_Max_Oeq__fold__idem_H,fact_Min_Oeq__fold__idem_H,fact_setprod_Oinsert__remove,fact_fold1__insert__idem,fact_fold1__eq__fold__idem,fact_Max_Oinsert,fact_Min_Oinsert,fact_Max_Oinsert__remove,fact_Min_Oinsert__remove,fact_Max_Oeq__fold_H,fact_Min_Oeq__fold_H,fact_semilattice__big_OF__eq,fact_dual__min,fact_dual__max,fact_max__ord__max,fact_min__ord__min,fact_Max_Oclosed,fact_Min_Oclosed,fact_fold1__in,fact_min__max_OSup__fin_Oremove,fact_min__max_OInf__fin_Oremove,fact_Compl__eq__Compl__iff,fact_double__complement,fact_min__max_OInf__le__Sup,fact_min__max_OInf__fin_Oin__idem,fact_min__max_OSup__fin_Oin__idem,fact_min__max_OInf__fin_Osingleton,fact_min__max_OSup__fin_Osingleton,fact_min__max_OInf__fin_OF__eq,fact_min__max_OSup__fin_OF__eq,fact_min__max_OInf__fin_Oinsert__idem,fact_min__max_OSup__fin_Oinsert__idem,fact_min__max_OInf__fin_Osubset__idem,fact_min__max_OSup__fin_Osubset__idem,fact_min__max_Oinf__Sup__absorb,fact_min__max_Osup__Inf__absorb,fact_min__max_OInf__fin_Oeq__fold__idem_H,fact_min__max_OSup__fin_Oeq__fold__idem_H,fact_min__max_OInf__fin_Oinsert,fact_min__max_OSup__fin_Oinsert,fact_min__max_OInf__fin_Oinsert__remove,fact_min__max_OSup__fin_Oinsert__remove,fact_min__max_OInf__fin_Oeq__fold_H,fact_min__max_OSup__fin_Oeq__fold_H,fact_min__max_OSup__fin_Oclosed,fact_min__max_OInf__fin_Oclosed,fact_min__max_OSup__fin_Ohom__commute,fact_min__max_OInf__fin_Ohom__commute,fact_Max_Ohom__commute,fact_Min_Ohom__commute,fact_hom__fold1__commute,fact_min__max_Ofold__sup__le__sup,fact_min__max_Oinf__le__fold__inf,fact_card__Diff2__less,fact_card__Diff1__less,fact_inj__image__Compl__subset,fact_fold__image__insert,fact_setsum__mono,fact_min__max_OSup__fin_Ounion__idem,fact_min__max_OInf__fin_Ounion__idem,fact_Max__Un,fact_Min__Un,fact_top1I,fact_sup1E,fact_sup1CI,fact_UNIV__I,fact_UnE,fact_UnCI,fact_finite__option__UNIV,fact_finite__Plus__UNIV__iff,fact_finite__Prod__UNIV,fact_Sup__fin_Oidem,fact_Un__UNIV__left,fact_Un__UNIV__right,fact_Un__absorb,fact_Un__commute,fact_Un__left__absorb,fact_Un__left__commute,fact_Un__assoc,fact_bex__Un,fact_ball__Un,fact_top__apply,fact_sup1I1,fact_sup1I2,fact_sup__top__left,fact_sup__top__right,fact_sup_Oidem,fact_sup__idem,fact_sup__fun__def,fact_sup_Ocommute,fact_inf__sup__aci_I5_J,fact_sup__commute,fact_sup_Oleft__idem,fact_inf__sup__aci_I8_J,fact_sup__left__idem,fact_sup_Oleft__commute,fact_inf__sup__aci_I7_J,fact_sup__left__commute,fact_sup_Oassoc,fact_inf__sup__aci_I6_J,fact_sup__assoc,fact_sup__apply,fact_finite__fun__UNIVD2,fact_card__eq__UNIV__imp__eq__UNIV,fact_Compl__partition,fact_Compl__partition2,fact_sup__compl__top,fact_compl__sup__top,fact_inf__sup__ord_I3_J,fact_sup__ge1,fact_inf__sup__ord_I4_J,fact_sup__ge2,fact_le__iff__sup,fact_le__sup__iff,fact_le__supI1,fact_le__supI2,fact_sup__absorb2,fact_sup__absorb1,fact_le__supI,fact_sup__least,fact_sup__mono,fact_le__supE,fact_less__supI1,fact_less__supI2,fact_sup__bot__left,fact_sup__bot__right,fact_sup__eq__bot__iff,fact_Un__iff,fact_UnI1,fact_UnI2,fact_sup__max,fact_Un__empty__left,fact_Un__empty__right,fact_Un__empty,fact_finite__Un,fact_finite__UnI,fact_Un__insert__right,fact_Un__insert__left,fact_Un__upper1,fact_Un__upper2,fact_subset__Un__eq,fact_Un__absorb1,fact_Un__absorb2,fact_Un__least,fact_Un__mono,fact_image__Un,fact_Un__Diff__cancel,fact_Un__Diff__cancel2,fact_Un__Diff,fact_UNIV__not__empty,fact_finite__UNIV,fact_subset__UNIV,fact_inj__eq,fact_injD,fact_fold__image__empty,fact_fun__left__comm__idem__sup,fact_sup__Un__eq,fact_range__composition,fact_inj__fun,fact_top__greatest,fact_fold__image__def,fact_card__insert__le,fact_card__mono,fact_card__seteq,fact_card__image__le,fact_pigeonhole,fact_card__image,fact_insert__is__Un,fact_Diff__subset__conv,fact_Diff__partition,fact_psubset__card__mono,fact_inj__on__Un__image__eq__iff,fact_rangeI,fact_range__eqI,fact_image__eq__fold__image,fact_Diff__UNIV,fact_Compl__Diff__eq,fact_inj__image__eq__iff,fact_Compl__empty__eq,fact_Compl__UNIV__eq,fact_finite__compl,fact_Compl__eq__Diff__UNIV,fact_inj__singleton,fact_finite__range__imageI,fact_the__inv__f__f,fact_folding__image__simple__idem_Ounion__idem,fact_folding__image__simple_Oeq__fold__g,fact_inj__on__iff__eq__card,fact_eq__card__imp__inj__on,fact_diff__card__le__card__Diff,fact_fold__sup__insert,fact_card__psubset,fact_compl__top__eq,fact_compl__bot__eq,fact_range__ex1__eq,fact_inj__image__mem__iff,fact_finite__UNIV__inj__surj,fact_finite__UNIV__surj__inj,fact_inj__image__subset__iff,fact_image__set__diff,fact_surj__Compl__image__subset,fact_folding__one__idem_Ounion__idem,fact_comm__monoid__big_OF__eq,fact_card__Diff1__le,fact_sup__le__fold__sup,fact_card__inj__on__le,fact_card__bij__eq,fact_card__Diff__subset,fact_union__fold__insert,fact_fold1__Un2,fact_inj__on__iff__card__le,fact_card__Diff__singleton__if,fact_card__Diff__singleton,fact_diff__less__mono,fact_less__diff__iff,fact_diff__less__mono2,fact_less__imp__diff__less,fact_add__diff__inverse,fact_less__diff__conv,fact_card__UNIV__unit,fact_le__refl,fact_le__add2,fact_le__add1,fact_inj__on__add__nat,fact_le__iff__add,fact_nat__le__linear,fact_nat__add__left__cancel__le,fact_eq__imp__le,fact_trans__le__add1,fact_trans__le__add2,fact_add__le__mono1,fact_le__trans,fact_le__antisym,fact_add__le__mono,fact_add__leD2,fact_add__leD1,fact_add__leE,fact_finite__nat__set__iff__bounded__le,fact_nat__add__right__cancel,fact_nat__add__left__cancel,fact_nat__add__assoc,fact_nat__add__left__commute,fact_nat__add__commute,fact_one__reorient,fact_nat__mult__eq__1__iff,fact_nat__mult__1__right,fact_nat__1__eq__mult__iff,fact_nat__mult__1,fact_add__mult__distrib2,fact_add__mult__distrib,fact_mult__le__mono,fact_mult__le__mono2,fact_mult__le__mono1,fact_le__cube,fact_le__square,fact_mult_Ocomm__neutral,fact_mult__1__right,fact_mult__1,fact_mult__1__left,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J,fact_setprod__eq__1__iff,fact_setprod__1,fact_less__add__one,fact_less__1__mult,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J,fact_comm__ring__1__class_Onormalizing__ring__rules_I1_J,fact_square__eq__1__iff,fact_setprod_Oempty,fact_setprod__empty,fact_setprod__infinite,fact_setprod_Oinfinite,fact_card__eq__setsum,fact_nat__less__le,fact_le__eq__less__or__eq,fact_less__imp__le__nat,fact_le__neq__implies__less,fact_less__or__eq__imp__le,fact_add__lessD1,fact_less__add__eq__less,fact_add__less__mono,fact_add__less__mono1,fact_trans__less__add2,fact_trans__less__add1,fact_nat__add__left__cancel__less,fact_not__add__less2,fact_not__add__less1,fact_less__not__refl,fact_nat__neq__iff,fact_linorder__neqE__nat,fact_less__irrefl__nat,fact_less__not__refl2,fact_less__not__refl3,fact_nat__less__cases,fact_finite__nat__set__iff__bounded,fact_setprod__delta,fact_setprod__delta_H,fact_nat__minus__add__max,fact_min__diff,fact_diff__mult__distrib2,fact_diff__mult__distrib,fact_diff__add__inverse2,fact_diff__add__inverse,fact_diff__diff__left,fact_diff__commute,fact_diff__cancel,fact_diff__cancel2,fact_le__diff__iff,fact_Nat_Odiff__diff__eq,fact_eq__diff__iff,fact_diff__add__assoc2,fact_add__diff__assoc2,fact_diff__add__assoc,fact_le__imp__diff__is__add,fact_le__add__diff__inverse2,fact_le__diff__conv2,fact_add__diff__assoc,fact_le__add__diff__inverse,fact_diff__diff__cancel,fact_diff__le__mono,fact_diff__le__mono2,fact_le__add__diff,fact_le__diff__conv,fact_diff__diff__right,fact_diff__le__self,fact_fold__image__distrib,fact_card_Oinsert,fact_setprod_OF__eq,fact_setprod_Oeq__fold,fact_card_Oinsert__remove,fact_card_Oremove,fact_card__Diff__insert,fact_nat__less__add__iff2,fact_nat__less__add__iff1,fact_nat__le__add__iff1,fact_nat__diff__add__eq1,fact_nat__eq__add__iff1,fact_nat__le__add__iff2,fact_nat__diff__add__eq2,fact_nat__eq__add__iff2,fact_sup__nat__def,fact_infinite__UNIV__nat,fact_nat__mult__assoc,fact_nat__mult__commute,fact_left__add__mult__distrib,fact_ord_OatMost__iff,fact_ord_OatLeast__iff,fact_ord_OlessThan__iff,fact_ord_OgreaterThan__iff,fact_ord_OatLeastAtMost__iff,fact_ord_OgreaterThanLessThan__iff,fact_ord_OatLeastLessThan__iff,fact_ord_OgreaterThanAtMost__iff,fact_setprod__gen__delta,fact_termination__basic__simps_I3_J,fact_termination__basic__simps_I4_J,fact_termination__basic__simps_I5_J,fact_termination__basic__simps_I2_J,fact_termination__basic__simps_I1_J,fact_Sup__fin_Oremove,fact_iso__tuple__UNIV__I,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_Sup__fin_Osingleton,fact_setprod__constant,fact_Sup__fin_Oin__idem,fact_Sup__fin_OF__eq,fact_Sup__fin_Oinsert__idem,fact_Sup__fin_Osubset__idem,fact_Sup__fin_Ounion__idem,fact_Sup__fin_Oeq__fold__idem_H,fact_Sup__fin_Oinsert,fact_Sup__fin_Oinsert__remove,fact_Sup__fin_Oeq__fold_H,fact_power__le__imp__le__exp,fact_power__increasing__iff,fact_power__minus,fact_power__increasing,fact_power__strict__increasing,fact_power__less__imp__less__exp,fact_power__strict__increasing__iff,fact_power__less__power__Suc,fact_power__commutes,fact_power__mult__distrib,fact_power__one,fact_power__mult,fact_power__one__right,fact_one__le__power,fact_power__inject__exp,fact_power__add,fact_power__gt1__lemma,fact_power__power__power,fact_Sup__fin_Oclosed,fact_inj__vimage__singleton,fact_Sup__fin_Ohom__commute,fact_SUPR__fold__sup,fact_setprod__mono__one__right,fact_setprod__mono__one__left,fact_fold__Un__disjoint,fact_inf1I,fact_inf1E,fact_SUP1__I,fact_SUP2__I,fact_IntI,fact_IntE,fact_finite__Int,fact_vimageI,fact_Inf__fin_Oidem,fact_Int__absorb,fact_Int__commute,fact_Int__left__absorb,fact_Int__left__commute,fact_vimage__Int,fact_Int__assoc,fact_vimage__code,fact_inf1D1,fact_inf1D2,fact_inf_Oidem,fact_inf__idem,fact_inf__fun__def,fact_inf_Ocommute,fact_inf__sup__aci_I1_J,fact_inf__commute,fact_inf_Oleft__idem,fact_inf__sup__aci_I4_J,fact_inf__left__idem,fact_inf_Oleft__commute,fact_inf__sup__aci_I3_J,fact_inf__left__commute,fact_inf_Oassoc,fact_inf__sup__aci_I2_J,fact_inf__assoc,fact_inf__apply,fact_vimage__ident,fact_image__vimage__eq,fact_finite__UN,fact_inf__sup__ord_I1_J,fact_inf__le1,fact_inf__sup__ord_I2_J,fact_inf__le2,fact_le__iff__inf,fact_le__inf__iff,fact_le__infI1,fact_le__infI2,fact_inf__absorb1,fact_inf__absorb2,fact_le__infI,fact_inf__greatest,fact_inf__mono,fact_le__infE,fact_less__infI1,fact_less__infI2,fact_inf__bot__left,fact_inf__bot__right,fact_inf__sup__absorb,fact_sup__inf__absorb,fact_inf__sup__distrib1,fact_sup__inf__distrib1,fact_inf__sup__distrib2,fact_sup__inf__distrib2,fact_inf__top__left,fact_inf__top__right,fact_inf__eq__top__iff,fact_vimage__eq,fact_vimageD,fact_vimageI2,fact_Int__iff,fact_IntD1,fact_IntD2,fact_inf__min,fact_vimage__empty,fact_Int__empty__left,fact_Int__empty__right,fact_disjoint__iff__not__equal,fact_vimage__mono,fact_vimage__UNIV,fact_insert__inter__insert,fact_vimage__Un,fact_Int__lower1,fact_Int__lower2,fact_Int__absorb2,fact_Int__absorb1,fact_Int__greatest,fact_Int__mono,fact_Int__UNIV__left,fact_Int__UNIV__right,fact_Int__Un__distrib,fact_Un__Int__distrib,fact_Int__Un__distrib2,fact_Un__Int__distrib2,fact_Un__Int__crazy,fact_vimage__Diff,fact_Diff__Int__distrib,fact_Int__Diff,fact_Diff__Int__distrib2,fact_Diff__Int2,fact_inj__on__Int,fact_vimage__Compl,fact_fun__left__comm__idem__inf,fact_inf__Int__eq,fact_distrib__inf__le,fact_distrib__sup__le,fact_inf__compl__bot,fact_compl__inf__bot,fact_diff__eq,fact_compl__inf,fact_compl__sup,fact_Int__insert__right,fact_Int__insert__left,fact_Int__insert__right__if0,fact_Int__insert__left__if0,fact_Int__insert__right__if1,fact_Int__insert__left__if1,fact_image__vimage__subset,fact_surj__image__vimage__eq,fact_image__Int__subset,fact_Diff__triv,fact_Diff__disjoint,fact_Un__Int__assoc__eq,fact_Un__Diff__Int,fact_Diff__Un,fact_Diff__Int,fact_SUP__UN__eq,fact_Compl__disjoint,fact_Compl__disjoint2,fact_Compl__Int,fact_Compl__Un,fact_Diff__Compl,fact_Diff__eq,fact_vimage__singleton__eq,fact_fold__inf__insert,fact_inf__Sup__absorb,fact_vimage__insert,fact_finite__vimageD,fact_vimage__subsetD,fact_finite__vimageI,fact_inj__vimage__image__eq,fact_inj__on__image__Int,fact_image__Int,fact_disjoint__eq__subset__Compl,fact_vimage__const,fact_folding__image__simple_Ounion__inter,fact_compl__unique,fact_fold__inf__le__inf,fact_fold1__belowI,fact_below__fold1__iff,fact_setsum__Un__Int,fact_vimage__subsetI,fact_setprod_Ounion__inter,fact_setprod__Un__Int,fact_card_Ounion__inter,fact_card__Un__Int,fact_card__Diff__subset__Int,fact_vimage__if,fact_folding__one_Ounion__inter,fact_folding__one_Ounion__disjoint,fact_folding__image__simple_Ounion__disjoint,fact_setsum__Un__disjoint,fact_setsum__Un,fact_setprod__Un__disjoint,fact_setprod_Ounion__disjoint,fact_sup__SUPR__fold__sup,fact_card__Un__disjoint,fact_inj__on__Un,fact_fold__image__Un__Int,fact_fold1__Un,fact_Sup__fin_Ounion__inter,fact_Sup__fin_Ounion__disjoint,fact_Min_Ounion__inter,fact_Min_Ounion__disjoint,fact_Max_Ounion__inter,fact_Max_Ounion__disjoint,fact_min__max_OInf__fin_Ounion__inter,fact_min__max_OInf__fin_Ounion__disjoint,fact_min__max_OSup__fin_Ounion__inter,fact_min__max_OSup__fin_Ounion__disjoint,fact_setsum__Un__nat,fact_vimage__eq__UN,fact_image__eq__UN,fact_UN__I,fact_le__SUPI,fact_SUP__subset,fact_SUP__const,fact_UN__insert,fact_UN__simps_I3_J,fact_UN__UN__flatten,fact_UN__simps_I9_J,fact_ball__UN,fact_UN__extend__simps_I9_J,fact_SUP1__iff,fact_SUP2__iff,fact_inf__nat__def,fact_UN__iff,fact_UNION__empty__conv_I2_J,fact_UN__constant,fact_UN__empty2,fact_UNION__empty__conv_I1_J,fact_UN__subset__iff,fact_UN__simps_I10_J,fact_image__UN,fact_UN__extend__simps_I10_J,fact_UN__Un__distrib,fact_UN__Un,fact_UN__simps_I5_J,fact_UN__simps_I4_J,fact_UN__extend__simps_I5_J,fact_Int__UN__distrib,fact_UN__extend__simps_I4_J,fact_Int__UN__distrib2,fact_SUP__commute,fact_SUPR__apply,fact_UN__simps_I6_J,fact_UN__extend__simps_I6_J,fact_vimage__UN,fact_UN__insert__distrib,fact_UN__upper,fact_UN__absorb,fact_UN__extend__simps_I1_J,fact_UN__singleton,fact_UN__simps_I1_J,fact_SUP__le__iff,fact_less__SUP__iff,fact_UN__extend__simps_I2_J,fact_UN__extend__simps_I3_J,fact_UN__simps_I2_J,fact_fold__image__Un__one,fact_setprod__Un__one,fact_setprod_Ounion__inter__neutral,fact_Inf__fin_Oremove,fact_INFI__fold__inf,fact_card__Suc__Diff1,fact_Inf__fold__inf,fact_InterE,fact_InterD,fact_finite__Inter,fact_INF1__D,fact_INF1__E,fact_INT__D,fact_INT__E,fact_INF2__D,fact_INF2__E,fact_finite__INT,fact_Suc__mono,fact_lessI,fact_Int__Inter__image,fact_INFI__apply,fact_Un__Inter,fact_n__not__Suc__n,fact_Suc__n__not__n,fact_nat_Oinject,fact_Suc__inject,fact_INF__commute,fact_Suc__less__SucD,fact_Suc__lessD,fact_less__SucE,fact_less__trans__Suc,fact_Suc__lessI,fact_less__SucI,fact_less__antisym,fact_not__less__less__Suc__eq,fact_Suc__less__eq,fact_less__Suc__eq,fact_not__less__eq,fact_add__Suc__right,fact_add__Suc,fact_add__Suc__shift,fact_Suc__leD,fact_le__SucE,fact_le__SucI,fact_Suc__le__mono,fact_le__Suc__eq,fact_not__less__eq__eq,fact_Suc__n__not__le__n,fact_Suc__diff__diff,fact_diff__Suc__Suc,fact_Suc__mult__cancel1,fact_Inter__UNIV,fact_Inf__fin__Inf,fact_Inter__anti__mono,fact_Inter__lower,fact_Inter__empty,fact_Int__eq__Inter,fact_Inter__insert,fact_Inter__Un__distrib,fact_INT__iff,fact_INT__simps_I5_J,fact_INT__extend__simps_I5_J,fact_INT__subset__iff,fact_INTER__UNIV__conv_I2_J,fact_INTER__UNIV__conv_I1_J,fact_INT__extend__simps_I10_J,fact_INT__simps_I10_J,fact_Un__INT__distrib2,fact_INT__extend__simps_I6_J,fact_Un__INT__distrib,fact_INT__extend__simps_I7_J,fact_INT__simps_I6_J,fact_INT__simps_I7_J,fact_INT__Int__distrib,fact_INT__extend__simps_I9_J,fact_INT__simps_I9_J,fact_min__Suc__Suc,fact_max__Suc__Suc,fact_vimage__INT,fact_le__Inf__iff,fact_Inf__less__iff,fact_power_Opower_Opower__Suc,fact_inj__Suc,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I27_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J,fact_power__Suc2,fact_power__Suc,fact_less__add__Suc1,fact_less__add__Suc2,fact_less__iff__Suc__add,fact_le__INF__iff,fact_Suc__le__lessD,fact_le__less__Suc__eq,fact_Suc__leI,fact_le__imp__less__Suc,fact_Suc__le__eq,fact_less__Suc__eq__le,fact_less__eq__Suc__le,fact_INF__less__iff,fact_INT__insert__distrib,fact_diff__less__Suc,fact_Suc__mult__less__cancel1,fact_INT__lower,fact_INF__INT__eq,fact_mult__Suc,fact_mult__Suc__right,fact_INT__absorb,fact_INF__const,fact_Suc__diff__le,fact_Suc__mult__le__cancel1,fact_INT__constant,fact_INT__empty,fact_INT__extend__simps_I1_J,fact_INT__extend__simps_I2_J,fact_INT__insert,fact_INT__Un,fact_diff__Suc__1,fact_UN__simps_I7_J,fact_UN__extend__simps_I7_J,fact_Inter__Un__subset,fact_Compl__UN,fact_Compl__INT,fact_Inf__fin_Osingleton,fact_less__eq__Suc__le__raw,fact_Inf__lower,fact_INF__subset,fact_Inf__singleton,fact_Inf__empty,fact_Inf__UNIV,fact_Inf__insert,fact_INT__simps_I1_J,fact_INT__simps_I2_J,fact_power__gt1,fact_INT__extend__simps_I3_J,fact_INT__simps_I3_J,fact_INT__extend__simps_I4_J,fact_diff__Suc__diff__eq1,fact_diff__Suc__diff__eq2,fact_INF__leI,fact_sup__Inf__absorb,fact_Inf__fin_Oin__idem,fact_Inf__fin_OF__eq,fact_INT__simps_I4_J,fact_card__insert__if,fact_card__insert__disjoint,fact_Inf__binary,fact_inf__Inf__fold__inf,fact_Inf__fin_Oinsert__idem,fact_Inf__fin_Osubset__idem,fact_Inf__fin_Ounion__idem,fact_Inf__le__Sup,fact_Inf__fin_Oeq__fold__idem_H,fact_inf__INFI__fold__inf,fact_card__insert,fact_Inf__fin_Oinsert,fact_Inf__fin_Oinsert__remove,fact_Inf__fin_Ounion__inter,fact_Inf__fin_Ounion__disjoint,fact_Inf__fin_Oeq__fold_H,fact_diff__Suc__eq__diff__pred,fact_Suc__eq__plus1__left,fact_Suc__eq__plus1,fact_Inf__fin_Oclosed,fact_finite__fun__UNIVD1,fact_Inf__fin_Ohom__commute,fact_less__zeroE,fact_le0,fact_zero__less__Suc,fact_Inter__def,fact_INTER__eq__Inter__image,fact_Inter__image__eq,fact_INF2__iff,fact_INF1__iff,fact_zero__reorient,fact_bot__nat__def,fact_power__eq__0__iff,fact_power__0__left,fact_add__0__left,fact_add__0,fact_double__zero__sym,fact_add__0__right,fact_add_Ocomm__neutral,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J,fact_add__0__iff,fact_mult__zero__left,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,fact_mult__zero__right,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,fact_mult__eq__0__iff,fact_no__zero__divisors,fact_divisors__zero,fact_diff__0__right,fact_diff__self,fact_eq__iff__diff__eq__0,fact_right__minus__eq,fact_zero__neq__one,fact_one__neq__zero,fact_neg__equal__zero,fact_neg__equal__0__iff__equal,fact_equal__neg__zero,fact_neg__0__equal__iff__equal,fact_minus__zero,fact_Suc__neq__Zero,fact_Zero__neq__Suc,fact_nat_Osimps_I3_J,fact_Suc__not__Zero,fact_nat_Osimps_I2_J,fact_Zero__not__Suc,fact_power__Suc__0,fact_nat__power__eq__Suc__0__iff,fact_field__power__not__zero,fact_nat__zero__less__power__iff,fact_nat__power__less__imp__less,fact_not__less0,fact_neq0__conv,fact_less__nat__zero__code,fact_gr__implies__not0,fact_gr0I,fact_add__eq__self__zero,fact_add__is__0,fact_Nat_Oadd__0__right,fact_plus__nat_Oadd__0,fact_less__eq__nat_Osimps_I1_J,fact_le__0__eq,fact_diff__0__eq__0,fact_minus__nat_Odiff__0,fact_diff__self__eq__0,fact_diffs0__imp__equal,fact_nat__mult__eq__cancel__disj,fact_mult__0,fact_mult__0__right,fact_mult__is__0,fact_mult__cancel1,fact_mult__cancel2,fact_sum__squares__eq__zero__iff,fact_min__0L,fact_min__0R,fact_max__0L,fact_max__0R,fact_power__eq__imp__eq__base,fact_setsum__0,fact_power_Opower_Opower__0,fact_power__strict__mono,fact_sum__squares__le__zero__iff,fact_sum__squares__ge__zero,fact_sum__squares__gt__zero__iff,fact_not__sum__squares__lt__zero,fact_add__nonpos__nonpos,fact_add__increasing2,fact_add__increasing,fact_add__nonneg__eq__0__iff,fact_add__nonneg__nonneg,fact_double__add__le__zero__iff__single__add__le__zero,fact_zero__le__double__add__iff__zero__le__single__add,fact_zero__le__square,fact_zero__le__mult__iff,fact_mult__le__0__iff,fact_mult__nonneg__nonneg,fact_mult__nonneg__nonpos,fact_mult__nonneg__nonpos2,fact_mult__nonpos__nonneg,fact_mult__nonpos__nonpos,fact_mult__right__mono,fact_mult__left__mono,fact_comm__mult__left__mono,fact_mult__right__mono__neg,fact_mult__left__mono__neg,fact_mult__mono_H,fact_mult__mono,fact_split__mult__pos__le,fact_split__mult__neg__le,fact_zero__less__double__add__iff__zero__less__single__add,fact_double__add__less__zero__iff__single__add__less__zero,fact_add__pos__pos,fact_add__neg__neg,fact_pos__add__strict,fact_not__square__less__zero,fact_mult__less__cancel__right__disj,fact_mult__less__cancel__left__disj,fact_mult__less__cancel__left__pos,fact_mult__pos__pos,fact_mult__pos__neg,fact_mult__pos__neg2,fact_zero__less__mult__pos,fact_zero__less__mult__pos2,fact_mult__less__cancel__left__neg,fact_mult__neg__pos,fact_mult__neg__neg,fact_mult__strict__right__mono,fact_mult__strict__left__mono,fact_comm__mult__strict__left__mono,fact_mult__strict__right__mono__neg,fact_mult__strict__left__mono__neg,fact_le__iff__diff__le__0,fact_less__iff__diff__less__0,fact_add__scale__eq__noteq,fact_zero__le__one,fact_not__one__le__zero,fact_zero__less__one,fact_not__one__less__zero,fact_neg__0__le__iff__le,fact_le__minus__self__iff,fact_neg__le__0__iff__le,fact_minus__le__self__iff,fact_less__minus__self__iff,fact_neg__0__less__iff__less,fact_neg__less__0__iff__less,fact_neg__less__nonneg,fact_minus__unique,fact_ab__left__minus,fact_left__minus,fact_eq__neg__iff__add__eq__0,fact_right__minus,fact_power__mono,fact_zero__le__power,fact_zero__less__power,fact_diff__0,fact_setsum__empty,fact_setsum_Oempty,fact_setsum_Oinfinite,fact_setsum__infinite,fact_power__0__Suc,fact_setprod__zero__iff,fact_setprod__zero,fact_gr0__conv__Suc,fact_less__Suc0,fact_less__Suc__eq__0__disj,fact_one__is__add,fact_add__is__1,fact_add__gr__0,fact_nat__one__le__power,fact_power__0,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J,fact_card_Oempty,fact_card__infinite,fact_mult__eq__1__iff,fact_zero__less__diff,fact_diff__less,fact_nat__0__less__mult__iff,fact_mult__less__cancel1,fact_mult__less__cancel2,fact_mult__less__mono1,fact_mult__less__mono2,fact_nat__mult__less__cancel1,fact_nat__mult__eq__cancel1,fact_diff__add__0,fact_power__eq__if,fact_diff__is__0__eq_H,fact_diff__is__0__eq,fact_One__nat__def,fact_mult__eq__self__implies__10,fact_setsum__eq__0__iff,fact_Suc__pred_H,fact_add__eq__if,fact_add__nonpos__neg,fact_add__neg__nonpos,fact_add__strict__increasing2,fact_add__strict__increasing,fact_add__nonneg__pos,fact_add__pos__nonneg,fact_mult__le__cancel__left__pos,fact_mult__le__cancel__left__neg,fact_mult__strict__mono,fact_mult__strict__mono_H,fact_mult__less__le__imp__less,fact_mult__le__less__imp__less,fact_mult__right__less__imp__less,fact_mult__less__imp__less__right,fact_mult__left__less__imp__less,fact_mult__less__imp__less__left,fact_mult__right__le__imp__le,fact_mult__left__le__imp__le,fact_mult__eq__if,fact_mult__right__le__one__le,fact_mult__left__le__one__le,fact_zero__less__two,fact_power__less__imp__less__base,fact_power__le__imp__le__base,fact_power__inject__base,fact_card__eq__0__iff,fact_card__ge__0__finite,fact_diff__Suc__less,fact_Suc__pred,fact_n__less__m__mult__n,fact_n__less__n__mult__m,fact_one__less__mult,fact_nat__diff__split__asm,fact_nat__diff__split,fact_one__le__mult__iff,fact_mult__le__cancel1,fact_mult__le__cancel2,fact_nat__mult__le__cancel1,fact_setsum__eq__Suc0__iff,fact_setsum__eq__1__iff,fact_setsum__delta,fact_setsum__delta_H,fact_setprod__pos__nat__iff,fact_convex__bound__le,fact_power__Suc__less,fact_power__Suc__less__one,fact_power__strict__decreasing,fact_power__decreasing,fact_one__less__power,fact_card__gt__0__iff,fact_finite__UNIV__card__ge__0,fact_setsum_Oeq__fold,fact_setsum_OF__eq,fact_Suc__diff__1,fact_setsum__restrict__set,fact_card__def,fact_card_Oeq__fold__g,fact_convex__bound__lt,fact_triple_Osize_I1_J,fact_even__less__0__iff,fact_triple_Osize_I2_J,fact_card_Ounion__inter__neutral,fact_setsum__mono2,fact_arith__series__nat,fact_finite__lessThan,fact_lessThan__eq__iff,fact_card__lessThan,fact_lessThan__0,fact_lessThan__Suc,fact_UN__lessThan__UNIV,fact_lessThan__Suc__eq__insert__0,fact_setsum__lessThan__Suc,fact_lessThan__iff,fact_lessThan__subset__iff,fact_lessThan__strict__subset__iff,fact_zpower__zadd__distrib,fact_zpower__zpower,fact_single__Diff__lessThan,fact_double__eq__0__iff,fact_arith__series__general,fact_setsum__Un__zero,fact_setsum_Ounion__inter__neutral,fact_card__Suc__eq,fact_setsum__mono3,fact_Ints__odd__less__0,fact_negative__zless,fact_pos__zmult__eq__1__iff,fact_zmult__zless__mono2,fact_Ints__of__nat,fact_zmult__zminus,fact_zmult__assoc,fact_zmult__commute,fact_zdiff__zmult__distrib2,fact_zdiff__zmult__distrib,fact_zadd__zmult__distrib,fact_zadd__zmult__distrib2,fact_zmult__1,fact_zmult__1__right,fact_of__nat__eq__iff,fact_int__zle__neg,fact_int__le__0__conv,fact_int__eq__0__conv,fact_int__0,fact_negative__eq__positive,fact_zless__iff__Suc__zadd,fact_int__Suc,fact_negative__zless__0,fact_not__zle__0__negative,fact_zless__int,fact_zadd__int,fact_zadd__int__left,fact_zle__int,fact_int__mult,fact_zmult__int,fact_int__1,fact_inj__int,fact_zpower__int,fact_int__power,fact_int__setsum,fact_int__setprod,fact_int__Suc0__eq__1,fact_zmult__zless__mono2__lemma,fact_zero__less__int__conv,fact_of__nat__0__le__iff,fact_zero__le__imp__of__nat,fact_zdiff__int,fact_of__nat__less__0__iff,fact_of__nat__0,fact_of__nat__less__imp__less,fact_less__imp__of__nat__less,fact_of__nat__less__iff,fact_of__nat__le__iff,fact_of__nat__add,fact_of__nat__mult,fact_of__nat__1,fact_of__nat__power,fact_of__nat__setsum,fact_inj__of__nat,fact_Ints__0,fact_Ints__add,fact_Ints__mult,fact_Ints__diff,fact_Ints__1,fact_Ints__minus,fact_Ints__power,fact_of__nat__setprod,fact_of__nat__Suc,fact_of__nat__diff,fact_setsum__constant,fact_of__nat__0__less__iff,fact_Ints__double__eq__0__iff,fact_Ints__odd__nonzero,fact_semiring__1__class_Oof__nat__code,fact_zdiff__int__split,fact_Nat__Transfer_Otransfer__int__nat__functions_I4_J,fact_setsum__bounded,fact_Nat__Transfer_Otransfer__int__nat__functions_I2_J,fact_image__minus__const__atLeastLessThan__nat,fact_finite__atLeastLessThan,fact_negative__zle,fact_int__less__0__conv,fact_zle__iff__zadd,fact_transfer__int__nat__quantifiers_I1_J,fact_transfer__int__nat__quantifiers_I2_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I9_J,fact_zero__zle__int,fact_negative__zle__0,fact_int__int__eq,fact_not__int__zless__negative,fact_transfer__int__nat__relations_I1_J,fact_transfer__nat__int__set__relations_I5_J,fact_transfer__nat__int__set__relations_I2_J,fact_transfer__nat__int__set__relations_I3_J,fact_transfer__nat__int__set__relations_I4_J,fact_zless__add1__eq,fact_zless__linear,fact_zminus__zminus,fact_zadd__commute,fact_zadd__left__commute,fact_zadd__assoc,fact_diff__int__def,fact_diff__int__def__symmetric,fact_zminus__zadd__distrib,fact_zadd__strict__right__mono,fact_zadd__zless__mono,fact_zless__le,fact_zadd__zminus__inverse2,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J,fact_zle__refl,fact_zle__linear,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J,fact_zadd__left__mono,fact_zle__trans,fact_zle__antisym,fact_zadd__0__right,fact_zadd__0,fact_zminus__0,fact_less__bin__lemma,fact_int__0__neq__1,fact_odd__nonzero,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J,fact_zle__diff1__eq,fact_int__one__le__iff__zero__less,fact_zle__add1__eq__le,fact_add1__zle__eq,fact_le__imp__0__less,fact_zless__imp__add1__zle,fact_odd__less__0,fact_int__0__less__1,fact_atLeastLessThan__inj_I2_J,fact_atLeastLessThan__inj_I1_J,fact_atLeastLessThan__eq__iff,fact_atLeastLessThan__add__Un,fact_atLeastLessThan0,fact_atLeast0LessThan,fact_subset__card__intvl__is__intvl,fact_card__atLeastLessThan,fact_image__Suc__atLeastLessThan,fact_atLeastLessThan__empty,fact_atLeastLessThan__empty__iff,fact_atLeastLessThan__empty__iff2,fact_atLeastLessThan__subset__iff,fact_setsum__shift__bounds__Suc__ivl,fact_ivl__disj__un_I17_J,fact_setsum__shift__bounds__nat__ivl,fact_ivl__diff,fact_ivl__disj__int_I11_J,fact_image__add__atLeastLessThan,fact_setsum__add__nat__ivl,fact_setsum__diff__nat__ivl,fact_of__nat__aux_Osimps_I1_J,fact_of__nat__aux_Osimps_I2_J,fact_transfer__int__nat__numerals_I1_J,fact_atLeastLessThan__singleton,fact_transfer__int__nat__relations_I2_J,fact_Nat__Transfer_Otransfer__int__nat__functions_I1_J,fact_transfer__int__nat__relations_I3_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J,fact_UN__UN__finite__eq,fact_transfer__int__nat__numerals_I2_J,fact_Int__atLeastLessThan,fact_ivl__disj__un_I8_J,fact_ivl__disj__int_I2_J,fact_setsum__shift__lb__Suc0__0__upt,fact_setsum__head__upt__Suc,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I2_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J,fact_atLeastLessThanSuc,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I1_J,fact_transfer__nat__int__set__relations_I1_J,fact_setsum__op__ivl__Suc,fact_self__quotient__aux2,fact_self__quotient__aux1,fact_q__pos__lemma,fact_q__neg__lemma,fact_unique__quotient__lemma,fact_zdiv__mono2__lemma,fact_finite__atLeastLessThan__int,fact_infinite__UNIV__int,fact_finite__atLeastZeroLessThan__int,fact_image__add__int__atLeastLessThan,fact_zdiv__mono2__neg__lemma,fact_unique__quotient__lemma__neg,fact_all__nat__less__eq,fact_ex__nat__less__eq,fact_UN__finite2__subset,fact_UN__finite2__eq,fact_UN__finite__subset,fact_tsub__def,fact_ivl__disj__un_I3_J,fact_int__power__div__base,fact_image__INT,fact_com_Osize_I4_J,fact_finite__greaterThanLessThan,fact_finite__greaterThanLessThan__int,fact_zdiv__zero,fact_zdiv__zminus__zminus,fact_zdiv__zminus2,fact_div__by__0,fact_div__0,fact_div__by__1,fact_Divides_Otransfer__nat__int__function__closures_I1_J,fact_div__neg__pos__less0,fact_neg__imp__zdiv__neg__iff,fact_pos__imp__zdiv__neg__iff,fact_zdiv__self,fact_div__mult__mult1__if,fact_div__mult__self2__is__id,fact_div__mult__self1__is__id,fact_div__mult__mult2,fact_div__mult__mult1,fact_div__self,fact_greaterThanLessThan__empty,fact_zdiv__eq__0__iff,fact_pos__imp__zdiv__nonneg__iff,fact_pos__imp__zdiv__pos__iff,fact_nonneg1__imp__zdiv__pos__iff,fact_zdiv__mono2,fact_div__nonneg__neg__le0,fact_div__pos__pos__trivial,fact_neg__imp__zdiv__nonneg__iff,fact_div__nonpos__pos__le0,fact_zdiv__mono2__neg,fact_div__neg__neg__trivial,fact_zdiv__mono1,fact_zdiv__mono1__neg,fact_atLeastSucLessThan__greaterThanLessThan,fact_image__uminus__greaterThanLessThan,fact_int__div__less__self,fact_zdiv__zmult2__eq,fact_div__mult__self2,fact_div__mult__self1,fact_div__add__self2,fact_div__add__self1,fact_com_Osize_I1_J,fact_ivl__disj__int_I9_J,fact_Int__greaterThanLessThan,fact_card__greaterThanLessThan,fact_atLeastPlusOneLessThan__greaterThanLessThan__int,fact_split__zdiv,fact_divmod__int__rel__div__eq,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I3_J,fact_tsub__eq,fact_Nat__Transfer_Otransfer__int__nat__functions_I3_J,fact_ivl__disj__un_I15_J,fact_com_Osize_I6_J,fact_z3div__def,fact_ivl__disj__un_I4_J,fact_Powp__mono,fact_card__Plus__conv__if,fact_com_Osize_I12_J,fact_finite__greaterThanAtMost,fact_finite__greaterThanAtMost__int,fact_div__mult2__eq,fact_div__le__dividend,fact_div__le__mono,fact_div__1,fact_div__less,fact_nat__mult__div__cancel__disj,fact_zdiv__int,fact_Divides_Otransfer__int__nat__functions_I1_J,fact_greaterThanAtMost__empty,fact_greaterThanAtMost__empty__iff,fact_greaterThanAtMost__empty__iff2,fact_ivl__disj__un_I20_J,fact_ivl__disj__int_I14_J,fact_div__le__mono2,fact_nat__mult__div__cancel1,fact_div__mult__self1__is__m,fact_div__mult__self__is__m,fact_div__less__dividend,fact_card__greaterThanAtMost,fact_com_Osize_I9_J,fact_div__geq,fact_div__if,fact_split__div,fact_Int__greaterThanAtMost,fact_image__uminus__atLeastLessThan,fact_image__uminus__greaterThanAtMost,fact_ivl__disj__int_I10_J,fact_finite__Plus__iff,fact_finite__Plus,fact_finite__PlusD_I1_J,fact_finite__PlusD_I2_J,fact_le__div__geq,fact_split__div_H,fact_split__div__lemma,fact_card__Plus,fact_ivl__disj__un_I16_J,fact_com_Osize_I14_J,fact_UNIV__Plus__UNIV,fact_Plus__eq__empty__conv,fact_setprod__diff1,fact_image__atLeastZeroLessThan__int,fact_setsum__nonneg__0,fact_power__divide,fact_nat__int,fact_divide__zero__left,fact_divide__zero,fact_minus__divide__left,fact_divide__1,fact_diff__divide__distrib,fact_times__divide__eq__right,fact_add__divide__distrib,fact_setsum__divide__distrib,fact_eq__divide__imp,fact_divide__eq__imp,fact_nonzero__divide__eq__eq,fact_nonzero__eq__divide__eq,fact_right__inverse__eq,fact_divide__self,fact_divide__self__if,fact_nonzero__minus__divide__divide,fact_nonzero__minus__divide__right,fact_nonzero__power__divide,fact_nat__0,fact_transfer__nat__int__numerals_I1_J,fact_eq__nat__nat__iff,fact_transfer__nat__int__relations_I1_J,fact_all__nat,fact_ex__nat,fact_power__one__over,fact_transfer__nat__int__numerals_I2_J,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I4_J,fact_transfer__int__nat__set__return__embed,fact_setprod__dividef,fact_card__greaterThanAtMost__int,fact_transfer__nat__int__sum__prod_I2_J,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I2_J,fact_nat__0__iff,fact_nat__le__0,fact_zless__nat__conj,fact_nat__mono__iff,fact_transfer__nat__int__relations_I3_J,fact_nat__1,fact_int__nat__eq,fact_int__eq__iff,fact_nat__0__le,fact_zless__nat__eq__int__zless,fact_Divides_Otransfer__nat__int__functions_I1_J,fact_nat__div__distrib,fact_nat__zminus__int,fact_transfer__nat__int__sum__prod_I1_J,fact_card__atLeastZeroLessThan__int,fact_card__atLeastLessThan__int,fact_zero__less__nat__eq,fact_power__diff,fact_nat__less__eq__zless,fact_transfer__nat__int__relations_I2_J,fact_nat__eq__iff,fact_nat__eq__iff2,fact_nat__le__eq__zle,fact_split__nat,fact_nat__add__distrib,fact_Nat__Transfer_Otransfer__nat__int__functions_I1_J,fact_nat__mult__distrib,fact_Nat__Transfer_Otransfer__nat__int__functions_I2_J,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I3_J,fact_nat__diff__distrib,fact_transfer__nat__int__sum__prod2_I1_J,fact_Nat__Transfer_Otransfer__nat__int__functions_I4_J,fact_nat__power__eq,fact_transfer__nat__int__sum__prod2_I2_J,fact_Nat__Transfer_Otransfer__nat__int__functions_I3_J,fact_one__less__nat__eq,fact_nat__less__iff,fact_Suc__nat__eq__nat__zadd1,fact_nat__mult__distrib__neg,fact_card__greaterThanLessThan__int,fact_geometric__sum,fact_le__divide__eq,fact_divide__le__eq,fact_pos__le__divide__eq,fact_pos__divide__le__eq,fact_mult__imp__div__pos__le,fact_times__divide__times__eq,fact_minus__divide__divide,fact_minus__divide__right,fact_zero__le__divide__iff,fact_divide__le__0__iff,fact_divide__right__mono,fact_divide__right__mono__neg,fact_zero__less__divide__iff,fact_divide__less__0__iff,fact_divide__pos__pos,fact_divide__pos__neg,fact_divide__neg__pos,fact_divide__neg__neg,fact_divide__strict__right__mono,fact_divide__strict__right__mono__neg,fact_frac__eq__eq,fact_mult__divide__mult__cancel__left,fact_mult__divide__mult__cancel__right,fact_divide__eq__eq,fact_eq__divide__eq,fact_divide__nonneg__pos,fact_divide__nonneg__neg,fact_frac__less2,fact_frac__less,fact_frac__le,fact_divide__nonpos__pos,fact_divide__nonpos__neg,fact_less__divide__eq,fact_divide__less__eq,fact_pos__less__divide__eq,fact_pos__divide__less__eq,fact_mult__imp__div__pos__less,fact_mult__imp__less__div__pos,fact_neg__less__divide__eq,fact_neg__divide__less__eq,fact_divide__strict__left__mono,fact_divide__strict__left__mono__neg,fact_add__frac__eq,fact_divide__add__eq__iff,fact_add__frac__num,fact_add__divide__eq__iff,fact_add__num__frac,fact_diff__frac__eq,fact_divide__diff__eq__iff,fact_diff__divide__eq__iff,fact_less__half__sum,fact_gt__half__sum,fact_divide__left__mono__neg,fact_divide__left__mono,fact_neg__divide__le__eq,fact_neg__le__divide__eq,fact_mult__imp__le__div__pos,fact_nat__aux__def,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I4_J,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I3_J,fact_transfer__morphism__nat__int,fact_transfer__int__nat__sum__prod_I2_J,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I1_J,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I3_J,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I2_J,fact_nat__set__def,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I5_J,fact_transfer__int__nat__set__relations_I3_J,fact_Nat__Transfer_Otransfer__nat__int__set__function__closures_I6_J,fact_transfer__nat__int__set__return__embed,fact_transfer__int__nat__set__relations_I1_J,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I1_J,fact_transfer__int__nat__set__relations_I5_J,fact_transfer__int__nat__set__relations_I4_J,fact_transfer__int__nat__sum__prod_I1_J,fact_setprod__Un,fact_transfer__int__nat__set__relations_I2_J,fact_of__int__of__nat,fact_setsum__nonneg__leq__bound,fact_greaterThan__0,fact_greaterThan__eq__iff,fact_of__int__eq__iff,fact_of__int__int__eq,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I5_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I1_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I9_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I6_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I2_J,fact_Divides_Otransfer__int__nat__function__closures_I1_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I4_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I3_J,fact_of__int__0,fact_of__int__0__eq__iff,fact_of__int__eq__0__iff,fact_of__int__le__iff,fact_of__int__less__iff,fact_of__int__add,fact_of__int__mult,fact_of__int__1,fact_of__int__diff,fact_of__int__of__nat__eq,fact_of__int__minus,fact_Ints__of__int,fact_of__int__power,fact_is__nat__def,fact_greaterThan__iff,fact_greaterThan__subset__iff,fact_of__int__setsum,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I6_J,fact_of__int__setprod,fact_INT__greaterThan__UNIV,fact_of__int__0__le__iff,fact_of__int__le__0__iff,fact_of__int__0__less__iff,fact_of__int__less__0__iff,fact_of__nat__nat,fact_ivl__disj__un_I11_J,fact_image__uminus__lessThan,fact_image__uminus__greaterThan,fact_ivl__disj__int_I5_J,fact_greaterThan__Suc,fact_transfer__int__nat__sum__prod2_I2_J,fact_transfer__int__nat__sum__prod2_I1_J,fact_sum__diff__distrib,fact_setsum__natinterval__difff,fact_gauss__sum,fact_finite__atLeastAtMost,fact_all__nat__less,fact_ex__nat__less,fact_atLeastLessThanSuc__atLeastAtMost,fact_atLeastatMost__empty__iff2,fact_atLeastatMost__empty__iff,fact_atLeastatMost__empty,fact_atLeastatMost__subset__iff,fact_atLeastAtMost__singleton_H,fact_atLeastAtMost__singleton__iff,fact_atLeastAtMost__singleton,fact_image__uminus__atLeastAtMost,fact_image__Suc__atLeastAtMost,fact_setsum__shift__bounds__cl__Suc__ivl,fact_setsum__shift__bounds__cl__nat__ivl,fact_atLeastSucAtMost__greaterThanAtMost,fact_image__add__atLeastAtMost,fact_card__atLeastAtMost,fact_atLeastAtMostSuc__conv,fact_setsum__shift__lb__Suc0__0,fact_ivl__disj__un_I21_J,fact_ivl__disj__int_I15_J,fact_Int__atLeastAtMost,fact_atLeastatMost__psubset__iff,fact_ivl__disj__un_I22_J,fact_ivl__disj__int_I4_J,fact_ivl__disj__int_I16_J,fact_ivl__disj__int_I13_J,fact_ivl__disj__int_I12_J,fact_ivl__disj__int_I7_J,fact_setsum__head__Suc,fact_setsum__cl__ivl__Suc,fact_setsum__head,fact_setsum__ub__add__nat,fact_ivl__disj__un_I6_J,fact_ivl__disj__un_I5_J,fact_ivl__disj__un_I18_J,fact_ivl__disj__un_I19_J,fact_atLeast__Suc,fact_UN__le__eq__Un0,fact_ivl__disj__un_I12_J,fact_decr__mult__lemma,fact_negD,fact_finite__atLeastAtMost__int,fact_finite__atMost,fact_atMost__eq__iff,fact_atLeast__eq__iff,fact_image__uminus__atMost,fact_image__uminus__atLeast,fact_atMost__Int__atLeast,fact_SetInterval_Otransfer__nat__int__set__functions_I1_J,fact_SetInterval_Otransfer__int__nat__set__function__closures,fact_atLeast0AtMost,fact_lessThan__Suc__atMost,fact_card__atMost,fact_atMost__Suc,fact_atMost__iff,fact_atLeast__iff,fact_atLeast__subset__iff,fact_atMost__subset__iff,fact_atLeast__0,fact_SetInterval_Otransfer__nat__int__set__function__closures,fact_atLeastLessThanPlusOne__atLeastAtMost__int,fact_Compl__atLeast,fact_Compl__lessThan,fact_Compl__greaterThan,fact_Compl__atMost,fact_atLeastPlusOneAtMost__greaterThanAtMost__int,fact_atLeast__Suc__greaterThan,fact_UN__atMost__UNIV,fact_SetInterval_Otransfer__nat__int__set__functions_I2_J,fact_setsum__atMost__Suc,fact_atMost__0,fact_ivl__disj__un_I14_J,fact_simp__from__to,fact_ivl__disj__int_I8_J,fact_Int__atLeastAtMostR1,fact_Int__atLeastAtMostL1,fact_Int__atLeastAtMostR2,fact_Int__atLeastAtMostL2,fact_UN__atLeast__UNIV,fact_ivl__disj__un_I9_J,fact_UN__le__add__shift,fact_ivl__disj__int_I3_J,fact_ivl__disj__int_I1_J,fact_ivl__disj__int_I6_J,fact_card__atLeastAtMost__int,fact_SetInterval_Otransfer__int__nat__set__functions,fact_ivl__disj__un_I2_J,fact_ivl__disj__un_I10_J,fact_ivl__disj__un_I1_J,fact_ivl__disj__un_I13_J,fact_ivl__disj__un_I7_J,fact_aset_I6_J,fact_bset_I8_J,fact_aset_I4_J,fact_bset_I4_J,fact_bset_I7_J,fact_bset_I3_J,fact_aset_I3_J,fact_aset_I5_J,fact_bset_I6_J,fact_aset_I8_J,fact_periodic__finite__ex,fact_bset_I5_J,fact_aset_I7_J,fact_incr__mult__lemma,fact_ex__least__nat__less,fact_zero__less__imp__eq__int,fact_setsum__mono__zero__right,fact_setsum__mono__zero__left,fact_card__Pow,fact_min__Suc2,fact_min__Suc1,fact_PowI,fact_finite__Pow__iff,fact_image__Pow__surj,fact_Pow__top,fact_Cantors__paradox,fact_Pow__not__empty,fact_Pow__INT__eq,fact_Pow__bottom,fact_PowD,fact_Pow__iff,fact_nat__case__0,fact_nat__case__Suc,fact_Pow__mono,fact_Pow__insert,fact_Pow__UNIV,fact_UN__Pow__subset,fact_Pow__Int__eq,fact_image__Pow__mono,fact_Pow__empty,fact_max__Suc2,fact_max__Suc1,fact_Un__Pow__subset,fact_Powp__Pow__eq,fact_diff__Suc,fact_field__le__mult__one__interval,fact_transfer__nat__int__sum__prod__cong_I2_J,fact_split__pos__lemma,fact_split__neg__lemma,fact_zpower__zmod,fact_zdiff__zmod__left,fact_zdiff__zmod__right,fact_mod__diff__cong,fact_mod__diff__eq,fact_mod__diff__left__eq,fact_mod__diff__right__eq,fact_zmod__simps_I3_J,fact_zmod__zmult1__eq,fact_zmod__self,fact_zmod__zero,fact_mod__add__cong,fact_zmod__simps_I1_J,fact_zmod__simps_I2_J,fact_mod__add__eq,fact_mod__add__left__eq,fact_mod__add__right__eq,fact_mod__add__self1,fact_mod__add__self2,fact_mod__minus__eq,fact_mod__minus__cong,fact_mod__self,fact_mod__by__0,fact_mod__0,fact_mod__mod__trivial,fact_mod__mult__cong,fact_zmod__simps_I4_J,fact_mod__mult__mult2,fact_mod__mult__mult1,fact_mod__mult__eq,fact_mod__mult__left__eq,fact_mod__mult__right__eq,fact_zminus__zmod,fact_zmod__zminus__zminus,fact_zmod__zminus2,fact_Divides_Otransfer__int__nat__function__closures_I2_J,fact_mod__mult__self1__is__0,fact_mod__mult__self2__is__0,fact_mod__mult__self2,fact_mod__mult__self1,fact_mod__by__1,fact_mod__div__trivial,fact_zmod__le__nonneg__dividend,fact_Divides_Otransfer__nat__int__function__closures_I2_J,fact_pos__mod__bound,fact_neg__mod__bound,fact_zmod__eq__0__iff,fact_zmod__zminus1__not__zero,fact_zmod__zminus2__not__zero,fact_zmod__zdiv__trivial,fact_DIVISION__BY__ZERO,fact_zdiv__zadd1__eq,fact_semiring__div__class_Omod__div__equality_H,fact_mod__div__equality2,fact_mod__div__equality,fact_div__mod__equality2,fact_div__mod__equality,fact_mod__neg__neg__trivial,fact_neg__mod__conj,fact_neg__mod__sign,fact_mod__pos__pos__trivial,fact_pos__mod__conj,fact_pos__mod__sign,fact_zmod__zminus2__eq__if,fact_zmod__zminus1__eq__if,fact_zmod__zdiv__equality,fact_zdiv__zmult1__eq,fact_zdiv__zmod__equality,fact_zdiv__zmod__equality2,fact_zmult__div__cancel,fact_zmod__zdiv__equality_H,fact_mod__pos__neg__trivial,fact_divmod__int__rel__mod__eq,fact_zmult2__lemma__aux2,fact_zmult2__lemma__aux1,fact_zmult2__lemma__aux4,fact_zmult2__lemma__aux3,fact_split__zmod,fact_zmod__zmult2__eq,fact_zdiv__zminus2__eq__if,fact_zdiv__zminus1__eq__if,fact_less__eq__nat_Osimps_I2_J,fact_z3mod__def,fact_sgn__neg,fact_sgn__1__neg,fact_sgn__if,fact_mod__less,fact_mod__Suc__eq__Suc__mod,fact_mod__mult__distrib,fact_mod__mult__distrib2,fact_mod__less__eq__dividend,fact_sgn__sgn,fact_sgn__0__0,fact_sgn0,fact_sgn__times,fact_mod__Suc,fact_mod__1,fact_mod__less__divisor,fact_mod__eq__0__iff,fact_mod__if,fact_mod__geq,fact_mod__mult__self3,fact_le__mod__geq,fact_Divides_Otransfer__int__nat__functions_I2_J,fact_zmod__int,fact_div__add1__eq,fact_mod__le__divisor,fact_mod__mult__self4,fact_sgn__greater,fact_sgn__less,fact_mod__mult2__eq,fact_div__mult1__eq,fact_div__mod__equality_H,fact_mult__div__cancel,fact_Divides_Omod__div__equality_H,fact_split__mod,fact_mod__lemma,fact_Suc__times__mod__eq,fact_Divides_Otransfer__nat__int__functions_I2_J,fact_nat__mod__distrib,fact_sgn__pos,fact_sgn__1__pos,fact_zsgn__def,fact_decr__lemma,fact_incr__lemma,fact_transfer__nat__int__sum__prod__cong_I1_J,fact_Sup__fold__sup,fact_UnionI,fact_setsum__abs,fact_setsum__abs__ge__zero,fact_Union__Pow__eq,fact_abs__minus__commute,fact_abs__le__D1,fact_abs__ge__self,fact_abs__one,fact_abs__minus__cancel,fact_abs__of__nat,fact_power__abs,fact_abs__idempotent,fact_abs__mult,fact_abs__mult__self,fact_abs__add__abs,fact_abs__eq__0,fact_abs__zero,fact_abs__int__eq,fact_abs__divide,fact_abs__setsum__abs,fact_abs__setprod,fact_image__Union,fact_Int__Union2,fact_Int__Union,fact_UN__extend__simps_I8_J,fact_UN__simps_I8_J,fact_Sup__le__iff,fact_less__Sup__iff,fact_vimage__Union,fact_abs__ge__zero,fact_abs__le__zero__iff,fact_abs__of__nonneg,fact_abs__of__pos,fact_zero__less__abs__iff,fact_abs__not__less__zero,fact_abs__triangle__ineq,fact_abs__mult__less,fact_abs__triangle__ineq2__sym,fact_abs__triangle__ineq2,fact_abs__triangle__ineq3,fact_abs__le__D2,fact_abs__leI,fact_abs__le__iff,fact_abs__ge__minus__self,fact_abs__less__iff,fact_nonzero__abs__divide,fact_abs__power__minus,fact_abs__zmult__eq__1,fact_Union__disjoint,fact_Union__upper,fact_mult__sgn__abs,fact_abs__sgn,fact_Union__empty,fact_Union__mono,fact_Union__insert,fact_finite__UnionD,fact_subset__Pow__Union,fact_Union__UNIV,fact_Union__Un__distrib,fact_abs__eq__mult,fact_abs__mult__pos,fact_UNION__eq__Union__image,fact_Union__image__eq,fact_abs__diff__triangle__ineq,fact_abs__triangle__ineq4,fact_abs__of__nonpos,fact_abs__minus__le__zero,fact_abs__if,fact_abs__of__neg,fact_zero__le__power__abs,fact_abs__div__pos,fact_Sup__upper,fact_Sup__empty,fact_Sup__singleton,fact_zabs__less__one__iff,fact_Sup__insert,fact_zabs__def,fact_Sup__UNIV,fact_nat__abs__mult__distrib,fact_zero__le__zpower__abs,fact_INT__simps_I8_J,fact_INT__extend__simps_I8_J,fact_Un__eq__Union,fact_Un__Union__image,fact_Union__Int__subset,fact_zero__less__zpower__abs__iff,fact_Sup__binary,fact_sup__Sup__fold__sup,fact_Sup__fin__Sup,fact_Nitpick_Oint__lcm__def,fact_inj__on__Inter,fact_Inter__subset,fact_int__val__lemma,fact_Union__def,fact_Nitpick_Onat__lcm__def,fact_finite__Union,fact_insert__partition,fact_card__partition,fact_nat__gcd_Osimps,fact_Nitpick_Oint__gcd__def,fact_nat0__intermed__int__val,fact_setprod__pos__nat,fact_inj__on__INTER,fact_folding__image__simple_Ounion__inter__neutral,fact_card__less__Suc2,fact_card__less,fact_card__less__Suc,fact_CollectI,fact_finite__Collect__conjI,fact_finite__Collect__less__nat,fact_finite__Collect__le__nat,fact_Collect__disj__eq,fact_Collect__conj__eq,fact_CollectE,fact_CollectD,fact_mem__Collect__eq,fact_Collect__mem__eq,fact_empty__def,fact_empty__Collect__eq,fact_Collect__empty__eq,fact_Collect__def,fact_UNIV__def,fact_insert__Collect,fact_finite__Collect__disjI,fact_Collect__neg__eq,fact_vimage__Collect__eq,fact_insert__compr,fact_insert__compr__raw,fact_Un__def,fact_Int__def,fact_Int__Collect,fact_singleton__conv2,fact_singleton__conv,fact_Collect__conv__if2,fact_Collect__conv__if,fact_set__diff__eq,fact_finite__Collect__not,fact_insert__def,fact_Compl__eq,fact_vimage__def,fact_Collect__imp__eq,fact_finite__M__bounded__by__nat,fact_setsum__setsum__restrict,fact_if__image__distrib,fact_nat__seg__image__imp__finite,fact_setsum__restrict__set_H,fact_setsum__image__gen,fact_setsum__cases,fact_setsum__multicount,fact_min__max_Osup__Inf1__distrib,fact_min__max_Oinf__Sup1__distrib,fact_min__max_Osup__Inf2__distrib,fact_finite__Collect__subsets,fact_Pow__Compl,fact_Pow__def,fact_finite__image__set,fact_finite__Collect__bounded__ex,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I4_J,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I5_J,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I5_J,fact_add__Min__commute,fact_add__Max__commute,fact_sup__Inf2__distrib,fact_sup__Inf1__distrib,fact_inf__Sup2__distrib,fact_inf__Sup1__distrib,fact_min__max_Oinf__Sup2__distrib,fact_setsum__multicount__gen,fact_finite__conv__nat__seg__image,fact_pigeonhole__infinite,fact_card__quotient__disjoint,fact_quotient__is__empty,fact_quotient__is__empty2,fact_quotient__empty,fact_quotient__diff1,fact_quotient__def,fact_singleton__quotient,fact_finite__UN__I,fact_inj__on__diff__nat,fact_quotientI,fact_Image__eq__UN,fact_Image__INT__subset,fact_Image__Int__subset,fact_Image__UN,fact_Image__empty,fact_Image__mono,fact_Image__Un,fact_Un__Image,fact_quotientE,fact_diff__nat__eq__if,fact_setsum__SucD,fact_nat__mod__eq__lemma,fact_not__neg__int,fact_not__neg__1,fact_less__by__empty,fact_not__neg__0,fact_not__neg__eq__ge__0,fact_neg__def,fact_neg__nat,fact_not__neg__nat,fact_neg__zminus__int,fact_com_Osize_I5_J,fact_com_Osize_I13_J,fact_fold__image__1,fact_card_Oneutral,fact_com_Osimps_I4_J,fact_com_Osimps_I52_J,fact_com_Osimps_I53_J,fact_com_Osimps_I45_J,fact_com_Osimps_I44_J,fact_com_Osimps_I15_J,fact_com_Osimps_I14_J,fact_mod__induct__0,fact_InterI,fact_fold__image__cong,fact_inf__le__fold__inf,fact_fold__sup__le__sup,fact_expand__Suc,fact_quotient__disj,fact_com_Osize_I3_J,fact_of__nat__number__of__eq,fact_of__nat__number__of__lemma,fact_number__of__eq,fact_of__int__number__of__eq,fact_com_Osimps_I2_J,fact_number__of__reorient,fact_eq__number__of,fact_com_Osimps_I39_J,fact_com_Osimps_I38_J,fact_com_Osimps_I37_J,fact_com_Osimps_I36_J,fact_com_Osimps_I34_J,fact_com_Osimps_I35_J,fact_com_Osimps_I11_J,fact_com_Osimps_I10_J,fact_le__number__of__eq__not__less,fact_right__distrib__number__of,fact_left__distrib__number__of,fact_right__diff__distrib__number__of,fact_left__diff__distrib__number__of,fact_le__number__of,fact_less__number__of,fact_min__number__of,fact_max__number__of,fact_add__number__of__left,fact_add__number__of__eq,fact_number__of__add,fact_mult__number__of__left,fact_arith__simps_I32_J,fact_number__of__mult,fact_number__of__diff,fact_arith__simps_I30_J,fact_number__of__minus,fact_Ints__number__of,fact_Union__quotient,fact_divide__eq__eq__number__of1,fact_divide__eq__eq__number__of,fact_eq__divide__eq__number__of,fact_eq__divide__eq__number__of1,fact_add__number__of__diff1,fact_minus__number__of__mult,fact_diff__number__of__eq,fact_divide__less__eq__number__of1,fact_divide__less__eq__number__of,fact_less__divide__eq__number__of,fact_less__divide__eq__number__of1,fact_abs__number__of,fact_add__number__of__diff2,fact_le__divide__eq__number__of1,fact_le__divide__eq__number__of,fact_divide__le__eq__number__of,fact_divide__le__eq__number__of1,fact_equiv__class__self,fact_com_Osize_I11_J,fact_UN__equiv__class,fact_UN__equiv__class2,fact_one__mod__nat__number__of,fact_one__div__nat__number__of,fact_less__eq__number__of__int__code,fact_minus__numeral__code_I5_J,fact_number__of__is__id,fact_times__numeral__code_I5_J,fact_plus__numeral__code_I9_J,fact_less__number__of__int__code,fact_int__number__of__def,fact_nat__number__of__def,fact_nat__number__of,fact_congruent2__implies__congruent,fact_minus__numeral__code_I6_J,fact_neg__imp__number__of__eq__0,fact_int__eq__iff__number__of,fact_eq__nat__number__of,fact_nat__number__of__add__left,fact_int__nat__number__of,fact_mod__nat__number__of,fact_congruent2__implies__congruent__UN,fact_div__nat__number__of,fact_power__nat__number__of,fact_power__nat__number__of__number__of,fact_Suc__nat__number__of__add,fact_diff__nat__number__of,fact_min__Suc__number__of,fact_min__number__of__Suc,fact_rel__simps_I19_J,fact_diff__bin__simps_I1_J,fact_minus__Pls,fact_add__Pls__right,fact_add__Pls,fact_mult__Pls,fact_succ__pred,fact_rel__simps_I2_J,fact_Pls__def,fact_semiring__norm_I112_J,fact_number__of__Pls,fact_add__numeral__0,fact_add__numeral__0__right,fact_bin__less__0__simps_I1_J,fact_semiring__norm_I113_J,fact_nat__number__of__Pls,fact_zero__is__num__zero,fact_Suc__diff__number__of,fact_not__neg__number__of__Pls,fact_nat__number__of__add__1,fact_nat__1__add__number__of,fact_le__iff__pred__less,fact_pred__def,fact_nat__number__of__diff__1,fact_divide__Numeral0,fact_eq__number__of__0,fact_eq__0__number__of,fact_number__of2,fact_less__nat__number__of,fact_le__nat__number__of,fact_succ__def,fact_le__special_I1_J,fact_le__special_I3_J,fact_less__special_I3_J,fact_less__special_I1_J,fact_less__0__number__of,fact_add__nat__number__of,fact_number__of__succ,fact_number__of__pred,fact_mult__nat__number__of,fact_nat__number__of__mult__left,fact_neg__number__of__pred__iff__0,fact_eq__number__of__Suc,fact_Suc__eq__number__of,fact_nat__case__number__of,fact_less__Suc__number__of,fact_less__number__of__Suc,fact_le__Suc__number__of,fact_le__number__of__Suc,fact_Suc__nat__number__of,fact_max__number__of__Suc,fact_max__Suc__number__of,fact_nat__case__add__eq__if,fact_nat__rec__add__eq__if,fact_nat__rec__number__of,fact_UN__equiv__class__type2,fact_UN__equiv__class__type,fact_nat__rec__0,fact_nat__rec__Suc,fact_eq__special_I3_J,fact_eq__special_I1_J,fact_power__number__of__odd__number__of,fact_zpower__number__of__odd,fact_iszero__number__of__Bit1,fact_rel__simps_I34_J,fact_less__eq__int__code_I16_J,fact_rel__simps_I51_J,fact_rel__simps_I17_J,fact_less__int__code_I16_J,fact_rel__simps_I46_J,fact_rel__simps_I39_J,fact_not__iszero__Numeral1,fact_iszero__0,fact_iszero__def,fact_not__iszero__1,fact_bin__less__0__simps_I4_J,fact_rel__simps_I22_J,fact_rel__simps_I12_J,fact_Bit1__def,fact_neg__number__of__Bit1,fact_minus__Bit1,fact_succ__Pls,fact_number__of__Bit1,fact_mult__numeral__1,fact_mult__numeral__1__right,fact_numeral__1__eq__1,fact_semiring__norm_I110_J,fact_rel__simps_I5_J,fact_rel__simps_I29_J,fact_divide__Numeral1,fact_divide__numeral__1,fact_eq__special_I2_J,fact_eq__special_I4_J,fact_one__is__num__one,fact_nat__numeral__1__eq__1,fact_Numeral1__eq1__nat,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I8_J,fact_iszero__Numeral0,fact_numeral__3__eq__3,fact_numeral__1__eq__Suc__0,fact_power3__eq__cube,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I8_J,fact_Suc3__eq__add__3,fact_transfer__int__nat__numerals_I4_J,fact_transfer__nat__int__numerals_I4_J,fact_le__special_I2_J,fact_le__special_I4_J,fact_less__special_I4_J,fact_less__special_I2_J,fact_add__special_I2_J,fact_add__special_I3_J,fact_Suc__diff__eq__diff__pred,fact_Suc__mod__eq__add3__mod__number__of,fact_Suc__mod__eq__add3__mod,fact_mod__Suc__eq__mod__add3,fact_Suc__div__eq__add3__div__number__of,fact_Suc__div__eq__add3__div,fact_div__Suc__eq__div__add3,fact_eq__number__of__eq,fact_diff__special_I1_J,fact_diff__special_I2_J,fact_nat__number__of__Bit1,fact_power__number__of__odd,fact_zmod__number__of__Bit1,fact_neg__zmod__mult__2,fact_arith__series__int,fact_pos__zdiv__mult__2,fact_rel__simps_I49_J,fact_rel__simps_I50_J,fact_Bit0__Pls,fact_rel__simps_I38_J,fact_rel__simps_I44_J,fact_minus__Bit0,fact_less__int__code_I13_J,fact_rel__simps_I14_J,fact_Bit0__def,fact_add__Bit0__Bit0,fact_rel__simps_I48_J,fact_mult__Bit0,fact_diff__bin__simps_I7_J,fact_less__eq__int__code_I13_J,fact_rel__simps_I31_J,fact_bin__less__0__simps_I3_J,fact_rel__simps_I21_J,fact_rel__simps_I27_J,fact_rel__simps_I32_J,fact_less__eq__int__code_I14_J,fact_rel__simps_I4_J,fact_rel__simps_I10_J,fact_rel__simps_I16_J,fact_less__int__code_I15_J,fact_add__Bit0__Bit1,fact_add__Bit1__Bit0,fact_diff__bin__simps_I3_J,fact_diff__bin__simps_I10_J,fact_diff__bin__simps_I9_J,fact_zdiv__number__of__Bit0,fact_neg__number__of__Bit0,fact_pred__Bit1,fact_pred__Bit0,fact_iszero__number__of__Bit0,fact_succ__Bit0,fact_succ__Bit1,fact_nat__number__of__Bit0,fact_number__of__Bit0,fact_less__eq__int__code_I15_J,fact_rel__simps_I33_J,fact_less__int__code_I14_J,fact_rel__simps_I15_J,fact_card__UNIV__bool,fact_mult__Bit1,fact_diff__bin__simps_I8_J,fact_add__Bit1__Bit1,fact_power__number__of__even,fact_zpower__number__of__even,fact_double__number__of__Bit0,fact_number__of1,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I7_J,fact_power__number__of__even__number__of,fact_mult__2,fact_mult__2__right,fact_one__add__one__is__two,fact_zero__eq__power2,fact_zero__power2,fact_semiring__norm_I115_J,fact_numeral__2__eq__2,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,fact_power2__eq__square,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I7_J,fact_add__2__eq__Suc,fact_add__2__eq__Suc_H,fact_one__power2,fact_power2__minus,fact_nat__mult__2,fact_nat__mult__2__right,fact_power__even__eq,fact_transfer__int__nat__numerals_I3_J,fact_transfer__nat__int__numerals_I3_J,fact_abs__power2,fact_power2__abs,fact_nat__1__add__1,fact_mod2__Suc__Suc,fact_div2__Suc__Suc,fact_zmod__number__of__Bit0,fact_add__self__div__2,fact_half__gt__zero__iff,fact_half__gt__zero,fact_zero__le__power2,fact_power2__le__imp__le,fact_power2__eq__imp__eq,fact_zero__less__power2,fact_power2__less__0,fact_sum__power2__eq__zero__iff,fact_power2__eq__square__number__of,fact_less__2__cases,fact_nat__2,fact_power2__eq__1__iff,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,fact_power__minus__even,fact_power2__less__imp__less,fact_sum__power2__ge__zero,fact_sum__power2__le__zero__iff,fact_sum__power2__gt__zero__iff,fact_not__sum__power2__lt__zero,fact_power2__sum,fact_zero__le__even__power_H,fact_power__odd__eq,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I37_J,fact_power__minus1__even,fact_zdiv__number__of__Bit1,fact_mod2__gr__0,fact_div__2__gt__zero,fact_power2__diff,fact_odd__0__le__power__imp__0__le,fact_odd__power__less__zero,fact_power__minus1__odd,fact_Suc__n__div__2__gt__zero,fact_of__nat__double,fact_pos__zmod__mult__2,fact_neg__zdiv__mult__2,fact_int__of__code,fact_of__int__num,fact_power__m1__odd,fact_rel__simps_I45_J,fact_rel__simps_I42_J,fact_rel__simps_I24_J,fact_code__numeral__zero__minus__one,fact_rel__simps_I7_J,fact_rel__simps_I37_J,fact_rel__simps_I40_J,fact_rel__simps_I47_J,fact_rel__simps_I43_J,fact_Bit1__Min,fact_bin__less__0__simps_I2_J,fact_rel__simps_I20_J,fact_rel__simps_I23_J,fact_rel__simps_I30_J,fact_rel__simps_I26_J,fact_rel__simps_I3_J,fact_rel__simps_I6_J,fact_rel__simps_I13_J,fact_rel__simps_I9_J,fact_rel__simps_I28_J,fact_rel__simps_I8_J,fact_eq__number__of__Pls__Min,fact_Int_OMin__def,fact_mult__Min,fact_neg__number__of__Min,fact_pred__Pls,fact_add__Min__right,fact_add__Min,fact_pred__Min,fact_nonzero__number__of__Min,fact_succ__Min,fact_diff__bin__simps_I2_J,fact_mult__minus1__right,fact_mult__minus1,fact_arith__simps_I31_J,fact_number__of__Min,fact_abs__minus__one,fact_divide__minus1,fact_rel__simps_I25_J,fact_rel__simps_I11_J,fact_zmod__minus1__right,fact_diff__bin__simps_I4_J,fact_minus__Min,fact_zmult__eq__1__iff,fact_pos__zmult__eq__1__iff__lemma,fact_diff__bin__simps_I6_J,fact_diff__bin__simps_I5_J,fact_of__int__m1,fact_zdiv__minus1__right,fact_zero__code__numeral__code,fact_minus1__divide,fact_abs__power__minus__one,fact_div__eq__minus1,fact_div__pos__neg__trivial,fact_zmod__minus1,fact_one__code__numeral__code,fact_power__m1__even,fact_Nitpick_OFrac__def,fact_int__ge__less__than__def,fact_int__ge__less__than2__def,fact_inj__graph,fact_Nitpick_Oprod__def,fact_nat__of__aux__code,fact_divmod__int__rel__def,fact_divmod__int__correct,fact_zmult2__lemma,fact_code__numeral_Osize_I1_J,fact_Nats__number__of,fact_sup__Un__eq2,fact_pred__subset__eq2,fact_bot__empty__eq2,fact_pred__equals__eq2,fact_inf__Int__eq2,fact_congruentD,fact_congruent2D,fact_Image__iff,fact_rev__ImageI,fact_unique__remainder,fact_unique__quotient,fact_self__remainder,fact_divmod__int__rel__0,fact_INF__INT__eq2,fact_SUP__UN__eq2,fact_self__quotient,fact_divmod__int__rel__mod,fact_divmod__int__rel__div,fact_Nats__0,fact_divmod__int__mod__div,fact_Nats__add,fact_Nats__mult,fact_Nats__1,fact_of__nat__in__Nats,fact_Image__singleton__iff,fact_equiv__class__eq,fact_quotient__eqI,fact_quotient__eq__iff,fact_divmod__int__rel__div__mod,fact_Image__singleton,fact_eq__equiv__class,fact_eq__equiv__class__iff,fact_equiv__class__eq__iff,fact_equiv__class__subset,fact_eq__equiv__class__iff2,fact_zadd1__lemma,fact_zminus1__lemma,fact_subset__equiv__class,fact_equiv__class__nondisjoint,fact_divmod__int__relI,fact_zmult1__lemma,fact_pair__imageI,fact_norm__frac_Osimps,fact_adjust__eq,fact_sup2CI,fact_sup2E,fact_inf2E,fact_inf2I,fact_mem__splitI,fact_splitI,fact_prod__caseI,fact_bot2E,fact_splitD_H,fact_swap__inj__on,fact_sup2I2,fact_sup2I1,fact_rev__predicate2D,fact_predicate2D,fact_inf2D2,fact_inf2D1,fact_Pair__inject,fact_Pair__eq,fact_split__paired__All,fact_split__weak__cong,fact_split__twice,fact_split__conv,fact_prod_Osimps_I2_J,fact_splitD,fact_split__eta,fact_The__split__eq,fact_split__paired__The,fact_adjust__def,fact_in__rel__def,fact_div__mod__code__numeral__def,fact_negDivAlg__eqn__1__number__of,fact_negDivAlg__correct,fact_negDivAlg__div__mod,fact_negDivAlg__minus1,fact_negDivAlg_Osimps,fact_negDivAlg__eqn,fact_negDivAlg__eqn__number__of,fact_Nitpick_Orefl_H__def,fact_posDivAlg__eqn__1__number__of,fact_posDivAlg_Osimps,fact_posDivAlg__0,fact_posDivAlg__correct,fact_posDivAlg__div__mod,fact_posDivAlg__eqn__number__of,fact_posDivAlg__eqn,fact_divmod__int__def,fact_divmod__nat__step,fact_divmod__int__pdivmod,fact_negateSnd__def,fact_apsnd__conv,fact_divmod__nat__zero,fact_divmod__nat__base,fact_negateSnd__eq,fact_divmod__nat__div__mod,fact_divmod__int__rel__neg,fact_divmod__nat__if,fact_pdivmod__def,fact_pdivmod__posDivAlg,fact_divmod__int__code,fact_UN__equiv__class__inject,fact_divmod__nat__rel__mult1__eq,fact_divmod__nat__rel__mult2__eq,fact_divmod__nat__rel__unique,fact_divmod__nat__rel__divmod__nat,fact_divmod__nat__eq,fact_divmod__nat__def,fact_mod__eq,fact_div__eq,fact_divmod__nat__rel,fact_divmod__nat__rel__add1__eq,fact_negDivAlg_Opsimps,fact_posDivAlg_Opsimps,fact_mod__pos__neg__1__number__of,fact_apsnd__eq__conv,fact_snd__apsnd,fact_snd__def,fact_snd__conv,fact_snd__eqD,fact_mod__int__def,fact_mod__neg__pos,fact_mod__pos__pos,fact_mod__pos__pos__1__number__of,fact_mod__pos__neg,fact_mod__neg__neg,fact_norm__frac_Opsimps,fact_negDivAlg_Opinduct,fact_posDivAlg_Opinduct,fact_mod__nat__def,fact_accp__subset,fact_irrefl__def,fact_norm__frac_Opinduct,fact_accp_Osimps,fact_accp_Oequations,fact_accp__downward,fact_nat__gcd_Opsimps,fact_nat_Osize_I2_J,fact_in__measure,fact_nat_Osize_I1_J,fact_div__pos__neg__1__number__of,fact_nat__def,fact_nat__gcd_Opinduct,fact_fst__apsnd,fact_fst__def,fact_Rep__Integ__inject,fact_fst__conv,fact_fst__eqD,fact_Pair__fst__snd__eq,fact_prod__eqI,fact_surjective__pairing,fact_pair__collapse,fact_prod__case__beta,fact_div__int__def,fact_split__comp__eq,fact_split__beta,fact_split__def,fact_The__split,fact_div__neg__pos,fact_div__pos__pos,fact_div__pos__pos__1__number__of,fact_div__pos__neg,fact_div__neg__neg,fact_prod__size__simp,fact_exI__realizer,fact_conjI__realizer,fact_div__nat__def,fact_divmod__nat__rel__def,fact_inv__image__def,fact_mlex__leq,fact_code__numeral_Osize_I2_J,fact_code__numeral_Oinject,fact_code__numeral_Osimps_I3_J,fact_code__numeral_Osimps_I2_J,fact_in__inv__image,fact_Suc__code__numeral__minus__one,fact_mlex__less,fact_code__numeral_Osize_I4_J,fact_rp__inv__image__def,fact_finite__psubset__def,fact_code__numeral_Osize_I3_J,fact_in__finite__psubset,fact_nat_Osize_I4_J,fact_prod_Orecs,fact_in__lex__prod,fact_nat__size,fact_nat_Osize_I3_J,fact_same__fstI,fact_equivp__equiv,fact_apsnd__apfst,fact_apfst__conv,fact_apfst__eq__conv,fact_fst__apfst,fact_snd__apfst,fact_identity__equivp,fact_equivp__def,fact_equivp__reflp,fact_equivp__symp,fact_equivp__transp,fact_apsnd__apfst__commute,fact_apfst__apsnd,fact_pair__lessI2,fact_ImageE,fact_mlex__prod__def,fact_pair__less__def,fact_measure__def,fact_less__than__iff,fact_pair__lessI1,fact_pair__leqI2,fact_smin__insertI,fact_smax__insertI,fact_smin__emptyI,fact_smax__emptyI,fact_pair__leqI1,fact_wmax__insertI,fact_wmin__insertI,fact_Field__insert,fact_Field__Union,fact_Field__empty,fact_mono__Field,fact_Field__Un,fact_finite__Field,fact_wmax__emptyI,fact_wmin__emptyI,fact_min__weak__def,fact_max__weak__def,fact_Id__on__def,fact_Id__on__def_H,fact_Id__on__empty,fact_Image__Id__on,fact_Id__on__eqI,fact_Id__on__iff,fact_max__strict__def,fact_max__ext__additive,fact_min__strict__def,fact_max__extp__max__ext__eq,fact_min__rpair__set,fact_max__rpair__set,fact_rp__inv__image__rp,fact_equiv__intrel__iff,fact_intrel__iff,fact_Id__onE,fact_equiv__intrel,fact_of__int,fact_One__int__def,fact_mult,fact_Rep__Integ__inverse,fact_minus,fact_Zero__int__def,fact_int__def,fact_add,fact_nat,fact_minus__int__def,fact_less,fact_le,fact_eq__Abs__Integ,fact_Integ__def,fact_code__numeral_Osimps_I5_J,fact_Rep__Integ,fact_code__numeral_Osimps_I4_J,fact_type__definition__Integ,fact_accp__acc__eq,fact_rel__comp__def,fact_rel__compI,fact_rel__comp__UNION__distrib,fact_rel__comp__UNION__distrib2,fact_rel__comp__empty1,fact_rel__comp__empty2,fact_rel__comp__distrib,fact_rel__comp__distrib2,fact_rel__comp__mono,fact_O__assoc,fact_union__comp__emptyL,fact_union__comp__emptyR,fact_acc__subset,fact_acc_Osimps,fact_acc__downward,fact_max__ext__compat,fact_min__ext__compat,fact_type__definition_OAbs__image,fact_type__definition_ORep__range,fact_type__definition_OAbs__inject,fact_type__definition_ORep__inject,fact_type__definition_ORep__inverse,fact_type__definition_ORep,fact_type__definition_OAbs__inverse,fact_pred__comp__rel__comp__eq,fact_reduction__pairI,fact_max__extp_Oequations,fact_wf__less__than,fact_pred__comp_Ointros,fact_wf__empty,fact_wf__inv__image,fact_wf__lex__prod,fact_wf__measure,fact_wf__comp__self,fact_wf__subset,fact_min__ext__wf,fact_wf__less,fact_wf__finite__psubset,fact_pred__comp_Oequations,fact_wf__Int2,fact_wf__Int1,fact_wf__mlex,fact_wf__pair__less,fact_max__ext__wf,fact_wf__irrefl,fact_wf__asym,fact_wf__not__sym,fact_wf__not__refl,fact_wf__int__ge__less__than2,fact_wf__int__ge__less__than,fact_wf__acc__iff,fact_acc__wfD,fact_wf__no__loop,fact_wf__union__merge,fact_wf__iff__no__infinite__down__chain,fact_wfE__pf,fact_wf__union__compatible,fact_wf,fact_reduction__pair__def,fact_reduction__pair__lemma,fact_wf__lenlex,fact_wf__if__measure,fact_max__ext_Ointros,fact_pred__nat__def,fact_wf__lex,fact_wf__lexn,fact_lex__def,fact_lexn_Osimps_I1_J,fact_wf__pred__nat,fact_wf__same__fst,fact_Nitpick_Ozero__frac__def,fact_Range__Collect__split,fact_RangeI,fact_Range__Id__on,fact_Range__Diff__subset,fact_Range__Union,fact_Range__empty__iff,fact_Range__empty,fact_Range__Un__eq,fact_finite__Range,fact_snd__eq__Range,fact_Range__iff,fact_Range__insert,fact_Range__Int__subset,fact_Nitpick_Oone__frac__def,fact_Nitpick_Onumber__of__frac__def,fact_RangeP__Range__eq,fact_RangeP_Ointros,fact_RangeP_Oequations,fact_Nitpick_Ofrac__def,fact_RangeE,fact_wf__Un,fact_DomainI,fact_Domain__Id__on,fact_Domain__empty__iff,fact_Domain__empty,fact_Domain__mono,fact_Domain__Un__eq,fact_finite__Domain,fact_fst__eq__Domain,fact_Domain__iff,fact_Domain__insert,fact_Domain__Int__subset,fact_Domain__Diff__subset,fact_Field__def,fact_Domain__Union,fact_Domain__Collect__split,fact_DomainP__Domain__eq,fact_DomainE,fact_image__split__eq__Sigma,fact_DomainP_Ointros,fact_SigmaI,fact_Sigma__empty1,fact_Times__eq__cancel2,fact_Sigma__Union,fact_card__cartesian__product,fact_setsum__cartesian__product,fact_Times__empty,fact_Sigma__empty2,fact_Compl__Times__UNIV2,fact_Compl__Times__UNIV1,fact_setprod__cartesian__product,fact_Sigma__Un__distrib2,fact_Times__Un__distrib1,fact_Sigma__Un__distrib1,fact_rel__comp__subset__Sigma,fact_swap__product,fact_finite__cartesian__product,fact_equiv__type,fact_Sigma__Int__distrib1,fact_Times__Int__distrib1,fact_Sigma__Int__distrib2,fact_Id__on__subset__Times,fact_Sigma__Diff__distrib1,fact_Times__Diff__distrib1,fact_Sigma__Diff__distrib2,fact_DomainP_Oequations,fact_UNIV__Times__UNIV,fact_mem__Sigma__iff,fact_SigmaD1,fact_SigmaD2,fact_SigmaE2,fact_card__cartesian__product__singleton,fact_Times__subset__cancel2,fact_Image__subset,fact_finite__cartesian__productD1,fact_finite__cartesian__productD2,fact_Collect__split,fact_SetCompr__Sigma__eq,fact_fst__image__times,fact_snd__image__times,fact_insert__times__insert,fact_finite__equiv__class,fact_UN__Times__distrib,fact_Sigma__def,fact_finite__quotient,fact_setsum__mult__setsum__if__inj,fact_Ex__inj__on__UNION__Sigma,fact_fold__image__Sigma,fact_image__id,fact_inj__on__id,fact_vimage__id,fact_id__apply,fact_id__def,fact_apsnd__id,fact_apfst__id,fact_of__int__eq__id,fact_surj__id,fact_split__Pair,fact_setsum__reindex__id,fact_setprod__reindex__id,fact_setprod__Sigma,fact_setsum__Sigma,fact_card__SigmaI,fact_finite__SigmaI,fact_SigmaE,fact_map__pair__surj,fact_map__pair__imageI,fact_map__pair__simp,fact_map__pair__ident,fact_snd__prod__fun,fact_fst__map__pair,fact_map__pair_Oidentity,fact_apsnd__def,fact_apfst__def,fact_map__pair_Oid,fact_map__pair__def,fact_map__pair__surj__on,fact_wf__map__pair__image,fact_map__pair__inj__on,fact_prod__fun__imageE,fact_refl__on__def,fact_wfP__def,fact_wfP__empty,fact_refl__on__Id__on,fact_wfP__accp__iff,fact_accp__wfPD,fact_wfP__subset,fact_refl__on__empty,fact_refl__on__Un,fact_refl__on__Int,fact_refl__onD,fact_refl__onD1,fact_refl__onD2,fact_wf__in__rel,fact_wfP__wf__eq,fact_reflp__def,fact_refl__onI,fact_wfP__acyclicP,fact_acyclic__subset,fact_reflpE,fact_wf__acyclic,fact_wf__iff__acyclic__if__finite,fact_finite__acyclic__wf,fact_Nitpick_Owf_H__def,fact_Rep__Integ__induct,fact_Rep__Integ__cases,fact_refl__on__def_H,fact_Abs__Integ__induct,fact_Abs__Integ__cases,fact_INFI__bool__eq,fact_ball__empty,fact_Powp__def,fact_Collect__ball__eq,fact_congruent__def,fact_INTER__def,fact_Sup__Inf,fact_Inf__Sup,fact_wfP__SUP,fact_mem__splitI2,fact_mem__splitE,fact_Inter__eq,fact_vimage__Times,fact_Eps__split,fact_wfI__pf,fact_id__o,fact_o__id,fact_o__eq__id__dest,fact_fun__left__comm__idem_Ofun__comp__idem,fact_fun__upd__comp,fact_vimage__compose,fact_o__assoc,fact_o__apply,fact_o__eq__dest,fact_o__eq__elim,fact_tfl__some,fact_someI,fact_comp__cong,fact_o__eq__dest__lhs,fact_fun__left__comm_Ofun__comp__comm,fact_someI__ex,fact_some__eq__ex,fact_some__eq__trivial,fact_some__sym__eq__trivial,fact_K__record__comp,fact_o__def,fact_exE__some,fact_apsnd__compose,fact_apfst__compose,fact_inj__on__imageI2,fact_inj__comp,fact_comp__surj,fact_comp__inj__on__iff,fact_comp__inj__on,fact_inj__on__imageI,fact_image__compose,fact_map__pair_Ocompositionality,fact_map__pair__compose,fact_map__pair_Ocomp,fact_setsum__reindex,fact_setprod__reindex,fact_setprod__reindex__cong,fact_Eps__split__eq,fact_split__paired__Eps,fact_setsum_Oreindex,fact_setprod_Oreindex,fact_the__inv__into__comp,fact_fold__image__reindex,fact_folding_Oremove,fact_folding__image_Oreindex,fact_folding_Ounion,fact_folding_Ocommute__comps_I1_J,fact_folding_Ocommute__comp,fact_folding_Ocommute__left__comp,fact_UN__o,fact_fst__comp__map__pair,fact_snd__comp__map__pair,fact_folding__image_Odistrib,fact_split__comp,fact_folding_Ocommute__comp_H,fact_folding_Ocommute__left__comp_H,fact_folding_Ocommute__comp_H_H,fact_folding_Ocommute__left__comp_H_H,fact_folding_Oempty,fact_folding_Oeq__fold,fact_folding__image_Oeq__fold,fact_folding_Oinsert,fact_folding_Ounion__inter,fact_folding_Oinsert__remove,fact_hoare__derivs_OIf,fact_Loop,fact_setsum__reindex__nonzero,fact_peek__and__def,fact_folding__idem_Ounion__idem,fact_folding__idem_Osubset__comp__idem,fact_folding__idem_Oinsert__idem,fact_folding__idem_Oidem__left__comp,fact_folding__idem_Oidem__comp,fact_folding__idem_Oin__comp__idem,fact_strong__setprod__reindex__cong,fact_Sigma__mono,fact_not__acc__down,fact_acc_OaccI,fact_max__ext_Osimps,fact_wf__no__infinite__down__chainE,fact_scomp__unfold,fact_setsum__ivl__cong,fact_less__eq,fact_Pair__scomp,fact_scomp__Pair,fact_scomp__scomp,fact_wf__trancl,fact_scomp__apply,fact_scomp__def,fact_less__than__def,fact_acyclic__def,fact_trancl_Or__into__trancl,fact_trancl__subset__Field2,fact_trancl__Int__subset,fact_r__into__trancl_H,fact_trancl__empty,fact_trancl__domain,fact_trancl__range,fact_finite__trancl,fact_trancl__trans,fact_Transitive__Closure_Otrancl__into__trancl,fact_trancl__into__trancl2,fact_r__r__into__trancl,fact_trancl__mono,fact_trancl__unfold,fact_trancl__subset__Sigma,fact_iterate_Osimps,fact_trancl__insert,fact_r__into__rtrancl,fact_rtrancl_Ortrancl__refl,fact_trancl__into__rtrancl,fact_trancl__rtrancl__absorb,fact_rtrancl__trancl__absorb,fact_trancl__unfold__right,fact_trancl__unfold__left,fact_Domain__rtrancl,fact_Range__rtrancl,fact_in__rtrancl__UnI,fact_r__comp__rtrancl__eq,fact_rtrancl__idemp__self__comp,fact_rtrancl__subset__rtrancl,fact_rtrancl__subset,fact_rtrancl__mono,fact_rtrancl__Un__subset,fact_rtrancl__Un__rtrancl,fact_Image__closed__trancl,fact_rtrancl__idemp,fact_rtrancl__trans,fact_rtrancl_Ortrancl__into__rtrancl,fact_converse__rtrancl__into__rtrancl,fact_refl__rtrancl,fact_rtrancl__trancl__trancl,fact_trancl__rtrancl__trancl,fact_rtrancl__into__trancl1,fact_rtranclD,fact_rtrancl__into__trancl2,fact_rtrancl__eq__or__trancl,fact_Not__Domain__rtrancl,fact_acc__downwards,fact_acc__downwards__aux,fact_wf__insert,fact_acyclic__insert,fact_pred__nat__trancl__eq__le,fact_trancl__subset__Sigma__aux,fact_log_Osimps,fact_minus__shift__def,fact_inc__shift__def,fact_range,fact_irrefl__tranclI,fact_sequence__trans,fact_acyclic__converse,fact_converse__UNION,fact_converse__rel__comp,fact_converse__Un,fact_converse__Id__on,fact_converse__inv__image,fact_converse__Int,fact_converse__converse,fact_finite__converse,fact_Field__converse,fact_converse__iff,fact_converseI,fact_converseD,fact_refl__on__converse,fact_converse__INTER,fact_trancl__converse,fact_rtrancl__converse,fact_wf__converse__trancl,fact_equiv__comp__eq,fact_Range__converse,fact_Domain__converse,fact_Range__def,fact_rtrancl__converseI,fact_rtrancl__converseD,fact_trancl__converseI,fact_trancl__converseD,fact_Image__subset__eq,fact_refl__on__comp__subset,fact_comp__equivI,fact_finite__acyclic__wf__converse,fact_converse__def,fact_Image__INT__eq,fact_reflcl__set__eq,fact_IdI,fact_converse__Id,fact_single__valued__subset,fact_single__valued__rel__comp,fact_single__valued__Id,fact_Image__Id,fact_Id__O__R,fact_R__O__Id,fact_single__valued__Id__on,fact_pair__in__Id__conv,fact_Domain__Id,fact_rtrancl__empty,fact_Range__Id,fact_rtrancl__reflcl,fact_rtrancl__reflcl__absorb,fact_refl__Id,fact_rtrancl__r__diff__Id,fact_single__valuedD,fact_single__valued__def,fact_pair__leq__def,fact_reflcl__trancl,fact_trancl__reflcl,fact_rtrancl__unfold,fact_refl__reflcl,fact_Id__def,fact_irrefl__diff__Id,fact_single__valued__confluent,fact_Image__Int__eq,fact_rtrancl__Int__subset,fact_total__on__diff__Id,fact_rtrancl__imp__UN__rel__pow,fact_single__valued__rel__pow,fact_comp__funpow,fact_wf__exp,fact_funpow__mult,fact_funpow__swap1,fact_rel__pow__1,fact_rel__pow__commute,fact_rel__pow__imp__rtrancl,fact_rtrancl__power,fact_relpow_Osimps_I2_J,fact_rel__pow__add,fact_relpow_Osimps_I1_J,fact_total__on__empty,fact_total__on__converse,fact_rel__pow__0__I,fact_rel__pow__0__E,fact_rel__pow__Suc__I2,fact_rel__pow__Suc__I,fact_funpow_Osimps_I2_J,fact_funpow__add,fact_funpow_Osimps_I1_J,fact_trancl__power,fact_total__on__def,fact_rtrancl__is__UN__rel__pow,fact_funpow__code__def,fact_rel__pow__E2,fact_rel__pow__E,fact_acyclicI,fact_rtrancl__Un__separator__converseE,fact_rtrancl__Un__separatorE,fact_rel__pow__Suc__D2,fact_rel__pow__Suc__E2,fact_rel__pow__Suc__E,fact_tranclD2,fact_tranclD,fact_IdE,fact_nat__intermed__int__val,fact_mod__div__decomp,fact_wf__eq__minimal,fact_transfer__nat__int__set__cong,fact_Int__Collect__mono,fact_UnionE,fact_rel__compE,fact_converseE,fact_Nitpick_Oplus__frac__def,fact_setprod__pos,fact_Nitpick_Otimes__frac__def,fact_Nitpick_Oof__frac__def,fact_Nitpick_Oinverse__frac__def,fact_Nitpick_Ouminus__frac__def,fact_Nitpick_Oless__frac__def,fact_Nitpick_Oless__eq__frac__def,fact_Nitpick_Onum__def,fact_Nitpick_Odenom__def,fact_internal__split__def,fact_setprod__nonneg,fact_internal__split__conv,fact_bool_Osize_I1_J,fact_bool_Osize_I2_J,fact_finite__less__ub,fact_lenlex__def,fact_neq__if__length__neq,fact_lexn__length,fact_lenlex__conv,fact_length__sublist,fact_lexn_Osimps_I2_J,fact_impossible__Cons,fact_not__Cons__self,fact_not__Cons__self2,fact_list_Oinject,fact_list_Osize_I4_J,fact_Cons__in__lex,fact_set__Cons__def,fact_pick_Osimps,fact_select__weight__cons__zero,fact_lexord__cons__cons,fact_lexord__lex,fact_rtrancl__listrel1__ConsI2,fact_list_Osize_I2_J,fact_Cons__acc__listrel1I,fact_listrel1__mono,fact_listrel1__rtrancl__subset__rtrancl__listrel1,fact_listrel1__converse,fact_rtrancl__listrel1__ConsI1,fact_listrel1I2,fact_rtrancl__listrel1__eq__len,fact_listrel1__eq__len,fact_in__listrel1__converse,fact_listrel1I1,fact_Cons__listrel1__Cons,fact_listrel__Cons,fact_lexord__irreflexive,fact_listrel__rtrancl__refl,fact_listrel__mono,fact_listrel__subset__rtrancl__listrel1,fact_listrel__eq__len,fact_listrel__rtrancl__trans,fact_listrel__rtrancl__eq__rtrancl__listrel1,fact_listrel__reflcl__if__listrel1,fact_listrel1__subset__listrel,fact_rtrancl__listrel1__if__listrel,fact_listrel_OCons,fact_listrelp__listrel__eq,fact_listrel__Cons2,fact_listrelp_OCons,fact_listrelp_Oequations_I2_J,fact_listrel__Cons1,fact_listrel__subset,fact_lists__UNIV,fact_lists__mono,fact_equiv__listrel,fact_listrel__refl__on,fact_Cons__in__lists__iff,fact_lists__accD,fact_lists__accI,fact_listrel__iff__nth,fact_lexord__linear,fact_infinite__UNIV__listI,fact_list__eq__iff__nth__eq,fact_nth__Cons__0,fact_nth__Cons__Suc,fact_nth_Osimps,fact_nth__Cons_H,fact_nth__Cons__number__of,fact_lexord__take__index__conv,fact_set__sublist,fact_finite__set,fact_set__subset__Cons,fact_take__all,fact_set__take__subset,fact_set__take__subset__set__take,fact_set__sublist__subset,fact_nth__take,fact_notin__set__sublistI,fact_in__set__takeD,fact_in__set__sublistD,fact_set__ConsD,fact_take__Suc__Cons,fact_length__take,fact_take__take,fact_List_Oset_Osimps_I2_J,fact_sublist__upt__eq__take,fact_card__length,fact_all__set__conv__all__nth,fact_list__size__estimation,fact_list__size__estimation_H,fact_in__lists__conv__set,fact_length__pos__if__in__set,fact_nth__mem,fact_in__set__conv__nth,fact_lists__eq__set,fact_set__conv__nth,fact_finite__lists__length__eq,fact_finite__lists__length__le,fact_listrel__iff__zip,fact_set__zip,fact_take__zip,fact_length__zip,fact_zip__Cons__Cons,fact_list__eq__iff__zip__eq,fact_zip__same,fact_set__zip__leftD,fact_set__zip__rightD,fact_in__set__zipE,fact_nth__zip,fact_greaterThanLessThan__upto,fact_listsum__setsum__nth,fact_atLeastAtMost__upto,fact_set__upto,fact_listsum__eq__0__nat__iff__nat,fact_elem__le__listsum__nat,fact_listsum__simps_I2_J,fact_atLeastLessThan__upto,fact_greaterThanAtMost__upto,fact_nat__list__def,fact_list__size__pointwise,fact_listsum__update__nat,fact_butlast__take,fact_list__update__beyond,fact_nth__list__update__neq,fact_list__update__id,fact_length__list__update,fact_butlast__list__update,fact_zip__update,fact_update__zip,fact_list__update__overwrite,fact_list__update__swap,fact_list__update_Osimps_I2_J,fact_list__update__code_I2_J,fact_list__update__code_I3_J,fact_in__set__butlastD,fact_set__update__subsetI,fact_set__update__subset__insert,fact_nth__list__update,fact_list__update__same__conv,fact_nth__list__update__eq,fact_take__butlast,fact_length__butlast,fact_set__update__memI,fact_butlast__conv__take,fact_listrel1__iff__update,fact_distinct__list__update,fact_distinct__upto,fact_distinct__take,fact_distinct__sublistI,fact_distinct__zipI1,fact_distinct__zipI2,fact_distinct_Osimps_I2_J,fact_card__distinct,fact_distinct__card,fact_distinct__conv__nth,fact_nth__eq__iff__index__eq,fact_distinct__listsum__conv__Setsum,fact_Nitpick_Ocard_H__def,fact_nth__take__lemma,fact_set__remove1__eq,fact_take__Cons__number__of,fact_lists_ONil,fact_listrel__Nil1,fact_listrel__Nil2,fact_distinct__butlast,fact_distinct__remove1,fact_distinct_Osimps_I1_J,fact_butlast_Osimps_I1_J,fact_butlast_Osimps_I2_J,fact_list_Osimps_I2_J,fact_list_Osimps_I3_J,fact_remove1_Osimps_I2_J,fact_upto__empty,fact_take__eq__Nil,fact_take__0,fact_take__Nil,fact_sublist__nil,fact_remove1__commute,fact_remove1_Osimps_I1_J,fact_listrelp_Oequations_I1_J,fact_listrelp_ONil,fact_zip__Nil,fact_zip_Osimps_I1_J,fact_listsum__simps_I1_J,fact_length__0__conv,fact_list_Osize_I3_J,fact_set__empty,fact_set__empty2,fact_List_Oset_Osimps_I1_J,fact_list_Osize_I1_J,fact_list__update__code_I1_J,fact_list__update_Osimps_I1_J,fact_list__update__nonempty,fact_remove1__idem,fact_notin__set__remove1,fact_in__set__remove1,fact_sublist__empty,fact_set__remove1__subset,fact_length__greater__0__conv,fact_take__1__Cons,fact_not__Nil__listrel1,fact_not__listrel1__Nil,fact_listrel_ONil,fact_lexord__Nil__right,fact_Nil__notin__lex,fact_Nil2__notin__lex,fact_take__Cons,fact_upto_Osimps,fact_sublist__singleton,fact_lists__empty,fact_take__Cons_H,fact_upto__rec__number__of,fact_listrel__Nil,fact_set__Cons__sing__Nil,fact_length__remove1,fact_upto_Opsimps,fact_select,fact_listset_Osimps_I1_J,fact_zip__Cons,fact_list_Osimps_I5_J,fact_list_Osimps_I4_J,fact_listset_Osimps_I2_J,fact_zip__Cons1,fact_sorted__list__of__set__remove,fact_upto_Opinduct,fact_sorted__list__of__set__empty,fact_anamorph_Osimps,fact_sublist__Cons,fact_append__eq__Cons__conv,fact_Cons__eq__append__conv,fact_append1__eq__conv,fact_append__Cons,fact_Cons__eq__appendI,fact_append__in__lists__conv,fact_append__eq__appendI,fact_append__same__eq,fact_same__append__eq,fact_append__eq__append__conv2,fact_append__assoc,fact_listsum__append,fact_length__append,fact_zip__append,fact_set__append,fact_append__Nil,fact_Nil__is__append__conv,fact_append__Nil2,fact_self__append__conv,fact_self__append__conv2,fact_append__is__Nil__conv,fact_append__self__conv,fact_append__self__conv2,fact_eq__Nil__appendI,fact_butlast__append,fact_nth__append__length,fact_nth__append__length__plus,fact_take__append,fact_list__update__append1,fact_list__update__length,fact_remove1__append,fact_in__set__butlast__appendI,fact_butlast__snoc,fact_append__listrel1I,fact_lexord__append__leftI,fact_distinct__append,fact_nth__append,fact_list__update__append,fact_sublist__append,fact_listrel1I,fact_lexord__append__left__rightI,fact_take__Suc__conv__app__nth,fact_snoc__listrel1__snoc__iff,fact_listrel1E,fact_lexord__append__leftD,fact_rotate1__def,fact_upd__conv__take__nth__drop,fact_append__take__drop__id,fact_drop__1__Cons,fact_drop__Suc__Cons,fact_nth__via__drop,fact_distinct__drop,fact_distinct1__rotate,fact_butlast__drop,fact_drop__butlast,fact_drop__take,fact_take__drop,fact_drop__0,fact_drop__drop,fact_drop__zip,fact_length__drop,fact_length__rotate1,fact_set__rotate1,fact_in__set__dropD,fact_set__drop__subset,fact_drop__Nil,fact_rotate1__is__Nil__conv,fact_set__drop__subset__set__drop,fact_drop__eq__Nil,fact_drop__all,fact_drop__append,fact_append__eq__conv__conj,fact_drop__Cons,fact_drop__Cons_H,fact_nth__drop,fact_append__eq__append__conv__if,fact_nth__drop_H,fact_rotate__simps,fact_drop__Cons__number__of,fact_take__add,fact_rotate1__length01,fact_zip__append2,fact_zip__append1,fact_id__take__nth__drop,fact_take__hd__drop,fact_hd__drop__conv__nth,fact_hd_Osimps,fact_hd__append2,fact_hd__append,fact_hd__in__set,fact_hd__conv__nth,fact_rotate1__hd__tl,fact_hd__rotate__conv__nth,fact_drop__tl,fact_tl__drop,fact_tl_Osimps_I2_J,fact_distinct__tl,fact_distinct__rotate,fact_rotate__add,fact_rotate0,fact_rotate__rotate,fact_length__rotate,fact_set__rotate,fact_tl_Osimps_I1_J,fact_rotate__is__Nil__conv,fact_rotate1__rotate__swap,fact_rotate__def,fact_tl__append2,fact_take__tl,fact_rotate__conv__mod,fact_drop__Suc,fact_rotate__Suc,fact_tl__append,fact_rotate__id,fact_rotate__length01,fact_length__tl,fact_tl__take,fact_take__Suc,fact_rotate__drop__take,fact_fold1__set,fact_lexord__append__rightI,fact_foldl__Nil,fact_start__le__sum,fact_foldl__assoc,fact_foldl__absorb0,fact_foldl__Cons,fact_foldl__append,fact_listsum__foldl,fact_sum__eq__0__conv,fact_fun__left__comm__idem_Ofold__set,fact_Sup__set__fold,fact_Inf__set__fold,fact_Sup__fin__set__fold,fact_Inf__fin__set__fold,fact_Min__fin__set__fold,fact_Max__fin__set__fold,fact_min__max_OInf__fin__set__fold,fact_min__max_OSup__fin__set__fold,fact_SUPR__set__fold,fact_INFI__set__fold,fact_elem__le__sum,fact_sorted__list__of__set__insert,fact_lexord__Nil__left,fact_insort__key_Osimps_I1_J,fact_insort__key_Osimps_I2_J,fact_set__insort,fact_length__insort,fact_fun__left__comm__insort,fact_insort__left__comm,fact_insort__key__left__comm,fact_remove1__insort,fact_insort__not__Nil,fact_distinct__insort,fact_insort__insert__insort__key,fact_insort__insert__insort,fact_distinct__insort__insert,fact_insort__insert__triv,fact_set__insort__insert,fact_insort__insert__key__triv,fact_last__list__update,fact_last__conv__nth,fact_last_Osimps,fact_last__ConsR,fact_last__ConsL,fact_last__append,fact_last__appendR,fact_last__appendL,fact_last__in__set,fact_last__snoc,fact_last__drop,fact_append__butlast__last__id,fact_snoc__eq__iff__butlast,fact_lists_Osimps,fact_select__weigth__select,fact_inj__mapI,fact_last__map,fact_foldl__map,fact_rotate__map,fact_map__tl,fact_zip__map2,fact_map__zip__map2,fact_map__zip__map,fact_zip__map1,fact_zip__map__map,fact_zip__same__conv__map,fact_map__is__Nil__conv,fact_map_Osimps_I1_J,fact_Nil__is__map__conv,fact_map__update,fact_map__eq__conv,fact_map__eq__imp__length__eq,fact_length__map,fact_listsum__addf,fact_listsum__subtractf,fact_listsum__0,fact_listsum__const__mult,fact_listsum__mult__const,fact_inj__map__eq__map,fact_map__injective,fact_map__ident,fact_take__map,fact_map__butlast,fact_set__map,fact_map_Osimps_I2_J,fact_map__append,fact_hd__map,fact_drop__map,fact_List_Omap_Ocomp,fact_map__comp__map,fact_List_Omap_Ocompositionality,fact_map__map,fact_List_Omap_Oidentity,fact_List_Omap_Oid,fact_list__size__map,fact_inj__on__map__eq__map,fact_map__inj__on,fact_nth__map,fact_map__fun__upd,fact_distinct__map,fact_listsum__abs,fact_uminus__listsum__map,fact_inj__on__mapI,fact_inj__mapD,fact_inj__map,fact_listsum__distinct__conv__setsum__set,fact_listsum__triv,fact_listsum__map__remove1,fact_Nitpick_Osetsum_H__def,fact_pick__same,fact_zero__code__numeral__def,fact_times__code__numeral__code,fact_Code__Numeral_Oof__nat__inject,fact_Code__Numeral_Oof__nat__code,fact_one__code__numeral__def,fact_less__code__numeral__code,fact_code__numeral_Oof__nat__inject,fact_map__fst__zip,fact_map__snd__zip,fact_number__of__code__numeral__def,fact_zip__map__fst__snd,fact_plus__code__numeral__code,fact_less__eq__code__numeral__code,fact_pick__member,fact_zip__eq__conv,fact_list__size__conv__listsum,fact_code__numeral__not__eq__zero,fact_setsum__set__upto__conv__listsum__int,fact_interv__listsum__conv__setsum__set__int,fact_select__weight__member,fact_select__weight__def,fact_select__def,fact_subtract__code__numeral__code,fact_times__code__numeral__def,fact_nat__of__inverse,fact_of__nat__nat__of,fact_nat__of__of__nat,fact_Code__Numeral_Onat__of__inject,fact_code__numeral_Onat__of__inject,fact_type__definition__code__numeral,fact_less__code__numeral__def,fact_nat__of,fact_nat__of__number,fact_int__of__def,fact_less__eq__code__numeral__def,fact_nat__of__code,fact_nat__of__aux__def,fact_Suc__code__numeral__def,fact_minus__code__numeral__def,fact_of__nat__inverse,fact_plus__code__numeral__def,fact_div__code__numeral__def,fact_subtract__code__numeral__def,fact_minus__code__numeral__code,fact_mod__code__numeral__def,fact_code__numeral__decr,fact_listsum__mono,fact_New__DSequence_Opos__not__seq__def,fact_partition__set,fact_lists__IntI,fact_listsp_ONil,fact_listsp_Oequations_I1_J,fact_in__listsp__conv__set,fact_listsp__conj__eq,fact_listsp__infI,fact_listsp__inf__eq,fact_listsp_Oequations_I2_J,fact_append__in__listsp__conv,fact_listsp__mono,fact_partition__P,fact_partition_Osimps_I1_J,fact_listsp__lists__eq,fact_partition_Osimps_I2_J,fact_lists__Int__eq,fact_product_Osimps_I2_J,fact_list__all2__def,fact_list__all2__map1,fact_list__all2__map2,fact_list__all2__dropI,fact_list__all2__appendI,fact_list__all2__append,fact_list__all2__Cons,fact_list__all2__takeI,fact_list__all2__eq,fact_list__all2__lengthD,fact_list__all2__Nil,fact_list__all2__Nil2,fact_product_Osimps_I1_J,fact_list__all2__conv__all__nth,fact_list__all2__nthD,fact_list__all2__nthD2,fact_list__all2__update__cong,fact_list__all2__update__cong2,fact_distinct__product,fact_product__list__set,fact_sublists__powset,fact_length__sublists,fact_sublists_Osimps_I1_J,fact_sublists_Osimps_I2_J,fact_distinct__set__sublists,fact_set__n__lists,fact_enum__the__def,fact_distinct__n__lists,fact_n__lists__Nil,fact_n__lists_Osimps_I1_J,fact_length__n__lists,fact_length__n__lists__elem,fact_list__all2I,fact_all__nth__imp__all__set,fact_fun__left__comm_Ofold__set__remdups,fact_map__removeAll__inj__on,fact_distinct__remdups,fact_length__remdups__leq,fact_distinct__remdups__id,fact_distinct__removeAll,fact_remdups__id__iff__distinct,fact_set__remdups,fact_length__remdups__eq,fact_remdups__remdups,fact_remdups__eq__nil__iff,fact_removeAll_Osimps_I1_J,fact_remdups__eq__nil__right__iff,fact_remdups_Osimps_I1_J,fact_removeAll_Osimps_I2_J,fact_removeAll__append,fact_remdups__map__remdups,fact_remove1__remdups,fact_removeAll__id,fact_distinct__remove1__removeAll,fact_remdups_Osimps_I2_J,fact_length__remdups__card__conv,fact_map__removeAll__inj,fact_set__removeAll,fact_length__remdups__concat,fact_sorted__list__of__set__sort__remdups,fact_sort__key__simps_I1_J,fact_foldl__conv__concat,fact_concat__conv__foldl,fact_length__sort,fact_set__sort,fact_distinct__sort,fact_concat_Osimps_I1_J,fact_concat_Osimps_I2_J,fact_concat__eq__Nil__conv,fact_Nil__eq__concat__conv,fact_map__concat,fact_length__concat,fact_set__concat,fact_sort__key__simps_I2_J,fact_concat__append,fact_sort__foldl__insort,fact_concat__injective,fact_concat__eq__concat__iff,fact_concat__map__singleton,fact_n__lists_Osimps_I2_J,fact_transpose_Osimps_I3_J,fact_transpose__aux__filter__head,fact_filter__concat,fact_filter__sort,fact_distinct__filter,fact_filter__is__subset,fact_filter__id__conv,fact_sum__length__filter__compl,fact_length__filter__le,fact_partition__filter1,fact_filter__filter,fact_filter__remove1,fact_remove1__filter__not,fact_filter__insort__triv,fact_filter__map,fact_filter_Osimps_I1_J,fact_transpose_Osimps_I1_J,fact_filter_Osimps_I2_J,fact_filter__append,fact_filter__empty__conv,fact_remdups__filter,fact_removeAll__filter__not,fact_removeAll__filter__not__eq,fact_partition__filter2,fact_transpose_Osimps_I2_J,fact_nth__transpose,fact_transpose__map__map,fact_set__filter,fact_length__filter__map,fact_length__filter__less,fact_partition__filter__conv,fact_set__minus__filter__out,fact_filter__in__sublist,fact_transpose__empty,fact_length__filter__conv__card,fact_transpose__aux__filter__tail,fact_transpose_Opsimps_I3_J,fact_transpose_Opsimps_I2_J,fact_sublist__shift__lemma__Suc,fact_select__weigth__drop__zero,fact_pick__drop__zero,fact_transpose_Opsimps_I1_J,fact_transpose__max__length,fact_transpose__aux__max,fact_foldr_Osimps_I1_J,fact_foldr_Osimps_I2_J,fact_foldr__append,fact_foldr__conv__foldl,fact_foldr__map,fact_foldl__foldr1,fact_foldl__foldr1__lemma,fact_length__transpose,fact_sublist__def,fact_sublist__shift__lemma,fact_set__upt,fact_atLeastLessThan__upt,fact_upt__Suc__append,fact_upt__Suc,fact_upt__add__eq__append,fact_upt__rec,fact_upt__conv__Cons,fact_upt__eq__Nil__conv,fact_upt__conv__Nil,fact_upt__0,fact_take__upt,fact_sorted__list__of__set__range,fact_hd__upt,fact_drop__upt,fact_distinct__upt,fact_length__upt,fact_upt__rec__number__of,fact_upt__eq__Cons__conv,fact_last__upt,fact_map__Suc__upt,fact_atLeastAtMost__upt,fact_atLeast__upt,fact_nth__upt,fact_greaterThanAtMost__upt,fact_greaterThanLessThan__upt,fact_atMost__upto,fact_map__nth,fact_setsum__set__upt__conv__listsum__nat,fact_interv__listsum__conv__setsum__set__nat,fact_nth__map__upt,fact_transpose__rectangle,fact_insort__key__remove1,fact_sorted_ONil,fact_sorted__single,fact_sorted__upt,fact_sorted__sort,fact_sorted__insort__insert,fact_sorted__drop,fact_sorted__upto,fact_sorted__take,fact_sorted__remove1,fact_sorted__tl,fact_sorted__insort,fact_sorted__butlast,fact_sorted_Oequations_I1_J,fact_sorted__many,fact_sorted__many__eq,fact_sorted__remdups,fact_sorted__distinct__set__unique,fact_sorted__sort__key,fact_sorted__insort__insert__key,fact_sorted__map__remove1,fact_sorted__insort__key,fact_sorted__filter,fact_sorted__map__same,fact_sorted__same,fact_sorted__Cons,fact_sorted__append,fact_filter__insort,fact_sorted_Oequations_I2_J,fact_sorted__list__of__set,fact_insort__remove1,fact_sorted__equals__nth__mono,fact_sorted__nth__mono,fact_map__sorted__distinct__set__unique,fact_transpose__column,fact_nth__nth__transpose__sorted,fact_inj__on__rev,fact_distinct__rev,fact_rev__is__Nil__conv,fact_Nil__is__rev__conv,fact_rev_Osimps_I1_J,fact_singleton__rev__conv,fact_rev__singleton__conv,fact_rev__append,fact_rev__concat,fact_rev__map,fact_rev__filter,fact_zip__rev,fact_set__rev,fact_list__all2__rev,fact_list__all2__rev1,fact_rev__rev__ident,fact_rev__swap,fact_rev__is__rev__conv,fact_listsum__rev,fact_length__rev,fact_foldr__foldl,fact_foldl__foldr,fact_rev__eq__Cons__iff,fact_rev_Osimps_I2_J,fact_hd__rev,fact_last__rev,fact_sorted__transpose,fact_rev__foldl__cons,fact_rev__drop,fact_rev__take,fact_rotate__rev,fact_rev__nth,fact_rev__update,fact_sorted__rev__nth__mono,fact_foldr__max__sorted,fact_length__transpose__sorted,fact_transpose__column__length,fact_transpose__transpose,fact_transfer__nat__int__list__functions_I2_J,fact_sorted__takeWhile,fact_length__takeWhile__le,fact_set__takeWhileD,fact_takeWhile__eq__all__conv,fact_zip__takeWhile__snd,fact_zip__takeWhile__fst,fact_takeWhile__map,fact_takeWhile__tail,fact_takeWhile_Osimps_I2_J,fact_takeWhile_Osimps_I1_J,fact_takeWhile__eq__take,fact_distinct__takeWhile,fact_return__list__def,fact_takeWhile__append1,fact_takeWhile__nth,fact_nth__length__takeWhile,fact_takeWhile__not__last,fact_filter__equals__takeWhile__sorted__rev,fact_transfer__nat__int__list__return__embed,fact_transfer__nat__int__list__functions_I1_J,fact_embed__list__def,fact_takeWhile__neq__rev,fact_dropWhile__neq__rev,fact_takeWhile__dropWhile__id,fact_hd__dropWhile,fact_sorted__dropWhile,fact_length__dropWhile__le,fact_dropWhile__eq__Nil__conv,fact_dropWhile_Osimps_I2_J,fact_dropWhile_Osimps_I1_J,fact_distinct__dropWhile,fact_dropWhile__map,fact_dropWhile__append1,fact_dropWhile__eq__Cons__conv,fact_dropWhile__eq__drop,fact_dropWhile__nth,fact_listsum__map__filter,fact_sorted__nth__monoI,fact_takeWhile__eq__filter,fact_takeWhile__eq__take__P__nth,fact_length__takeWhile__less__P__nth,fact_sorted_Osimps,fact_List_Oinsert__def,fact_not__in__set__insert,fact_insert__remdups,fact_distinct__insert,fact_in__set__insert,fact_List_Oset__insert,fact_insert__Nil,fact_maps__def,fact_concat__map__maps,fact_maps__simps_I2_J,fact_maps__simps_I1_J,fact_distinct__concat,fact_measures__lesseq,fact_wf__measures,fact_in__measures_I1_J,fact_measures__def,fact_in__measures_I2_J,fact_measures__less,fact_foldl__apply,fact_order__fun_I2_J,fact_enum__ex__prod__def,fact_enum__ex,fact_exists__code,fact_zip__obtain__same__length,fact_pos__not__random__dseq__def,fact_dropWhile__append2,fact_list__all2__all__nthI,fact_finite__sorted__distinct__unique,fact_takeWhile__append2,fact_insort__is__Cons,fact_Cons__eq__filter__iff,fact_filter__eq__Cons__iff,fact_order__fun_I1_J,fact_all__code,fact_enum__all,fact_enum__all__prod__def,fact_list__ball__nth,fact_sorted_OCons,fact_list__ex__length,fact_in__set__conv__decomp,fact_list__ex__simps_I2_J,fact_list__ex__append,fact_list__ex__iff,fact_list__ex__rev,fact_list__ex__simps_I1_J,fact_in__set__conv__decomp__first,fact_in__set__conv__decomp__last,fact_list__all__length,fact_measure__function__int,fact_list__all__simps_I2_J,fact_list__all__append,fact_measure__size,fact_is__measure_Osimps,fact_is__measure_Oequations,fact_is__measure_Ointros,fact_list__all__iff,fact_measure__fst,fact_measure__snd,fact_list__all__rev,fact_list__all__simps_I1_J,fact_Ball__set__list__all,fact_list__all__iff__raw,fact_list__ex1__simps_I2_J,fact_transfer__morphism__int__nat,fact_list__ex1__simps_I1_J,fact_bool_Osize_I4_J,fact_bool_Osize_I3_J,fact_list__ex1__iff,fact_New__DSequence_Oneg__decr__bind__def,fact_New__DSequence_Opos__decr__bind__def,fact_New__Random__Sequence_Oneg__decr__bind__def,fact_New__Random__Sequence_Opos__decr__bind__def,fact_New__DSequence_Oneg__bind__def,fact_New__DSequence_Opos__empty__def,fact_pos__empty__def,fact_neg__bind__def,fact_New__DSequence_Opos__bind__def,fact_neg__map__def,fact_neg__single__def,fact_pos__bind__def,fact_New__DSequence_Oneg__single__def,fact_pos__map__def,fact_pos__single__def,fact_length__splice,fact_splice_Osimps_I3_J,fact_splice_Osimps_I1_J,fact_splice__Nil2,fact_splice_Osimps_I2_J,fact_New__DSequence_Opos__single__def,fact_acyclicP__converse,fact_conversep__noteq,fact_conversepD,fact_conversep_Ointros,fact_conversep_Oequations,fact_conversep__iff,fact_conversep__conversep,fact_conversep__eq,fact_converse__pred__comp,fact_converse__join,fact_converse__meet,fact_conversep__converse__eq,fact_,fact_tl__replicate,fact_replicate__length__filter,fact_length__replicate,fact_map__replicate__const,fact_replicate__app__Cons__same,fact_replicate__Suc,fact_rev__replicate,fact_drop__replicate,fact_hd__replicate,fact_take__replicate,fact_last__replicate,fact_zip__replicate,fact_Bex__set__replicate,fact_Ball__set__replicate,fact_replicate__eq__replicate,fact_nth__replicate,fact_append__replicate__commute,fact_replicate__add,fact_filter__replicate,fact_concat__replicate__trivial,fact_replicate__0,fact_empty__replicate,fact_replicate__empty,fact_map__replicate,fact_in__set__replicate,fact_replicate__append__same,fact_map__replicate__trivial,fact_set__replicate,fact_set__replicate__conv__if,fact_set__replicate__Suc,fact_small__lazy__list_Osimps,fact_eq__comp__r,fact_small__lazy__prod__def,fact_New__DSequence_Opos__union__def,fact_field__le__epsilon,fact_pos__union__def,fact_small__lazy_H_Osimps,fact_small__lazy__int__def,fact_small__lazy_H_Opsimps,fact_lazy__sequence_Osize_I4_J,fact__01,fact_lazy__sequence_Oinject,fact_lazy__sequence_Osize_I2_J,fact_small__lazy_H_Opinduct,fact_size__code,fact_lazy__sequence__size__code,fact_seq__case,fact_yieldn__def,fact_lazy__sequence_Osimps_I5_J,fact_refl__on__INTER,fact_in__set__member,fact_member__rec_I1_J,fact_member__set,fact_member__rec_I2_J,fact_List_Omember__def,fact_pair__box_Osize_I1_J,fact_list__ex1__iff__raw,fact_pair__box_Osize_I2_J,fact_pair__box_Oinject,fact_pair__box_Osimps_I2_J,fact_pair__box_Orecs,fact_THE__default__def,fact_setsum__UNION__zero,fact_INF2__I,fact_SUP2__E,fact_finite__maxlen,fact_lazy__sequence_Osize_I3_J,fact_lazy__sequence_Osimps_I2_J,fact_lazy__sequence_Osimps_I3_J,fact__02,fact_lazy__sequence_Osimps_I4_J,fact_lazy__sequence_Osize_I1_J,fact_list__all__iff__all__interval__int,fact_list__ex__iff__not__all__inverval__int,fact_all__interval__int__def,fact_code__numeral_Orecs_I2_J,fact_Random_Osimps,fact_code__numeral_Orecs_I1_J,fact_Random__Sequence_Oempty__def,fact_Random__Sequence_Osingle__def,fact_Random__Sequence_Omap__def,fact_exE__realizer,fact_Image__Collect__split,fact_lexord__trans,fact_trans__less__than,fact_trans__lex__prod,fact_transD,fact_trans__def,fact_Union__eq,fact_trans__O__subset,fact_trans__Int,fact_trans__rtrancl,fact_trans__Id,fact_trans__finite__psubset,fact_trancl__id,fact_trans__trancl,fact_trans__Id__on,fact_lexord__transI,fact_bex__empty,fact_listrel__trans,fact_trans__converse,fact_finite__Collect__bex,fact_bex__UNIV,fact_SUPR__bool__eq,fact_trans__reflclI,fact_trans__inv__image,fact_Bex__set__list__ex,fact_list__ex__iff__raw,fact_UN__eq,fact_INT__eq,fact_Sup__fun__def,fact_Sup__apply,fact_Inf__apply,fact_Inf__fun__def,fact_max__extp_Ointros,fact_transp__def,fact_transpE,fact_equivpE,fact_equivpI,fact_sympE,fact_equivp__reflp__symp__transp,fact_max__extp_Osimps,fact_trans__diff__Id,fact_antisym__converse,fact_antisym__empty,fact_antisym__Id,fact_antisym__Id__on,fact_antisym__subset,fact_antisym__def,fact_antisymD,fact_antisym__reflcl,fact_acyclic__impl__antisym__rtrancl,fact_fun__lub__def,fact_sym__trans__comp__subset,fact_symD,fact_sym__def,fact_sym__Int,fact_sym__rtrancl,fact_sym__Id,fact_sym__Un,fact_sym__trancl,fact_sym__Id__on,fact_listrel__sym,fact_sym__conv__converse__eq,fact_sym__converse,fact_sym__Un__converse,fact_sym__inv__image,fact_sym__Int__converse,fact_equiv__def,fact_equivI,fact_equivE,fact_symp__def,fact_part__equivpI,fact_part__equivp__refl__symp__transp,fact_equivp__implies__part__equivp,fact_part__equivp__transp,fact_part__equivp__symp,fact_part__equivp__def,fact_part__equivpE,fact_part__equivp__typedef,fact_inj__iff,fact_inv__o__cancel,fact_inv__def,fact_inv__id,fact_inv__f__eq,fact_inv__f__f,fact_inv__into__f__eq,fact_inv__into__f__f,fact_f__inv__into__f,fact_inv__into__into,fact_inv__into__injective,fact_image__surj__f__inv__f,fact_surj__f__inv__f,fact_surj__iff__all,fact_image__inv__into__cancel,fact_inv__into__def,fact_o__inv__o__cancel,fact_inj__imp__surj__inv,fact_image__inv__f__f,fact_inv__image__comp,fact_surj__imp__inj__inv,fact_inv__into__image__cancel,fact_inj__on__inv__into,fact_inv__into__comp,fact_surj__iff,fact_inj__transfer,fact_fold__image__UN__disjoint,fact_nat__of__cases,fact_nat__of__induct,fact_of__nat__cases,fact_of__nat__induct,fact_lazy__sequence_Orecs_I1_J,fact_beyond__def,fact_beyond__zero,fact_lazy__sequence_Orecs_I2_J,fact_bij__image__Collect__eq,fact_curry__def,fact_curryI,fact_bij__betw__id,fact_bij__betw__inv__into,fact_inv__into__inv__into__eq,fact_inv__inv__eq,fact_bij__imp__bij__inv,fact_o__inv__distrib,fact_bij__image__INT,fact_bij__betw__comp__iff2,fact_bij__betw__trans,fact_bij__betw__comp__iff,fact_bij__comp,fact_curryE,fact_curryD,fact_curry__conv,fact_split__curry,fact_curry__split,fact_finite__vimage__iff,fact_bij__image__Compl__eq,fact_bij__betw__subset,fact_bij__is__surj,fact_bij__betw__imp__surj,fact_bij__betw__def,fact_inj__on__imp__bij__betw,fact_bij__betw__imp__inj__on,fact_bij__is__inj,fact_bij__betw__the__inv__into,fact_bij__betw__same__card,fact_bij__betw__empty2,fact_bij__betw__empty1,fact_BIJ,fact_bij__betw__finite,fact_bij__betw__id__iff,fact_bij__id,fact_bij__betw__combine,fact_bij__betw__Disj__Un,fact_bij__def,fact_bijI,fact_vimage__subset__eq,fact_bij__vimage__eq__inv__image,fact_ex__bij__betw__nat__finite__1,fact_Cantor__Bernstein,fact_ex__bij__betw__nat__finite,fact_ex__bij__betw__finite__nat,fact_refl__on__UNION,fact_bex__reg__eqv,fact_in__respects,fact_Respects__def,fact_bex__reg__right,fact_babs__reg__eqv,fact_Babs__def,fact_wf__weak__decr__stable,fact_INT__greatest,fact_INT__anti__mono,fact_rtrancl__induct2,fact_converse__rtranclE2,fact_converse__rtrancl__induct2,fact_congruent2I_H,fact_congruentI,fact__03,fact_all__interval__nat__def,fact__04,fact_list__all__iff__all__interval__nat,fact_list__ex__iff__not__all__inverval__nat,fact__05,fact_folding__image_Ocong,fact__06,fact__07,fact_New__DSequence_Opos__map__def,fact_power__dvd__imp__le,fact_dvd_Oorder__refl,fact_dvd__0__right,fact_dvd__1__left,fact_dvd__imp__le,fact_dvd__mult__cancel,fact_nat__mult__dvd__cancel1,fact_setprod__dvd__setprod__subset,fact_inf__period_I4_J,fact_inf__period_I3_J,fact_dvd__div__eq__mult,fact_dvd__div__div__eq__mult,fact_dvd__mult__div__cancel,fact_div__mult__swap,fact_dvd__div__mult__self,fact_dvd__div__mult,fact_div__mult__div__if__dvd,fact_dvd__triv__left,fact_dvd__triv__right,fact_dvd__mult2,fact_dvd__mult,fact_mult__dvd__mono,fact_dvdI,fact_dvd__mult__left,fact_dvd__mult__right,fact_dvd__mult__cancel__left,fact_dvd__mult__cancel__right,fact_nat__mult__dvd__cancel__disj,fact_unity__coeff__ex,fact_dvd_OatLeastAtMost__singleton_H,fact_dvd_OatLeastAtMost__singleton,fact_dvd_OatLeastAtMost__singleton__iff,fact_dvd_OatLeastLessThan__empty__iff2,fact_dvd_OgreaterThanAtMost__empty__iff2,fact_dvd_OatLeastLessThan__empty__iff,fact_dvd_OgreaterThanAtMost__empty__iff,fact_dvd_OgreaterThanLessThan__empty,fact_dvd_OatLeastLessThan__empty,fact_dvd_OgreaterThanAtMost__empty,fact_dvd_OatLeastatMost__empty__iff2,fact_dvd_OatLeastatMost__empty__iff,fact_dvd_OatLeastatMost__empty,fact_dvd__div__neg,fact_dvd__neg__div,fact_minus__dvd__iff,fact_dvd__minus__iff,fact_dvd__1__iff__1,fact_dvd__imp__mod__0,fact_dvd__eq__mod__eq__0,fact_div__dvd__div,fact_dvd__0__left,fact_dvd__mod__imp__dvd,fact_dvd__mod,fact_mod__mod__cancel,fact_dvd__mod__iff,fact_dvd__trans,fact_dvd__refl,fact_dvd_Oless__asym,fact_dvd_Oless__trans,arity_HOL__Obool__Lattices_Obounded__lattice,arity_fun__Lattices_Obounded__lattice,arity_fun__Complete__Lattice_Ocomplete__lattice,arity_fun__Lattices_Obounded__lattice__top,arity_fun__Lattices_Obounded__lattice__bot,arity_fun__Lattices_Osemilattice__sup,arity_fun__Lattices_Osemilattice__inf,arity_fun__Lattices_Odistrib__lattice,arity_fun__Lattices_Oboolean__algebra,arity_fun__Orderings_Opreorder,arity_fun__Finite__Set_Ofinite,arity_fun__Lattices_Olattice,arity_fun__Orderings_Oorder,arity_fun__Orderings_Otop,arity_fun__Orderings_Oord,arity_fun__Orderings_Obot,arity_fun__Groups_Ouminus,arity_fun__Groups_Ominus,arity_fun__Enum_Oenum,arity_Com__Ocom__Nat_Osize,arity_Int__Oint__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,arity_Int__Oint__Groups_Oordered__cancel__ab__semigroup__add,arity_Int__Oint__Groups_Oordered__ab__semigroup__add__imp__le,arity_Int__Oint__Rings_Olinordered__comm__semiring__strict,arity_Int__Oint__Rings_Olinordered__semiring__1__strict,arity_Int__Oint__Groups_Olinordered__ab__semigroup__add,arity_Int__Oint__Rings_Olinordered__semiring__strict,arity_Int__Oint__Groups_Oordered__ab__semigroup__add,arity_Int__Oint__Groups_Oordered__ab__group__add__abs,arity_Int__Oint__Groups_Oordered__comm__monoid__add,arity_Int__Oint__Groups_Olinordered__ab__group__add,arity_Int__Oint__Groups_Ocancel__ab__semigroup__add,arity_Int__Oint__Rings_Oring__1__no__zero__divisors,arity_Int__Oint__Rings_Oordered__cancel__semiring,arity_Int__Oint__Rings_Olinordered__ring__strict,arity_Int__Oint__Rings_Oring__no__zero__divisors,arity_Int__Oint__Rings_Oordered__comm__semiring,arity_Int__Oint__Rings_Olinordered__semiring__1,arity_Int__Oint__Groups_Oordered__ab__group__add,arity_Int__Oint__Groups_Ocancel__semigroup__add,arity_Int__Oint__Rings_Olinordered__semiring,arity_Int__Oint__Rings_Olinordered__semidom,arity_Int__Oint__Lazy__Sequence_Osmall__lazy,arity_Int__Oint__Lattices_Osemilattice__sup,arity_Int__Oint__Lattices_Osemilattice__inf,arity_Int__Oint__Lattices_Odistrib__lattice,arity_Int__Oint__Groups_Oab__semigroup__mult,arity_Int__Oint__Groups_Ocomm__monoid__mult,arity_Int__Oint__Groups_Oab__semigroup__add,arity_Int__Oint__Rings_Oordered__semiring,arity_Int__Oint__Rings_Oordered__ring__abs,arity_Int__Oint__Rings_Ono__zero__divisors,arity_Int__Oint__Groups_Ocomm__monoid__add,arity_Int__Oint__Rings_Olinordered__ring,arity_Int__Oint__Rings_Olinordered__idom,arity_Int__Oint__Rings_Ocomm__semiring__1,arity_Int__Oint__Groups_Osemigroup__add,arity_Int__Oint__Divides_Osemiring__div,arity_Int__Oint__Rings_Ocomm__semiring,arity_Int__Oint__Nat_Osemiring__char__0,arity_Int__Oint__Groups_Oab__group__add,arity_Int__Oint__Rings_Ozero__neq__one,arity_Int__Oint__Rings_Oordered__ring,arity_Int__Oint__Orderings_Opreorder,arity_Int__Oint__Orderings_Olinorder,arity_Int__Oint__Groups_Omonoid__mult,arity_Int__Oint__Rings_Ocomm__ring__1,arity_Int__Oint__Groups_Omonoid__add,arity_Int__Oint__Rings_Osemiring__1,arity_Int__Oint__Rings_Osemiring__0,arity_Int__Oint__Lattices_Olattice,arity_Int__Oint__Groups_Ogroup__add,arity_Int__Oint__Divides_Oring__div,arity_Int__Oint__Rings_Omult__zero,arity_Int__Oint__Rings_Ocomm__ring,arity_Int__Oint__Orderings_Oorder,arity_Int__Oint__Int_Oring__char__0,arity_Int__Oint__Int_Onumber__ring,arity_Int__Oint__Rings_Osemiring,arity_Int__Oint__Orderings_Oord,arity_Int__Oint__Groups_Ouminus,arity_Int__Oint__Groups_Osgn__if,arity_Int__Oint__Groups_Oabs__if,arity_Int__Oint__Rings_Oring__1,arity_Int__Oint__Groups_Ominus,arity_Int__Oint__Power_Opower,arity_Int__Oint__Groups_Ozero,arity_Int__Oint__Rings_Oring,arity_Int__Oint__Rings_Oidom,arity_Int__Oint__Int_Onumber,arity_Int__Oint__Groups_Oone,arity_Int__Oint__Rings_Odvd,arity_Nat__Onat__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,arity_Nat__Onat__Groups_Oordered__cancel__ab__semigroup__add,arity_Nat__Onat__Groups_Oordered__ab__semigroup__add__imp__le,arity_Nat__Onat__Rings_Olinordered__comm__semiring__strict,arity_Nat__Onat__Groups_Olinordered__ab__semigroup__add,arity_Nat__Onat__Rings_Olinordered__semiring__strict,arity_Nat__Onat__Groups_Oordered__ab__semigroup__add,arity_Nat__Onat__Groups_Oordered__comm__monoid__add,arity_Nat__Onat__Groups_Ocancel__ab__semigroup__add,arity_Nat__Onat__Rings_Oordered__cancel__semiring,arity_Nat__Onat__Rings_Oordered__comm__semiring,arity_Nat__Onat__Groups_Ocancel__semigroup__add,arity_Nat__Onat__Rings_Olinordered__semiring,arity_Nat__Onat__Rings_Olinordered__semidom,arity_Nat__Onat__Lattices_Osemilattice__sup,arity_Nat__Onat__Lattices_Osemilattice__inf,arity_Nat__Onat__Lattices_Odistrib__lattice,arity_Nat__Onat__Groups_Oab__semigroup__mult,arity_Nat__Onat__Groups_Ocomm__monoid__mult,arity_Nat__Onat__Groups_Oab__semigroup__add,arity_Nat__Onat__Rings_Oordered__semiring,arity_Nat__Onat__Rings_Ono__zero__divisors,arity_Nat__Onat__Groups_Ocomm__monoid__add,arity_Nat__Onat__Rings_Ocomm__semiring__1,arity_Nat__Onat__Groups_Osemigroup__add,arity_Nat__Onat__Divides_Osemiring__div,arity_Nat__Onat__Rings_Ocomm__semiring,arity_Nat__Onat__Orderings_Owellorder,arity_Nat__Onat__Nat_Osemiring__char__0,arity_Nat__Onat__Rings_Ozero__neq__one,arity_Nat__Onat__Orderings_Opreorder,arity_Nat__Onat__Orderings_Olinorder,arity_Nat__Onat__Groups_Omonoid__mult,arity_Nat__Onat__Groups_Omonoid__add,arity_Nat__Onat__Rings_Osemiring__1,arity_Nat__Onat__Rings_Osemiring__0,arity_Nat__Onat__Lattices_Olattice,arity_Nat__Onat__Rings_Omult__zero,arity_Nat__Onat__Orderings_Oorder,arity_Nat__Onat__Rings_Osemiring,arity_Nat__Onat__Orderings_Oord,arity_Nat__Onat__Orderings_Obot,arity_Nat__Onat__Groups_Ominus,arity_Nat__Onat__Power_Opower,arity_Nat__Onat__Groups_Ozero,arity_Nat__Onat__Int_Onumber,arity_Nat__Onat__Groups_Oone,arity_Nat__Onat__Rings_Odvd,arity_Nat__Onat__Nat_Osize,arity_HOL__Obool__Complete__Lattice_Ocomplete__lattice,arity_HOL__Obool__Lattices_Obounded__lattice__top,arity_HOL__Obool__Lattices_Obounded__lattice__bot,arity_HOL__Obool__Lattices_Osemilattice__sup,arity_HOL__Obool__Lattices_Osemilattice__inf,arity_HOL__Obool__Lattices_Odistrib__lattice,arity_HOL__Obool__Lattices_Oboolean__algebra,arity_HOL__Obool__Orderings_Opreorder,arity_HOL__Obool__Finite__Set_Ofinite,arity_HOL__Obool__Lattices_Olattice,arity_HOL__Obool__Orderings_Oorder,arity_HOL__Obool__Orderings_Otop,arity_HOL__Obool__Orderings_Oord,arity_HOL__Obool__Orderings_Obot,arity_HOL__Obool__Groups_Ouminus,arity_HOL__Obool__Groups_Ominus,arity_HOL__Obool__Enum_Oenum,arity_HOL__Obool__Nat_Osize,arity_Com__Ostate__Nat_Osize,arity_List__Olist__Lazy__Sequence_Osmall__lazy,arity_List__Olist__Nat_Osize,arity_sum__Finite__Set_Ofinite,arity_sum__Enum_Oenum,arity_sum__Nat_Osize,arity_Option__Ooption__Finite__Set_Ofinite,arity_Option__Ooption__Enum_Oenum,arity_Option__Ooption__Nat_Osize,arity_Nitpick__Opair____box__Nat_Osize,arity_prod__Lazy__Sequence_Osmall__lazy,arity_prod__Finite__Set_Ofinite,arity_prod__Enum_Oenum,arity_prod__Nat_Osize,arity_Product____Type__Ounit__Lazy__Sequence_Osmall__lazy,arity_Product____Type__Ounit__Finite__Set_Ofinite,arity_Product____Type__Ounit__Enum_Oenum,arity_Product____Type__Ounit__Nat_Osize,arity_Code____Evaluation__Oterm__Nat_Osize,arity_Hoare____Mirabelle__Otriple__Nat_Osize,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__cancel__ab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__ab__semigroup__add__imp__le,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__comm__semiring__strict,arity_Code____Numeral__Ocode____numeral__Groups_Olinordered__ab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__semiring__strict,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__ab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__comm__monoid__add,arity_Code____Numeral__Ocode____numeral__Groups_Ocancel__ab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Rings_Oordered__cancel__semiring,arity_Code____Numeral__Ocode____numeral__Rings_Oordered__comm__semiring,arity_Code____Numeral__Ocode____numeral__Groups_Ocancel__semigroup__add,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__semiring,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__semidom,arity_Code____Numeral__Ocode____numeral__Groups_Oab__semigroup__mult,arity_Code____Numeral__Ocode____numeral__Groups_Ocomm__monoid__mult,arity_Code____Numeral__Ocode____numeral__Groups_Oab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Rings_Oordered__semiring,arity_Code____Numeral__Ocode____numeral__Rings_Ono__zero__divisors,arity_Code____Numeral__Ocode____numeral__Groups_Ocomm__monoid__add,arity_Code____Numeral__Ocode____numeral__Rings_Ocomm__semiring__1,arity_Code____Numeral__Ocode____numeral__Groups_Osemigroup__add,arity_Code____Numeral__Ocode____numeral__Divides_Osemiring__div,arity_Code____Numeral__Ocode____numeral__Rings_Ocomm__semiring,arity_Code____Numeral__Ocode____numeral__Nat_Osemiring__char__0,arity_Code____Numeral__Ocode____numeral__Rings_Ozero__neq__one,arity_Code____Numeral__Ocode____numeral__Orderings_Opreorder,arity_Code____Numeral__Ocode____numeral__Orderings_Olinorder,arity_Code____Numeral__Ocode____numeral__Groups_Omonoid__mult,arity_Code____Numeral__Ocode____numeral__Groups_Omonoid__add,arity_Code____Numeral__Ocode____numeral__Rings_Osemiring__1,arity_Code____Numeral__Ocode____numeral__Rings_Osemiring__0,arity_Code____Numeral__Ocode____numeral__Rings_Omult__zero,arity_Code____Numeral__Ocode____numeral__Orderings_Oorder,arity_Code____Numeral__Ocode____numeral__Rings_Osemiring,arity_Code____Numeral__Ocode____numeral__Orderings_Oord,arity_Code____Numeral__Ocode____numeral__Groups_Ominus,arity_Code____Numeral__Ocode____numeral__Power_Opower,arity_Code____Numeral__Ocode____numeral__Groups_Ozero,arity_Code____Numeral__Ocode____numeral__Int_Onumber,arity_Code____Numeral__Ocode____numeral__Groups_Oone,arity_Code____Numeral__Ocode____numeral__Rings_Odvd,arity_Code____Numeral__Ocode____numeral__Nat_Osize,arity_Lazy____Sequence__Olazy____sequence__Nat_Osize,help_c__COMBI__1,help_c__COMBK__1,help_c__COMBB__1,help_c__COMBC__1,help_c__COMBS__1,help_c__fequal__1,help_c__fequal__2,help_c__fFalse__1,help_c__fTrue__1,help_c__fNot__1,help_c__fNot__2,help_c__fconj__1,help_c__fconj__2,help_c__fconj__3,help_c__fdisj__1,help_c__fdisj__2,help_c__fdisj__3,help_c__fimplies__1,help_c__fimplies__2,help_c__fimplies__3,conj_0,conj_1,conj_2,conj_3,conj_4] % 72.02/69.92 =============================================================== % 72.02/69.92 % 72.02/69.92 Combined formula: 5232 axiom(s) => conjecture % 72.02/69.92 % 72.02/69.92 % Equality/functions detected -> nanoCoP oracle mode % 72.02/69.92 nanoCoP : % 72.02/69.92 % 20,474,362 inferences, 59.958 CPU in 59.964 seconds (100% CPU, 341477 Lips) % 72.02/69.92 % 72.02/69.92 % nanoCoP proof (equality/functions) % 72.02/69.92 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 72.02/69.92 % 72.02/69.92 % SZS output end Proof %------------------------------------------------------------------------------