%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW317+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n012.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:43 PM UTC 2026 % Result : Theorem 79.07s 78.73s % Output : Proof 79.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SWW317+1 : TPTP v9.2.1. Released v5.2.0. % 0.00/0.06 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.06/0.24 % Computer : n012.cluster.edu % 0.06/0.24 % Model : x86_64 x86_64 % 0.06/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.24 % Memory : 8042.1875MB % 0.06/0.24 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.24 % CPULimit : 300 % 0.06/0.24 % WCLimit : 300 % 0.06/0.24 % DateTime : Mon May 11 14:28:01 EDT 2026 % 0.06/0.24 % CPUTime : % 79.07/78.73 % SZS status Theorem % 79.07/78.73 % SZS output start Proof % 79.07/78.73 % 79.07/78.73 =============================================================== % 79.07/78.73 TPTP Problem: conj_1 (conjecture with 5241 axiom(s)) % 79.07/78.73 Axioms: [fact_ext,fact_empty,fact_hoare__derivs_OSkip,fact_hoare__derivs_Oequations_I1_J,fact_hoare__derivs_Oequations_I7_J,fact_triple_Oinject,fact_asm,fact_weaken,fact_cut,fact_hoare__derivs_Oinsert,fact_empty__subsetI,fact_subset__singletonD,fact_equalityI,fact_order__refl,fact_bot__fun__def,fact_triple_Orecs,fact_triple_Osimps_I2_J,fact_subset__insertI,fact_subset__insertI2,fact_insert__mono,fact_subset__empty,fact_empty__not__insert,fact_linorder__le__cases,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_order__antisym__conv,fact_order__eq__refl,fact_order__eq__iff,fact_linorder__linear,fact_insert__code,fact_insert__commute,fact_insert__absorb2,fact_equalityE,fact_subset__trans,fact_equalityD2,fact_equalityD1,fact_set__eq__subset,fact_subset__refl,fact_bot__least,fact_le__funE,fact_le__funD,fact_le__fun__def,fact_bot__apply,fact_singleton__inject,fact_doubleton__eq__iff,fact_insert__not__empty,fact_the__elem__eq,fact_escape,fact_conseq1,fact_conseq2,fact_Comp,fact_LoopF,fact_predicate1D,fact_rev__predicate1D,fact_conseq12,fact_hoare__derivs_Oequations_I8_J,fact_Ass,fact_order__fun_I1_J,fact_all__code,fact_enum__all,fact_com_Osimps_I12_J,fact_com_Osimps_I13_J,fact_com_Osimps_I8_J,fact_com_Osimps_I9_J,fact_com_Osimps_I25_J,fact_com_Osimps_I24_J,fact_com_Osimps_I16_J,fact_com_Osimps_I17_J,fact_com_Osimps_I47_J,fact_com_Osimps_I46_J,fact_com_Osimps_I29_J,fact_com_Osimps_I28_J,fact_com_Osimps_I5_J,fact_com_Osimps_I1_J,fact_com_Osimps_I3_J,fact_the__elem__def,fact_Loop,fact_Powp__mono,fact_Least__le,fact_le__funI,fact_inv__imagep__def,fact_com_Osimps_I64_J,fact_com_Osimps_I67_J,fact_com_Osimps_I65_J,fact_strict__mono__less__eq,fact_com_Osimps_I69_J,fact_hoare__derivs_OLocal,fact_vname_Osimps_I2_J,fact_com_Osimps_I2_J,fact_com_Osimps_I66_J,fact_LeastI__ex,fact_strict__mono__eq,fact_LeastI,fact_in__inv__imagep,fact_peek__and__def,fact_com_Osimps_I38_J,fact_com_Osimps_I39_J,fact_com_Osimps_I23_J,fact_com_Osimps_I22_J,fact_com_Osimps_I34_J,fact_com_Osimps_I35_J,fact_com_Osimps_I10_J,fact_com_Osimps_I11_J,fact_hoare__derivs_OIf,fact_enum__the__def,fact_the__eq__trivial,fact_the__sym__eq__trivial,fact_vname_Orecs_I2_J,fact_vname_Osimps_I6_J,fact_K__record__comp,fact_o__def,fact_evalc_OLocal,fact_evaln_OLocal,fact_o__eq__elim,fact_evaln_OWhileFalse,fact_evaln_OWhileTrue,fact_evalc_OWhileFalse,fact_evalc_OWhileTrue,fact_evaln_OIfFalse,fact_evaln_OIfTrue,fact_evaln__elim__cases_I5_J,fact_evalc_OIfFalse,fact_evalc_OIfTrue,fact_evalc__elim__cases_I5_J,fact_evaln_OSemi,fact_evaln__elim__cases_I1_J,fact_evaln_OSkip,fact_evalc_OSemi,fact_evalc__elim__cases_I1_J,fact_evalc_OSkip,fact_evaln_OAssign,fact_evaln__elim__cases_I2_J,fact_evalc_OAssign,fact_evalc__elim__cases_I2_J,fact_evaln__nonstrict,fact_eval__eq,fact_evalc_Oequations_I5_J,fact_evalc_Oequations_I6_J,fact_evaln_Oequations_I5_J,fact_evaln_Oequations_I6_J,fact_com__det,fact_evaln__evalc,fact_com_Osimps_I4_J,fact_evaln_Oequations_I7_J,fact_evaln_Oequations_I8_J,fact_evalc_Oequations_I7_J,fact_evalc_Oequations_I8_J,fact_evaln_Oequations_I4_J,fact_evaln_Oequations_I1_J,fact_evalc_Oequations_I4_J,fact_evalc_Oequations_I1_J,fact_com_Osimps_I53_J,fact_com_Osimps_I52_J,fact_evaln_Oequations_I2_J,fact_com_Osimps_I26_J,fact_com_Osimps_I27_J,fact_com_Osimps_I44_J,fact_com_Osimps_I45_J,fact_com_Osimps_I36_J,fact_com_Osimps_I37_J,fact_com_Osimps_I15_J,fact_com_Osimps_I14_J,fact_evalc_Oequations_I2_J,fact_com_Osimps_I68_J,fact_evaln_Oequations_I3_J,fact_evalc_Oequations_I3_J,fact_o__assoc,fact_o__apply,fact_o__eq__dest__lhs,fact_o__eq__dest,fact_MGT__def,fact_evalc__elim__cases_I3_J,fact_evaln__elim__cases_I3_J,fact_vname_Osimps_I5_J,fact_vname_Orecs_I1_J,fact_triple__valid__def2,fact_evalc__elim__cases_I4_J,fact_evaln__elim__cases_I4_J,fact_comp__cong,fact_override__on__emptyset,fact_evalc__WHILE__case,fact_vname_Osimps_I1_J,fact_vname_Osimps_I3_J,fact_vname_Osimps_I4_J,fact_le__refl,fact_nat__le__linear,fact_eq__imp__le,fact_le__trans,fact_le__antisym,fact_evaln__WHILE__case,fact_Least__equality,fact_evalc__evaln,fact_Pow__mono,fact_the__equality,fact_singleton__conv2,fact_Collect__def,fact_Pow__not__empty,fact_Pow__def,fact_Collect__empty__eq,fact_empty__Collect__eq,fact_Pow__empty,fact_empty__def,fact_insert__Collect,fact_Collect__conv__if,fact_Collect__conv__if2,fact_singleton__conv,fact_PowI,fact_Collect__mono,fact_insert__compr__raw,fact_insert__compr,fact_insert__def,fact_Pow__iff,fact_PowD,fact_Pow__bottom,fact_image__constant__conv,fact_strict__mono__mono,fact_subset__insert,fact_equalityCE,fact_sup1E,fact_sup1CI,fact_emptyE,fact_insertE,fact_insertCI,fact_subsetD,fact_image__eqI,fact_UnE,fact_UnCI,fact_CollectI,fact_Un__absorb,fact_mem__def,fact_Un__commute,fact_Un__left__absorb,fact_image__iff,fact_Un__left__commute,fact_image__Un,fact_Un__iff,fact_Un__assoc,fact_bex__Un,fact_ball__Un,fact_UnI1,fact_UnI2,fact_imageI,fact_eqset__imp__iff,fact_eqelem__imp__iff,fact_eq__mem__trans,fact_rev__image__eqI,fact_eq__mem,fact_sup__Un__eq,fact_sup1I1,fact_sup1I2,fact_insert__image,fact_image__image,fact_image__ident,fact_image__Pow__surj,fact_mono__Un,fact_pred__equals__eq,fact_Un__def,fact_Least__mono,fact_Pow__insert,fact_empty__is__image,fact_image__empty,fact_image__is__empty,fact_image__insert,fact_subset__image__iff,fact_image__mono,fact_image__compose,fact_image__constant,fact_Un__empty__left,fact_Un__empty__right,fact_Un__empty,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_all__not__in__conv,fact_ex__in__conv,fact_empty__iff,fact_equals0D,fact_insertI1,fact_insert__iff,fact_insert__ident,fact_insertI2,fact_insert__absorb,fact_in__mono,fact_set__rev__mp,fact_set__mp,fact_Un__Pow__subset,fact_Cantors__paradox,fact_Pow__top,fact_Collect__disj__eq,fact_monoD,fact_bot__empty__eq,fact_image__Pow__mono,fact_Collect__mem__eq,fact_mem__Collect__eq,fact_CollectD,fact_CollectE,fact_pred__subset__eq,fact_Powp__Pow__eq,fact_override__on__apply__notin,fact_override__on__apply__in,fact_insert__is__Un,fact_override__on__def,fact_singleton__iff,fact_singletonE,fact_insert__subset,fact_mono__sup,fact_sup__fun__def,fact_sup__apply,fact_sup__bot__left,fact_sup__bot__right,fact_sup__eq__bot__iff,fact_inf__sup__ord_I3_J,fact_sup__ge1,fact_inf__sup__ord_I4_J,fact_sup__ge2,fact_le__iff__sup,fact_sup_Oidem,fact_sup__idem,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_le__supE,fact_sup__mono,fact_sup__least,fact_le__supI,fact_sup__absorb1,fact_sup__absorb2,fact_le__supI2,fact_le__supI1,fact_le__sup__iff,fact_coinduct3__mono__lemma,fact_the__inv__into__def,fact_diff__single__insert,fact_subset__insert__iff,fact_imageE,fact_image__subsetI,fact_coinduct__set,fact_def__coinduct__set,fact_if__image__distrib,fact_Sup__fin_Oidem,fact_inf1I,fact_inf1E,fact_IntI,fact_IntE,fact_DiffI,fact_DiffE,fact_inf_Oidem,fact_inf__idem,fact_fun__diff__def,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_minus__apply,fact_inf__apply,fact_Diff__disjoint,fact_Diff__triv,fact_Int__absorb,fact_Int__commute,fact_Int__left__absorb,fact_Int__left__commute,fact_Diff__Int__distrib,fact_Diff__idemp,fact_Int__Diff,fact_Int__assoc,fact_Diff__Int__distrib2,fact_Diff__Int2,fact_Inf__fin_Oidem,fact_inf1D1,fact_inf1D2,fact_Diff__Int,fact_Diff__Un,fact_Un__Diff__Int,fact_Pow__Int__eq,fact_gfp__upperbound,fact_def__gfp__unfold,fact_gfp__unfold,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_inf__bot__left,fact_inf__bot__right,fact_sup__inf__distrib2,fact_inf__sup__distrib2,fact_sup__inf__distrib1,fact_inf__sup__distrib1,fact_sup__inf__absorb,fact_inf__sup__absorb,fact_Diff__iff,fact_DiffD1,fact_DiffD2,fact_Int__iff,fact_IntD1,fact_IntD2,fact_empty__Diff,fact_Diff__empty,fact_Diff__cancel,fact_Int__empty__left,fact_Int__empty__right,fact_disjoint__iff__not__equal,fact_Diff__subset,fact_Diff__mono,fact_double__diff,fact_insert__inter__insert,fact_Un__Diff__cancel,fact_Un__Diff__cancel2,fact_Un__Diff,fact_Int__lower1,fact_Int__lower2,fact_Int__absorb2,fact_Int__absorb1,fact_Int__greatest,fact_Int__mono,fact_Int__Un__distrib,fact_Un__Int__distrib,fact_Int__Un__distrib2,fact_Un__Int__distrib2,fact_Un__Int__crazy,fact_inf__Int__eq,fact_weak__coinduct,fact_Collect__conj__eq,fact_gfp__lemma3,fact_gfp__lemma2,fact_distrib__inf__le,fact_distrib__sup__le,fact_insert__Diff1,fact_insert__Diff__if,fact_Diff__insert,fact_Diff__insert2,fact_insert__Diff__single,fact_Int__insert__left__if1,fact_Int__insert__right__if1,fact_Int__insert__left__if0,fact_Int__insert__right__if0,fact_Int__insert__left,fact_Int__insert__right,fact_image__diff__subset,fact_mono__inf,fact_Diff__partition,fact_Diff__subset__conv,fact_image__Int__subset,fact_Un__Int__assoc__eq,fact_weak__coinduct__image,fact_set__diff__eq,fact_mono__Int,fact_Int__def,fact_Int__Collect,fact_gfp__fun__UnI2,fact_def__coinduct,fact_coinduct__lemma,fact_coinduct,fact_Diff__insert__absorb,fact_insert__Diff,fact_flat__lub__def,fact_def__coinduct3,fact_coinduct3,fact_def__Collect__coinduct,fact_diff__eq__diff__less__eq,fact_fun__upd__image,fact_coinduct3__lemma,fact_psubset__insert__iff,fact_Int__Collect__mono,fact_fold__graph_H_Ointros_I2_J,fact_fun__upd__triv,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_psubset__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_fun__upd__idem,fact_fun__upd__other,fact_fun__upd__twist,fact_fun__upd__apply,fact_fun__upd__same,fact_fun__upd__upd,fact_fun__upd__idem__iff,fact_diff__eq__diff__less,fact_fun__upd__def,fact_lfp__const,fact_fold__graph_H_Ointros_I1_J,fact_fold__graph_H_Oequations_I1_J,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_le__diff__iff,fact_Nat_Odiff__diff__eq,fact_eq__diff__iff,fact_diff__diff__cancel,fact_diff__le__mono,fact_diff__le__mono2,fact_diff__le__self,fact_not__psubset__empty,fact_less__supI1,fact_less__supI2,fact_less__infI2,fact_less__infI1,fact_subset__psubset__trans,fact_psubset__subset__trans,fact_psubset__imp__subset,fact_subset__iff__psubset__eq,fact_psubset__eq,fact_fun__upd__comp,fact_strict__monoD,fact_strict__mono__less,fact_lfp__lowerbound,fact_not__less__Least,fact_lfp__unfold,fact_def__lfp__unfold,fact_lfp__lemma3,fact_lfp__lemma2,fact_diff__eq__diff__eq,fact_lfp__induct,fact_def__lfp__induct,fact_def__lfp__induct__set,fact_lfp__induct__set,fact_fold__graph_H_Oequations_I2_J,fact_order__fun_I2_J,fact_inj__on__Un,fact_inj__on__insert,fact_mk__less__def,fact_dom__override__on,fact_psubset__imp__ex__mem,fact_inj__on__empty,fact_diff__commute,fact_less__imp__diff__less,fact_diff__less__mono2,fact_inj__on__id2,fact_inj__on__def,fact_exists__code,fact_enum__ex,fact_inj__on__contraD,fact_inj__on__iff,fact_inj__onD,fact_subset__inj__on,fact_inj__on__Int,fact_inj__on__imageI2,fact_inj__on__diff,fact_termination__basic__simps_I5_J,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_less__diff__iff,fact_diff__less__mono,fact_strict__mono__imp__inj__on,fact_inj__on__Un__image__eq__iff,fact_comp__inj__on__iff,fact_comp__inj__on,fact_inj__on__imageI,fact_inj__on__strict__subset,fact_the__inv__into__f__f,fact_the__inv__into__f__eq,fact_inj__on__the__inv__into,fact_the__inv__into__onto,fact_dom__if,fact_inj__on__image__Int,fact_inj__on__image__set__diff,fact_inj__on__fun__updI,fact_f__the__inv__into__f,fact_the__inv__into__into,fact_the__inv__into__comp,fact_inj__on__iff__surj,fact_restrict__fun__upd,fact_fun__upd__restrict__conv,fact_setsum__diff1__nat,fact_dom__fun__upd,fact_fun__upd__restrict,fact_quotient__diff1,fact_map__add__comm,fact_fun__left__comm__idem__remove,fact_empty__upd__none,fact_nat__less__cases,fact_less__not__refl3,fact_less__not__refl2,fact_less__irrefl__nat,fact_linorder__neqE__nat,fact_nat__neq__iff,fact_less__not__refl,fact_map__add__None,fact_restrict__map__empty,fact_empty__map__add,fact_map__add__assoc,fact_map__add__empty,fact_restrict__out,fact_setsum__commute,fact_fun__left__comm__idem_Ofun__left__comm__idem__apply,fact_fun__left__comm__idem_Ofun__left__idem,fact_restrict__map__def,fact_restrict__map__to__empty,fact_fun__left__comm__idem__insert,fact_fun__left__comm__idem__sup,fact_fun__left__comm__idem__inf,fact_fun__left__comm__idem_Ofun__comp__idem,fact_setsum__subtractf,fact_restrict__in,fact_restrict__map__insert,fact_restrict__restrict,fact_inj__on__map__add__dom,fact_quotient__is__empty,fact_quotient__is__empty2,fact_quotient__empty,fact_fun__upd__None__restrict,fact_domIff,fact_map__add__dom__app__simps_I1_J,fact_map__add__dom__app__simps_I3_J,fact_map__add__dom__app__simps_I2_J,fact_dom__eq__empty__conv,fact_dom__empty,fact_dom__def,fact_dom__map__add,fact_dom__restrict,fact_setsum__reindex,fact_dom__minus,fact_setsum__diff1,fact_setsum__diff1__ring,fact_singleton__quotient,fact_quotientI,fact_dom__eq__singleton__conv,fact_restrict__complement__singleton__eq,fact_ran__empty,fact_quotient__disj,fact_setsum__reindex__cong,fact_finite__Collect__less__nat,fact_finite__Collect__le__nat,fact_finite_OemptyI,fact_finite_OinsertI,fact_finite__imageI,fact_finite__Int,fact_finite__Diff,fact_inj__uminus,fact_ComplI,fact_finite__Collect__conjI,fact_finite__Collect__subsets,fact_finite,fact_finite__code,fact_minus__minus,fact_equation__minus__iff,fact_minus__equation__iff,fact_neg__equal__iff__equal,fact_fun__Compl__def,fact_double__compl,fact_uminus__apply,fact_compl__eq__compl__iff,fact_double__complement,fact_Compl__eq__Compl__iff,fact_finite__Pow__iff,fact_ranI,fact_compl__le__compl__iff,fact_compl__mono,fact_le__minus__iff,fact_minus__le__iff,fact_neg__le__iff__le,fact_le__imp__neg__le,fact_neg__less__iff__less,fact_minus__less__iff,fact_less__minus__iff,fact_Compl__iff,fact_ComplD,fact_ComplE,fact_minus__diff__eq,fact_Compl__subset__Compl__iff,fact_Compl__anti__mono,fact_map__upd__eqD1,fact_map__upd__triv,fact_map__upd__Some__unfold,fact_map__add__find__right,fact_finite_Oequations_I1_J,fact_finite__insert,fact_rev__finite__subset,fact_finite__subset,fact_finite__UnI,fact_finite__Un,fact_finite__Diff2,fact_setsum__negf,fact_Collect__neg__eq,fact_equiv__class__self,fact_nat__seg__image__imp__finite,fact_finite__Collect__disjI,fact_restrict__upd__same,fact_ran__map__upd,fact_inf__compl__bot,fact_compl__inf__bot,fact_diff__eq,fact_compl__sup,fact_compl__inf,fact_domI,fact_image__map__upd,fact_subset__Compl__self__eq,fact_Compl__disjoint,fact_Compl__disjoint2,fact_insert__dom,fact_Compl__Int,fact_Compl__Un,fact_Compl__Diff__eq,fact_Diff__eq,fact_Diff__Compl,fact_map__add__Some__iff,fact_map__add__SomeD,fact_map__add__upd,fact_finite__surj,fact_finite__Diff__insert,fact_finite__imageD,fact_Compl__eq,fact_Collect__imp__eq,fact_map__upd__nonempty,fact_enum__ex__option__def,fact_enum__all__option__def,fact_disjoint__eq__subset__Compl,fact_endo__inj__surj,fact_finite__surj__inj,fact_map__add__upd__left,fact_setsum__diff,fact_setsum_Oreindex,fact_setsum__diff__nat,fact_setsum__image__gen,fact_setsum__setsum__restrict,fact_Image__Int__subset,fact_inj__Some,fact_folding_Oremove,fact_folding__one_Oremove,fact_folding__image__simple_Oremove,fact_folding__image_Oreindex,fact_quotientE,fact_folding_Ocommute__comps_I1_J,fact_folding_Ocommute__comp,fact_folding_Ocommute__left__comp,fact_folding__image__simple_Oempty,fact_folding__image_Odistrib,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_finite__nat__set__iff__bounded,fact_finite__nat__set__iff__bounded__le,fact_option_Oinject,fact_folding__one_Osingleton,fact_finite__M__bounded__by__nat,fact_folding__image__simple_Oinsert,fact_folding__image__simple_Ounion__inter,fact_folding_Oinsert,fact_folding_Ounion__inter,fact_folding__one_Oinsert,fact_Image__empty,fact_folding__image__simple_Oinsert__remove,fact_folding__one_Oinsert__remove,fact_folding__image__simple_Ounion__disjoint,fact_folding__one_Ounion__disjoint,fact_folding__one_Ounion__inter,fact_Image__mono,fact_Image__Un,fact_Un__Image,fact_not__None__eq,fact_not__Some__eq,fact_option_Osimps_I3_J,fact_option_Osimps_I2_J,fact_folding_Oinsert__remove,fact_folding_Ounion,fact_Option_Oset_Osimps_I2_J,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_less__by__empty,fact_elem__set,fact_Option_Oset_Osimps_I1_J,fact_set__empty__eq,fact_ord_OgreaterThanAtMost__iff,fact_Inf__fin_Oremove,fact_Sup__fin_Oremove,fact_folding__idem_Ounion__idem,fact_folding__idem_Osubset__comp__idem,fact_folding__idem_Oinsert__idem,fact_folding__one_Oclosed,fact_folding__idem_Oin__comp__idem,fact_Inf__le__Sup,fact_Sup__fin_Osingleton,fact_Inf__fin_Osingleton,fact_folding__idem_Oidem__comp,fact_folding__idem_Oidem__left__comp,fact_sup__Inf__absorb,fact_Sup__fin_Oin__idem,fact_Inf__fin_Oin__idem,fact_inf__Sup__absorb,fact_Sup__fin_Oinsert__idem,fact_Inf__fin_Oinsert__idem,fact_Sup__fin_Osubset__idem,fact_Inf__fin_Osubset__idem,fact_Sup__fin_Ounion__idem,fact_Inf__fin_Ounion__idem,fact_Sup__fin_Oinsert,fact_Inf__fin_Oinsert,fact_Sup__fin_Oinsert__remove,fact_Inf__fin_Oinsert__remove,fact_Sup__fin_Ounion__disjoint,fact_Sup__fin_Ounion__inter,fact_Inf__fin_Ounion__disjoint,fact_Inf__fin_Ounion__inter,fact_Inf__fin_Oclosed,fact_Sup__fin_Oclosed,fact_inf__Sup1__distrib,fact_inf__Sup2__distrib,fact_sup__Inf1__distrib,fact_sup__Inf2__distrib,fact_quotient__def,fact_Inf__fin_Ohom__commute,fact_SUP1__I,fact_SUP1__iff,fact_finite__UN,fact_UN__o,fact_Image__UN,fact_finite__Collect__bounded__ex,fact_finite__image__set,fact_Image__eq__UN,fact_ran__def,fact_Pow__Compl,fact_UN__I,fact_UN__Pow__subset,fact_image__eq__UN,fact_UN__equiv__class,fact_UN__equiv__class2,fact_UN__insert,fact_UN__extend__simps_I2_J,fact_UN__extend__simps_I3_J,fact_congruent2__implies__congruent,fact_ball__UN,fact_SUP__commute,fact_UN__extend__simps_I9_J,fact_UN__simps_I9_J,fact_UN__UN__flatten,fact_congruent2__implies__congruent__UN,fact_SUP__le__iff,fact_less__SUP__iff,fact_UN__iff,fact_SUP__const,fact_UNION__empty__conv_I2_J,fact_UN__constant,fact_UN__empty2,fact_UNION__empty__conv_I1_J,fact_UN__subset__iff,fact_UN__extend__simps_I10_J,fact_image__UN,fact_UN__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_SUPR__apply,fact_UN__simps_I6_J,fact_UN__extend__simps_I6_J,fact_SUP__subset,fact_le__SUPI,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_UN__simps_I3_J,fact_UN__simps_I2_J,fact_UN__equiv__class__type2,fact_UN__equiv__class__type,fact_Sup__fin_Ohom__commute,fact_equiv__class__nondisjoint,fact_subset__equiv__class,fact_finite__empty__induct,fact_folding__one__idem_Ounion__idem,fact_finite__subset__induct,fact_SUP2__I,fact_folding__one__idem_Oidem,fact_inf__Int__eq2,fact_pred__equals__eq2,fact_congruent2D,fact_congruentD,fact_pred__subset__eq2,fact_bot__empty__eq2,fact_sup__Un__eq2,fact_enum__ex__prod__def,fact_enum__all__prod__def,fact_Image__iff,fact_rev__ImageI,fact_Image__singleton__iff,fact_folding__one__idem_Oin__idem,fact_equiv__class__eq,fact_quotient__eq__iff,fact_quotient__eqI,fact_Image__singleton,fact_equiv__class__eq__iff,fact_eq__equiv__class__iff,fact_eq__equiv__class,fact_equiv__class__subset,fact_eq__equiv__class__iff2,fact_folding__one__idem_Oinsert__idem,fact_folding__one__idem_Osubset__idem,fact_in__rel__def,fact_Nitpick_Orefl_H__def,fact_UN__equiv__class__inject,fact_irrefl__def,fact_ImageE,fact_Field__insert,fact_setsum__strict__mono,fact_finite__conv__nat__seg__image,fact_sup2E,fact_sup2CI,fact_inf2E,fact_inf2I,fact_bot2E,fact_SUP2__iff,fact_sup2I1,fact_sup2I2,fact_rev__predicate2D,fact_predicate2D,fact_inf2D2,fact_inf2D1,fact_finite__Field,fact_Field__empty,fact_mono__Field,fact_Field__Un,fact_setsum__diff1_H,fact_setsum_Oremove,fact_ran__restrictD,fact_map__add__def,fact_image__eq__fold__image,fact_compl__unique,fact_card__Diff2__less,fact_card__Diff1__less,fact_UNIV__I,fact_finite__option__UNIV,fact_finite__Plus__UNIV__iff,fact_finite__Prod__UNIV,fact_card__eq__UNIV__imp__eq__UNIV,fact_Pow__UNIV,fact_ab__semigroup__add__class_Oadd__ac_I1_J,fact_add__left__cancel,fact_add__right__cancel,fact_add__left__imp__eq,fact_add__imp__eq,fact_add__right__imp__eq,fact_top__apply,fact_add__le__cancel__right,fact_add__le__cancel__left,fact_add__right__mono,fact_add__left__mono,fact_add__mono,fact_add__le__imp__le__right,fact_add__le__imp__le__left,fact_add__less__imp__less__left,fact_add__less__imp__less__right,fact_add__strict__mono,fact_add__strict__left__mono,fact_add__strict__right__mono,fact_add__less__cancel__left,fact_add__less__cancel__right,fact_add__diff__cancel,fact_diff__add__cancel,fact_minus__add__distrib,fact_minus__add,fact_add__minus__cancel,fact_minus__add__cancel,fact_iso__tuple__UNIV__I,fact_finite__fun__UNIVD2,fact_not__add__less1,fact_not__add__less2,fact_nat__add__left__cancel__less,fact_trans__less__add1,fact_trans__less__add2,fact_add__less__mono1,fact_add__less__mono,fact_less__add__eq__less,fact_add__lessD1,fact_termination__basic__simps_I1_J,fact_termination__basic__simps_I2_J,fact_UNIV__not__empty,fact_finite__UNIV,fact_termination__basic__simps_I3_J,fact_termination__basic__simps_I4_J,fact_le__add2,fact_le__add1,fact_le__iff__add,fact_nat__add__left__cancel__le,fact_trans__le__add1,fact_trans__le__add2,fact_add__le__mono1,fact_add__le__mono,fact_add__leD2,fact_add__leD1,fact_add__leE,fact_subset__UNIV,fact_diff__add__inverse2,fact_diff__add__inverse,fact_diff__diff__left,fact_diff__cancel,fact_diff__cancel2,fact_Un__UNIV__left,fact_Un__UNIV__right,fact_Int__UNIV__left,fact_Int__UNIV__right,fact_inj__eq,fact_injD,fact_fold__image__empty,fact_card_Ounion__inter,fact_card__Un__Int,fact_infinite__UNIV__nat,fact_setsum__addf,fact_UNIV__def,fact_range__composition,fact_top__greatest,fact_sup__top__right,fact_sup__top__left,fact_inf__top__left,fact_inf__top__right,fact_inf__eq__top__iff,fact_UNIV__option__conv,fact_card__Un__disjoint,fact_add__le__less__mono,fact_add__less__le__mono,fact_card__image,fact_diff__minus__eq__add,fact_ab__diff__minus,fact_diff__def,fact_rangeI,fact_range__eqI,fact_less__diff__conv,fact_add__diff__inverse,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_le__add__diff,fact_le__diff__conv,fact_diff__diff__right,fact_Diff__UNIV,fact_comp__surj,fact_inj__image__eq__iff,fact_inj__comp,fact_Compl__empty__eq,fact_Compl__UNIV__eq,fact_finite__compl,fact_Compl__partition2,fact_Compl__partition,fact_Compl__eq__Diff__UNIV,fact_setsum_Odistrib,fact_finite__Collect__not,fact_SUP__UN__eq,fact_finite__range__imageI,fact_the__inv__f__f,fact_folding__image__simple_Oeq__fold__g,fact_folding__image_Oeq__fold,fact_dom__const,fact_card__insert__le,fact_card__mono,fact_card__seteq,fact_card__image__le,fact_eq__card__imp__inj__on,fact_inj__on__iff__eq__card,fact_pigeonhole,fact_inj__fun,fact_card__quotient__disjoint,fact_psubset__card__mono,fact_compl__bot__eq,fact_compl__top__eq,fact_compl__sup__top,fact_sup__compl__top,fact_range__ex1__eq,fact_inj__image__mem__iff,fact_finite__UNIV__surj__inj,fact_finite__UNIV__inj__surj,fact_inj__image__subset__iff,fact_image__Int,fact_image__set__diff,fact_surj__Compl__image__subset,fact_card__bij__eq,fact_card__Diff__subset,fact_finite__range__updI,fact_card__Diff__subset__Int,fact_diff__card__le__card__Diff,fact_inj__singleton,fact_setsum_Oinsert,fact_setsum__insert,fact_card__psubset,fact_setsum__Un__Int,fact_SUP__UN__eq2,fact_inj__image__Compl__subset,fact_card__Diff1__le,fact_card__inj__on__le,fact_inj__on__iff__card__le,fact_setsum_Oinsert__remove,fact_setsum__Un__disjoint,fact_setsum__Un,fact_option_Osimps_I4_J,fact_option_Osimps_I5_J,fact_setsum__Un__nat,fact_setsum__cases,fact_comm__ring__1__class_Onormalizing__ring__rules_I2_J,fact_comm__monoid__big_OF__eq,fact_card__Diff__singleton,fact_card__Diff__singleton__if,fact_add__Min__commute,fact_add__Max__commute,fact_setsum__multicount__gen,fact_,fact_top1I,fact_card__UNIV__unit,fact_nat__add__commute,fact_nat__add__left__commute,fact_nat__add__assoc,fact_nat__add__left__cancel,fact_nat__add__right__cancel,fact_inj__on__add__nat,fact_one__reorient,fact_minus__Max__eq__Min,fact_minus__Min__eq__Max,fact_Min_Osingleton,fact_Max_Osingleton,fact_card__eq__setsum,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,fact_Max__ge,fact_Min__le,fact_Min__in,fact_Max__in,fact_card_Oinsert,fact_Min__antimono,fact_Max__mono,fact_comm__monoid__big_Oinfinite,fact_card_Oinsert__remove,fact_card_Oremove,fact_card__Diff__insert,fact_less__add__one,fact_Id__on__def,fact_equivp__equiv,fact_inj__vimage__singleton,fact_fold__Un__disjoint,fact_map__comp__def,fact_card__Suc__Diff1,fact_lessI,fact_Suc__mono,fact_vimageI,fact_mult__Suc__right,fact_mult__Suc,fact_combine__common__factor,fact_comm__semiring__class_Odistrib,fact_inj__Suc,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,fact_Suc__mult__le__cancel1,fact_square__eq__iff,fact_minus__mult__minus,fact_minus__mult__commute,fact_minus__mult__left,fact_minus__mult__right,fact_Suc__mult__less__cancel1,fact_identity__equivp,fact_equivp__def,fact_equivp__reflp,fact_equivp__symp,fact_equivp__transp,fact_ab__semigroup__mult__class_Omult__ac_I1_J,fact_vimage__ident,fact_times_Oidem,fact_mult__idem,fact_mult__left__idem,fact_n__not__Suc__n,fact_Suc__n__not__n,fact_nat_Oinject,fact_Suc__mult__cancel1,fact_Suc__inject,fact_vimage__code,fact_mono__Suc,fact_vimage__eq,fact_vimageD,fact_vimageI2,fact_mono__iff__le__Suc,fact_vimage__empty,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J,fact_crossproduct__noteq,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I8_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J,fact_crossproduct__eq,fact_vimage__mono,fact_vimage__UNIV,fact_vimage__Un,fact_vimage__Int,fact_vimage__compose,fact_not__less__eq,fact_less__Suc__eq,fact_Suc__less__eq,fact_not__less__less__Suc__eq,fact_less__antisym,fact_less__SucI,fact_Suc__lessI,fact_less__trans__Suc,fact_less__SucE,fact_Suc__lessD,fact_Suc__less__SucD,fact_mult__1__left,fact_mult__1,fact_mult__1__right,fact_mult_Ocomm__neutral,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J,fact_add__Suc__shift,fact_add__Suc,fact_add__Suc__right,fact_vimage__Diff,fact_Suc__n__not__le__n,fact_not__less__eq__eq,fact_le__Suc__eq,fact_Suc__le__mono,fact_le__SucI,fact_le__SucE,fact_Suc__leD,fact_diff__Suc__Suc,fact_Suc__diff__diff,fact_add__mult__distrib,fact_add__mult__distrib2,fact_le__square,fact_le__cube,fact_mult__le__mono1,fact_mult__le__mono2,fact_mult__le__mono,fact_diff__mult__distrib2,fact_diff__mult__distrib,fact_vimage__Compl,fact_nat__mult__1,fact_nat__1__eq__mult__iff,fact_nat__mult__1__right,fact_nat__mult__eq__1__iff,fact_evaln__Suc,fact_less__1__mult,fact_eq__add__iff1,fact_eq__add__iff2,fact_square__eq__1__iff,fact_fun__left__comm__idem,fact_vimage__Collect__eq,fact_triple__valid__Suc,fact_vimage__UN,fact_setsum__right__distrib,fact_setsum__left__distrib,fact_setsum__product,fact_le__add__iff2,fact_le__add__iff1,fact_less__add__iff1,fact_less__add__iff2,fact_image__vimage__subset,fact_surj__image__vimage__eq,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J,fact_less__iff__Suc__add,fact_less__add__Suc2,fact_less__add__Suc1,fact_comm__ring__1__class_Onormalizing__ring__rules_I1_J,fact_less__eq__Suc__le,fact_less__Suc__eq__le,fact_Suc__le__eq,fact_le__imp__less__Suc,fact_Suc__leI,fact_le__less__Suc__eq,fact_Suc__le__lessD,fact_diff__less__Suc,fact_Suc__diff__le,fact_diff__Suc__1,fact_vimage__def,fact_less__eq__Suc__le__raw,fact_map__comp__simps_I1_J,fact_map__comp__Some__iff,fact_map__comp__simps_I2_J,fact_vimage__singleton__eq,fact_vimage__insert,fact_finite__vimageD,fact_vimage__subsetD,fact_image__vimage__eq,fact_finite__vimageI,fact_inj__vimage__image__eq,fact_diff__Suc__diff__eq1,fact_diff__Suc__diff__eq2,fact_linorder__neqE__linordered__idom,fact_map__comp__empty_I1_J,fact_map__comp__empty_I2_J,fact_Id__on__empty,fact_vimage__const,fact_Image__Id__on,fact_vimage__eq__UN,fact_fold__image__distrib,fact_card__insert__if,fact_card__insert__disjoint,fact_vimage__subsetI,fact_fold__image__insert,fact_vimage__if,fact_Id__on__eqI,fact_Id__on__iff,fact_map__comp__None__iff,fact_card__insert,fact_fold__image__Un__Int,fact_fold__image__reindex,fact_nat__less__add__iff1,fact_nat__less__add__iff2,fact_diff__Suc__eq__diff__pred,fact_Suc__eq__plus1__left,fact_Suc__eq__plus1,fact_nat__le__add__iff1,fact_nat__diff__add__eq1,fact_nat__mult__commute,fact_nat__mult__assoc,fact_left__add__mult__distrib,fact_nat__eq__add__iff2,fact_nat__diff__add__eq2,fact_nat__le__add__iff2,fact_nat__eq__add__iff1,fact_setsum__multicount,fact_fold__image__Un__one,fact_finite__fun__UNIVD1,fact_Id__onE,fact_fold__graph__permute__diff,fact_Min_Oremove,fact_less__zeroE,fact_le0,fact_zero__less__Suc,fact_bot__nat__def,fact_zero__reorient,fact_min__max_Oinf_Oidem,fact_min__max_Oinf_Ocommute,fact_min__max_Oinf__commute,fact_min__max_Oinf_Oleft__idem,fact_min__max_Oinf__left__idem,fact_min__max_Oinf_Oleft__commute,fact_min__max_Oinf__left__commute,fact_min__max_Oinf_Oassoc,fact_min__max_Oinf__assoc,fact_min__0L,fact_min__0R,fact_Min_Oidem,fact_min__le__iff__disj,fact_min__max_Oinf__le1,fact_min__max_Oinf__le2,fact_min__max_Ole__iff__inf,fact_min__max_Ole__inf__iff,fact_min__max_Ole__infI1,fact_min__max_Ole__infI2,fact_min__max_Oinf__absorb1,fact_min__max_Oinf__absorb2,fact_min__max_Ole__infI,fact_min__max_Oinf__greatest,fact_min__max_Oinf__mono,fact_min__max_Ole__infE,fact_min__max_Oless__infI1,fact_min__max_Oless__infI2,fact_min__less__iff__conj,fact_min__less__iff__disj,fact_min__add__distrib__left,fact_min__diff__distrib__left,fact_inf__min,fact_min__Suc__Suc,fact_min__diff,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_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,fact_divisors__zero,fact_no__zero__divisors,fact_mult__eq__0__iff,fact_mult__zero__right,fact_mult__zero__left,fact_right__minus__eq,fact_eq__iff__diff__eq__0,fact_diff__self,fact_diff__0__right,fact_one__neq__zero,fact_zero__neq__one,fact_min__of__mono,fact_minus__zero,fact_neg__0__equal__iff__equal,fact_equal__neg__zero,fact_neg__equal__0__iff__equal,fact_neg__equal__zero,fact_Zero__not__Suc,fact_nat_Osimps_I2_J,fact_Suc__not__Zero,fact_nat_Osimps_I3_J,fact_Zero__neq__Suc,fact_Suc__neq__Zero,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__cancel2,fact_mult__cancel1,fact_mult__is__0,fact_mult__0__right,fact_mult__0,fact_fold__graph_Oequations_I1_J,fact_fold__graph_OemptyI,fact_empty__fold__graphE,fact_fold__graph__imp__finite,fact_min__max_Ofun__left__comm__idem__inf,fact_setsum__0,fact_Least__Suc,fact_zero__le__double__add__iff__zero__le__single__add,fact_double__add__le__zero__iff__single__add__le__zero,fact_add__nonneg__nonneg,fact_add__nonneg__eq__0__iff,fact_add__increasing,fact_add__increasing2,fact_add__nonpos__nonpos,fact_split__mult__neg__le,fact_split__mult__pos__le,fact_mult__mono,fact_mult__mono_H,fact_mult__left__mono__neg,fact_mult__right__mono__neg,fact_comm__mult__left__mono,fact_mult__left__mono,fact_mult__right__mono,fact_mult__nonpos__nonpos,fact_mult__nonpos__nonneg,fact_mult__nonneg__nonpos2,fact_mult__nonneg__nonpos,fact_mult__nonneg__nonneg,fact_mult__le__0__iff,fact_zero__le__mult__iff,fact_zero__le__square,fact_pos__add__strict,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_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_sum__squares__eq__zero__iff,fact_zero__le__one,fact_not__one__le__zero,fact_not__one__less__zero,fact_zero__less__one,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_right__minus,fact_eq__neg__iff__add__eq__0,fact_left__minus,fact_ab__left__minus,fact_minus__unique,fact_diff__0,fact_setsum__empty,fact_setsum_Oempty,fact_setsum_Oinfinite,fact_setsum__infinite,fact_less__Suc__eq__0__disj,fact_less__Suc0,fact_gr0__conv__Suc,fact_one__is__add,fact_add__is__1,fact_add__gr__0,fact_card_Oempty,fact_card__infinite,fact_mult__eq__1__iff,fact_zero__less__diff,fact_diff__less,fact_mult__less__mono2,fact_mult__less__mono1,fact_mult__less__cancel2,fact_mult__less__cancel1,fact_nat__0__less__mult__iff,fact_nat__mult__less__cancel1,fact_nat__mult__eq__cancel1,fact_diff__add__0,fact_diff__is__0__eq_H,fact_diff__is__0__eq,fact_One__nat__def,fact_mult__eq__self__implies__10,fact_fold__graph_OinsertI,fact_setsum__eq__0__iff,fact_Min_Oin__idem,fact_min__max_Omono__inf,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__left__le__imp__le,fact_mult__right__le__imp__le,fact_mult__less__imp__less__left,fact_mult__left__less__imp__less,fact_mult__less__imp__less__right,fact_mult__right__less__imp__less,fact_mult__le__less__imp__less,fact_mult__less__le__imp__less,fact_mult__strict__mono_H,fact_mult__strict__mono,fact_mult__le__cancel__left__neg,fact_mult__le__cancel__left__pos,fact_sum__squares__le__zero__iff,fact_sum__squares__ge__zero,fact_not__sum__squares__lt__zero,fact_sum__squares__gt__zero__iff,fact_mult__right__le__one__le,fact_mult__left__le__one__le,fact_zero__less__two,fact_card__eq__0__iff,fact_card__ge__0__finite,fact_diff__Suc__less,fact_Suc__pred,fact_one__less__mult,fact_n__less__n__mult__m,fact_n__less__m__mult__n,fact_nat__diff__split,fact_nat__diff__split__asm,fact_one__le__mult__iff,fact_mult__le__cancel1,fact_mult__le__cancel2,fact_nat__mult__le__cancel1,fact_setsum__eq__Suc0__iff,fact_fold__graph__insert__swap,fact_setsum__eq__1__iff,fact_setsum__delta,fact_setsum__delta_H,fact_Min__insert,fact_Min_Osubset__idem,fact_Min__Un,fact_card__less__Suc2,fact_card__less,fact_card__less__Suc,fact_convex__bound__le,fact_card__gt__0__iff,fact_finite__UNIV__card__ge__0,fact_setsum_OF__eq,fact_setsum_Oeq__fold,fact_Suc__diff__1,fact_Suc__pred_H,fact_add__eq__if,fact_mult__eq__if,fact_setsum__restrict__set_H,fact_setsum__restrict__set,fact_Diff1__fold__graph,fact_Min_Oinsert,fact_card__def,fact_card_Oeq__fold__g,fact_Min_Oinsert__remove,fact_Min_Ounion__inter,fact_Min_Ounion__disjoint,fact_convex__bound__lt,fact_triple_Osize_I1_J,fact_vname_Osize_I1_J,fact_even__less__0__iff,fact_dual__max,fact_vname_Osize_I2_J,fact_triple_Osize_I2_J,fact_inf__nat__def,fact_double__eq__0__iff,fact_card_Ounion__inter__neutral,fact_setsum__mono2,fact_min__ord__min,fact_fold1Set_Ointros,fact_vname_Osize_I3_J,fact_Min_Oclosed,fact_empty__fold1SetE,fact_fold1Set__nonempty,fact_fold1Set__sing,fact_vname_Osize_I4_J,fact_arith__series__nat,fact_setsum__Un__zero,fact_setsum_Ounion__inter__neutral,fact_card__Suc__eq,fact_setsum__mono3,fact_setsum__reindex__nonzero,fact_finite__lessThan,fact_lessThan__eq__iff,fact_lessThan__0,fact_lessThan__Suc,fact_card__lessThan,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_single__Diff__lessThan,fact_arith__series__general,fact_option_Osize_I2_J,fact_Ints__odd__less__0,fact_com_Osize_I3_J,fact_com_Osize_I4_J,fact_negative__zless,fact_Ints__of__nat,fact_of__nat__eq__iff,fact_int__0,fact_int__eq__0__conv,fact_negative__eq__positive,fact_int__le__0__conv,fact_int__zle__neg,fact_int__Suc,fact_zless__iff__Suc__zadd,fact_not__zle__0__negative,fact_negative__zless__0,fact_zless__int,fact_zadd__int__left,fact_zadd__int,fact_zle__int,fact_zmult__int,fact_int__mult,fact_int__1,fact_inj__int,fact_int__setsum,fact_int__Suc0__eq__1,fact_zmult__zless__mono2__lemma,fact_zero__less__int__conv,fact_zero__le__imp__of__nat,fact_of__nat__0__le__iff,fact_zdiff__int,fact_of__nat__less__0__iff,fact_of__nat__0,fact_of__nat__less__iff,fact_less__imp__of__nat__less,fact_of__nat__less__imp__less,fact_of__nat__le__iff,fact_of__nat__add,fact_of__nat__mult,fact_of__nat__1,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_of__nat__Suc,fact_of__nat__diff,fact_option_Osize_I1_J,fact_setsum__constant,fact_com_Osize_I2_J,fact_com_Osize_I1_J,fact_of__nat__0__less__iff,fact_Ints__double__eq__0__iff,fact_Ints__odd__nonzero,fact_com_Osize_I6_J,fact_com_Osize_I5_J,fact_semiring__1__class_Oof__nat__code,fact_zdiff__int__split,fact_nat_Osize_I2_J,fact_in__measure,fact_mlex__leq,fact_negative__zle,fact_negative__zle__0,fact_zero__zle__int,fact_int__less__0__conv,fact_int__int__eq,fact_not__int__zless__negative,fact_zle__iff__zadd,fact_zadd__zmult__distrib,fact_zadd__zmult__distrib2,fact_zmult__1,fact_zmult__1__right,fact_zmult__zminus,fact_zdiff__zmult__distrib,fact_zdiff__zmult__distrib2,fact_zmult__assoc,fact_zmult__commute,fact_zadd__zless__mono,fact_zadd__left__mono,fact_diff__int__def__symmetric,fact_diff__int__def,fact_zminus__zadd__distrib,fact_zadd__strict__right__mono,fact_zadd__assoc,fact_zadd__left__commute,fact_zadd__commute,fact_zless__le,fact_zle__antisym,fact_zle__trans,fact_zle__linear,fact_zle__refl,fact_zminus__zminus,fact_zless__linear,fact_zle__diff1__eq,fact_zless__add1__eq,fact_zless__imp__add1__zle,fact_add1__zle__eq,fact_zle__add1__eq__le,fact_le__imp__0__less,fact_odd__less__0,fact_odd__nonzero,fact_int__0__neq__1,fact_int__0__less__1,fact_int__one__le__iff__zero__less,fact_less__bin__lemma,fact_zminus__0,fact_zadd__0,fact_zadd__0__right,fact_zadd__zminus__inverse2,fact_zmult__zless__mono2,fact_pos__zmult__eq__1__iff,fact_of__nat__aux_Osimps_I1_J,fact_of__nat__aux_Osimps_I2_J,fact_nat_Osize_I1_J,fact_mlex__less,fact_self__quotient__aux1,fact_self__quotient__aux2,fact_zdiv__mono2__neg__lemma,fact_unique__quotient__lemma__neg,fact_zdiv__mono2__lemma,fact_q__pos__lemma,fact_q__neg__lemma,fact_unique__quotient__lemma,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I5_J,fact_transfer__int__nat__numerals_I2_J,fact_Nat__Transfer_Otransfer__int__nat__functions_I2_J,fact_Nat__Transfer_Otransfer__int__nat__functions_I1_J,fact_transfer__int__nat__relations_I3_J,fact_transfer__nat__int__set__relations_I5_J,fact_transfer__nat__int__set__relations_I3_J,fact_transfer__nat__int__set__relations_I4_J,fact_transfer__int__nat__relations_I1_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J,fact_transfer__nat__int__set__relations_I2_J,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I2_J,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I1_J,fact_transfer__nat__int__set__relations_I1_J,fact_transfer__int__nat__numerals_I1_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J,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_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J,fact_transfer__int__nat__relations_I2_J,fact_nat_Osize_I4_J,fact_small_H_Osimps,fact_setsum__bounded,fact_tsub__def,fact_option_Osize_I4_J,fact_infinite__UNIV__int,fact_nat__size,fact_nat_Osize_I3_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I3_J,fact_tsub__eq,fact_Nat__Transfer_Otransfer__int__nat__functions_I3_J,fact_option_Osize_I3_J,fact_small_H_Opsimps,fact_image__minus__const__atLeastLessThan__nat,fact_in__lex__prod,fact_card__Pow,fact_card__Plus__conv__if,fact_finite__atLeastLessThan,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_accp__downward,fact_accp_Oequations,fact_accp_Osimps,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_atLeastLessThan__eq__iff,fact_atLeastLessThan__inj_I1_J,fact_atLeastLessThan__inj_I2_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I27_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_atLeastLessThan__add__Un,fact_atLeastLessThan0,fact_Ints__power,fact_atLeast0LessThan,fact_card__atLeastLessThan,fact_image__Suc__atLeastLessThan,fact_atLeastLessThan__empty,fact_atLeastLessThan__empty__iff2,fact_atLeastLessThan__empty__iff,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_accp__subset,fact_atLeastLessThan__singleton,fact_UN__UN__finite__eq,fact_ivl__disj__un_I8_J,fact_subset__card__intvl__is__intvl,fact_ivl__disj__int_I2_J,fact_setsum__shift__lb__Suc0__0__upt,fact_setsum__head__upt__Suc,fact_power__eq__if,fact_atLeastLessThanSuc,fact_finite__PlusD_I2_J,fact_finite__PlusD_I1_J,fact_finite__Plus,fact_finite__Plus__iff,fact_setsum__op__ivl__Suc,fact_card__Plus,fact_power__strict__mono,fact_one__less__power,fact_power__increasing__iff,fact_power__le__imp__le__exp,fact_power__decreasing,fact_finite__atLeastLessThan__int,fact_zpower__zpower,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J,fact_zpower__zadd__distrib,fact_Nat__Transfer_Otransfer__int__nat__functions_I4_J,fact_int__power,fact_zpower__int,fact_finite__atLeastZeroLessThan__int,fact_image__add__int__atLeastLessThan,fact_field__power__not__zero,fact_power__commutes,fact_power__mult__distrib,fact_power__one,fact_power__mult,fact_power__one__right,fact_power__mono,fact_zero__le__power,fact_zero__less__power,fact_power__eq__0__iff,fact_one__le__power,fact_power__0__Suc,fact_power__inject__exp,fact_power__Suc2,fact_power__Suc,fact_power__0,fact_power__add,fact_power__Suc__0,fact_nat__power__eq__Suc__0__iff,fact_nat__zero__less__power__iff,fact_nat__power__less__imp__less,fact_of__nat__power,fact_power__less__imp__less__base,fact_power__le__imp__le__base,fact_power__inject__base,fact_power__less__power__Suc,fact_power__gt1__lemma,fact_power__0__left,fact_power__gt1,fact_power__strict__increasing__iff,fact_power__less__imp__less__exp,fact_power__strict__increasing,fact_power__increasing,fact_power__minus,fact_nat__one__le__power,fact_power__Suc__less,fact_power__eq__imp__eq__base,fact_power__Suc__less__one,fact_power__strict__decreasing,fact_UNIV__Plus__UNIV,fact_small_H_Opinduct,fact_same__fstI,fact_ex__nat__less__eq,fact_all__nat__less__eq,fact_Plus__eq__empty__conv,fact_UN__finite2__subset,fact_power__power__power,fact_divmod__int__relI,fact_UN__finite2__eq,fact_UN__finite__subset,fact_unique__remainder,fact_unique__quotient,fact_self__remainder,fact_divmod__int__rel__0,fact_power_Opower_Opower__0,fact_power_Opower_Opower__Suc,fact_self__quotient,fact_zminus1__lemma,fact_ivl__disj__un_I3_J,fact_int__power__div__base,fact_in__finite__psubset,fact_min__max_OInf__fin_Oremove,fact_com_Osize_I12_J,fact_finite__greaterThanLessThan,fact_finite__greaterThanLessThan__int,fact_zdiv__zero,fact_zdiv__zminus2,fact_zdiv__zminus__zminus,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__mono1__neg,fact_zdiv__mono1,fact_div__neg__neg__trivial,fact_zdiv__mono2__neg,fact_div__nonpos__pos__le0,fact_neg__imp__zdiv__nonneg__iff,fact_div__pos__pos__trivial,fact_div__nonneg__neg__le0,fact_zdiv__mono2,fact_nonneg1__imp__zdiv__pos__iff,fact_pos__imp__zdiv__pos__iff,fact_pos__imp__zdiv__nonneg__iff,fact_zdiv__eq__0__iff,fact_atLeastSucLessThan__greaterThanLessThan,fact_image__uminus__greaterThanLessThan,fact_int__div__less__self,fact_zdiv__zmult2__eq,fact_divmod__int__rel__div,fact_div__mult__self2,fact_div__mult__self1,fact_div__add__self1,fact_div__add__self2,fact_min__max_OInf__fin_Oin__idem,fact_min__max_OInf__fin_Osingleton,fact_com_Osize_I10_J,fact_com_Osize_I9_J,fact_ivl__disj__int_I9_J,fact_card__greaterThanLessThan,fact_min__max_OInf__fin_Oinsert__idem,fact_min__max_OInf__fin_Osubset__idem,fact_min__max_OInf__fin_Ounion__idem,fact_atLeastPlusOneLessThan__greaterThanLessThan__int,fact_divmod__int__rel__div__eq,fact_split__zdiv,fact_min__max_OInf__fin_Oinsert,fact_ivl__disj__un_I15_J,fact_min__max_OInf__fin_Oinsert__remove,fact_min__max_OInf__fin_Ounion__disjoint,fact_min__max_OInf__fin_Ounion__inter,fact_com_Osize_I14_J,fact_com_Osize_I13_J,fact_com_Osize_I11_J,fact_z3div__def,fact_norm__frac_Osimps,fact_min__max_OInf__fin_Oclosed,fact_zmult2__lemma,fact_min__max_Osup__Inf1__distrib,fact_div__le__mono,fact_div__le__dividend,fact_div__mult2__eq,fact_min__max_Oinf__sup__distrib2,fact_min__max_Osup__inf__distrib2,fact_min__max_Oinf__sup__distrib1,fact_min__max_Osup__inf__distrib1,fact_min__max_Oinf__sup__absorb,fact_min__max_Osup__inf__absorb,fact_max__add__distrib__left,fact_max__diff__distrib__left,fact_max__0R,fact_max__0L,fact_min__max_Osup_Oidem,fact_min__max_Osup_Ocommute,fact_min__max_Osup__commute,fact_min__max_Osup_Oleft__idem,fact_min__max_Osup__left__idem,fact_min__max_Osup_Oleft__commute,fact_min__max_Osup__left__commute,fact_min__max_Osup_Oassoc,fact_min__max_Osup__assoc,fact_Max_Oidem,fact_max__Suc__Suc,fact_mod__mod__trivial,fact_zmod__self,fact_mod__self,fact_mod__by__0,fact_zmod__zero,fact_mod__0,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_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__cong,fact_mod__minus__eq,fact_mod__diff__right__eq,fact_mod__diff__left__eq,fact_mod__diff__eq,fact_mod__diff__cong,fact_max__less__iff__conj,fact_less__max__iff__disj,fact_min__max_Oless__supI2,fact_min__max_Oless__supI1,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_zminus__zmod,fact_zmod__zminus__zminus,fact_zmod__zminus2,fact_zdiff__zmod__left,fact_zdiff__zmod__right,fact_zmod__simps_I3_J,fact_zmod__zmult1__eq,fact_sup__max,fact_max__of__mono,fact_zpower__zmod,fact_min__max_Ofun__left__comm__idem__sup,fact_mod__mult__self1__is__0,fact_mod__mult__self2__is__0,fact_mod__mult__self1,fact_mod__mult__self2,fact_mod__by__1,fact_mod__div__trivial,fact_div__1,fact_div__less,fact_nat__mult__div__cancel__disj,fact_min__max_Odistrib__sup__le,fact_min__max_Odistrib__inf__le,fact_Divides_Otransfer__nat__int__function__closures_I2_J,fact_zmod__le__nonneg__dividend,fact_pos__mod__bound,fact_neg__mod__bound,fact_minus__max__eq__min,fact_minus__min__eq__max,fact_zdiv__int,fact_Divides_Otransfer__int__nat__functions_I1_J,fact_nat__minus__add__max,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_div__mod__equality,fact_div__mod__equality2,fact_mod__div__equality,fact_mod__div__equality2,fact_semiring__div__class_Omod__div__equality_H,fact_div__le__mono2,fact_div__mult__self__is__m,fact_div__mult__self1__is__m,fact_nat__mult__div__cancel1,fact_div__less__dividend,fact_pos__mod__sign,fact_pos__mod__conj,fact_mod__pos__pos__trivial,fact_neg__mod__sign,fact_neg__mod__conj,fact_mod__neg__neg__trivial,fact_max__ord__max,fact_Max_Oin__idem,fact_min__max_Omono__sup,fact_Int__atLeastLessThan,fact_zmod__zminus1__eq__if,fact_zmod__zminus2__eq__if,fact_zdiv__zmod__equality2,fact_zdiv__zmod__equality,fact_zdiv__zmult1__eq,fact_zmod__zdiv__equality,fact_zmult__div__cancel,fact_zmod__zdiv__equality_H,fact_Int__greaterThanLessThan,fact_divmod__int__rel__mod,fact_dual__min,fact_div__geq,fact_div__if,fact_split__div,fact_mod__pos__neg__trivial,fact_Max__insert,fact_Max_Osubset__idem,fact_min__max_Osup__Inf__absorb,fact_Max__Un,fact_divmod__int__rel__div__mod,fact_le__div__geq,fact_split__div_H,fact_split__div__lemma,fact_Max_Oinsert,fact_split__zmod,fact_zmult2__lemma__aux3,fact_zmult2__lemma__aux4,fact_zmult2__lemma__aux1,fact_zmult2__lemma__aux2,fact_divmod__int__rel__mod__eq,fact_Max_Oinsert__remove,fact_Max_Ounion__inter,fact_Max_Ounion__disjoint,fact_zmod__zmult2__eq,fact_zdiv__zminus1__eq__if,fact_zdiv__zminus2__eq__if,fact_zadd1__lemma,fact_Max_Oremove,fact_split__pos__lemma,fact_split__neg__lemma,fact_zmult1__lemma,fact_min__max_Osup__Inf2__distrib,fact_norm__frac_Opsimps,fact_z3mod__def,fact_min__max_Oinf__Sup2__distrib,fact_min__max_Oinf__Sup1__distrib,fact_Max_Oclosed,fact_div__add1__eq,fact_mod__mult__distrib,fact_mod__mult__distrib2,fact_mod__Suc__eq__Suc__mod,fact_mod__less,fact_mod__less__eq__dividend,fact_sup__nat__def,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_div__mult1__eq,fact_mod__mult2__eq,fact_le__mod__geq,fact_div__mod__equality_H,fact_mult__div__cancel,fact_Divides_Omod__div__equality_H,fact_Divides_Otransfer__int__nat__functions_I2_J,fact_zmod__int,fact_mod__le__divisor,fact_mod__mult__self4,fact_min__max_OSup__fin_Oin__idem,fact_min__max_OSup__fin_Osingleton,fact_split__mod,fact_mod__lemma,fact_Suc__times__mod__eq,fact_min__max_OSup__fin_Oinsert__idem,fact_min__max_OSup__fin_Osubset__idem,fact_min__max_Oinf__Sup__absorb,fact_min__max_OSup__fin_Ounion__idem,fact_min__max_OSup__fin_Oinsert,fact_min__max_OSup__fin_Oinsert__remove,fact_min__max_OSup__fin_Ounion__disjoint,fact_min__max_OSup__fin_Ounion__inter,fact_min__max_OSup__fin_Oremove,fact_min__max_OInf__le__Sup,fact_divmod__nat__step,fact_norm__frac_Opinduct,fact_divmod__nat__rel__mult2__eq,fact_divmod__nat__rel__mult1__eq,fact_mod__eq,fact_divmod__nat__def,fact_divmod__nat__rel__divmod__nat,fact_divmod__nat__eq,fact_divmod__nat__rel__unique,fact_divmod__nat__rel,fact_div__eq,fact_divmod__nat__zero,fact_divmod__nat__div__mod,fact_divmod__nat__base,fact_divmod__nat__rel__add1__eq,fact_min__max_OSup__fin_Oclosed,fact_negDivAlg__div__mod,fact_divmod__nat__if,fact_posDivAlg__div__mod,fact_posDivAlg__0,fact_negDivAlg__correct,fact_posDivAlg__correct,fact_pair__imageI,fact_split__twice,fact_swap__inj__on,fact_split__eta,fact_splitI,fact_prod__caseI,fact_mem__splitI,fact_splitD,fact_splitD_H,fact_Id__on__def_H,fact_split__paired__The,fact_The__split__eq,fact_inj__graph,fact_Pair__inject,fact_Pair__eq,fact_split__paired__All,fact_split__weak__cong,fact_finite__psubset__def,fact_divmod__int__rel__def,fact_prod_Osimps_I2_J,fact_split__conv,fact_Nitpick_OFrac__def,fact_int__ge__less__than__def,fact_int__ge__less__than2__def,fact_Nitpick_Oprod__def,fact_inv__image__def,fact_prod_Orecs,fact_lfp__induct2,fact_divmod__int__def,fact_in__inv__image,fact_negateSnd__eq,fact_divmod__int__rel__neg,fact_divmod__int__correct,fact_divmod__int__mod__div,fact_rp__inv__image__def,fact_mod__neg__neg,fact_div__neg__neg,fact_mod__pos__neg,fact_prod__eqI,fact_Pair__fst__snd__eq,fact_snd__eqD,fact_fst__eqD,fact_pair__collapse,fact_snd__conv,fact_fst__conv,fact_surjective__pairing,fact_split__comp,fact_split__beta,fact_prod__case__beta,fact_split__comp__eq,fact_split__def,fact_The__split,fact_fst__def,fact_snd__def,fact_div__int__def,fact_mod__int__def,fact_div__neg__pos,fact_mod__neg__pos,fact_div__pos__pos,fact_mod__pos__pos,fact_div__pos__neg,fact_prod__size__simp,fact_conjI__realizer,fact_exI__realizer,fact_div__pos__neg__1__number__of,fact_of__nat__number__of__lemma,fact_minus__numeral__code_I5_J,fact_times__numeral__code_I5_J,fact_number__of__is__id,fact_number__of__reorient,fact_eq__number__of,fact_plus__numeral__code_I9_J,fact_less__number__of__int__code,fact_less__eq__number__of__int__code,fact_le__number__of__eq__not__less,fact_left__distrib__number__of,fact_right__distrib__number__of,fact_left__diff__distrib__number__of,fact_right__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_number__of__minus,fact_arith__simps_I30_J,fact_Ints__number__of,fact_div__nat__def,fact_mod__nat__def,fact_add__number__of__diff1,fact_minus__number__of__mult,fact_diff__number__of__eq,fact_divmod__nat__rel__def,fact_minus__numeral__code_I6_J,fact_add__number__of__diff2,fact_mod__pos__pos__1__number__of,fact_div__pos__pos__1__number__of,fact_mod__pos__neg__1__number__of,fact_power__number__of__odd__number__of,fact_ivl__disj__un_I4_J,fact_setprod__gen__delta,fact_image__atLeastZeroLessThan__int,fact_finite__greaterThanAtMost,fact_finite__greaterThanAtMost__int,fact_nat__number__of__def,fact_nat__number__of,fact_card__greaterThanAtMost__int,fact_less__eq__int__code_I16_J,fact_rel__simps_I34_J,fact_less__int__code_I16_J,fact_rel__simps_I17_J,fact_nat__int,fact_rel__simps_I51_J,fact_setprod__timesf,fact_setprod__1,fact_transfer__nat__int__sum__prod2_I2_J,fact_of__nat__setprod,fact_int__setprod,fact_transfer__nat__int__sum__prod_I2_J,fact_setprod__zero,fact_setprod__zero__iff,fact_setprod_Oempty,fact_setprod__empty,fact_setprod__infinite,fact_setprod_Oinfinite,fact_setprod__eq__1__iff,fact_transfer__nat__int__numerals_I1_J,fact_nat__0,fact_ex__nat,fact_all__nat,fact_transfer__nat__int__relations_I1_J,fact_eq__nat__nat__iff,fact_bin__less__0__simps_I4_J,fact_transfer__nat__int__numerals_I2_J,fact_Bit1__def,fact_setprod_Odistrib,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I4_J,fact_transfer__int__nat__set__return__embed,fact_setprod__pos__nat__iff,fact_greaterThanAtMost__empty,fact_setprod__reindex,fact_setprod__reindex__cong,fact_greaterThanAtMost__empty__iff2,fact_greaterThanAtMost__empty__iff,fact_ivl__disj__un_I20_J,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I2_J,fact_ivl__disj__int_I14_J,fact_nat__le__0,fact_nat__0__iff,fact_one__div__nat__number__of,fact_zless__nat__conj,fact_nat__mono__iff,fact_number__of__Bit1,fact_transfer__nat__int__relations_I3_J,fact_nat__1,fact_setprod__delta_H,fact_setprod__delta,fact_nat__0__le,fact_int__eq__iff,fact_int__nat__eq,fact_zless__nat__eq__int__zless,fact_nat__zminus__int,fact_power__number__of__odd,fact_card__greaterThanAtMost,fact_setprod__constant,fact_zpower__number__of__odd,fact_setprod_Oinsert,fact_setprod__insert,fact_setprod_Ounion__inter,fact_setprod__Un__Int,fact_setprod_Oreindex,fact_transfer__nat__int__sum__prod_I1_J,fact_setprod_OF__eq,fact_setprod_Oeq__fold,fact_card__atLeastZeroLessThan__int,fact_card__atLeastLessThan__int,fact_zero__less__nat__eq,fact_transfer__nat__int__relations_I2_J,fact_nat__less__eq__zless,fact_nat__eq__iff2,fact_nat__eq__iff,fact_nat__le__eq__zle,fact_split__nat,fact_Nat__Transfer_Otransfer__nat__int__functions_I1_J,fact_nat__add__distrib,fact_int__eq__iff__number__of,fact_Nat__Transfer_Otransfer__nat__int__functions_I2_J,fact_nat__mult__distrib,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I3_J,fact_nat__diff__distrib,fact_transfer__nat__int__sum__prod2_I1_J,fact_Divides_Otransfer__nat__int__functions_I2_J,fact_nat__mod__distrib,fact_Divides_Otransfer__nat__int__functions_I1_J,fact_nat__div__distrib,fact_Int__greaterThanAtMost,fact_image__uminus__atLeastLessThan,fact_image__uminus__greaterThanAtMost,fact_Nat__Transfer_Otransfer__nat__int__functions_I4_J,fact_nat__power__eq,fact_ivl__disj__int_I10_J,fact_Nat__Transfer_Otransfer__nat__int__functions_I3_J,fact_setprod_Oinsert__remove,fact_setprod_Ounion__disjoint,fact_setprod__Un__disjoint,fact_one__less__nat__eq,fact_nat__less__iff,fact_Suc__nat__eq__nat__zadd1,fact_nat__mult__distrib__neg,fact_Nat__Transfer_Otransfer__nat__int__set__functions_I5_J,fact_expand__Suc,fact_setprod_Oremove,fact_ivl__disj__un_I16_J,fact_card__greaterThanLessThan__int,fact_nat__aux__def,fact_transfer__morphism__nat__int,fact_one__mod__nat__number__of,fact_nat__def,fact_not__neg__0,fact_Rep__Integ__inject,fact_not__neg__1,fact_not__neg__int,fact_not__neg__eq__ge__0,fact_neg__def,fact_neg__nat,fact_neg__number__of__Bit1,fact_not__neg__nat,fact_neg__imp__number__of__eq__0,fact_neg__zminus__int,fact_eq__nat__number__of,fact_nat__number__of__add__left,fact_int__nat__number__of,fact_diff__nat__eq__if,fact_of__nat__number__of__eq,fact_mod__nat__number__of,fact_div__nat__number__of,fact_nat__number__of__Bit1,fact_power__nat__number__of,fact_power__nat__number__of__number__of,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I4_J,fact_Nat__Transfer_Otransfer__int__nat__set__functions_I3_J,fact_Suc__nat__number__of__add,fact_diff__nat__number__of,fact_mult__Pls,fact_diff__bin__simps_I1_J,fact_minus__Pls,fact_rel__simps_I2_J,fact_rel__simps_I19_J,fact_Pls__def,fact_add__Pls,fact_add__Pls__right,fact_succ__Pls,fact_rel__simps_I39_J,fact_rel__simps_I46_J,fact_semiring__norm_I112_J,fact_number__of__Pls,fact_add__numeral__0__right,fact_add__numeral__0,fact_bin__less__0__simps_I1_J,fact_nat__number__of__Pls,fact_semiring__norm_I113_J,fact_zero__is__num__zero,fact_rel__simps_I22_J,fact_rel__simps_I12_J,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I1_J,fact_not__neg__number__of__Pls,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I2_J,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I3_J,fact_nat__1__add__number__of,fact_nat__number__of__add__1,fact_nat__set__def,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I5_J,fact_transfer__int__nat__set__relations_I3_J,fact_mult__numeral__1,fact_mult__numeral__1__right,fact_semiring__norm_I110_J,fact_numeral__1__eq__1,fact_eq__0__number__of,fact_eq__number__of__0,fact_number__of2,fact_rel__simps_I5_J,fact_rel__simps_I29_J,fact_less__nat__number__of,fact_le__nat__number__of,fact_one__is__num__one,fact_nat__numeral__1__eq__1,fact_Numeral1__eq1__nat,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_numeral__1__eq__Suc__0,fact_numeral__3__eq__3,fact_power3__eq__cube,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I8_J,fact_Suc3__eq__add__3,fact_add__nat__number__of,fact_transfer__int__nat__numerals_I4_J,fact_transfer__nat__int__numerals_I4_J,fact_Nat__Transfer_Otransfer__nat__int__set__function__closures_I6_J,fact_number__of__succ,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I4_J,fact_le__special_I4_J,fact_le__special_I2_J,fact_less__special_I2_J,fact_less__special_I4_J,fact_add__special_I3_J,fact_add__special_I2_J,fact_Suc__diff__eq__diff__pred,fact_mult__nat__number__of,fact_nat__number__of__mult__left,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_transfer__nat__int__set__return__embed,fact_diff__special_I2_J,fact_diff__special_I1_J,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_Suc__nat__number__of,fact_transfer__int__nat__sum__prod_I2_J,fact_eq__special_I4_J,fact_eq__special_I2_J,fact_neg__zmod__mult__2,fact_zmod__number__of__Bit1,fact_rel__simps_I44_J,fact_rel__simps_I38_J,fact_Bit0__Pls,fact_iszero__number__of__Bit0,fact_rel__simps_I50_J,fact_rel__simps_I49_J,fact_mult__Bit0,fact_add__Bit0__Bit0,fact_Bit0__def,fact_rel__simps_I48_J,fact_rel__simps_I31_J,fact_less__eq__int__code_I13_J,fact_less__int__code_I13_J,fact_rel__simps_I14_J,fact_minus__Bit0,fact_diff__bin__simps_I7_J,fact_iszero__0,fact_iszero__def,fact_not__iszero__1,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_I10_J,fact_rel__simps_I4_J,fact_less__int__code_I15_J,fact_rel__simps_I16_J,fact_add__Bit1__Bit0,fact_add__Bit0__Bit1,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_succ__Bit1,fact_succ__Bit0,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_add__Bit1__Bit1,fact_power__number__of__even,fact_zpower__number__of__even,fact_iszero__Numeral0,fact_iszero__number__of__Bit1,fact_double__number__of__Bit0,fact_number__of1,fact_power__number__of__even__number__of,fact_mult__2__right,fact_mult__2,fact_one__add__one__is__two,fact_zero__eq__power2,fact_zero__power2,fact_numeral__2__eq__2,fact_semiring__norm_I115_J,fact_power2__eq__square,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,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_nat__1__add__1,fact_mod2__Suc__Suc,fact_div2__Suc__Suc,fact_zmod__number__of__Bit0,fact_add__self__div__2,fact_not__iszero__Numeral1,fact_eq__number__of__eq,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_eq__special_I1_J,fact_eq__special_I3_J,fact_of__nat__double,fact_pos__zmod__mult__2,fact_neg__zdiv__mult__2,fact_pos__zdiv__mult__2,fact_arith__series__int,fact_adjust__def,fact_adjust__eq,fact_posDivAlg__eqn__1__number__of,fact_posDivAlg_Osimps,fact_posDivAlg__eqn,fact_posDivAlg__eqn__number__of,fact_posDivAlg_Opsimps,fact_of__int__num,fact_negDivAlg__eqn__1__number__of,fact_rel__simps_I37_J,fact_rel__simps_I40_J,fact_number__of__eq,fact_int__number__of__def,fact_of__int__m1,fact_rel__simps_I47_J,fact_rel__simps_I43_J,fact_Bit1__Min,fact_of__int__int__eq,fact_of__int__eq__iff,fact_rel__simps_I7_J,fact_rel__simps_I24_J,fact_rel__simps_I45_J,fact_rel__simps_I42_J,fact_bin__less__0__simps_I2_J,fact_rel__simps_I23_J,fact_rel__simps_I20_J,fact_rel__simps_I26_J,fact_rel__simps_I30_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_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_nonzero__number__of__Min,fact_of__int__add,fact_of__int__number__of__eq,fact_of__int__mult,fact_succ__Min,fact_of__int__1,fact_of__int__diff,fact_diff__bin__simps_I2_J,fact_of__int__of__nat__eq,fact_of__int__minus,fact_Ints__of__int,fact_of__int__power,fact_mult__minus1,fact_mult__minus1__right,fact_number__of__Min,fact_arith__simps_I31_J,fact_rel__simps_I11_J,fact_rel__simps_I25_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_I5_J,fact_diff__bin__simps_I6_J,fact_zdiv__minus1__right,fact_of__int__setsum,fact_of__int__setprod,fact_div__eq__minus1,fact_of__int__le__0__iff,fact_of__int__0__le__iff,fact_of__int__0__less__iff,fact_of__int__less__0__iff,fact_of__nat__nat,fact_negDivAlg__minus1,fact_div__pos__neg__trivial,fact_zmod__minus1,fact_of__int__of__nat,fact_power__m1__even,fact_power__m1__odd,fact_negDivAlg_Osimps,fact_negDivAlg__eqn__number__of,fact_negDivAlg__eqn,fact_negDivAlg_Opsimps,fact_posDivAlg_Opinduct,fact_int__of__code,fact_code__numeral__zero__minus__one,fact_zero__code__numeral__code,fact_one__code__numeral__code,fact_div__mod__code__numeral__def,fact_negDivAlg_Opinduct,fact_small__int__def,fact_small__prod__def,fact_nat__of__aux__code,fact_min__number__of__Suc,fact_min__Suc__number__of,fact_succ__pred,fact_le__iff__pred__less,fact_pred__Bit1,fact_pred__Bit0,fact_minus__Bit1,fact_pred__Pls,fact_pred__def,fact_add__Min,fact_add__Min__right,fact_pred__Min,fact_diff__bin__simps_I8_J,fact_number__of__pred,fact_neg__number__of__pred__iff__0,fact_Suc__diff__number__of,fact_Suc__eq__number__of,fact_eq__number__of__Suc,fact_nat__number__of__diff__1,fact_less__number__of__Suc,fact_less__Suc__number__of,fact_le__Suc__number__of,fact_le__number__of__Suc,fact_max__number__of__Suc,fact_max__Suc__number__of,fact_nat__case__add__eq__if,fact_nat__case__number__of,fact_nat__rec__add__eq__if,fact_nat__rec__0,fact_nat__rec__Suc,fact_nat__case__0,fact_nat__case__Suc,fact_max__Suc1,fact_max__Suc2,fact_less__eq__nat_Osimps_I2_J,fact_diff__Suc,fact_min__Suc1,fact_min__Suc2,fact_nat__rec__number__of,fact_transfer__int__nat__set__relations_I2_J,fact_full__small__int__def,fact_setprod_Ounion__inter__neutral,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I6_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I1_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I2_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I9_J,fact_Divides_Otransfer__int__nat__function__closures_I2_J,fact_Divides_Otransfer__int__nat__function__closures_I1_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I5_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I4_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I3_J,fact_is__nat__def,fact_Nat__Transfer_Otransfer__int__nat__set__function__closures_I6_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I8_J,fact_Nat__Transfer_Otransfer__int__nat__function__closures_I7_J,fact_transfer__int__nat__sum__prod2_I2_J,fact_transfer__int__nat__sum__prod2_I1_J,fact_setprod__Un__one,fact_code__numeral_Osize_I1_J,fact_Nats__number__of,fact_setprod__diff1,fact_diff__divide__distrib,fact_divide__1,fact_minus__divide__left,fact_times__divide__eq__right,fact_add__divide__distrib,fact_power__divide,fact_setsum__divide__distrib,fact_divide__zero__left,fact_divide__zero,fact_nonzero__eq__divide__eq,fact_nonzero__divide__eq__eq,fact_divide__eq__imp,fact_eq__divide__imp,fact_divide__self__if,fact_divide__self,fact_right__inverse__eq,fact_nonzero__minus__divide__divide,fact_nonzero__minus__divide__right,fact_nonzero__power__divide,fact_power__one__over,fact_setprod__dividef,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_divide__Numeral0,fact_divide__Numeral1,fact_divide__numeral__1,fact_divide__minus1,fact_Nats__0,fact_Nats__add,fact_Nats__mult,fact_less__divide__eq__number__of1,fact_less__divide__eq__number__of,fact_divide__less__eq__number__of,fact_divide__less__eq__number__of1,fact_Nats__1,fact_of__nat__in__Nats,fact_power__diff,fact_minus1__divide,fact_divide__le__eq__number__of1,fact_divide__le__eq__number__of,fact_le__divide__eq__number__of,fact_le__divide__eq__number__of1,fact_half__gt__zero,fact_half__gt__zero__iff,fact_geometric__sum,fact_divide__left__mono__neg,fact_divide__left__mono,fact_neg__divide__le__eq,fact_times__divide__times__eq,fact_minus__divide__right,fact_minus__divide__divide,fact_divide__right__mono__neg,fact_divide__right__mono,fact_divide__le__0__iff,fact_zero__le__divide__iff,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_gt__half__sum,fact_less__half__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_mult__imp__le__div__pos,fact_neg__le__divide__eq,fact_setprod__Un,fact_code__numeral_Osize_I2_J,fact_setsum__nonneg__leq__bound,fact_code__numeral_Oinject,fact_code__numeral_Osimps_I3_J,fact_code__numeral_Osimps_I2_J,fact_Suc__code__numeral__minus__one,fact_code__numeral_Osize_I4_J,fact_setsum__nonneg__0,fact_greaterThan__0,fact_greaterThan__eq__iff,fact_greaterThan__iff,fact_greaterThan__subset__iff,fact_ivl__disj__un_I11_J,fact_image__uminus__greaterThan,fact_image__uminus__lessThan,fact_ivl__disj__int_I5_J,fact_greaterThan__Suc,fact_code__numeral_Osize_I3_J,fact_sum__diff__distrib,fact_pair__lessI2,fact_min__max_OSup__fin_Ohom__commute,fact_pair__lessI1,fact_pair__leqI2,fact_smin__insertI,fact_smax__insertI,fact_smax__emptyI,fact_smin__emptyI,fact_pair__leqI1,fact_wmax__insertI,fact_wmin__insertI,fact_atLeast__Suc,fact_atLeast__eq__iff,fact_atLeast__iff,fact_atLeast__subset__iff,fact_atLeast__0,fact_Compl__atLeast,fact_Compl__lessThan,fact_atLeast__Suc__greaterThan,fact_ivl__disj__un_I14_J,fact_ivl__disj__int_I8_J,fact_UN__atLeast__UNIV,fact_ivl__disj__int_I6_J,fact_ivl__disj__un_I1_J,fact_ivl__disj__un_I12_J,fact_wmin__emptyI,fact_wmax__emptyI,fact_min__weak__def,fact_max__weak__def,fact_max__rpair__set,fact_max__strict__def,fact_rp__inv__image__rp,fact_max__ext__additive,fact_min__strict__def,fact_min__rpair__set,fact_max__extp__max__ext__eq,fact_equiv__intrel__iff,fact_less__than__iff,fact_equiv__intrel,fact_pair__less__def,fact_measure__def,fact_mlex__prod__def,fact_intrel__iff,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_min__max_OInf__fin_Ohom__commute,fact_Rep__Integ,fact_type__definition__Integ,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,fact_atLeastAtMost__singleton__iff,fact_atLeastAtMost__singleton_H,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_Int__atLeastAtMostR2,fact_Int__atLeastAtMostL2,fact_setsum__head__Suc,fact_setsum__cl__ivl__Suc,fact_setsum__head,fact_setsum__ub__add__nat,fact_ivl__disj__un_I13_J,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_type__definition_ORep__range,fact_type__definition_OAbs__image,fact_type__definition_ORep,fact_finite__atLeastAtMost__int,fact_SetInterval_Otransfer__int__nat__set__function__closures,fact_SetInterval_Otransfer__nat__int__set__function__closures,fact_atLeastLessThanPlusOne__atLeastAtMost__int,fact_atLeastPlusOneAtMost__greaterThanAtMost__int,fact_type__definition_ORep__inverse,fact_type__definition_ORep__inject,fact_SetInterval_Otransfer__nat__int__set__functions_I2_J,fact_simp__from__to,fact_card__atLeastAtMost__int,fact_SetInterval_Otransfer__int__nat__set__functions,fact_type__definition_OAbs__inject,fact_type__definition_OAbs__inverse,fact_aset_I6_J,fact_bset_I8_J,fact_bset_I3_J,fact_aset_I4_J,fact_bset_I4_J,fact_bset_I7_J,fact_aset_I3_J,fact_aset_I5_J,fact_bset_I6_J,fact_aset_I8_J,fact_periodic__finite__ex,fact_aset_I7_J,fact_bset_I5_J,fact_UN__le__eq__Un0,fact_SetInterval_Otransfer__nat__int__set__functions_I1_J,fact_finite__atMost,fact_atMost__eq__iff,fact_atLeast0AtMost,fact_lessThan__Suc__atMost,fact_card__atMost,fact_atMost__Suc,fact_atMost__iff,fact_atMost__subset__iff,fact_Compl__atMost,fact_Compl__greaterThan,fact_UN__atMost__UNIV,fact_setsum__atMost__Suc,fact_atMost__0,fact_Int__atLeastAtMostL1,fact_Int__atLeastAtMostR1,fact_ivl__disj__un_I9_J,fact_UN__le__add__shift,fact_ivl__disj__int_I3_J,fact_ivl__disj__int_I1_J,fact_image__uminus__atMost,fact_image__uminus__atLeast,fact_ivl__disj__un_I2_J,fact_ivl__disj__un_I10_J,fact_atMost__Int__atLeast,fact_ivl__disj__un_I7_J,fact_Max_Ohom__commute,fact_Min_Ohom__commute,fact_decr__mult__lemma,fact_negD,fact_incr__mult__lemma,fact_ex__least__nat__less,fact_strong__setprod__reindex__cong,fact_setprod__mono__one__right,fact_setprod__mono__one__left,fact_zero__less__imp__eq__int,fact_setsum__mono__zero__right,fact_setsum__mono__zero__left,fact_field__le__mult__one__interval,fact_transfer__nat__int__sum__prod__cong_I2_J,fact_sgn__1__neg,fact_sgn__times,fact_sgn__sgn,fact_sgn0,fact_sgn__0__0,fact_sgn__greater,fact_sgn__less,fact_sgn__pos,fact_sgn__1__pos,fact_zsgn__def,fact_sgn__if,fact_sgn__neg,fact_code__numeral_Osimps_I5_J,fact_incr__lemma,fact_decr__lemma,fact_setsum__abs,fact_setsum__abs__ge__zero,fact_abs__power__minus,fact_nonzero__abs__divide,fact_abs__le__D2,fact_abs__leI,fact_abs__le__iff,fact_abs__ge__minus__self,fact_abs__less__iff,fact_abs__mult__less,fact_abs__triangle__ineq3,fact_abs__triangle__ineq2,fact_abs__triangle__ineq2__sym,fact_abs__minus__commute,fact_abs__eq__0,fact_abs__zero,fact_abs__setsum__abs,fact_power__abs,fact_abs__minus__cancel,fact_abs__mult__self,fact_abs__mult,fact_abs__add__abs,fact_abs__of__nat,fact_abs__idempotent,fact_abs__int__eq,fact_abs__le__D1,fact_abs__ge__self,fact_abs__setprod,fact_abs__one,fact_abs__divide,fact_abs__of__pos,fact_zero__less__abs__iff,fact_abs__not__less__zero,fact_abs__of__nonneg,fact_abs__le__zero__iff,fact_abs__ge__zero,fact_abs__triangle__ineq,fact_abs__zmult__eq__1,fact_abs__sgn,fact_mult__sgn__abs,fact_abs__eq__mult,fact_abs__mult__pos,fact_abs__diff__triangle__ineq,fact_abs__triangle__ineq4,fact_abs__minus__le__zero,fact_abs__of__nonpos,fact_abs__if,fact_abs__of__neg,fact_zero__le__power__abs,fact_abs__div__pos,fact_abs__minus__one,fact_zabs__less__one__iff,fact_zabs__def,fact_nat__abs__mult__distrib,fact_zero__le__zpower__abs,fact_abs__number__of,fact_abs__power__minus__one,fact_zero__less__zpower__abs__iff,fact_power2__abs,fact_abs__power2,fact_code__numeral_Osimps_I4_J,fact_divmod__int__pdivmod,fact_Nitpick_Oint__gcd__def,fact_divmod__int__code,fact_apsnd__conv,fact_apsnd__compose,fact_fst__apsnd,fact_snd__apsnd,fact_apsnd__eq__conv,fact_negateSnd__def,fact_nat__gcd_Osimps,fact_pdivmod__def,fact_pdivmod__posDivAlg,fact_nat__gcd_Opsimps,fact_Nitpick_Onat__lcm__def,fact_Nitpick_Oint__lcm__def,fact_nat__gcd_Opinduct,fact_apfst__apsnd,fact_apsnd__apfst,fact_apfst__conv,fact_snd__apfst,fact_fst__apfst,fact_apfst__eq__conv,fact_apfst__compose,fact_apsnd__apfst__commute,fact_transfer__nat__int__sum__prod__cong_I1_J,fact_accp__acc__eq,fact_rel__comp__def,fact_rel__compI,fact_rel__comp__UNION__distrib,fact_rel__comp__UNION__distrib2,fact_rel__comp__mono,fact_O__assoc,fact_rel__comp__distrib,fact_rel__comp__distrib2,fact_rel__comp__empty2,fact_rel__comp__empty1,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_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_min__ext__wf,fact_wf__finite__psubset,fact_wf__Int1,fact_wf__Int2,fact_wf__subset,fact_pred__comp_Oequations,fact_wf__mlex,fact_wf__pair__less,fact_max__ext__wf,fact_wf__less,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__empty,fact_Range__empty__iff,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,fact_Domain__empty__iff,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__Collect__split,fact_DomainP__Domain__eq,fact_DomainE,fact_fold1Set_Oequations,fact_DomainP_Ointros,fact_DomainP_Oequations,fact_insert__fold1SetE,fact_image__split__eq__Sigma,fact_nat0__intermed__int__val,fact_SigmaI,fact_Times__eq__cancel2,fact_Sigma__empty1,fact_card__cartesian__product,fact_setsum__cartesian__product,fact_Sigma__empty2,fact_Times__empty,fact_Compl__Times__UNIV2,fact_Compl__Times__UNIV1,fact_setprod__cartesian__product,fact_Sigma__Un__distrib1,fact_Times__Un__distrib1,fact_Sigma__Un__distrib2,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_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__productD2,fact_finite__cartesian__productD1,fact_SetCompr__Sigma__eq,fact_Collect__split,fact_fst__image__times,fact_snd__image__times,fact_insert__times__insert,fact_finite__equiv__class,fact_vimage__Times,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_of__int__eq__id,fact_apsnd__id,fact_id__o,fact_o__id,fact_o__eq__id__dest,fact_vimage__id,fact_id__apply,fact_id__def,fact_inj__on__id,fact_apfst__id,fact_surj__id,fact_folding_Oempty,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_snd__prod__fun,fact_fst__map__pair,fact_map__pair__simp,fact_map__pair__ident,fact_map__pair_Ocompositionality,fact_map__pair__compose,fact_map__pair_Ocomp,fact_fst__comp__map__pair,fact_snd__comp__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_int__val__lemma,fact_refl__on__Id__on,fact_refl__on__empty,fact_refl__on__Un,fact_refl__on__Int,fact_refl__onD2,fact_refl__onD1,fact_refl__onD,fact_reflp__def,fact_refl__onI,fact_fold1__Un,fact_reflpE,fact_fold1__singleton__def,fact_fold1__singleton,fact_folding__one_Oeq__fold,fact_fold1__def,fact_Sup__fin_OF__eq,fact_Inf__fin_OF__eq,fact_Min_OF__eq,fact_Max_OF__eq,fact_min__max_OInf__fin_OF__eq,fact_min__max_OSup__fin_OF__eq,fact_fold1__belowI,fact_below__fold1__iff,fact_min__max_Ofold1__belowI,fact_fold1__insert__idem,fact_min__max_Obelow__fold1__iff,fact_fold1__below__iff,fact_fold1__Un2,fact_fold1__strict__below__iff,fact_strict__below__fold1__iff,fact_fold1__insert,fact_fold1__antimono,fact_semilattice__big_OF__eq,fact_fold1__in,fact_hom__fold1__commute,fact_wfP__def,fact_Option_Omap__def,fact_setprod__pos__nat,fact_wfP__empty,fact_Option_Omap_Ocomp,fact_Option_Omap_Ocompositionality,fact_option__map__comp,fact_option__map__o__empty,fact_Option_Omap_Oid,fact_Option_Omap_Oidentity,fact_dom__option__map,fact_accp__wfPD,fact_wfP__accp__iff,fact_option__map__is__None,fact_option__map__None,fact_option__map__eq__Some,fact_option__map__Some,fact_wfP__subset,fact_option__map__o__map__upd,fact_wf__in__rel,fact_wfP__wf__eq,fact_wfP__acyclicP,fact_folding__one__idem_Ohom__commute,fact_Rep__Integ__cases,fact_acyclic__subset,fact_wf__acyclic,fact_wf__iff__acyclic__if__finite,fact_finite__acyclic__wf,fact_Nitpick_Owf_H__def,fact_Rep__Integ__induct,fact_folding__image__simple_Ounion__inter__neutral,fact_pigeonhole__infinite,fact_refl__on__def_H,fact_Abs__Integ__cases,fact_ball__empty,fact_Powp__def,fact_congruent__def,fact_Abs__Integ__induct,fact_finite__range__map__of__map__add,fact_finite__dom__map__of,fact_triples__valid__Suc,fact_finite__range__map__of,fact_hoare__valids__def,fact_map__add__map__of__foldr,fact_map__of__mapk__SomeI,fact_map__of__map,fact_inj__mapI,fact_foldr__map,fact_map__injective,fact_inj__mapD,fact_inj__map__eq__map,fact_inj__map,fact_map__ident,fact_map__map,fact_List_Omap_Ocompositionality,fact_map__comp__map,fact_List_Omap_Ocomp,fact_List_Omap_Oid,fact_List_Omap_Oidentity,fact_map__of__map__restrict,fact_map__of_Osimps_I2_J,fact_finite__set,fact_set__map,fact_map_Osimps_I2_J,fact_map__eq__conv,fact_set__ConsD,fact_infinite__UNIV__listI,fact_list_Oinject,fact_not__Cons__self2,fact_not__Cons__self,fact_set__subset__Cons,fact_List_Oset_Osimps_I2_J,fact_foldr_Osimps_I2_J,fact_map__inj__on,fact_inj__on__map__eq__map,fact_map__fun__upd,fact_map__of__Cons__code_I2_J,fact_map__of__eq__dom,fact_map__of__SomeD,fact_map__of__is__SomeD,fact_dom__map__of__conv__image__fst,fact_map__of__eq__None__iff,fact_map__of__map__keys,fact_set__Cons__def,fact_the_Osimps,fact_product__list__set,fact_ran__distinct,fact_distinct__product,fact_distinct_Osimps_I2_J,fact_distinct__map,fact_map__of__inject__set,fact_Some__eq__map__of__iff,fact_map__of__eq__Some__iff,fact_map__of__is__SomeI,fact_set__map__of__compr,fact_finite__lists__length__le,fact_list_Osize_I2_J,fact_list__size__map,fact_length__map,fact_map__eq__imp__length__eq,fact_neq__if__length__neq,fact_lexn__length,fact_impossible__Cons,fact_card__length,fact_card__distinct,fact_distinct__card,fact_lexn_Osimps_I2_J,fact_length__pos__if__in__set,fact_list_Osize_I4_J,fact_Cons__in__lex,fact_lenlex__conv,fact_lenlex__def,fact_list__size__estimation,fact_list__size__estimation_H,fact_finite__lists__length__eq,fact_length__sublists,fact_length__sublist,fact_distinct__sublistI,fact_notin__set__sublistI,fact_in__set__sublistD,fact_set__sublist__subset,fact_distinct__set__sublists,fact_sublists__powset,fact_set__n__lists,fact_lexord__cons__cons,fact_distinct__n__lists,fact_length__n__lists__elem,fact_length__n__lists,fact_lexord__lex,fact_listrel__Cons,fact_greaterThanLessThan__upto,fact_atLeastAtMost__upto,fact_set__upto,fact_distinct__upto,fact_listrel__mono,fact_listrel__eq__len,fact_atLeastLessThan__upto,fact_greaterThanAtMost__upto,fact_listrel_OCons,fact_nat__list__def,fact_listrelp__listrel__eq,fact_listrelp_Oequations_I2_J,fact_listrelp_OCons,fact_listrel__iff__zip,fact_listrel__Cons2,fact_length__zip,fact_zip__same__conv__map,fact_distinct__zipI1,fact_distinct__zipI2,fact_map__of__zip__inject,fact_map__fst__zip,fact_map__snd__zip,fact_zip__map__fst__snd,fact_zip__Cons__Cons,fact_zip__eq__conv,fact_map__zip__map,fact_map__zip__map2,fact_list__eq__iff__zip__eq,fact_in__set__zipE,fact_set__zip__rightD,fact_set__zip__leftD,fact_zip__same,fact_map__of__zip__is__None,fact_map__of__zip__is__Some,fact_zip__map__map,fact_zip__map1,fact_zip__map2,fact_dom__map__of__zip,fact_map__of__zip__upd,fact_map__of__zip__map,fact_listrel__Cons1,fact_map__of__zip__enum__inject,fact_enum__prod__def,fact_enum__option__def,fact_enum__distinct,fact_in__enum,fact_UNIV__enum,fact_enum__UNIV,fact_enum__fun__code,fact_enum__fun__def,fact_enum__all__fun__code,fact_enum__all__fun__def,fact_all__n__lists__def,fact_enum__ex__fun__code,fact_enum__ex__fun__def,fact_ex__n__lists__def,fact_set__zip,fact_listrel__subset,fact_nth__zip,fact_list__eq__iff__nth__eq,fact_lists__mono,fact_nth__Cons__0,fact_nth__Cons__Suc,fact_nth_Osimps,fact_all__set__conv__all__nth,fact_nth__map,fact_nth__eq__iff__index__eq,fact_distinct__conv__nth,fact_lists__UNIV,fact_equiv__listrel,fact_listrel__refl__on,fact_in__set__conv__nth,fact_nth__mem,fact_nth__Cons_H,fact_set__conv__nth,fact_Cons__in__lists__iff,fact_in__lists__conv__set,fact_nth__Cons__number__of,fact_lists__eq__set,fact_set__sublist,fact_listrel__iff__nth,fact_lexord__take__index__conv,fact_distinct__list__update,fact_nth__list__update__neq,fact_list__update__id,fact_nth__take,fact_map__update,fact_take__map,fact_take__Suc__Cons,fact_list__update_Osimps_I2_J,fact_list__update__code_I2_J,fact_list__update__code_I3_J,fact_update__zip,fact_take__zip,fact_zip__update,fact_in__set__takeD,fact_take__take,fact_list__update__overwrite,fact_list__update__swap,fact_distinct__take,fact_set__take__subset,fact_take__all,fact_list__update__beyond,fact_length__take,fact_length__list__update,fact_sublist__upt__eq__take,fact_set__take__subset__set__take,fact_set__update__subsetI,fact_set__update__subset__insert,fact_nth__list__update__eq,fact_list__update__same__conv,fact_nth__list__update,fact_set__update__memI,fact_map__upd__upds__conv__if,fact_listrel1__subset__listrel,fact_Cons__acc__listrel1I,fact_map__add__upds,fact_map__upds__apply__nontin,fact_listrel1__mono,fact_listrel1I2,fact_listrel1__eq__len,fact_map__upds__Cons,fact_lists__accI,fact_lists__accD,fact_map__upds__list__update2__drop,fact_map__upds__twist,fact_listrel1I1,fact_Cons__listrel1__Cons,fact_restrict__map__upds,fact_dom__map__upds,fact_listrel1__iff__update,fact_map__of__zip__enum__is__Some,fact_lexord__linear,fact_lexord__irreflexive,fact_inj__on__mapI,fact_weak__map__of__SomeI,fact_UnionI,fact_Union__quotient,fact_Union__insert,fact_Sigma__Union,fact_Union__disjoint,fact_Int__Union2,fact_Int__Union,fact_Domain__Union,fact_Range__Union,fact_Union__def,fact_UN__simps_I8_J,fact_UN__extend__simps_I8_J,fact_vimage__Union,fact_less__Sup__iff,fact_Union__Pow__eq,fact_Field__Union,fact_image__Union,fact_Union__empty,fact_Union__upper,fact_Sup__le__iff,fact_Union__mono,fact_finite__UnionD,fact_subset__Pow__Union,fact_Union__UNIV,fact_Union__Un__distrib,fact_Union__image__eq,fact_UNION__eq__Union__image,fact_Sup__upper,fact_Sup__empty,fact_Sup__singleton,fact_Sup__insert,fact_Sup__UNIV,fact_Un__eq__Union,fact_Un__Union__image,fact_Union__Int__subset,fact_Sup__binary,fact_Sup__fin__Sup,fact_finite__Union,fact_insert__partition,fact_listsum__setsum__nth,fact_list__size__pointwise,fact_listsum__eq__0__nat__iff__nat,fact_elem__le__listsum__nat,fact_listsum__simps_I2_J,fact_listsum__0,fact_listsum__addf,fact_listsum__const__mult,fact_listsum__mult__const,fact_listsum__subtractf,fact_listsum__update__nat,fact_listsum__abs,fact_uminus__listsum__map,fact_list__size__conv__listsum,fact_distinct__listsum__conv__Setsum,fact_listsum__distinct__conv__setsum__set,fact_setsum__set__upto__conv__listsum__int,fact_interv__listsum__conv__setsum__set__int,fact_listsum__triv,fact_Nitpick_Osetsum_H__def,fact_listsum__mono,fact_someI,fact_tfl__some,fact_some__sym__eq__trivial,fact_some__eq__trivial,fact_some__eq__ex,fact_someI__ex,fact_exE__some,fact_Nitpick_Ocard_H__def,fact_butlast__take,fact_map__butlast,fact_in__set__butlastD,fact_Eps__split__eq,fact_split__paired__Eps,fact_take__butlast,fact_length__butlast,fact_Eps__split,fact_butlast__conv__take,fact_butlast__list__update,fact_nth__take__lemma,fact_length__transpose,fact_transpose__map__map,fact_nth__transpose,fact_listsum__map__remove1,fact_filter__map,fact_filter__is__subset,fact_length__filter__le,fact_filter__id__conv,fact_sum__length__filter__compl,fact_remove1_Osimps_I2_J,fact_filter_Osimps_I2_J,fact_filter__filter,fact_filter__remove1,fact_remove1__commute,fact_remove1__filter__not,fact_distinct__remove1,fact_distinct__filter,fact_remove1__idem,fact_notin__set__remove1,fact_in__set__remove1,fact_set__remove1__subset,fact_set__filter,fact_length__filter__map,fact_length__filter__less,fact_set__minus__filter__out,fact_filter__in__sublist,fact_length__filter__conv__card,fact_length__remove1,fact_set__remove1__eq,fact_map__filter__def,fact_map__filter__map__filter,fact_map__of__filter__in,fact_map__filter__simps_I1_J,fact_sublist__shift__lemma__Suc,fact_sorted__list__of__set__remove,fact_transpose__max__length,fact_lists_ONil,fact_listrel__Nil1,fact_listrel__Nil2,fact_filter__empty__conv,fact_filter_Osimps_I1_J,fact_map__filter__simps_I2_J,fact_transpose_Osimps_I1_J,fact_foldr_Osimps_I1_J,fact_transpose_Osimps_I2_J,fact_transpose__empty,fact_listsum__simps_I1_J,fact_list_Osize_I3_J,fact_length__0__conv,fact_set__empty,fact_set__empty2,fact_List_Oset_Osimps_I1_J,fact_list__update__code_I1_J,fact_list__update_Osimps_I1_J,fact_list__update__nonempty,fact_list_Osize_I1_J,fact_take__0,fact_take__eq__Nil,fact_take__Nil,fact_map__upds__Nil2,fact_map__upds__Nil1,fact_n__lists_Osimps_I1_J,fact_n__lists__Nil,fact_list_Osimps_I3_J,fact_list_Osimps_I2_J,fact_sublists_Osimps_I1_J,fact_zip_Osimps_I1_J,fact_zip__Nil,fact_sorted__list__of__set__empty,fact_sublist__nil,fact_product_Osimps_I1_J,fact_listrelp_ONil,fact_listrelp_Oequations_I1_J,fact_distinct_Osimps_I1_J,fact_map__of__Cons__code_I1_J,fact_upto__empty,fact_distinct__butlast,fact_butlast_Osimps_I1_J,fact_butlast_Osimps_I2_J,fact_remove1_Osimps_I1_J,fact_map__is__Nil__conv,fact_map_Osimps_I1_J,fact_Nil__is__map__conv,fact_sublist__empty,fact_map__of_Osimps_I1_J,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_take__Cons__number__of,fact_transpose__aux__max,fact_upto_Opsimps,fact_sublist__def,fact_upt__rec,fact_upt__0,fact_sorted__list__of__set__range,fact_upt__conv__Nil,fact_upt__eq__Nil__conv,fact_distinct__upt,fact_upt__conv__Cons,fact_take__upt,fact_atLeastLessThan__upt,fact_set__upt,fact_length__upt,fact_upt__rec__number__of,fact_upt__eq__Cons__conv,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_interv__listsum__conv__setsum__set__nat,fact_setsum__set__upt__conv__listsum__nat,fact_nth__map__upt,fact_sublist__shift__lemma,fact_transpose__rectangle,fact_anamorph_Osimps,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_transpose_Opsimps_I2_J,fact_upto_Opinduct,fact_transpose_Opsimps_I1_J,fact_transfer__nat__int__list__functions_I2_J,fact_map__upds__append1,fact_append1__eq__conv,fact_Cons__eq__append__conv,fact_append__eq__Cons__conv,fact_Cons__eq__appendI,fact_append__Cons,fact_map__append,fact_filter__append,fact_zip__append,fact_map__of__append,fact_append__eq__appendI,fact_append__same__eq,fact_same__append__eq,fact_append__eq__append__conv2,fact_append__assoc,fact_append__in__lists__conv,fact_fun__upds__append__drop,fact_fun__upds__append2__drop,fact_set__append,fact_length__append,fact_listsum__append,fact_foldr__append,fact_butlast__append,fact_eq__Nil__appendI,fact_append__self__conv2,fact_append__self__conv,fact_append__is__Nil__conv,fact_self__append__conv2,fact_self__append__conv,fact_append__Nil2,fact_Nil__is__append__conv,fact_append__Nil,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_upt__add__eq__append,fact_butlast__snoc,fact_append__listrel1I,fact_lexord__append__leftI,fact_return__list__def,fact_distinct__append,fact_nth__append,fact_list__update__append,fact_sublists_Osimps_I2_J,fact_product_Osimps_I2_J,fact_sublist__append,fact_upt__Suc__append,fact_upt__Suc,fact_listrel1I,fact_lexord__append__left__rightI,fact_take__Suc__conv__app__nth,fact_snoc__listrel1__snoc__iff,fact_sublist__Cons,fact_transfer__nat__int__list__return__embed,fact_listrel1E,fact_embed__list__def,fact_transfer__nat__int__list__functions_I1_J,fact_lexord__append__leftD,fact_rotate1__def,fact_distinct1__rotate,fact_set__rotate1,fact_length__rotate1,fact_rotate1__is__Nil__conv,fact_rotate__simps,fact_rotate1__length01,fact_listsum__map__filter,fact_partition__filter__conv,fact_partition__filter1,fact_partition__P,fact_partition_Osimps_I1_J,fact_partition_Osimps_I2_J,fact_partition__filter2,fact_partition__set,fact_transpose_Opsimps_I3_J,fact_upd__conv__take__nth__drop,fact_drop__1__Cons,fact_drop__Suc__Cons,fact_nth__via__drop,fact_drop__take,fact_take__drop,fact_distinct__drop,fact_drop__zip,fact_butlast__drop,fact_drop__butlast,fact_drop__drop,fact_drop__0,fact_in__set__dropD,fact_length__drop,fact_set__drop__subset,fact_drop__upt,fact_drop__Nil,fact_drop__map,fact_append__take__drop__id,fact_concat_Osimps_I1_J,fact_concat_Osimps_I2_J,fact_Nil__eq__concat__conv,fact_concat__eq__Nil__conv,fact_map__concat,fact_filter__concat,fact_set__drop__subset__set__drop,fact_drop__eq__Nil,fact_drop__all,fact_drop__append,fact_append__eq__conv__conj,fact_length__concat,fact_drop__Cons,fact_set__concat,fact_concat__append,fact_drop__Cons_H,fact_nth__drop,fact_append__eq__append__conv__if,fact_nth__drop_H,fact_transpose_Osimps_I3_J,fact_drop__Cons__number__of,fact_take__add,fact_concat__eq__concat__iff,fact_concat__injective,fact_concat__map__singleton,fact_zip__append1,fact_zip__append2,fact_n__lists_Osimps_I2_J,fact_id__take__nth__drop,fact_transpose__aux__filter__tail,fact_transpose__aux__filter__head,fact_drop__tl,fact_tl__drop,fact_map__tl,fact_tl_Osimps_I1_J,fact_distinct__tl,fact_hd_Osimps,fact_tl_Osimps_I2_J,fact_take__Suc,fact_tl__append2,fact_rotate1__hd__tl,fact_take__tl,fact_drop__Suc,fact_hd__map,fact_hd__append,fact_hd__append2,fact_hd__upt,fact_tl__append,fact_length__tl,fact_hd__in__set,fact_tl__take,fact_hd__conv__nth,fact_hd__drop__conv__nth,fact_take__hd__drop,fact_length__remdups__concat,fact_fold1__set,fact_distinct__remdups,fact_length__remdups__leq,fact_foldl__map,fact_remdups__map__remdups,fact_set__remdups,fact_foldl__Cons,fact_distinct__remdups__id,fact_remdups__id__iff__distinct,fact_remdups__filter,fact_foldr__conv__foldl,fact_start__le__sum,fact_foldl__absorb0,fact_foldl__assoc,fact_remdups__remdups,fact_length__remdups__eq,fact_foldl__Nil,fact_remdups__eq__nil__iff,fact_remdups__eq__nil__right__iff,fact_remdups_Osimps_I1_J,fact_foldl__append,fact_foldl__conv__concat,fact_remove1__remdups,fact_listsum__foldl,fact_concat__conv__foldl,fact_foldl__foldr1__lemma,fact_foldl__foldr1,fact_sum__eq__0__conv,fact_remdups_Osimps_I2_J,fact_length__remdups__card__conv,fact_Sup__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_map__upds__fold__map__upd,fact_elem__le__sum,fact_hd__rotate__conv__nth,fact_rotate__drop__take,fact_rotate1__rotate__swap,fact_rotate__is__Nil__conv,fact_length__rotate,fact_rotate__rotate,fact_distinct__rotate,fact_set__rotate,fact_rotate__map,fact_rotate__conv__mod,fact_rotate__Suc,fact_rotate0,fact_rotate__add,fact_rotate__id,fact_rotate__length01,fact_lexord__append__rightI,fact_sorted__list__of__set__insert,fact_set__insort,fact_insort__key_Osimps_I1_J,fact_insort__key_Osimps_I2_J,fact_filter__insort__triv,fact_remove1__insort,fact_insort__key__left__comm,fact_insort__left__comm,fact_length__insort,fact_insort__not__Nil,fact_distinct__insort,fact_insort__key__remove1,fact_insort__insert__insort__key,fact_sorted_ONil,fact_sorted__single,fact_sorted__insort__key,fact_sorted__insort,fact_sorted__remdups,fact_sorted__map__same,fact_sorted_Oequations_I1_J,fact_sorted__butlast,fact_sorted__upt,fact_sorted__upto,fact_sorted__insort__insert,fact_sorted__remove1,fact_sorted__same,fact_distinct__insort__insert,fact_sorted__take,fact_sorted__many,fact_sorted__many__eq,fact_sorted__distinct__set__unique,fact_sorted__tl,fact_sorted__filter,fact_sorted__insort__insert__key,fact_sorted__map__remove1,fact_sorted__drop,fact_sorted__Cons,fact_sorted__append,fact_filter__insort,fact_sorted_Oequations_I2_J,fact_insort__insert__triv,fact_set__insort__insert,fact_sorted__list__of__set,fact_insort__remove1,fact_sorted__nth__mono,fact_sorted__equals__nth__mono,fact_map__sorted__distinct__set__unique,fact_insort__insert__key__triv,fact_insort__insert__insort,fact_transpose__column,fact_nth__nth__transpose__sorted,fact_inj__on__rev,fact_rev__concat,fact_rev__map,fact_set__rev,fact_zip__rev,fact_singleton__rev__conv,fact_rev__singleton__conv,fact_distinct__rev,fact_rev__filter,fact_rev__is__rev__conv,fact_rev__swap,fact_rev__rev__ident,fact_length__rev,fact_listsum__rev,fact_rev__is__Nil__conv,fact_Nil__is__rev__conv,fact_rev_Osimps_I1_J,fact_rev__append,fact_foldl__foldr,fact_foldr__foldl,fact_rev__eq__Cons__iff,fact_rev_Osimps_I2_J,fact_sorted__transpose,fact_rev__foldl__cons,fact_rev__take,fact_rev__drop,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_sorted__nth__monoI,fact_sorted__takeWhile,fact_takeWhile__tail,fact_takeWhile_Osimps_I1_J,fact_length__takeWhile__le,fact_takeWhile__eq__take,fact_distinct__takeWhile,fact_takeWhile_Osimps_I2_J,fact_set__takeWhileD,fact_takeWhile__eq__all__conv,fact_zip__takeWhile__fst,fact_zip__takeWhile__snd,fact_takeWhile__map,fact_takeWhile__append1,fact_takeWhile__nth,fact_nth__length__takeWhile,fact_map__upds__def,fact_filter__equals__takeWhile__sorted__rev,fact_takeWhile__neq__rev,fact_dropWhile__neq__rev,fact_length__dropWhile__le,fact_dropWhile_Osimps_I2_J,fact_distinct__dropWhile,fact_dropWhile_Osimps_I1_J,fact_dropWhile__eq__Nil__conv,fact_sorted__dropWhile,fact_takeWhile__dropWhile__id,fact_hd__dropWhile,fact_dropWhile__map,fact_dropWhile__append1,fact_dropWhile__eq__Cons__conv,fact_dropWhile__eq__drop,fact_dropWhile__nth,fact_sort__foldl__insort,fact_lexord__Nil__left,fact_sorted__sort,fact_sort__key__simps_I1_J,fact_length__sort,fact_filter__sort,fact_distinct__sort,fact_set__sort,fact_sorted__sort__key,fact_sort__key__simps_I2_J,fact_sorted__list__of__set__sort__remdups,fact_last__list__update,fact_takeWhile__eq__filter,fact_last__map,fact_last__append,fact_last__appendR,fact_last__appendL,fact_last__ConsL,fact_last__ConsR,fact_last_Osimps,fact_last__in__set,fact_last__snoc,fact_last__drop,fact_last__rev,fact_hd__rev,fact_last__upt,fact_snoc__eq__iff__butlast,fact_append__butlast__last__id,fact_takeWhile__not__last,fact_last__conv__nth,fact_lists_Osimps,fact_takeWhile__eq__take__P__nth,fact_length__takeWhile__less__P__nth,fact_INFI__set__fold,fact_INT__D,fact_INT__E,fact_INF1__E,fact_INF1__D,fact_INF2__D,fact_INF2__E,fact_finite__INT,fact_INF__subset,fact_UN__extend__simps_I7_J,fact_UN__simps_I7_J,fact_INT__extend__simps_I9_J,fact_INT__simps_I9_J,fact_Compl__UN,fact_Compl__INT,fact_Collect__ball__eq,fact_INFI__bool__eq,fact_INF__INT__eq2,fact_le__INF__iff,fact_INT__subset__iff,fact_INT__lower,fact_Image__INT__subset,fact_INF__commute,fact_INFI__apply,fact_Pow__INT__eq,fact_INT__simps_I7_J,fact_INT__simps_I6_J,fact_INT__extend__simps_I7_J,fact_Un__INT__distrib,fact_INT__extend__simps_I6_J,fact_Un__INT__distrib2,fact_INF__less__iff,fact_vimage__INT,fact_INTER__UNIV__conv_I2_J,fact_INTER__UNIV__conv_I1_J,fact_INT__Int__distrib,fact_INT__Un,fact_INT__iff,fact_INT__absorb,fact_INF__INT__eq,fact_INT__insert__distrib,fact_INT__insert,fact_INT__extend__simps_I1_J,fact_INT__extend__simps_I2_J,fact_INT__constant,fact_INT__empty,fact_INF__const,fact_INT__simps_I5_J,fact_INT__extend__simps_I5_J,fact_INT__extend__simps_I8_J,fact_INT__simps_I8_J,fact_INT__extend__simps_I10_J,fact_INT__simps_I10_J,fact_INTER__def,fact_INT__simps_I2_J,fact_INT__simps_I1_J,fact_INT__simps_I3_J,fact_INT__extend__simps_I3_J,fact_INT__extend__simps_I4_J,fact_INF__leI,fact_INT__greaterThan__UNIV,fact_INT__simps_I4_J,fact_lists__Int__eq,fact_lists__IntI,fact_listsp_ONil,fact_INF2__iff,fact_INF1__iff,fact_append__in__listsp__conv,fact_listsp_Oequations_I1_J,fact_listsp__infI,fact_listsp__inf__eq,fact_listsp__conj__eq,fact_listsp_Oequations_I2_J,fact_in__listsp__conv__set,fact_listsp__mono,fact_listsp__lists__eq,fact_image__INT,fact_Sup__Inf,fact_finite__Inter,fact_InterE,fact_InterD,fact_Inter__def,fact_Inter__image__eq,fact_INTER__eq__Inter__image,fact_Inter__insert,fact_Inter__Un__distrib,fact_Inf__singleton,fact_Inf__empty,fact_Inf__UNIV,fact_Inf__insert,fact_Inf__lower,fact_Inter__eq,fact_Inter__anti__mono,fact_Inter__empty,fact_le__Inf__iff,fact_Inter__lower,fact_Inf__less__iff,fact_Inter__UNIV,fact_Un__Inter,fact_Int__eq__Inter,fact_Int__Inter__image,fact_Inter__Un__subset,fact_Inf__binary,fact_Inf__fin__Inf,fact_Inf__set__fold,fact_Inf__Sup,fact_list__all2__def,fact_sorted_Osimps,fact_list__all2__appendI,fact_list__all2__append,fact_list__all2__Nil,fact_list__all2__Nil2,fact_list__all2__lengthD,fact_list__all2__eq,fact_list__all2__takeI,fact_list__all2__Cons,fact_list__all2__map2,fact_list__all2__map1,fact_list__all2__dropI,fact_list__all2__rev1,fact_list__all2__rev,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_list__all2I,fact_card__partition,fact_all__nth__imp__all__set,fact_map__removeAll__inj__on,fact_removeAll__append,fact_removeAll_Osimps_I1_J,fact_removeAll__filter__not,fact_removeAll__filter__not__eq,fact_distinct__removeAll,fact_removeAll_Osimps_I2_J,fact_removeAll__id,fact_distinct__remove1__removeAll,fact_map__removeAll__inj,fact_set__removeAll,fact_not__in__set__insert,fact_List_Oinsert__def,fact_distinct__insert,fact_insert__remdups,fact_in__set__insert,fact_List_Oset__insert,fact_insert__Nil,fact_concat__map__maps,fact_maps__def,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_measures__less,fact_in__measures_I2_J,fact_inj__on__Inter,fact_Inter__subset,fact_foldl__apply,fact_inj__on__INTER,fact_zip__obtain__same__length,fact_map__of__eqI,fact_finite__UN__I,fact_inj__on__diff__nat,fact_wfP__SUP,fact_dropWhile__append2,fact_list__all2__all__nthI,fact_finite__map__freshness,fact_mem__splitI2,fact_mem__splitE,fact_finite__sorted__distinct__unique,fact_setsum__SucD,fact_nat__mod__eq__lemma,fact_takeWhile__append2,fact_insort__is__Cons,fact_wfI__pf,fact_Cons__eq__filter__iff,fact_filter__eq__Cons__iff,fact_Sigma__mono,fact_acc_OaccI,fact_not__acc__down,fact_fold__image__1,fact_card_Oneutral,fact_max__ext_Osimps,fact_list__ball__nth,fact_mod__induct__0,fact_sorted_OCons,fact_InterI,fact_fold__image__cong,fact_Max__eqI,fact_Min__eqI,fact_wf__no__infinite__down__chainE,fact_list__ex__length,fact_scomp__unfold,fact_list__ex__simps_I1_J,fact_list__ex__append,fact_scomp__scomp,fact_scomp__Pair,fact_Pair__scomp,fact_list__ex__iff,fact_scomp__apply,fact_scomp__def,fact_list__ex__rev,fact_list__ex__simps_I2_J,fact_iterate_Osimps,fact_setsum__ivl__cong,fact_log_Osimps,fact_minus__shift__def,fact_inc__shift__def,fact_select,fact_select__weight__member,fact_select__weigth__select,fact_select__weight__cons__zero,fact_select__weigth__drop__zero,fact_pick__member,fact_pick_Osimps,fact_pick__drop__zero,fact_select__weight__def,fact_pick__same,fact_number__of__code__numeral__def,fact_code__numeral_Oof__nat__inject,fact_Code__Numeral_Oof__nat__inject,fact_times__code__numeral__code,fact_Code__Numeral_Oof__nat__code,fact_zero__code__numeral__def,fact_one__code__numeral__def,fact_less__eq__code__numeral__code,fact_plus__code__numeral__code,fact_less__code__numeral__code,fact_code__numeral__not__eq__zero,fact_range,fact_select__def,fact_subtract__code__numeral__code,fact_type__definition__code__numeral,fact_nat__of__of__nat,fact_of__nat__nat__of,fact_nat__of__inverse,fact_times__code__numeral__def,fact_less__code__numeral__def,fact_code__numeral_Onat__of__inject,fact_Code__Numeral_Onat__of__inject,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_New__DSequence_Opos__not__seq__def,fact_less__eq,fact_wf__trancl,fact_less__than__def,fact_acyclic__def,fact_trancl_Or__into__trancl,fact_trancl__subset__Field2,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_trancl__Int__subset,fact_trancl__insert,fact_reflcl__set__eq,fact_r__into__rtrancl,fact_rtrancl_Ortrancl__refl,fact_IdI,fact_trancl__into__rtrancl,fact_listrel__rtrancl__refl,fact_trancl__unfold__right,fact_trancl__unfold__left,fact_trancl__reflcl,fact_reflcl__trancl,fact_trancl__rtrancl__absorb,fact_rtrancl__trancl__absorb,fact_rtrancl__eq__or__trancl,fact_rtrancl__into__trancl2,fact_rtranclD,fact_rtrancl__into__trancl1,fact_trancl__rtrancl__trancl,fact_rtrancl__trancl__trancl,fact_rtrancl__trans,fact_rtrancl_Ortrancl__into__rtrancl,fact_converse__rtrancl__into__rtrancl,fact_Image__closed__trancl,fact_rtrancl__Un__subset,fact_rtrancl__mono,fact_rtrancl__subset,fact_rtrancl__subset__rtrancl,fact_rtrancl__Int__subset,fact_refl__rtrancl,fact_rtrancl__idemp,fact_rtrancl__reflcl__absorb,fact_rtrancl__Un__rtrancl,fact_rtrancl__reflcl,fact_rtrancl__unfold,fact_r__comp__rtrancl__eq,fact_rtrancl__idemp__self__comp,fact_rtrancl__r__diff__Id,fact_Range__rtrancl,fact_Domain__rtrancl,fact_in__rtrancl__UnI,fact_rtrancl__empty,fact_Domain__Id,fact_listrel__rtrancl__eq__rtrancl__listrel1,fact_Image__Id,fact_Id__O__R,fact_R__O__Id,fact_Range__Id,fact_refl__Id,fact_listrel1__rtrancl__subset__rtrancl__listrel1,fact_pair__in__Id__conv,fact_listrel__rtrancl__trans,fact_rtrancl__listrel1__ConsI2,fact_listrel__subset__rtrancl__listrel1,fact_pair__leq__def,fact_Not__Domain__rtrancl,fact_acc__downwards,fact_acc__downwards__aux,fact_wf__insert,fact_rtrancl__listrel1__ConsI1,fact_rtrancl__listrel1__eq__len,fact_acyclic__insert,fact_listrel__reflcl__if__listrel1,fact_rtrancl__listrel1__if__listrel,fact_refl__reflcl,fact_Id__def,fact_irrefl__diff__Id,fact_pred__nat__trancl__eq__le,fact_trancl__subset__Sigma__aux,fact_irrefl__tranclI,fact_sequence__trans,fact_rtrancl__converseD,fact_rtrancl__converseI,fact_rtrancl__converse,fact_converse__Id,fact_in__listrel1__converse,fact_converse__iff,fact_converseI,fact_converseD,fact_converse__inv__image,fact_converse__INTER,fact_converse__Int,fact_converse__UNION,fact_refl__on__converse,fact_finite__converse,fact_acyclic__converse,fact_converse__Id__on,fact_Field__converse,fact_converse__converse,fact_converse__Un,fact_converse__rel__comp,fact_listrel1__converse,fact_equiv__comp__eq,fact_Range__def,fact_Domain__converse,fact_Range__converse,fact_trancl__converseD,fact_trancl__converseI,fact_wf__converse__trancl,fact_trancl__converse,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_total__on__diff__Id,fact_single__valued__Id,fact_total__on__converse,fact_single__valued__rel__comp,fact_single__valued__Id__on,fact_total__on__empty,fact_single__valued__subset,fact_single__valuedD,fact_single__valued__def,fact_total__on__def,fact_single__valued__confluent,fact_Image__Int__eq,fact_rtrancl__imp__UN__rel__pow,fact_acyclicI,fact_single__valued__rel__pow,fact_funpow_Osimps_I2_J,fact_funpow__add,fact_comp__funpow,fact_wf__exp,fact_funpow__swap1,fact_funpow__mult,fact_rel__pow__commute,fact_relpow_Osimps_I2_J,fact_rel__pow__1,fact_rel__pow__add,fact_rel__pow__Suc__I,fact_rel__pow__Suc__I2,fact_rel__pow__0__E,fact_rel__pow__0__I,fact_rtrancl__power,fact_rel__pow__imp__rtrancl,fact_relpow_Osimps_I1_J,fact_funpow_Osimps_I1_J,fact_trancl__power,fact_rtrancl__is__UN__rel__pow,fact_funpow__code__def,fact_rel__pow__E,fact_rotate__def,fact_rel__pow__E2,fact_pos__not__random__dseq__def,fact_rtrancl__Un__separatorE,fact_rtrancl__Un__separator__converseE,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_in__set__conv__decomp,fact_in__set__conv__decomp__first,fact_in__set__conv__decomp__last,fact_min__max_OSup__fin_Oeq__fold_H,fact_min__max_OInf__fin_Oeq__fold_H,fact_sup__SUPR__fold__sup,fact_inf__INFI__fold__inf,fact_sup__Sup__fold__sup,fact_union__fold__insert,fact_fold__sup__insert,fact_inf__Inf__fold__inf,fact_fold__def,fact_fold__empty,fact_fold__image__def,fact_folding_Oeq__fold,fact_min__max_Ofold__sup__insert,fact_min__max_Ofold__inf__insert,fact_fold__inf__insert,fact_fun__left__comm__idem_Ofold__insert__idem,fact_fun__left__comm__idem_Ofold__insert__idem2,fact_folding__one__idem_Oeq__fold__idem_H,fact_fun__left__comm__idem_Ofold__set,fact_sup__le__fold__sup,fact_fold__inf__le__inf,fact_min__max_Ofold__inf__le__inf,fact_min__max_Osup__le__fold__sup,fact_Sup__fold__sup,fact_Inf__fold__inf,fact_fold1__eq__fold__idem,fact_Sup__fin_Oeq__fold__idem_H,fact_Inf__fin_Oeq__fold__idem_H,fact_Min_Oeq__fold__idem_H,fact_Max_Oeq__fold__idem_H,fact_min__max_OInf__fin_Oeq__fold__idem_H,fact_min__max_OSup__fin_Oeq__fold__idem_H,fact_minus__fold__remove,fact_folding__one_Oeq__fold_H,fact_SUPR__fold__sup,fact_INFI__fold__inf,fact_fold1__eq__fold,fact_Sup__fin_Oeq__fold_H,fact_Inf__fin_Oeq__fold_H,fact_Min_Oeq__fold_H,fact_Max_Oeq__fold_H,fact_fun__left__comm_Ofold__rec,fact_fun__left__comm_Ofold__insert__remove,fact_fun__left__comm_Ofold__fun__comm,fact_fun__left__comm_Ofun__comp__comm,fact_fun__left__comm_Ofold__graph__determ,fact_fun__left__comm_Ofun__left__comm,fact_fun__left__comm_Ofun__left__comm__apply,fact_fun__left__comm__insort,fact_fun__left__comm,fact_fun__left__comm_Ofold__equality,fact_fun__left__comm_Ofold__graph__fold,fact_fun__left__comm_Ofold__insert2,fact_fun__left__comm_Ofold__insert,fact_fun__left__comm_Ofold__set__remdups,fact_fun__left__comm_Ofold__graph__insertE__aux,fact_fun__left__comm_Ofold__graph__insertE,fact_min__max_Ofold__sup__le__sup,fact_min__max_Oinf__le__fold__inf,fact_inf__le__fold__inf,fact_fold__sup__le__sup,fact_mod__div__decomp,fact_wf__eq__minimal,fact_folding__image__simple__idem_Ounion__idem,fact_transfer__nat__int__set__cong,fact_folding__image__simple__idem_Oidem,fact_folding__image__simple__idem_Oin__idem,fact_folding__image__simple__idem_Oinsert__idem,fact_folding__image__simple__idem_Osubset__idem,fact_UnionE,fact_option_Orecs_I2_J,fact_option_Orecs_I1_J,fact_converseE,fact_rel__compE,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_Odenom__def,fact_Nitpick_Onum__def,fact_list__all__length,fact_internal__split__def,fact_list__all__simps_I1_J,fact_list__all__append,fact_list__all__iff,fact_list__all__rev,fact_list__all__simps_I2_J,fact_Ball__set__list__all,fact_list__all__iff__raw,fact_internal__split__conv,fact_list__ex1__simps_I2_J,fact_setprod__nonneg,fact_list__ex1__simps_I1_J,fact_exists1__code,fact_list__ex1__iff,fact_bool_Osize_I1_J,fact_bool_Osize_I2_J,fact_finite__less__ub,fact_finite__induct,fact_measure__function__int,fact_equal__fun__def,fact_measure__fst,fact_is__measure_Ointros,fact_is__measure_Oequations,fact_is__measure_Osimps,fact_equal,fact_equal__refl,fact_equal__eq,fact_eq__equal,fact_measure__size,fact_measure__snd,fact_transfer__morphism__int__nat,fact_New__DSequence_Oneg__decr__bind__def,fact_eq__int__code_I7_J,fact_eq__int__code_I11_J,fact_eq__number__of__int__code,fact_eq__int__code_I1_J,fact_eq__int__code_I16_J,fact_eq__int__code_I13_J,fact_eq__int__code_I6_J,fact_eq__int__code_I4_J,fact_eq__int__code_I10_J,fact_equal__int__def,fact_eq__int__code_I14_J,fact_eq__int__code_I15_J,fact_eq__int__code_I3_J,fact_eq__int__code_I9_J,fact_eq__int__code_I8_J,fact_eq__int__code_I12_J,fact_eq__int__code_I5_J,fact_eq__int__code_I2_J,fact_bool_Osize_I3_J,fact_bool_Osize_I4_J,fact_New__Random__Sequence_Oneg__decr__bind__def,fact_New__DSequence_Oneg__bind__def,fact_eq__int__refl,fact_neg__bind__def,fact_size__code,fact_lazy__sequence__size__code,fact_seq__case,fact_yieldn__def,fact_lazy__sequence_Osize_I2_J,fact_lazy__sequence_Osimps_I5_J,fact_lazy__sequence_Oinject,fact__01,fact_lazy__sequence_Osize_I4_J,fact_neg__map__def,fact_New__DSequence_Opos__decr__bind__def,fact_New__Random__Sequence_Opos__decr__bind__def,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__HOL_Oequal,arity_fun__Enum_Oenum,arity_Com__Ocom__HOL_Oequal,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__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__Smallcheck_Osmall,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__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__HOL_Oequal,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__HOL_Oequal,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__HOL_Oequal,arity_HOL__Obool__Enum_Oenum,arity_HOL__Obool__Nat_Osize,arity_Com__Ostate__HOL_Oequal,arity_Com__Ostate__Nat_Osize,arity_Com__Ovname__HOL_Oequal,arity_Com__Ovname__Nat_Osize,arity_List__Olist__HOL_Oequal,arity_List__Olist__Nat_Osize,arity_sum__Finite__Set_Ofinite,arity_sum__HOL_Oequal,arity_sum__Enum_Oenum,arity_sum__Nat_Osize,arity_Option__Ooption__Finite__Set_Ofinite,arity_Option__Ooption__HOL_Oequal,arity_Option__Ooption__Enum_Oenum,arity_Option__Ooption__Nat_Osize,arity_prod__Finite__Set_Ofinite,arity_prod__Smallcheck_Osmall,arity_prod__HOL_Oequal,arity_prod__Enum_Oenum,arity_prod__Nat_Osize,arity_Product____Type__Ounit__Finite__Set_Ofinite,arity_Product____Type__Ounit__Smallcheck_Osmall,arity_Product____Type__Ounit__HOL_Oequal,arity_Product____Type__Ounit__Enum_Oenum,arity_Product____Type__Ounit__Nat_Osize,arity_Code____Evaluation__Oterm__HOL_Oequal,arity_Code____Evaluation__Oterm__Nat_Osize,arity_Hoare____Mirabelle__Otriple__HOL_Oequal,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__HOL_Oequal,arity_Code____Numeral__Ocode____numeral__Nat_Osize,arity_Lazy____Sequence__Olazy____sequence__HOL_Oequal,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] % 79.07/78.73 =============================================================== % 79.07/78.73 % 79.07/78.73 Combined formula: 5241 axiom(s) => conjecture % 79.07/78.73 % 79.07/78.73 % Equality/functions detected -> nanoCoP oracle mode % 79.07/78.73 nanoCoP : % 79.07/78.73 % 19,442,636 inferences, 66.622 CPU in 66.630 seconds (100% CPU, 291836 Lips) % 79.07/78.73 % 79.07/78.73 % nanoCoP proof (equality/functions) % 79.07/78.73 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 79.07/78.73 % 79.07/78.73 % SZS output end Proof %------------------------------------------------------------------------------